From 953673b1f73de96f7504e01d2af08c68560635a0 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 17 Dec 2022 17:37:55 -0500 Subject: [PATCH] Teach online `what4` backend about smtFile option (#1476) This passes the value of `smtFile` to each call to `startSolverProcess` in the online `what4` backend, thereby fixing #1475. After this patch, the test case in #1475 now produces an `.smt2` file, as expected. --- src/Cryptol/Symbolic/What4.hs | 47 +++++++++++++++++++++-------------- 1 file changed, 29 insertions(+), 18 deletions(-) diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index d3ca83f8a..6dbee31b9 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -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) @@ -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 @@ -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 = @@ -477,6 +477,7 @@ multiSATQuery :: forall sym t fm. sym ~ W4.ExprBuilder t CryptolState fm => What4 sym -> W4ProverConfig -> + ProverCommand -> PrimMap -> W4.LogData -> [FinType] -> @@ -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 @@ -627,6 +629,7 @@ singleQuery :: sym ~ W4.ExprBuilder t CryptolState fm => What4 sym -> W4ProverConfig -> + ProverCommand -> PrimMap -> W4.LogData -> [FinType] -> @@ -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 @@ -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") @@ -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 @@ -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 ->