From eb2040cf24967309e933ae20c1a60cbb0e972af6 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 7 Apr 2021 17:25:52 -0700 Subject: [PATCH 1/3] Adapt to GaloisInc/cryptol#1128 "persistent-solver2". --- cryptol-saw-core/css/Main.hs | 6 +++--- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 17 +++++++++++++++-- 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/cryptol-saw-core/css/Main.hs b/cryptol-saw-core/css/Main.hs index 7dec5cc44d..0517eb14dc 100644 --- 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 index 4d640ce7e4..5bde4dbd26 100644 --- 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 From 2ff337c84af6c8dcbd36d28a85ef1a98ca45bfc8 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 26 Apr 2021 18:07:15 -0700 Subject: [PATCH 2/3] Adapt saw-script to GaloisInc/cryptol#1128 "persist-solver2". --- deps/cryptol | 2 +- src/SAWScript/AutoMatch/Cryptol.hs | 4 +++- src/SAWScript/Builtins.hs | 4 ++-- src/SAWScript/Interpreter.hs | 3 +-- 4 files changed, 7 insertions(+), 6 deletions(-) diff --git a/deps/cryptol b/deps/cryptol index 8ed946ea75..b4e0a7fbe3 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 8ed946ea75646f732e46c6917dd4e95a4d4e964e +Subproject commit b4e0a7fbe3bd5ea450efc46cfdf0992cc857219b diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs index a782ef8c86..97de1ef35a 100644 --- 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 index 9a38fd73fe..4dc754678d 100644 --- a/src/SAWScript/Builtins.hs +++ b/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 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 66f84344c2..d2b86f6ea9 100644 --- a/src/SAWScript/Interpreter.hs +++ b/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 From 8615fc06c270bcb30a285d8223334b97a42c0144 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 18 May 2021 11:22:25 -0700 Subject: [PATCH 3/3] Fixups to saw-remote-api This mostly consists of commenting-out the `validateSAWState` function. It doesn't apper to have any call sites, so I'm not sure what it is intended to be used for. --- saw-remote-api/src/SAWServer.hs | 49 ++++++++++--------- .../src/SAWServer/CryptolExpression.hs | 3 +- 2 files changed, 27 insertions(+), 25 deletions(-) diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 57a910e2db..4d00a97c4f 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/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 = diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs index b52b8e5f57..a464c7716f 100644 --- a/saw-remote-api/src/SAWServer/CryptolExpression.hs +++ b/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)