From d9938706fc0b29058194dc1082e36e13d1d56e8a Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 16 Apr 2021 12:32:15 -0700 Subject: [PATCH] Updates flowing from cryptol PRs #1084 and #1136 --- deps/cryptol | 2 +- deps/saw-core | 2 +- saw/SAWScript/REPL/Monad.hs | 5 +++-- src/SAWScript/AutoMatch/Cryptol.hs | 5 ++++- src/SAWScript/Builtins.hs | 6 ++++-- src/SAWScript/Interpreter.hs | 2 +- src/SAWScript/Value.hs | 2 +- src/SAWScript/VerificationCheck.hs | 4 ++-- src/SAWScript/X86Spec.hs | 4 ++-- 9 files changed, 19 insertions(+), 13 deletions(-) diff --git a/deps/cryptol b/deps/cryptol index 23c396b1a9..a279e78d53 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 23c396b1a9951108aeedbd51fa2bc9d5a9369365 +Subproject commit a279e78d5313d70e8fff47e5965fdfba5c2e1215 diff --git a/deps/saw-core b/deps/saw-core index 6e32c659fd..eee8543c8a 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit 6e32c659fdadfcf99d3d586e7dcda2b7bd9a0e10 +Subproject commit eee8543c8ad7e8c329b33d579e06d1aae6ddea07 diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index 3e7f425a23..b2e6d02ba8 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -55,6 +55,7 @@ import Cryptol.Parser (ParseError,ppError) import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError) import Cryptol.Parser.NoPat (Error) import qualified Cryptol.TypeCheck.AST as T +import Cryptol.Utils.Ident (Namespace(..)) import Cryptol.Utils.PP #if !MIN_VERSION_base(4,8,0) @@ -297,13 +298,13 @@ getNewtypes = do getExprNames :: REPL [String] getExprNames = do fNames <- fmap getNamingEnv getCryptolEnv - return (map (show . pp) (Map.keys (MN.neExprs fNames))) + return (map (show . pp) (Map.keys (MN.namespaceMap NSValue fNames))) -- | Get visible type signature names. getTypeNames :: REPL [String] getTypeNames = do fNames <- fmap getNamingEnv getCryptolEnv - return (map (show . pp) (Map.keys (MN.neTypes fNames))) + return (map (show . pp) (Map.keys (MN.namespaceMap NSType fNames))) getPropertyNames :: REPL [String] getPropertyNames = diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs index a782ef8c86..78d3e47ee9 100644 --- a/src/SAWScript/AutoMatch/Cryptol.hs +++ b/src/SAWScript/AutoMatch/Cryptol.hs @@ -25,6 +25,9 @@ import qualified Cryptol.TypeCheck.AST as AST import qualified Cryptol.TypeCheck.Solver.SMT as SMT import Cryptol.Utils.PP +import Verifier.SAW.CryptolEnv( meSolverConfig ) + + -- | Parse a Cryptol module into a list of declarations -- Yields an Interaction so that we can talk to the user about what went wrong getDeclsCryptol :: FilePath -> IO (Interaction (Maybe [Decl])) @@ -33,7 +36,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 39f6575958..828f503708 100644 --- 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, (<+>)) @@ -124,6 +124,8 @@ import qualified SAWScript.Prover.Exporter as Prover import qualified SAWScript.Prover.MRSolver as Prover import SAWScript.VerificationSummary +import Verifier.SAW.CryptolEnv( meSolverConfig ) + showPrim :: SV.Value -> TopLevel String showPrim v = do opts <- fmap rwPPOpts getTopLevelRW @@ -1140,7 +1142,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 = 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 932b5d616c..b405344ac2 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -88,7 +88,7 @@ import SAWScript.Crucible.LLVM.Skeleton.Builtins import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CIR -- Cryptol -import Cryptol.ModuleSystem.Env (meSolverConfig) +import Verifier.SAW.CryptolEnv (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) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 78db76a374..4855368899 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -338,7 +338,7 @@ evaluate sc t = evaluateTypedTerm :: SharedContext -> TypedTerm -> IO C.Value evaluateTypedTerm sc (TypedTerm schema trm) = - exportValueWithSchema schema <$> evaluate sc trm + C.runEval mempty . exportValueWithSchema schema =<< evaluate sc trm applyValue :: Value -> Value -> TopLevel Value applyValue (VLambda f) x = f x diff --git a/src/SAWScript/VerificationCheck.hs b/src/SAWScript/VerificationCheck.hs index 58fc679308..2bd4694259 100644 --- a/src/SAWScript/VerificationCheck.hs +++ b/src/SAWScript/VerificationCheck.hs @@ -61,8 +61,8 @@ vcCounterexample sc opts (EqualityCheck nm impNode specNode) evalFn = sv = exportValueWithSchema sschema sn opts' = SV.cryptolPPOpts opts -- Grr. Different pretty-printers. - lv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' lv) - sv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' sv) + lv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' =<< lv) + sv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' =<< sv) return $ vcat diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index c34f195981..1c53e145d8 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -135,7 +135,7 @@ import Cryptol.ModuleSystem.Name(Name) import Cryptol.ModuleSystem.Interface(ifTySyns) import Cryptol.TypeCheck.AST(TySyn(tsDef)) import Cryptol.TypeCheck.TypePat(aNat) -import Cryptol.Utils.PP(alwaysQualify,runDoc,pp) +import Cryptol.Utils.PP(render,pp) import Cryptol.Utils.Patterns(matchMaybe) import SAWScript.Crucible.Common (Sym, sawCoreState) @@ -1249,7 +1249,7 @@ lookupCry x mp = ) Right a -> Right a - where ppName = show . runDoc alwaysQualify . pp + where ppName = render . pp