Merge pull request #1267 from GaloisInc/persist-solver2

Adapt to cryptol PR #1128 "persist-solver2"

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') <-

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

saw-remote-api/src/SAWServer.hs

@@ -24,7 +24,7 @@ import Data.Parameterized.Some ( Some(..) )
 import Data.Text (Text)
 import qualified Data.Text as T
 import qualified Crypto.Hash as Hash
-import qualified Crypto.Hash.Conduit as Hash
+--import qualified Crypto.Hash.Conduit as Hash
 import System.Directory (getCurrentDirectory)
 import System.IO.Silently (silence)
 
@@ -38,7 +38,7 @@ import qualified Data.AIG as AIG
 import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator)
 import qualified Lang.Crucible.JVM as CJ
 import qualified Lang.JVM.Codebase as JSS
-import qualified Verifier.SAW.CryptolEnv as CryptolEnv
+--import qualified Verifier.SAW.CryptolEnv as CryptolEnv
 import Verifier.SAW.Module (emptyModule)
 import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule)
 import Verifier.SAW.Term.Functor (mkModuleName)
@@ -59,7 +59,7 @@ import Verifier.SAW.Rewriter (Simpset)
 import qualified Cryptol.Utils.Ident as Cryptol
 
 import qualified Argo
-import qualified CryptolServer (validateServerState, ServerState(..))
+--import qualified CryptolServer (validateServerState, ServerState(..))
 import SAWServer.Exceptions
     ( serverValNotFound,
       notAnLLVMModule,
@@ -230,27 +230,28 @@ initialState readFileFn =
 -- recompute a cached result, the cached result may be used even if it is
 -- associated with stale filesystem state. See the discussion of this issue at:
 -- https://github.com/GaloisInc/argo/pull/70#discussion_r412462908
-validateSAWState :: SAWState -> IO Bool
-validateSAWState sawState =
-  checkAll
-    [ CryptolServer.validateServerState cryptolState
-    , checkAll $ map (uncurry checkHash) (M.assocs (view trackedFiles sawState))
-    ]
-  where
-    checkAll [] = pure True
-    checkAll (c : cs) =
-      do result <- c
-         if result
-           then checkAll cs
-           else pure False
-
-    checkHash path hash =
-      do currentHash <- Hash.hashFile path
-         pure (currentHash == hash)
-
-    cryptolState =
-      CryptolServer.ServerState Nothing
-        (CryptolEnv.eModuleEnv . rwCryptol . view sawTopLevelRW $ sawState)
+
+-- validateSAWState :: SAWState -> IO Bool
+-- validateSAWState sawState =
+--   checkAll
+--     [ CryptolServer.validateServerState cryptolState
+--     , checkAll $ map (uncurry checkHash) (M.assocs (view trackedFiles sawState))
+--     ]
+--   where
+--     checkAll [] = pure True
+--     checkAll (c : cs) =
+--       do result <- c
+--          if result
+--            then checkAll cs
+--            else pure False
+
+--     checkHash path hash =
+--       do currentHash <- Hash.hashFile path
+--          pure (currentHash == hash)
+
+--     cryptolState =
+--       CryptolServer.ServerState Nothing
+--         (CryptolEnv.eModuleEnv . rwCryptol . view sawTopLevelRW $ sawState)
 
 
 newtype SAWEnv =

saw-remote-api/src/SAWServer/CryptolExpression.hs

@@ -19,7 +19,7 @@ import Data.Maybe (fromMaybe)
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleError, ModuleInput(..), ModuleRes, ModuleWarning)
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
-import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
+import Cryptol.ModuleSystem.Env (ModuleEnv)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
 import Cryptol.ModuleSystem.Monad (ModuleM, interactive, runModuleM, setNameSeeds, setSupply, typeCheckWarnings, typeCheckingFailed)
 import qualified Cryptol.ModuleSystem.Renamer as MR
@@ -35,6 +35,7 @@ import SAWScript.Value (biSharedContext, TopLevelRW(..))
 import Verifier.SAW.CryptolEnv
     ( getAllIfaceDecls,
       getNamingEnv,
+      meSolverConfig,
       translateExpr,
       CryptolEnv(eExtraTypes, eExtraTSyns, eModuleEnv) )
 import Verifier.SAW.SharedTerm (SharedContext)

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

src/SAWScript/Builtins.hs

@@ -90,7 +90,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, (<+>))
@@ -1147,7 +1147,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

src/SAWScript/Interpreter.hs

@@ -89,7 +89,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)
@@ -610,7 +609,7 @@ print_value (VString s) = printOutLnTop Info (Text.unpack 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