Update cryptol and saw-core, adapt to GaloisInc/cryptol#995.

GaloisInc · Jan 28, 2021 · 06c08d2 · 06c08d2
1 parent 040a23f
commit 06c08d2
Show file tree

Hide file tree

Showing 9 changed files with 15 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-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -9,7 +9,7 @@ import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
 
 import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
-import Cryptol.ModuleSystem (ModuleRes)
+import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
 import Cryptol.ModuleSystem.Env (ModuleEnv)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
@@ -47,7 +47,8 @@ getTypedTermOfCExp ::
 getTypedTermOfCExp fileReader sc cenv expr =
   do let ?fileReader = fileReader
      let env = eModuleEnv cenv
-     mres <- runModuleM (defaultEvalOpts, B.readFile, env) $
+     let minp = ModuleInput True defaultEvalOpts B.readFile env
+     mres <- runModuleM minp $
        do npe <- interactive (noPat expr) -- eliminate patterns
 
           -- resolve names

diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs
@@ -47,7 +47,7 @@ module SAWScript.REPL.Monad (
   , getSAWScriptNames
   ) where
 
-import Cryptol.Eval (EvalError)
+import Cryptol.Eval (EvalError, EvalErrorEx(..))
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.NamingEnv as MN
 import Cryptol.ModuleSystem.NamingEnv (NamingEnv)
@@ -235,8 +235,8 @@ rethrowEvalError m = run `X.catch` rethrow
     a <- m
     return $! a
 
-  rethrow :: EvalError -> IO a
-  rethrow exn = X.throwIO (EvalError exn)
+  rethrow :: EvalErrorEx -> IO a
+  rethrow (EvalErrorEx _ exn) = X.throwIO (EvalError exn)
 
 
 

diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -30,7 +30,8 @@ getDeclsCryptol :: FilePath -> IO (Interaction (Maybe [Decl]))
 getDeclsCryptol path = do
    let evalOpts = EvalOpts quietLogger defaultPPOpts
    modEnv <- M.initialModuleEnv
-   (result, warnings) <- M.loadModuleByPath path (evalOpts, BS.readFile, modEnv)
+   let minp = M.ModuleInput True evalOpts BS.readFile modEnv
+   (result, warnings) <- M.loadModuleByPath path minp
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty
       case result of

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
@@ -1328,7 +1328,7 @@ eval_int t = do
     C.Forall [] [] (isInteger -> True) -> return ()
     _ -> fail "eval_int: argument is not a finite bitvector"
   v <- io $ rethrowEvalError $ SV.evaluateTypedTerm sc t'
-  io $ C.runEval (C.bvVal <$> C.fromVWord C.Concrete "eval_int" v)
+  io $ C.runEval mempty (C.bvVal <$> C.fromVWord C.Concrete "eval_int" v)
 
 -- Predicate on Cryptol types true of integer types, i.e. types
 -- @[n]Bit@ for *finite* @n@.

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
@@ -585,7 +585,7 @@ print_value (VTerm t) = do
                               , V.useBase = ppOptsBase opts
                               }
   evaled_t <- io $ evaluateTypedTerm sc t'
-  doc <- io $ V.runEval (V.ppValue V.Concrete opts' evaled_t)
+  doc <- io $ V.runEval mempty (V.ppValue V.Concrete opts' evaled_t)
   sawOpts <- getOptions
   io (rethrowEvalError $ printOutLn sawOpts Info $ show $ doc)
 

diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs
@@ -308,7 +308,7 @@ showCexResults vpopts sc opts ms vs exts vals = do
   printOutLn vpopts Info $ "When verifying " ++ specName ms ++ ":"
   printOutLn vpopts Info $ "Proof of " ++ vsVCName vs ++ " failed."
   printOutLn vpopts Info $ "Counterexample:"
-  let showVal v = show <$> (Cryptol.runEval
+  let showVal v = show <$> (Cryptol.runEval mempty
                     (Cryptol.ppValue Cryptol.Concrete (cryptolPPOpts opts) (exportFirstOrderValue v)))
   mapM_ (\(n, v) -> do vdoc <- showVal v
                        printOutLn vpopts Info ("  " ++ n ++ ": " ++ vdoc)) vals

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 (CV.ppValue CV.Concrete opts' lv)
-     sv_doc <- CV.runEval (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
+11 −0		CHANGES.md
+8 −2		cryptol-remote-api/src/CryptolServer.hs
+3 −1		cryptol-remote-api/src/CryptolServer/Data/Expression.hs
+1 −0		cryptol.cabal
+10 −0		cryptol/Main.hs
+20 −20		cryptol/REPL/Haskeline.hs
+25 −15		src/Cryptol/Backend.hs
+6 −5		src/Cryptol/Backend/Concrete.hs
+158 −57		src/Cryptol/Backend/Monad.hs
+29 −21		src/Cryptol/Backend/SBV.hs
+13 −6		src/Cryptol/Backend/What4.hs
+116 −74		src/Cryptol/Eval.hs
+145 −290		src/Cryptol/Eval/Concrete.hs
+12 −8		src/Cryptol/Eval/Env.hs
+504 −277		src/Cryptol/Eval/Generic.hs
+39 −0		src/Cryptol/Eval/Prims.hs
+4 −1		src/Cryptol/Eval/Reference.lhs
+24 −146		src/Cryptol/Eval/SBV.hs
+2 −2		src/Cryptol/Eval/Type.hs
+72 −67		src/Cryptol/Eval/Value.hs
+104 −210		src/Cryptol/Eval/What4.hs
+1 −0		src/Cryptol/IR/FreeVars.hs
+6 −8		src/Cryptol/ModuleSystem.hs
+15 −4		src/Cryptol/ModuleSystem/Base.hs
+1 −0		src/Cryptol/ModuleSystem/InstantiateModule.hs
+33 −14		src/Cryptol/ModuleSystem/Monad.hs
+2 −2		src/Cryptol/Parser.y
+2 −1		src/Cryptol/Parser/AST.hs
+1 −1		src/Cryptol/Parser/Lexer.x
+2 −0		src/Cryptol/Parser/LexerUtils.hs
+0 −1		src/Cryptol/Parser/Position.hs
+170 −102		src/Cryptol/REPL/Command.hs
+24 −9		src/Cryptol/REPL/Monad.hs
+1 −1		src/Cryptol/Symbolic.hs
+17 −10		src/Cryptol/Symbolic/SBV.hs
+13 −9		src/Cryptol/Symbolic/What4.hs
+18 −14		src/Cryptol/Testing/Random.hs
+1 −0		src/Cryptol/Transform/AddModParams.hs
+1 −0		src/Cryptol/Transform/MonoValues.hs
+4 −3		src/Cryptol/Transform/Specialize.hs
+3 −1		src/Cryptol/TypeCheck.hs
+8 −2		src/Cryptol/TypeCheck/AST.hs
+7 −2		src/Cryptol/TypeCheck/Infer.hs
+10 −2		src/Cryptol/TypeCheck/Monad.hs
+1 −0		src/Cryptol/TypeCheck/Parseable.hs
+18 −7		src/Cryptol/TypeCheck/Sanity.hs
+1 −0		src/Cryptol/TypeCheck/Subst.hs
+3 −0		src/Cryptol/TypeCheck/TypeOf.hs
+4 −4		tests/issues/T820.icry.stdout
+4 −0		tests/issues/issue066.icry.stdout
+1 −1		tests/issues/issue084.icry.stdout
+2 −2		tests/issues/issue101.icry.stdout
+7 −0		tests/issues/issue103.icry.stdout
+3 −0		tests/issues/issue211.icry.stdout
+1 −1		tests/issues/issue322.icry.stdout
+1 −1		tests/issues/issue364.icry.stdout
+11 −11		tests/issues/issue382.icry.stdout
+6 −0		tests/issues/issue413.icry.stdout
+12 −12		tests/issues/issue582.icry.stdout
+1 −1		tests/issues/issue712.icry.stdout
+1 −1		tests/issues/issue713.icry.stdout
+1 −1		tests/issues/issue746.icry.stdout
+3 −3		tests/issues/issue818.icry.stdout
+2 −2		tests/issues/issue835.icry.stdout
+10 −10		tests/issues/issue845.icry.stdout
+16 −0		tests/issues/issue861.icry.stdout
+8 −8		tests/issues/issue910.icry.stdout
+2 −2		tests/issues/issue913.icry.stdout
+8 −8		tests/regression/float.icry.stdout
+142 −142		tests/regression/instance.icry.stdout
+4 −4		tests/regression/primes.icry.stdout
+3 −3		tests/regression/repeatFields.icry.stdout
+14 −0		tests/regression/safety.icry.stdout
+11 −11		tests/regression/tc-errors.icry.stdout
+4 −2		cryptol-saw-core/css/Main.hs
+13 −7		cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+4 −2		cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs