Adapt to GaloisInc/cryptol#1128 "persistent-solver2".

GaloisInc · Apr 27, 2021 · 46467ab · 46467ab
1 parent fdb8987
commit 46467ab
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 5 deletions.
diff --git a/cryptol-saw-core/css/Main.hs b/cryptol-saw-core/css/Main.hs
@@ -22,7 +22,7 @@ import           Cryptol.Utils.Logger (quietLogger)
 import qualified Verifier.SAW.Cryptol as C
 import           Verifier.SAW.SharedTerm
 import qualified Verifier.SAW.Cryptol.Prelude as C
-import           Verifier.SAW.CryptolEnv (schemaNoUser)
+import           Verifier.SAW.CryptolEnv (schemaNoUser, meSolverConfig)
 
 
 import qualified Data.ABC as ABC
@@ -92,7 +92,7 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do
     modEnv <- CM.initialModuleEnv
     let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
     (e,warn) <-
-      SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
+      SMT.withSolver (meSolverConfig modEnv) $ \s ->
       CM.loadModuleByPath inputModule (minp s)
     mapM_ (print . pp) warn
     case e of
@@ -133,7 +133,7 @@ extractCryptol sc modEnv input = do
       Right x -> return x
   let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
   (exprResult, exprWarnings) <-
-    SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
+    SMT.withSolver (meSolverConfig modEnv) $ \s ->
     CM.checkExpr pexpr (minp s)
   mapM_ (print . pp) exprWarnings
   ((_, expr, schema), _modEnv') <-

diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -32,6 +32,7 @@ module Verifier.SAW.CryptolEnv
   , InputText(..)
   , lookupIn
   , resolveIdentifier
+  , meSolverConfig
   )
   where
 
@@ -466,6 +467,18 @@ bindInteger (ident, n) env =
 
 --------------------------------------------------------------------------------
 
+-- FIXME: This definition was copied from a local declaration inside
+-- function 'defaultRW' in module 'Cryptol.REPL.Monad'. The cryptol
+-- package should probably export it so we don't have to copy it.
+meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig
+meSolverConfig env =
+  TM.SolverConfig
+  { TM.solverPath = "z3"
+  , TM.solverArgs = [ "-smt2", "-in" ]
+  , TM.solverVerbose = 0
+  , TM.solverPreludePath = ME.meSearchPath env
+  }
+
 resolveIdentifier ::
   (?fileReader :: FilePath -> IO ByteString) =>
   CryptolEnv -> Text -> IO (Maybe T.Name)
@@ -480,7 +493,7 @@ resolveIdentifier env nm =
   nameEnv = getNamingEnv env
 
   doResolve pnm =
-    SMT.withSolver (ME.meSolverConfig modEnv) $ \s ->
+    SMT.withSolver (meSolverConfig modEnv) $ \s ->
     do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv
        (res, _ws) <- MM.runModuleM (minp s) $
           MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm))
@@ -646,7 +659,7 @@ liftModuleM ::
   ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv)
 liftModuleM env m =
   do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env
-     SMT.withSolver (ME.meSolverConfig env) $ \s ->
+     SMT.withSolver (meSolverConfig env) $ \s ->
        MM.runModuleM (minp s) m >>= moduleCmdResult
 
 defaultEvalOpts :: E.EvalOpts