Updates flowing from cryptol PRs #1084 and #1136

GaloisInc · Apr 16, 2021 · d993870 · d993870
1 parent 9b51cd1
commit d993870
Show file tree

Hide file tree

Showing 9 changed files with 19 additions and 13 deletions.
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/saw-core b/deps/saw-core
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
+3 −3		cryptol-saw-core/css/Main.hs
+26 −11		cryptol-saw-core/saw/Cryptol.sawcore
+46 −37		cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+14 −16		cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
+10 −4		saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+21 −19		saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs