Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Teach online what4 backend about smtFile option #1476

Merged
merged 1 commit into from
Dec 17, 2022
+29 −18
Merged

Teach online what4 backend about smtFile option #1476

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 29 additions & 18 deletions src/Cryptol/Symbolic/What4.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ import Control.Concurrent.MVar
import Control.Monad.IO.Class
import Control.Monad (when, foldM, forM_, void)
import qualified Control.Exception as X
import System.IO (Handle)
import System.IO (Handle, IOMode(..), withFile)
import Data.Time
import Data.IORef
import Data.List (intercalate, tails, inits)
Expand Down Expand Up @@ -373,7 +373,7 @@ satProve ::
ProverCommand ->
M.ModuleCmd (Maybe String, ProverResult)

satProve solverCfg hashConsing warnUninterp ProverCommand {..} =
satProve solverCfg hashConsing warnUninterp pc@ProverCommand {..} =
protectStack proverError \modIn ->
M.runModuleM modIn
do w4sym <- liftIO makeSym
Expand Down Expand Up @@ -414,13 +414,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 pc primMap logData ts args (Just safety) query

SafetyQuery ->
singleQuery sym solverCfg primMap logData ts args (Just safety) query
singleQuery sym solverCfg pc primMap logData ts args (Just safety) query

SatQuery num ->
multiSATQuery sym solverCfg primMap logData ts args query num
multiSATQuery sym solverCfg pc primMap logData ts args query num

printUninterpWarn :: Logger -> Set Text -> IO ()
printUninterpWarn lg uninterpWarns =
Expand Down Expand Up @@ -477,6 +477,7 @@ multiSATQuery :: forall sym t fm.
sym ~ W4.ExprBuilder t CryptolState fm =>
What4 sym ->
W4ProverConfig ->
ProverCommand ->
PrimMap ->
W4.LogData ->
[FinType] ->
Expand All @@ -485,23 +486,24 @@ multiSATQuery :: forall sym t fm.
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 solverCfg pc primMap logData ts args query (SomeSat n) | n <= 1 =
singleQuery sym solverCfg pc primMap logData ts args Nothing query

multiSATQuery _sym W4OfflineConfig _primMap _logData _ts _args _query _satNum =
multiSATQuery _sym W4OfflineConfig _pc _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 =
multiSATQuery _sym (W4Portfolio _) _pc _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 =
multiSATQuery _sym (W4ProverConfig (AnAdapter adpt)) _pc _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 =
ProverCommand{..} primMap _logData ts args query satNum0 =
withMaybeFile pcSmtFile WriteMode $ \smtFileHdl ->
X.bracket
(W4.startSolverProcess fs Nothing (w4 sym))
(W4.startSolverProcess fs smtFileHdl (w4 sym))
(void . W4.shutdownSolverProcess)
(\ (proc :: W4.SolverProcess t s) ->
do W4.assume (W4.solverConn proc) query
Expand Down Expand Up @@ -627,6 +629,7 @@ singleQuery ::
sym ~ W4.ExprBuilder t CryptolState fm =>
What4 sym ->
W4ProverConfig ->
ProverCommand ->
PrimMap ->
W4.LogData ->
[FinType] ->
Expand All @@ -635,12 +638,12 @@ singleQuery ::
W4.Pred sym ->
IO (Maybe String, ProverResult)

singleQuery _ W4OfflineConfig _primMap _logData _ts _args _msafe _query =
singleQuery _ W4OfflineConfig _pc _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
singleQuery sym (W4Portfolio ps) pc primMap logData ts args msafe query =
do as <- mapM async [ singleQuery sym (W4ProverConfig p) pc primMap logData ts args msafe query
| p <- NE.toList ps
]
waitForResults [] as
Expand All @@ -659,7 +662,7 @@ singleQuery sym (W4Portfolio ps) primMap logData ts args msafe query =
do forM_ others (\a -> X.throwTo (asyncThreadId a) ExitSuccess)
return r

singleQuery sym (W4ProverConfig (AnAdapter adpt)) primMap logData ts args msafe query =
singleQuery sym (W4ProverConfig (AnAdapter adpt)) _pc primMap logData ts args msafe query =
do pres <- W4.solver_adapter_check_sat adpt (w4 sym) logData [query] $ \res ->
case res of
W4.Unknown -> return (ProverError "Solver returned UNKNOWN")
Expand All @@ -677,9 +680,10 @@ 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 =
ProverCommand{..} primMap _logData ts args msafe query =
withMaybeFile pcSmtFile WriteMode $ \smtFileHdl ->
X.bracket
(W4.startSolverProcess fs Nothing (w4 sym))
(W4.startSolverProcess fs smtFileHdl (w4 sym))
(void . W4.shutdownSolverProcess)
(\ (proc :: W4.SolverProcess t s) ->
do W4.assume (W4.solverConn proc) query
Expand All @@ -699,6 +703,13 @@ singleQuery sym (W4ProverConfig (AnOnlineAdapter nm fs _opts (_ :: Proxy s)))
)


-- | Like 'withFile', but lifted to work over 'Maybe'.
withMaybeFile :: Maybe FilePath -> IOMode -> (Maybe Handle -> IO r) -> IO r
withMaybeFile mbFP mode action =
case mbFP of
Just fp -> withFile fp mode (action . Just)
Nothing -> action Nothing

computeModelPred ::
sym ~ W4.ExprBuilder t CryptolState fm =>
What4 sym ->
Expand Down