Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

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

Merged
merged 1 commit into from
Apr 22, 2021
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions cryptol-saw-core/css/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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') <-
Expand Down
17 changes: 15 additions & 2 deletions cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ module Verifier.SAW.CryptolEnv
, InputText(..)
, lookupIn
, resolveIdentifier
, meSolverConfig
)
where

Expand Down Expand Up @@ -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)
Expand All @@ -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))
Expand Down Expand Up @@ -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
Expand Down