Update cryptol and saw-core, and adapt to "persist-solver2" PRs.

This patch includes the following submodule PRs: - GaloisInc/cryptol#1128 "persist-solver2" - GaloisInc/saw-core#197 "persist-solver2"
GaloisInc · Apr 26, 2021 · ee8d927 · ee8d927
1 parent 3e4169b
commit ee8d927
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 7 deletions.
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -16,6 +16,8 @@ import Data.List hiding (sort)
 import Data.Maybe
 import Data.Ord
 
+import Verifier.SAW.CryptolEnv (meSolverConfig)
+
 import Cryptol.Eval (EvalOpts(..))
 import qualified Cryptol.ModuleSystem as M
 import Cryptol.ModuleSystem.Name
@@ -33,7 +35,7 @@ getDeclsCryptol path = do
    modEnv <- M.initialModuleEnv
    let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
    (result, warnings) <-
-     SMT.withSolver (M.meSolverConfig modEnv) $ \s ->
+     SMT.withSolver (meSolverConfig modEnv) $ \s ->
      M.loadModuleByPath path (minp s)
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
@@ -89,7 +89,7 @@ import qualified Data.SBV.Dynamic as SBV
 import qualified Data.AIG as AIG
 
 -- cryptol
-import qualified Cryptol.ModuleSystem.Env as C (meSolverConfig, meSearchPath)
+import qualified Cryptol.ModuleSystem.Env as C (meSearchPath)
 import qualified Cryptol.TypeCheck as C (SolverConfig)
 import qualified Cryptol.TypeCheck.AST as C
 import qualified Cryptol.TypeCheck.PP as C (ppWithNames, pp, text, (<+>))
@@ -1148,7 +1148,7 @@ eval_int :: TypedTerm -> TopLevel Integer
 eval_int t = do
   sc <- getSharedContext
   cenv <- fmap rwCryptol getTopLevelRW
-  let cfg = C.meSolverConfig (CEnv.eModuleEnv cenv)
+  let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv)
   unless (null (getAllExts (ttTerm t))) $
     fail "term contains symbolic variables"
   opts <- getOptions

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
@@ -88,7 +88,6 @@ import           SAWScript.Crucible.LLVM.Skeleton.Builtins
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CIR
 
 -- Cryptol
-import Cryptol.ModuleSystem.Env (meSolverConfig)
 import qualified Cryptol.Eval as V (PPOpts(..))
 import qualified Cryptol.Backend.Monad as V (runEval)
 import qualified Cryptol.Eval.Value as V (defaultPPOpts, ppValue)
@@ -609,7 +608,7 @@ print_value (VString s) = printOutLnTop Info s
 print_value (VTerm t) = do
   sc <- getSharedContext
   cenv <- fmap rwCryptol getTopLevelRW
-  let cfg = meSolverConfig (CEnv.eModuleEnv cenv)
+  let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv)
   unless (null (getAllExts (ttTerm t))) $
     fail "term contains symbolic variables"
   sawopts <- getOptions
+7 −7		cryptol-remote-api/cryptol-eval-server/Main.hs
+24 −6		cryptol-remote-api/src/CryptolServer.hs
+3 −5		cryptol-remote-api/src/CryptolServer/EvalExpr.hs
+4 −4		cryptol-remote-api/src/CryptolServer/Sat.hs
+0 −3		cryptol-remote-api/src/CryptolServer/TypeCheck.hs
+0 −2		src/Cryptol/ModuleSystem/Base.hs
+0 −9		src/Cryptol/ModuleSystem/Env.hs
+0 −10		src/Cryptol/ModuleSystem/Monad.hs
+6 −8		src/Cryptol/REPL/Command.hs
+53 −11		src/Cryptol/REPL/Monad.hs
+0 −1		src/Cryptol/TypeCheck/Monad.hs
+3 −3		cryptol-saw-core/css/Main.hs
+15 −2		cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs