Merge pull request #591 from GaloisInc/bh-performance

Remove completely unnecessary call to `mkTypedTerm`.
GaloisInc · Nov 18, 2019 · 0177adb · 0177adb
2 parents 47aa9f3 + 207dab9
commit 0177adb
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 6 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/saw-core b/deps/saw-core
diff --git 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
@@ -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/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"
 
 ------------------------------------------------------------------------

diff --git 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
@@ -369,7 +368,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
+56 −79		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+3 −3		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs
+14 −10		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+6 −4		crucible/src/Lang/Crucible/CFG/Expr.hs
+1 −1		crucible/src/Lang/Crucible/Simulator/RegValue.hs
+65 −38		what4/src/What4/Expr/Builder.hs
+28 −16		what4/src/What4/Expr/WeightedSum.hs
+4 −4		what4/src/What4/Interface.hs
+13 −13		what4/src/What4/SemiRing.hs
+1 −1		what4/src/What4/Symbol.hs
+3 −63		src/Verifier/SAW/Module.hs
+3 −6		src/Verifier/SAW/SharedTerm.hs
+0 −2		src/Verifier/SAW/TypedAST.hs