Merge pull request #1089 from GaloisInc/update-deps

Update submodules.
GaloisInc · Mar 9, 2021 · a818032 · a818032
2 parents 2ac13ae + a9d3979
commit a818032
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 10 deletions.
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/cryptol-specs b/deps/cryptol-specs
diff --git a/deps/flexdis86 b/deps/flexdis86
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
diff --git a/deps/parameterized-utils b/deps/parameterized-utils
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
@@ -24,7 +24,7 @@ import Data.Traversable (for)
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
-import Cryptol.ModuleSystem.Env (ModuleEnv)
+import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
 import Cryptol.ModuleSystem.Monad (ModuleM, interactive, runModuleM, setNameSeeds, setSupply, typeCheckWarnings, typeCheckingFailed)
 import qualified Cryptol.ModuleSystem.Renamer as MR
@@ -33,6 +33,7 @@ import qualified Cryptol.Parser as CP
 import Cryptol.Parser.Position (emptyRange, getLoc)
 import Cryptol.TypeCheck (tcExpr)
 import Cryptol.TypeCheck.Monad (InferOutput(..), inpVars, inpTSyns)
+import Cryptol.TypeCheck.Solver.SMT (withSolver)
 import Cryptol.Utils.Ident (interactiveName)
 import Cryptol.Utils.Logger (quietLogger)
 import Cryptol.Utils.PP
@@ -64,7 +65,9 @@ getTypedTermOfCExp fileReader sc cenv expr =
   do let ?fileReader = fileReader
      let env = eModuleEnv cenv
      let minp = ModuleInput True (pure defaultEvalOpts) B.readFile env
-     mres <- runModuleM minp $
+     mres <-
+       withSolver (meSolverConfig env) $ \s ->
+       runModuleM (minp s) $
        do npe <- interactive (noPat expr) -- eliminate patterns
 
           -- resolve names

diff --git a/src/SAWScript/AutoMatch.hs b/src/SAWScript/AutoMatch.hs
@@ -435,7 +435,8 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
 
       cryptolAbstractNamesSAW :: [SAWScript.LName] -> Cryptol.Expr Cryptol.PName -> Cryptol.Expr Cryptol.PName
       cryptolAbstractNamesSAW names expr =
-         Cryptol.EFun (for names $ Cryptol.PVar . cryptolLocate . SAWScript.getVal) expr
+         Cryptol.EFun Cryptol.emptyFunDesc
+         (for names $ Cryptol.PVar . cryptolLocate . SAWScript.getVal) expr
 
       cryptolApplyFunctionSAW :: SAWScript.LName -> [SAWScript.LName] -> Cryptol.Expr Cryptol.PName
       cryptolApplyFunctionSAW function args =

diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -22,6 +22,7 @@ import Cryptol.ModuleSystem.Name
 import Cryptol.Utils.Ident (unpackIdent)
 import Cryptol.Utils.Logger (quietLogger)
 import qualified Cryptol.TypeCheck.AST as AST
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.PP
 
 -- | Parse a Cryptol module into a list of declarations
@@ -31,7 +32,9 @@ getDeclsCryptol path = do
    let evalOpts = EvalOpts quietLogger defaultPPOpts
    modEnv <- M.initialModuleEnv
    let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
-   (result, warnings) <- M.loadModuleByPath path minp
+   (result, warnings) <-
+     SMT.withSolver (M.meSolverConfig modEnv) $ \s ->
+     M.loadModuleByPath path (minp s)
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty
       case result of
+1 −0		cryptol-remote-api/Dockerfile
+6 −5		cryptol-remote-api/cryptol-eval-server/Main.hs
+11 −5		cryptol-remote-api/cryptol-remote-api.cabal
+12 −9		cryptol-remote-api/src/CryptolServer.hs
+1 −1		cryptol.cabal
+ −		docs/ProgrammingCryptol.pdf
+1 −1		docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
+6 −1		src/Cryptol/Backend/Monad.hs
+4 −3		src/Cryptol/ModuleSystem/Base.hs
+8 −0		src/Cryptol/ModuleSystem/Monad.hs
+9 −3		src/Cryptol/ModuleSystem/Renamer.hs
+6 −5		src/Cryptol/Parser.y
+18 −3		src/Cryptol/Parser/AST.hs
+2 −2		src/Cryptol/Parser/Names.hs
+23 −13		src/Cryptol/Parser/NoPat.hs
+63 −20		src/Cryptol/Parser/ParserUtils.hs
+5 −0		src/Cryptol/Parser/Position.hs
+5 −2		src/Cryptol/REPL/Command.hs
+3 −2		src/Cryptol/Symbolic.hs
+6 −1		src/Cryptol/Symbolic/SBV.hs
+2 −0		src/Cryptol/TypeCheck.hs
+28 −5		src/Cryptol/TypeCheck/Error.hs
+14 −9		src/Cryptol/TypeCheck/Infer.hs
+1 −0		src/Cryptol/TypeCheck/InferTypes.hs
+3 −3		src/Cryptol/TypeCheck/Instantiate.hs
+3 −3		src/Cryptol/TypeCheck/Kind.hs
+46 −13		src/Cryptol/TypeCheck/Monad.hs
+22 −19		src/Cryptol/TypeCheck/Solver/SMT.hs
+24 −10		src/Cryptol/TypeCheck/Type.hs
+4 −4		tests/issues/T146.icry.stdout
+4 −0		tests/issues/issue1024.icry
+27 −0		tests/issues/issue1024.icry.stdout
+5 −0		tests/issues/issue1024a.cry
+5 −0		tests/issues/issue1024b.cry
+8 −0		tests/issues/issue1093.icry
+7 −0		tests/issues/issue1093.icry.stdout
+2 −2		tests/issues/issue290v2.icry.stdout
+3 −2		tests/issues/issue322.icry.stdout
+5 −0		tests/issues/issue567.icry
+27 −0		tests/issues/issue567.icry.stdout
+2 −2		tests/issues/issue723.icry.stdout
+1 −1		tests/issues/issue845.icry.stdout
+9 −0		tests/issues/issue962.icry
+23 −0		tests/issues/issue962.icry.stdout
+13 −0		tests/issues/issue962a.cry
+36 −0		tests/issues/issue962b.cry
+8 −8		tests/regression/specialize.icry.stdout
+7 −6		tests/regression/tc-errors.icry.stdout
+7 −4		utils/CryHtml.hs
+13 −9		Primitive/Asymmetric/Signature/Dilithium/Round1/DilithiumBitVec.cry
+5 −6		Primitive/Asymmetric/Signature/Dilithium/Round1/DilithiumInteger.cry
+1 −1		Primitive/Asymmetric/Signature/Dilithium/Round1/DilithiumMedium.cry
+20 −0		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumMedium.cry
+314 −406		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry
+20 −0		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumRecommended.cry
+20 −0		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumVeryhigh.cry
+19 −0		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumWeak.cry
+65 −0		Primitive/Asymmetric/Signature/Dilithium/Utils.cry
+33 −0		Primitive/Asymmetric/Signature/Dilithium/test/keypair_round2.cry
+1 −1		Primitive/Asymmetric/Signature/Dilithium/test/signFinal.cry
+1 −1		Primitive/Asymmetric/Signature/Dilithium/test/testDilithium.cry
+1 −1		Primitive/Asymmetric/Signature/Dilithium/test/testDilithium2.cry
+1 −1		Primitive/Asymmetric/Signature/Dilithium/test/test_latest.cry
+2 −3		Primitive/Asymmetric/Signature/Dilithium/test/testcase0.cry
+14 −2		src/Data/Parameterized/Context.hs
+8 −0		test/Test/Context.hs
+7 −2		cryptol-saw-core/css/Main.hs
+29 −3		cryptol-saw-core/saw/Cryptol.sawcore
+9 −1		cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+9 −6		cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs