From 3a556b445e196b6a2de69876a1ecbc99909970e3 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 23 Feb 2021 17:18:41 -0800 Subject: [PATCH 1/2] Update cryptol submodule and adapt to changes. The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver" --- deps/cryptol | 2 +- deps/saw-core | 2 +- saw-remote-api/src/SAWServer/CryptolExpression.hs | 7 +++++-- src/SAWScript/AutoMatch.hs | 3 ++- src/SAWScript/AutoMatch/Cryptol.hs | 5 ++++- 5 files changed, 13 insertions(+), 6 deletions(-) diff --git a/deps/cryptol b/deps/cryptol index 0abde1e55e..538b6c4ff5 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 0abde1e55e4db85a054e8976c61531ca7d29137a +Subproject commit 538b6c4ff5c8ae83ca27f320357d534c9ae69249 diff --git a/deps/saw-core b/deps/saw-core index ed0d14aa85..78185d35a9 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit ed0d14aa85818be4eb258832115ed77348ea8846 +Subproject commit 78185d35a936765a906e1181b3a5c13e28336bef diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs index 6cff2c924b..6da82d66ee 100644 --- 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 index 497070bb54..23b86b825e 100644 --- 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 index ef6e4f8bb0..a782ef8c86 100644 --- 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 From a9d397917d0f549390d1d683798407c2cbced1ce Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 2 Mar 2021 17:25:30 -0800 Subject: [PATCH 2/2] Update submodules. --- deps/cryptol | 2 +- deps/cryptol-specs | 2 +- deps/flexdis86 | 2 +- deps/llvm-pretty-bc-parser | 2 +- deps/parameterized-utils | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/deps/cryptol b/deps/cryptol index 538b6c4ff5..8f914a7b88 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 538b6c4ff5c8ae83ca27f320357d534c9ae69249 +Subproject commit 8f914a7b8815718d4e510966199045e0bec4d099 diff --git a/deps/cryptol-specs b/deps/cryptol-specs index d6690d8db9..728b984fed 160000 --- a/deps/cryptol-specs +++ b/deps/cryptol-specs @@ -1 +1 @@ -Subproject commit d6690d8db90aa5e00dad1e952c1e42b33e9791b2 +Subproject commit 728b984fedef37ad2ffcc65f4c16430c31f484f1 diff --git a/deps/flexdis86 b/deps/flexdis86 index 3bcd016529..3833a0f87a 160000 --- a/deps/flexdis86 +++ b/deps/flexdis86 @@ -1 +1 @@ -Subproject commit 3bcd0165296775d3928981d4291348001280c1c4 +Subproject commit 3833a0f87afaaa7f7becab94006a8817818b1897 diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index c38b86b8b4..54737bd367 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit c38b86b8b485c85181ab1bfc682fae194c8d4027 +Subproject commit 54737bd3675d54a795203bbd54a027e36119d233 diff --git a/deps/parameterized-utils b/deps/parameterized-utils index 51ff7241a4..f7ab148ace 160000 --- a/deps/parameterized-utils +++ b/deps/parameterized-utils @@ -1 +1 @@ -Subproject commit 51ff7241a4e96383b54513734bb2c3c6930435d5 +Subproject commit f7ab148ace220fb28ce7760552351f5f55f9db04