From 6f9d9e72a66697181d46faa8d2c0a4057bc0320e Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 15 Jul 2021 16:43:40 -0700 Subject: [PATCH 01/11] Report the number of models found, if a multisat query returns more than one model. --- src/Cryptol/REPL/Command.hs | 3 +++ tests/issues/issue072.icry.stdout | 2 ++ 2 files changed, 5 insertions(+) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 8f914364..f91b37e9 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -785,6 +785,9 @@ proveSatExpr isSat rng exprDoc texpr schema = do ~(EnvBool yes) <- getUser "showExamples" when yes $ forM_ vss (printSatisfyingModel exprDoc) + let numModels = length tevss + when (numModels > 1) (rPutStrLn ("Models found: " ++ show numModels)) + case exprs of [e] -> void $ bindItVariable ty e _ -> bindItVariables ty exprs diff --git a/tests/issues/issue072.icry.stdout b/tests/issues/issue072.icry.stdout index 0c8e044f..e84e2b55 100644 --- a/tests/issues/issue072.icry.stdout +++ b/tests/issues/issue072.icry.stdout @@ -2,8 +2,10 @@ Loading module Cryptol Satisfiable it : {result : Bit, arg1 : [4]} Satisfiable +Models found: 11 it : [11]{result : Bit, arg1 : [4]} must be an integer > 0 or "all" must be an integer > 0 or "all" Satisfiable +Models found: 3 it : [3]{result : Bit, arg1 : [4]} From ac9d8a9cd740c438995495cd675cd2b830e72959 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 15 Jul 2021 17:16:40 -0700 Subject: [PATCH 02/11] Allow What4 solvers to be configured in incremental mode. The solvers we currently support all have an incremental/online mode, and we reconfigure the `:sat` `:prove` and `:safe` commands to use them. In particular, we use incremental solving to significantly speed up multi-SAT queries, partially addressing #1125. --- src/Cryptol/REPL/Command.hs | 4 +- src/Cryptol/Symbolic/What4.hs | 223 +++++++++++++++++++++++----------- 2 files changed, 152 insertions(+), 75 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index f91b37e9..51921e8e 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -888,10 +888,10 @@ offlineProveSat proverName qtype expr schema mfile = do Just path -> io $ writeFile path smtlib Nothing -> rPutStr smtlib - Right w4Cfg -> + Right _w4Cfg -> do ~(EnvBool hashConsing) <- getUser "hashConsing" ~(EnvBool warnUninterp) <- getUser "warnUninterp" - result <- liftModuleCmd $ W4.satProveOffline w4Cfg hashConsing warnUninterp cmd $ \f -> + result <- liftModuleCmd $ W4.satProveOffline hashConsing warnUninterp cmd $ \f -> do displayMsg case mfile of Just path -> diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index b4cdda49..a477e541 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -8,6 +8,7 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternGuards #-} @@ -33,13 +34,14 @@ import Control.Applicative import Control.Concurrent.Async import Control.Concurrent.MVar import Control.Monad.IO.Class -import Control.Monad (when, foldM, forM_) +import Control.Monad (when, foldM, forM_, void) import qualified Control.Exception as X import System.IO (Handle) import Data.Time import Data.IORef import Data.List (intercalate) import Data.List.NonEmpty (NonEmpty(..)) +import Data.Proxy import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set @@ -75,7 +77,14 @@ import qualified What4.SatResult as W4 import qualified What4.SFloat as W4 import qualified What4.SWord as SW import What4.Solver +import qualified What4.Solver.Boolector as W4 +import qualified What4.Solver.Z3 as W4 +import qualified What4.Solver.CVC4 as W4 +import qualified What4.Solver.Yices as W4 import qualified What4.Solver.Adapter as W4 +import qualified What4.Protocol.Online as W4 +import qualified What4.Protocol.SMTLib2 as W4 +import qualified What4.ProblemFeatures as W4 import qualified Data.BitVector.Sized as BV import Data.Parameterized.Nonce @@ -130,32 +139,60 @@ doW4Eval sym m = W4Result p x -> pure (p,x) -data AnAdapter = AnAdapter (forall st. SolverAdapter st) +data AnAdapter + = AnAdapter (forall st. SolverAdapter st) + | forall s. W4.OnlineSolver s => + AnOnlineAdapter + String + W4.ProblemFeatures + [W4.ConfigDesc] + (Proxy s) data W4ProverConfig = W4ProverConfig AnAdapter + | W4OfflineConfig | W4Portfolio (NonEmpty AnAdapter) proverConfigs :: [(String, W4ProverConfig)] proverConfigs = - [ ("w4-cvc4" , W4ProverConfig (AnAdapter cvc4Adapter) ) - , ("w4-yices" , W4ProverConfig (AnAdapter yicesAdapter) ) - , ("w4-z3" , W4ProverConfig (AnAdapter z3Adapter) ) - , ("w4-boolector", W4ProverConfig (AnAdapter boolectorAdapter) ) - , ("w4-offline" , W4ProverConfig (AnAdapter z3Adapter) ) - , ("w4-any" , allSolvers) + [ ("w4-cvc4" , W4ProverConfig cvc4OnlineAdapter) + , ("w4-yices" , W4ProverConfig yicesOnlineAdapter) + , ("w4-z3" , W4ProverConfig z3OnlineAdapter) + , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter) + , ("w4-offline" , W4OfflineConfig ) + , ("w4-any" , allSolvers) ] +z3OnlineAdapter :: AnAdapter +z3OnlineAdapter = + AnOnlineAdapter "Z3" W4.z3Features W4.z3Options + (Proxy :: Proxy (W4.Writer W4.Z3)) + +yicesOnlineAdapter :: AnAdapter +yicesOnlineAdapter = + AnOnlineAdapter "Yices" W4.yicesDefaultFeatures W4.yicesOptions + (Proxy :: Proxy W4.Connection) + +cvc4OnlineAdapter :: AnAdapter +cvc4OnlineAdapter = + AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options + (Proxy :: Proxy (W4.Writer W4.CVC4)) + +boolectorOnlineAdapter :: AnAdapter +boolectorOnlineAdapter = + AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions + (Proxy :: Proxy (W4.Writer W4.Boolector)) + allSolvers :: W4ProverConfig allSolvers = W4Portfolio - $ AnAdapter z3Adapter :| - [ AnAdapter cvc4Adapter - , AnAdapter boolectorAdapter - , AnAdapter yicesAdapter + $ z3OnlineAdapter :| + [ cvc4OnlineAdapter + , boolectorOnlineAdapter + , yicesOnlineAdapter ] defaultProver :: W4ProverConfig -defaultProver = W4ProverConfig (AnAdapter z3Adapter) +defaultProver = W4ProverConfig z3OnlineAdapter proverNames :: [String] proverNames = map fst proverConfigs @@ -178,12 +215,16 @@ setupProver nm = let msg = "What4 found the following solvers: " ++ show (adapterNames (p:ps')) in pure (Right ([msg], W4Portfolio (p:|ps'))) + Just W4OfflineConfig -> pure (Right ([], W4OfflineConfig)) + Nothing -> pure (Left ("unknown solver name: " ++ nm)) where adapterNames [] = [] adapterNames (AnAdapter adpt : ps) = solver_adapter_name adpt : adapterNames ps + adapterNames (AnOnlineAdapter n _ _ _ : ps) = + n : adapterNames ps filterAdapters [] = pure [] filterAdapters (p:ps) = @@ -191,12 +232,25 @@ setupProver nm = Just _err -> filterAdapters ps Nothing -> (p:) <$> filterAdapters ps + tryAdapter :: AnAdapter -> IO (Maybe X.SomeException) + tryAdapter (AnAdapter adpt) = do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym) W4.smokeTest sym adpt - + tryAdapter (AnOnlineAdapter _ fs opts (_ :: Proxy s)) = test `X.catch` (pure . Just) + where + test = + do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator + W4.extendConfig opts (W4.getConfiguration sym) + (proc :: W4.SolverProcess GlobalNonceGenerator s) <- W4.startSolverProcess fs Nothing sym + res <- W4.checkSatisfiable proc "smoke test" (W4.falsePred sym) + case res of + W4.Unsat () -> return () + _ -> fail "smoke test failed, expected UNSAT!" + void (W4.shutdownSolverProcess proc) + return Nothing proverError :: String -> M.ModuleCmd (Maybe String, ProverResult) proverError msg minp = @@ -211,11 +265,13 @@ setupAdapterOptions cfg sym = case cfg of W4ProverConfig p -> setupAnAdapter p W4Portfolio ps -> mapM_ setupAnAdapter ps + W4OfflineConfig -> return () where setupAnAdapter (AnAdapter adpt) = W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym) - + setupAnAdapter (AnOnlineAdapter _n _fs opts _p) = + W4.extendConfig opts (W4.getConfiguration sym) what4FreshFns :: W4.IsSymExprBuilder sym => sym -> FreshVarFns (What4 sym) what4FreshFns sym = @@ -350,16 +406,13 @@ satProve solverCfg hashConsing warnUninterp ProverCommand {..} = Right (ts,args,safety,query) -> case pcQueryType of ProveQuery -> - singleQuery sym solverCfg primMap logData ts args - (Just safety) query + singleQuery sym solverCfg primMap logData ts args (Just safety) query SafetyQuery -> - singleQuery sym solverCfg primMap logData ts args - (Just safety) query + singleQuery sym solverCfg primMap logData ts args (Just safety) query SatQuery num -> - multiSATQuery sym solverCfg primMap logData ts args - query num + multiSATQuery sym solverCfg primMap logData ts args query num printUninterpWarn :: Logger -> Set Text -> IO () printUninterpWarn lg uninterpWarns = @@ -371,17 +424,14 @@ printUninterpWarn lg uninterpWarns = , " " ++ intercalate ", " (map Text.unpack xs) ] satProveOffline :: - W4ProverConfig -> Bool {- ^ hash consing -} -> Bool {- ^ warn on uninterpreted functions -} -> ProverCommand -> ((Handle -> IO ()) -> IO ()) -> M.ModuleCmd (Maybe String) -satProveOffline (W4Portfolio (p:|_)) hashConsing warnUninterp cmd outputContinuation = - satProveOffline (W4ProverConfig p) hashConsing warnUninterp cmd outputContinuation +satProveOffline hashConsing warnUninterp ProverCommand{ .. } outputContinuation = -satProveOffline (W4ProverConfig (AnAdapter adpt)) hashConsing warnUninterp ProverCommand {..} outputContinuation = protectStack onError \modIn -> M.runModuleM modIn do w4sym <- liftIO makeSym @@ -396,15 +446,12 @@ satProveOffline (W4ProverConfig (AnAdapter adpt)) hashConsing warnUninterp Prove case ok of Left msg -> return (Just msg) Right (_ts,_args,_safety,query) -> - do outputContinuation - (\hdl -> solver_adapter_write_smt2 adpt w4sym hdl [query]) + do outputContinuation (\hdl -> W4.writeZ3SMT2File w4sym hdl [query]) return Nothing where makeSym = - do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState - globalNonceGenerator - W4.extendConfig (W4.solver_adapter_config_options adpt) - (W4.getConfiguration sym) + do sym <- W4.newExprBuilder W4.FloatIEEERepr CryptolState globalNonceGenerator + W4.extendConfig W4.z3Options (W4.getConfiguration sym) when hashConsing (W4.startCaching sym) pure sym @@ -427,57 +474,61 @@ multiSATQuery :: W4.Pred sym -> SatNum -> IO (Maybe String, ProverResult) + multiSATQuery sym solverCfg primMap logData ts args query (SomeSat n) | n <= 1 = singleQuery sym solverCfg primMap logData ts args Nothing query +multiSATQuery _sym W4OfflineConfig _primMap _logData _ts _args _query _satNum = + fail "What4 offline solver cannot be used for multi-SAT queries" + multiSATQuery _sym (W4Portfolio _) _primMap _logData _ts _args _query _satNum = - fail "What4 portfolio solver cannot be used for multi SAT queries" + fail "What4 portfolio solver cannot be used for multi-SAT queries" -multiSATQuery sym (W4ProverConfig (AnAdapter adpt)) primMap logData ts args query satNum0 = - do pres <- W4.solver_adapter_check_sat adpt (w4 sym) logData [query] $ \res -> - case res of - W4.Unknown -> return (Left (ProverError "Solver returned UNKNOWN")) - W4.Unsat _ -> return (Left (ThmResult (map unFinType ts))) - W4.Sat (evalFn,_) -> - do xs <- mapM (varShapeToConcrete evalFn) args - let model = computeModel primMap ts xs - blockingPred <- computeBlockingPred sym args xs - return (Right (model, blockingPred)) +multiSATQuery _sym (W4ProverConfig (AnAdapter adpt)) _primMap _logData _ts _args _query _satNum = + fail ("Solver " ++ solver_adapter_name adpt ++ " does not support incremental solving and " ++ + "cannot be used for multi-SAT queries.") - case pres of - Left res -> pure (Just (solver_adapter_name adpt), res) - Right (mdl,block) -> - do mdls <- (mdl:) <$> computeMoreModels [block,query] (decSatNum satNum0) - return (Just (solver_adapter_name adpt), AllSatResult mdls) +multiSATQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts (_ :: Proxy s))) + primMap _logData ts args query satNum0 = + X.bracket + (W4.startSolverProcess fs Nothing (w4 sym)) + (void . W4.shutdownSolverProcess) + (\ (proc :: W4.SolverProcess t s) -> + do W4.assume (W4.solverConn proc) query + res <- W4.checkAndGetModel proc "query" + pres <- case res of + W4.Unknown -> return (Left (ProverError "Solver returned UNKNOWN")) + W4.Unsat _ -> return (Left (ThmResult (map unFinType ts))) + W4.Sat evalFn -> + do xs <- mapM (varShapeToConcrete evalFn) args + let model = computeModel primMap ts xs + blockingPred <- computeBlockingPred sym args xs + return (Right (model, blockingPred)) + case pres of + Left x -> pure (Just nm, x) + Right (mdl,block) -> + do W4.assume (W4.solverConn proc) block + mdls <- (mdl:) <$> computeMoreModels proc (decSatNum satNum0) + return (Just nm, AllSatResult mdls)) where + computeMoreModels _proc (SomeSat n) | n <= 0 = return [] -- should never happen... - computeMoreModels _qs (SomeSat n) | n <= 0 = return [] -- should never happen... - computeMoreModels qs (SomeSat n) | n <= 1 = -- final model - W4.solver_adapter_check_sat adpt (w4 sym) logData qs $ \res -> - case res of - W4.Unknown -> return [] - W4.Unsat _ -> return [] - W4.Sat (evalFn,_) -> - do xs <- mapM (varShapeToConcrete evalFn) args - let model = computeModel primMap ts xs - return [model] - - computeMoreModels qs satNum = - do pres <- W4.solver_adapter_check_sat adpt (w4 sym) logData qs $ \res -> - case res of - W4.Unknown -> return Nothing - W4.Unsat _ -> return Nothing - W4.Sat (evalFn,_) -> - do xs <- mapM (varShapeToConcrete evalFn) args - let model = computeModel primMap ts xs - blockingPred <- computeBlockingPred sym args xs - return (Just (model, blockingPred)) - - case pres of - Nothing -> return [] - Just (mdl, block) -> - (mdl:) <$> computeMoreModels (block:qs) (decSatNum satNum) + computeMoreModels proc satNum = + do res <- W4.checkAndGetModel proc "more models" + case res of + W4.Unknown -> return [] + W4.Unsat _ -> return [] + W4.Sat evalFn -> + do xs <- mapM (varShapeToConcrete evalFn) args + let model = computeModel primMap ts xs + case satNum of + -- final model + SomeSat n | n <= 1 -> return [model] + -- keep going + _ -> do blockingPred <- computeBlockingPred sym args xs + W4.assume (W4.solverConn proc) blockingPred + (model:) <$> computeMoreModels proc (decSatNum satNum) singleQuery :: sym ~ W4.ExprBuilder t CryptolState fm => @@ -491,6 +542,10 @@ singleQuery :: W4.Pred sym -> IO (Maybe String, ProverResult) +singleQuery _ W4OfflineConfig _primMap _logData _ts _args _msafe _query = + -- this shouldn't happen... + fail "What4 offline solver cannot be used for direct queries" + singleQuery sym (W4Portfolio ps) primMap logData ts args msafe query = do as <- mapM async [ singleQuery sym (W4ProverConfig p) primMap logData ts args msafe query | p <- NE.toList ps @@ -528,6 +583,28 @@ singleQuery sym (W4ProverConfig (AnAdapter adpt)) primMap logData ts args msafe return (Just (W4.solver_adapter_name adpt), pres) +singleQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts (_ :: Proxy s))) + primMap _logData ts args msafe query = + X.bracket + (W4.startSolverProcess fs Nothing (w4 sym)) + (void . W4.shutdownSolverProcess) + (\ (proc :: W4.SolverProcess t s) -> + do W4.assume (W4.solverConn proc) query + res <- W4.checkAndGetModel proc "query" + case res of + W4.Unknown -> return (Just nm, ProverError "Solver returned UNKNOWN") + W4.Unsat _ -> return (Just nm, ThmResult (map unFinType ts)) + W4.Sat evalFn -> + do xs <- mapM (varShapeToConcrete evalFn) args + let model = computeModel primMap ts xs + case msafe of + Just s -> + do s' <- W4.groundEval evalFn s + let cexType = if s' then PredicateFalsified else SafetyViolation + return (Just nm, CounterExample cexType model) + Nothing -> return (Just nm, AllSatResult [ model ]) + ) + computeBlockingPred :: sym ~ W4.ExprBuilder t CryptolState fm => From 19d84745c7c3a7b917971c41bd855f85dc3bf96a Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 15 Jul 2021 17:21:02 -0700 Subject: [PATCH 03/11] Add a new regression test that better exercises multi-SAT queries. --- tests/regression/allsat.cry | 3 +++ tests/regression/allsat.icry | 9 +++++++++ tests/regression/allsat.icry.stdout | 7 +++++++ 3 files changed, 19 insertions(+) create mode 100644 tests/regression/allsat.cry create mode 100644 tests/regression/allsat.icry create mode 100644 tests/regression/allsat.icry.stdout diff --git a/tests/regression/allsat.cry b/tests/regression/allsat.cry new file mode 100644 index 00000000..1b56eeda --- /dev/null +++ b/tests/regression/allsat.cry @@ -0,0 +1,3 @@ +f : (Integer, Integer, Integer) -> Bit +f (x, y, z) = inRange x && inRange y && inRange z + where inRange v = (1 <= v) && (v <= 15) diff --git a/tests/regression/allsat.icry b/tests/regression/allsat.icry new file mode 100644 index 00000000..7821d37e --- /dev/null +++ b/tests/regression/allsat.icry @@ -0,0 +1,9 @@ +:l allsat.cry + +:set satNum=all +:set showExamples=false +:set prover=sbv-yices +:sat f + +:set prover=w4-yices +:sat f diff --git a/tests/regression/allsat.icry.stdout b/tests/regression/allsat.icry.stdout new file mode 100644 index 00000000..12c5a4c0 --- /dev/null +++ b/tests/regression/allsat.icry.stdout @@ -0,0 +1,7 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +Satisfiable +Models found: 3375 +Satisfiable +Models found: 3375 From 4dc7a6ca8227571989124af9a386fe53f3dad286 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 15 Jul 2021 17:42:45 -0700 Subject: [PATCH 04/11] Add support for ABC via the relatively new What4 support for calling ABC as an external process. --- src/Cryptol/Symbolic/What4.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index a477e541..f531618d 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -78,9 +78,10 @@ import qualified What4.SFloat as W4 import qualified What4.SWord as SW import What4.Solver import qualified What4.Solver.Boolector as W4 -import qualified What4.Solver.Z3 as W4 import qualified What4.Solver.CVC4 as W4 +import qualified What4.Solver.ExternalABC as W4 import qualified What4.Solver.Yices as W4 +import qualified What4.Solver.Z3 as W4 import qualified What4.Solver.Adapter as W4 import qualified What4.Protocol.Online as W4 import qualified What4.Protocol.SMTLib2 as W4 @@ -159,6 +160,9 @@ proverConfigs = , ("w4-yices" , W4ProverConfig yicesOnlineAdapter) , ("w4-z3" , W4ProverConfig z3OnlineAdapter) , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter) + + , ("w4-abc" , W4ProverConfig (AnAdapter W4.externalABCAdapter)) + , ("w4-offline" , W4OfflineConfig ) , ("w4-any" , allSolvers) ] From dd8fca4cfecb50bf4048cbdd47b7dd019225a6c2 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 16 Jul 2021 09:32:27 -0700 Subject: [PATCH 05/11] Update cryptol-remote-api --- cryptol-remote-api/src/CryptolServer/Sat.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cryptol-remote-api/src/CryptolServer/Sat.hs b/cryptol-remote-api/src/CryptolServer/Sat.hs index 752a0853..23ec7094 100644 --- a/cryptol-remote-api/src/CryptolServer/Sat.hs +++ b/cryptol-remote-api/src/CryptolServer/Sat.hs @@ -118,10 +118,10 @@ offlineProveSat proverName cmd hConsing = do Left msg -> do raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg Right smtlib -> pure $ OfflineSMTQuery $ T.pack smtlib - Right w4Cfg -> do + Right _w4Cfg -> do smtlibRef <- liftIO $ newIORef ("" :: Text) result <- liftModuleCmd $ - W4.satProveOffline w4Cfg hConsing False cmd $ \f -> do + W4.satProveOffline hConsing False cmd $ \f -> do withRWTempFile "smtOutput.tmp" $ \h -> do f h hSeek h AbsoluteSeek 0 From 62d413ec66837b8844cd1bbb7207b5dbbf7b9631 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 16 Jul 2021 11:46:48 -0700 Subject: [PATCH 06/11] Implement a new multi-SAT algorithm for What4 solvers. Fixes #1125 --- src/Cryptol/Symbolic.hs | 20 +++++ src/Cryptol/Symbolic/What4.hs | 157 ++++++++++++++++++++++++++-------- 2 files changed, 142 insertions(+), 35 deletions(-) diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index 845b65ab..4fbed62a 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -38,6 +38,8 @@ module Cryptol.Symbolic , modelPred , varModelPred , varToExpr + , flattenShape + , flattenShapes ) where @@ -222,6 +224,24 @@ ppVarShape sym (VarRecord fs) = ppField (f,v) = pp f <+> char '=' <+> ppVarShape sym v +-- | Flatten structured shapes (like tuples and sequences), leaving only +-- a sequence of variable shapes of base type. +flattenShapes :: [VarShape sym] -> [VarShape sym] -> [VarShape sym] +flattenShapes [] tl = tl +flattenShapes (x:xs) tl = flattenShape x (flattenShapes xs tl) + +flattenShape :: VarShape sym -> [VarShape sym] -> [VarShape sym] +flattenShape x tl = + case x of + VarBit{} -> x : tl + VarInteger{} -> x : tl + VarRational{} -> x : tl + VarWord{} -> x : tl + VarFloat{} -> x : tl + VarFinSeq _ vs -> flattenShapes vs tl + VarTuple vs -> flattenShapes vs tl + VarRecord fs -> flattenShapes (recordElements fs) tl + varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym varShapeToValue sym var = case var of diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index f531618d..8955b35b 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -11,6 +11,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ParallelListComp #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} @@ -39,7 +40,7 @@ import qualified Control.Exception as X import System.IO (Handle) import Data.Time import Data.IORef -import Data.List (intercalate) +import Data.List (intercalate, tails, inits) import Data.List.NonEmpty (NonEmpty(..)) import Data.Proxy import qualified Data.Map as Map @@ -62,7 +63,9 @@ import Cryptol.Backend.What4 import qualified Cryptol.Eval as Eval import qualified Cryptol.Eval.Concrete as Concrete import qualified Cryptol.Eval.Value as Eval +import Cryptol.Eval.Type (TValue) import Cryptol.Eval.What4 + import Cryptol.Parser.Position (emptyRange) import Cryptol.Symbolic import Cryptol.TypeCheck.AST @@ -462,12 +465,14 @@ satProveOffline hashConsing warnUninterp ProverCommand{ .. } outputContinuation onError msg minp = pure (Right (Just msg, M.minpModuleEnv minp), []) +{- decSatNum :: SatNum -> SatNum decSatNum (SomeSat n) | n > 0 = SomeSat (n-1) decSatNum n = n +-} -multiSATQuery :: +multiSATQuery :: forall sym t fm. sym ~ W4.ExprBuilder t CryptolState fm => What4 sym -> W4ProverConfig -> @@ -500,39 +505,122 @@ multiSATQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts (_ :: Proxy s))) (\ (proc :: W4.SolverProcess t s) -> do W4.assume (W4.solverConn proc) query res <- W4.checkAndGetModel proc "query" - pres <- case res of - W4.Unknown -> return (Left (ProverError "Solver returned UNKNOWN")) - W4.Unsat _ -> return (Left (ThmResult (map unFinType ts))) - W4.Sat evalFn -> - do xs <- mapM (varShapeToConcrete evalFn) args - let model = computeModel primMap ts xs - blockingPred <- computeBlockingPred sym args xs - return (Right (model, blockingPred)) - case pres of - Left x -> pure (Just nm, x) - Right (mdl,block) -> - do W4.assume (W4.solverConn proc) block - mdls <- (mdl:) <$> computeMoreModels proc (decSatNum satNum0) + case res of + W4.Unknown -> return (Just nm, ProverError "Solver returned UNKNOWN") + W4.Unsat _ -> return (Just nm, ThmResult (map unFinType ts)) + W4.Sat evalFn -> + do xs <- mapM (varShapeToConcrete evalFn) args + let mdl = computeModel primMap ts xs + -- NB, we flatten these shapes to make sure that we can split + -- our search across all of the atomic variables + let vs = flattenShapes args [] + let cs = flattenShapes xs [] + mdls <- runMultiSat satNum0 $ + do yield mdl + computeMoreModels proc vs cs return (Just nm, AllSatResult mdls)) where - computeMoreModels _proc (SomeSat n) | n <= 0 = return [] -- should never happen... + -- This search procedure uses incremental solving and push/pop to split on the concrete + -- values of variables, while also helping to prevent the accumulation of unhelpful + -- lemmas in the solver state. This algorithm is basically taken from: + -- http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations + computeMoreModels :: + W4.SolverProcess t s -> + [VarShape (What4 sym)] -> + [VarShape Concrete.Concrete] -> + MultiSat () + computeMoreModels proc vs cs = + -- Enumerate all the ways to split up the current model + forM_ (computeSplits vs cs) $ \ (prefix, vi, ci, suffix) -> + do -- open a new solver frame + liftIO $ W4.push proc + -- force the selected pair to be different + liftIO $ W4.assume (W4.solverConn proc) =<< W4.notPred (w4 sym) =<< computeModelPred sym vi ci + -- force the prefix values to be the same + liftIO $ forM_ prefix $ \(v,c) -> + W4.assume (W4.solverConn proc) =<< computeModelPred sym v c + -- under these assumptions, find all the remaining models + findMoreModels proc (vi:suffix) + -- pop the current assumption frame + liftIO $ W4.pop proc - computeMoreModels proc satNum = - do res <- W4.checkAndGetModel proc "more models" + findMoreModels :: + W4.SolverProcess t s -> + [VarShape (What4 sym)] -> + MultiSat () + findMoreModels proc vs = + -- see if our current assumptions are consistent + do res <- liftIO (W4.checkAndGetModel proc "find model") case res of - W4.Unknown -> return [] - W4.Unsat _ -> return [] + -- if the solver gets stuck, drop all the way out and stop search + W4.Unknown -> done + -- if our assumptions are already unsatisfiable, stop search and return + W4.Unsat _ -> return () W4.Sat evalFn -> - do xs <- mapM (varShapeToConcrete evalFn) args - let model = computeModel primMap ts xs - case satNum of - -- final model - SomeSat n | n <= 1 -> return [model] - -- keep going - _ -> do blockingPred <- computeBlockingPred sym args xs - W4.assume (W4.solverConn proc) blockingPred - (model:) <$> computeMoreModels proc (decSatNum satNum) + -- We found a model. Record it and then use it to split the remaining + -- search variables some more. + do xs <- liftIO (mapM (varShapeToConcrete evalFn) args) + yield (computeModel primMap ts xs) + cs <- liftIO (mapM (varShapeToConcrete evalFn) vs) + computeMoreModels proc vs cs + +-- == Support operations for multi-SAT == +type Models = [[(TValue, Expr, Concrete.Value)]] + +newtype MultiSat a = + MultiSat { unMultiSat :: Models -> SatNum -> (a -> Models -> SatNum -> IO Models) -> IO Models } + +instance Functor MultiSat where + fmap f m = MultiSat (\ms satNum k -> unMultiSat m ms satNum (k . f)) + +instance Applicative MultiSat where + pure x = MultiSat (\ms satNum k -> k x ms satNum) + mf <*> mx = mf >>= \f -> fmap f mx + +instance Monad MultiSat where + m >>= f = MultiSat (\ms satNum k -> unMultiSat m ms satNum (\x ms' satNum' -> unMultiSat (f x) ms' satNum' k)) + +instance MonadIO MultiSat where + liftIO m = MultiSat (\ms satNum k -> do x <- m; k x ms satNum) + +runMultiSat :: SatNum -> MultiSat a -> IO Models +runMultiSat satNum m = reverse <$> unMultiSat m [] satNum (\_ ms _ -> return ms) + +done :: MultiSat a +done = MultiSat (\ms _satNum _k -> return ms) + +yield :: [(TValue, Expr, Concrete.Value)] -> MultiSat () +yield mdl = MultiSat (\ms satNum k -> + case satNum of + SomeSat n + | n > 1 -> k () (mdl:ms) (SomeSat (n-1)) + | otherwise -> return (mdl:ms) + _ -> k () (mdl:ms) satNum) + +-- Compute all the ways to split a sequences of variables +-- and concrete values for those variables. Each element +-- of the list consists of a prefix of (varaible,value) +-- pairs whose values we will fix, a single (varaible,value) +-- pair that we will force to be different, and a list of +-- additional unconstrained variables. +computeSplits :: + [VarShape (What4 sym)] -> + [VarShape Concrete.Concrete] -> + [ ( [(VarShape (What4 sym), VarShape Concrete.Concrete)] + , VarShape (What4 sym) + , VarShape Concrete.Concrete + , [VarShape (What4 sym)] + ) + ] +computeSplits vs cs = reverse + [ (prefix, v, c, tl) + | prefix <- inits (zip vs cs) + | v <- vs + | c <- cs + | tl <- tail (tails vs) + ] +-- == END Support operations for multi-SAT == singleQuery :: sym ~ W4.ExprBuilder t CryptolState fm => @@ -610,15 +698,14 @@ singleQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts (_ :: Proxy s))) ) -computeBlockingPred :: +computeModelPred :: sym ~ W4.ExprBuilder t CryptolState fm => What4 sym -> - [VarShape (What4 sym)] -> - [VarShape Concrete.Concrete] -> + VarShape (What4 sym) -> + VarShape Concrete.Concrete -> IO (W4.Pred sym) -computeBlockingPred sym vs xs = - do res <- doW4Eval (w4 sym) (modelPred sym vs xs) - W4.notPred (w4 sym) (snd res) +computeModelPred sym v c = + snd <$> doW4Eval (w4 sym) (varModelPred sym (v, c)) varShapeToConcrete :: W4.GroundEvalFn t -> From 9e65822651acc501570cb5e5619131bebbd08e04 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 20 Jul 2021 10:21:29 -0700 Subject: [PATCH 07/11] Update RPC docs with new `w4-abc` solver option. --- cryptol-remote-api/docs/Cryptol.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index d2adc682..b88da448 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -557,7 +557,7 @@ Parameter fields ``prover`` - The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``. + The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``. From 2eb155eea7230b739179fd6da7a3e10e2a3f0345 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 20 Jul 2021 11:03:32 -0700 Subject: [PATCH 08/11] Add ABC to the `w4-any` portfolio solver. --- src/Cryptol/Symbolic/What4.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index 8955b35b..d3ca83f8 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -196,6 +196,7 @@ allSolvers = W4Portfolio [ cvc4OnlineAdapter , boolectorOnlineAdapter , yicesOnlineAdapter + , AnAdapter W4.externalABCAdapter ] defaultProver :: W4ProverConfig From c248320ca51d3f6b122c0ea627fa40270327ce31 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 20 Jul 2021 11:05:12 -0700 Subject: [PATCH 09/11] Change to use Z3 instead of yices for the all-sat test. Despite the fact that Z3 is easily the slowest solver at this task, it is the one that is reliably avaliable on the CI servers. --- tests/regression/allsat.icry | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/allsat.icry b/tests/regression/allsat.icry index 7821d37e..b920cac4 100644 --- a/tests/regression/allsat.icry +++ b/tests/regression/allsat.icry @@ -2,8 +2,8 @@ :set satNum=all :set showExamples=false -:set prover=sbv-yices +:set prover=sbv-z3 :sat f -:set prover=w4-yices +:set prover=w4-z3 :sat f From 9fcdb9be21e2231784a5a1e04e09fa94fa0e0047 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 20 Jul 2021 11:13:03 -0700 Subject: [PATCH 10/11] Remove unnecessary SBV upper bound in cryptol-remote-api --- cryptol-remote-api/cryptol-remote-api.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index f0f75d18..51892775 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -91,7 +91,7 @@ executable cryptol-remote-api build-depends: cryptol-remote-api, - sbv < 8.10 + sbv if os(linux) && flag(static) ld-options: -static -pthread @@ -108,7 +108,7 @@ executable cryptol-eval-server build-depends: cryptol-remote-api, optparse-applicative, - sbv < 8.10 + sbv if os(linux) && flag(static) ld-options: -static -pthread From 7a1843056da94f10cc5b27d4ab51b997508efed0 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 20 Jul 2021 12:48:21 -0700 Subject: [PATCH 11/11] Update CHANGES --- CHANGES.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index 18e36fd4..9d1de57b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -6,9 +6,19 @@ - Paren blocks nested in a layout block need to respect the indentation if the layout block - We allow nested layout blocks to have the same indentation, which is - conveninet when writing `private` declarations as they don't need to + convenient when writing `private` declarations as they don't need to be indented as long as they are at the end of the file. +## New features + +* What4 prover backends now feature an improved multi-SAT procedure + which is significantly faster than the old algorithm. Thanks to + Levent Erkök for the suggestion. + +* There is a new `w4-abc` solver option, which communicates to ABC + as an external process via What4. + + # 2.11.0 ## Language changes