From f155fd781499b0aeb2379f3f47eb3ffb62ac62c5 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 16 Nov 2019 05:44:04 -0800 Subject: [PATCH 1/5] Remove completely unnecessary call to `mkTypedTerm`. The Cryptol type inferred by `mkTypedTerm` was immediately ignored, so there was never any point in calling it in the first place. --- src/SAWScript/Crucible/LLVM/Override.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 6412edf0c0..e4e8776397 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -683,8 +683,8 @@ refreshTerms sc ss = where freshenTerm tt = case asExtCns (ttTerm tt) of - Just ec -> do new <- liftIO (mkTypedTerm sc =<< scFreshGlobal sc (ecName ec) (ecType ec)) - return (termId (ttTerm tt), ttTerm new) + Just ec -> do new <- liftIO (scFreshGlobal sc (ecName ec) (ecType ec)) + return (termId (ttTerm tt), new) Nothing -> error "refreshTerms: not a variable" ------------------------------------------------------------------------ From cb714ce2d32f5e4023c7cde9cda60034b407ff97 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 16 Nov 2019 19:05:45 -0800 Subject: [PATCH 2/5] Update saw-core submodule, for performance improvements in scTypeOf. --- deps/saw-core | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/saw-core b/deps/saw-core index 52d8d43d79..82d1666d13 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit 52d8d43d7913e62c7e3f50a9835de2a7a4da27c9 +Subproject commit 82d1666d139b413f573f2ec86a389c5fd5c310a2 From 8fa63131be83ba98825cb32f89c5ec11a270263a Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 16 Nov 2019 19:07:19 -0800 Subject: [PATCH 3/5] Cache basic_ss inside LLVMCrucibleContext, for use in resolveSAWTerm. Fixes #590. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 1 + src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 2 ++ src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs | 2 +- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index eb77483e70..9f271ffb77 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1044,6 +1044,7 @@ setupLLVMCrucibleContext bic opts lm@(LLVMModule _ llvm_mod mtrans) action = do , _ccBackend = sym , _ccLLVMSimContext = lsimctx , _ccLLVMGlobals = lglobals + , _ccBasicSS = biBasicSS bic } ) diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 3d94067db6..e9eb7c59cc 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -64,6 +64,7 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL +import Verifier.SAW.Rewriter (Simpset) import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm @@ -211,6 +212,7 @@ data LLVMCrucibleContext arch = , _ccBackend :: Sym , _ccLLVMSimContext :: Crucible.SimContext (Crucible.SAWCruciblePersonality Sym) Sym (CL.LLVM arch) , _ccLLVMGlobals :: Crucible.SymGlobalState Sym + , _ccBasicSS :: Simpset } makeLenses ''LLVMCrucibleContext diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 1f1b15119c..f792ac9ab1 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -369,7 +369,7 @@ resolveSAWTerm cc tp tm = Just (Some w) | Just LeqProof <- isPosNat w -> do sc <- Crucible.saw_ctx <$> readIORef (W4.sbStateManager sym) - ss <- basic_ss sc + let ss = cc^.ccBasicSS tm' <- rewriteSharedTerm sc ss tm mx <- case getAllExts tm' of [] -> do From 16c3373e3927c96f8a13a0e3ff9a63432347fa5c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 16 Nov 2019 19:08:21 -0800 Subject: [PATCH 4/5] Update crucible submodule for performance improvements. --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 6fdb562aa0..8f7db760a8 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 6fdb562aa0cd915ea45eb3f14bb6af467dd5d00f +Subproject commit 8f7db760a89915133e6b623ceed05f34f64f3e42 From 207dab90faf60857bee3a0bd58bcadba03c36a86 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 16 Nov 2019 19:09:52 -0800 Subject: [PATCH 5/5] Remove redundant import. --- src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index f792ac9ab1..df154a8cf6 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -71,7 +71,6 @@ import qualified Data.SBV.Dynamic as SBV (svAsInteger) import SAWScript.Crucible.Common (Sym) import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..)) -import SAWScript.Prover.Rewrite import SAWScript.Crucible.LLVM.MethodSpecIR --import qualified SAWScript.LLVMBuiltins as LB