Skip to content

Commit

Permalink
Allow What4 solvers to be configured in incremental mode.
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@robdockins
robdockins committed Jul 20, 2021
1 parent 6f9d9e7 commit ac9d8a9
Show file tree
Hide file tree
Showing 2 changed files with 155 additions and 78 deletions.
4 changes: 2 additions & 2 deletions src/Cryptol/REPL/Command.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
229 changes: 153 additions & 76 deletions src/Cryptol/Symbolic/What4.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -178,25 +215,42 @@ 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) =
tryAdapter p >>= \case
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 =
Expand All @@ -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 =
Expand Down Expand Up @@ -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 =
Expand All @@ -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
Expand All @@ -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

Expand All @@ -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 =>
Expand All @@ -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
Expand Down Expand Up @@ -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 =>
Expand Down

0 comments on commit ac9d8a9

Please sign in to comment.