From 8fa63131be83ba98825cb32f89c5ec11a270263a Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Sat, 16 Nov 2019 19:07:19 -0800
Subject: [PATCH] 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