From f3f846b0a23ec7eceb417eaec058f2fc493d93f7 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 22 Apr 2021 15:26:57 -0700
Subject: [PATCH] update to latest crucible + macaw

---
 deps/crucible                               |  2 +-
 deps/macaw                                  |  2 +-
 src/SAWScript/Crucible/LLVM/Builtins.hs     |  4 ++--
 src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs |  3 ++-
 src/SAWScript/Crucible/LLVM/MethodSpecIR.hs |  4 +++-
 src/SAWScript/X86.hs                        | 12 ++----------
 6 files changed, 11 insertions(+), 16 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index 53a726630a..97be912e7a 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 53a726630a59602bb8d702dddd9fac5b25e77c0b
+Subproject commit 97be912e7a08699e90f19aba861872022e4ff46d
diff --git a/deps/macaw b/deps/macaw
index 8a0c760886..b813ecda9a 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit 8a0c760886ae6b9d4563bc6b647666a3a36c8c72
+Subproject commit b813ecda9a4339ce31b6fb4b48f7e0f8d394ca55
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 1c12ef289a..ceac360f54 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -545,7 +545,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
                  }
                Nothing -> mem0
 
-     let globals1 = Crucible.llvmGlobals (ccLLVMContext cc) mem
+     let globals1 = Crucible.llvmGlobals mvar mem
 
      -- construct the initial state for verifications
      opts <- getOptions
@@ -1353,7 +1353,7 @@ setupLLVMCrucibleContext pathSat lm action =
                mem <- Crucible.populateConstGlobals sym (Crucible.globalInitMap mtrans)
                         =<< Crucible.initializeMemoryConstGlobals sym ctx llvm_mod
 
-               let globals  = Crucible.llvmGlobals ctx mem
+               let globals  = Crucible.llvmGlobals (Crucible.llvmMemVar ctx) mem
 
                let setupMem =
                      do -- register the callable override functions
diff --git a/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs b/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs
index c951f756f2..afbcf89988 100644
--- a/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs
+++ b/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs
@@ -130,6 +130,7 @@ module SAWScript.Crucible.LLVM.CrucibleLLVM
   , pattern PtrRepr
   , ppPtr
   , projectLLVM_bv
+  , mkMemVar
   ) where
 
 import Lang.Crucible.LLVM
@@ -171,7 +172,7 @@ import Lang.Crucible.LLVM.MemModel
   (Mem, MemImpl, doResolveGlobal, storeRaw, storeConstRaw, mallocRaw, mallocConstRaw,
    ppMem, packMemValue, unpackMemValue, buildDisjointRegionsAssertion,
    doLoad, doStore, loadRaw, doPtrAddOffset, assertSafe, isZero, testEqual,
-   emptyMem, doMalloc,
+   emptyMem, doMalloc, mkMemVar,
    LLVMVal(..),
    LLVMPtr, HasPtrWidth, ptrToPtrVal, mkNullPointer, ptrIsNull, ppPtr, ptrEq,
    pattern LLVMPointerRepr, LLVMPointerType,
diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
index 93ded0c184..859dd6dfb4 100644
--- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
+++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
@@ -105,6 +105,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
 import           Control.Lens
 import           Control.Monad (when)
 import           Data.Functor.Compose (Compose(..))
+import qualified Data.Text as Text
 import           Data.Type.Equality (TestEquality(..))
 import qualified Prettyprinter as PPL
 import qualified Text.LLVM.AST as L
@@ -254,7 +255,8 @@ loadLLVMModule file halloc =
        Left err -> return (Left err)
        Right llvm_mod ->
          do let ?optLoopMerge = False
-            Some mtrans <- CL.translateModule halloc llvm_mod
+            memVar <- CL.mkMemVar (Text.pack "saw:llvm_memory") halloc
+            Some mtrans <- CL.translateModule halloc memVar llvm_mod
             return (Right (Some (LLVMModule file llvm_mod mtrans)))
 
 instance TestEquality LLVMModule where
diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
index 940ff8fbb0..384d75b38f 100644
--- a/src/SAWScript/X86.hs
+++ b/src/SAWScript/X86.hs
@@ -29,7 +29,6 @@ module SAWScript.X86
 
 import Control.Lens (toListOf, folded, (^.))
 import Control.Exception(Exception(..),throwIO)
-import Control.Monad.ST (stToIO)
 import Control.Monad.IO.Class(liftIO)
 
 import qualified Data.BitVector.Sized as BV
@@ -201,7 +200,7 @@ proof fileReader archi file mbCry globs fun =
      sym <- newSAWCoreBackend sc
      let ?fileReader = fileReader
      cenv <- loadCry sym mbCry
-     mvar <- mkMemVar halloc
+     mvar <- mkMemVar "saw_x86:llvm_memory" halloc
      proofWithOptions Options
        { fileName = file
        , function = fun
@@ -521,7 +520,7 @@ makeCFG ::
   MemSegmentOff 64 ->
   IO TheCFG
 makeCFG opts elf name addr =
-  do (_,Some funInfo) <- stToIO $ analyzeFunction quiet addr UserRequest empty
+  do (_,Some funInfo) <- return $ analyzeFunction addr UserRequest empty
      -- writeFile "MACAW.cfg" (show (pretty funInfo))
      mkFunCFG x86 (allocator opts) cruxName posFn funInfo
   where
@@ -610,13 +609,6 @@ x86 = x86_64MacawSymbolicFns
 --    * not modified by interrupts
 
 
---------------------------------------------------------------------------------
--- Logging
-quiet :: Applicative m => a -> m ()
-quiet _ = pure ()
-
-
-
 --------------------------------------------------------------------------------
 -- Errors