From ac9d8a9cd740c438995495cd675cd2b830e72959 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 15 Jul 2021 17:16:40 -0700 Subject: [PATCH] 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 | 229 +++++++++++++++++++++++----------- 2 files changed, 155 insertions(+), 78 deletions(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index f91b37e9f..51921e8e2 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 b4cdda496..a477e5417 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 (W4Portfolio _) _primMap _logData _ts _args _query _satNum = - 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 W4OfflineConfig _primMap _logData _ts _args _query _satNum = + fail "What4 offline solver 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 (W4Portfolio _) _primMap _logData _ts _args _query _satNum = + fail "What4 portfolio solver cannot be used for multi-SAT queries" + +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.") + +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 _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 (SomeSat n) | n <= 0 = return [] -- should never happen... + + 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 =>