From 4fb3fd215d4614c3d3cb23fb1222fb8ed0a15bac Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Fri, 10 Mar 2023 13:02:36 -0500
Subject: [PATCH 1/2] Bump elf-edit, macaw submodules

---
 deps/elf-edit | 2 +-
 deps/macaw    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/deps/elf-edit b/deps/elf-edit
index d6d26540ed..dc5eabec3c 160000
--- a/deps/elf-edit
+++ b/deps/elf-edit
@@ -1 +1 @@
-Subproject commit d6d26540ed50348a597720b0015357bde34d504d
+Subproject commit dc5eabec3c00df530962ec41391356dc491cb0dc
diff --git a/deps/macaw b/deps/macaw
index d9525554ca..97c61e471a 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit d9525554ca3d6414e20a9f7571e38758ea5a3c3f
+Subproject commit 97c61e471aa60a48393bb6496260db416c4dca55

From e74a79a7ea09c0a9813ef10c3dcdb08c5805885e Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Fri, 10 Mar 2023 13:46:20 -0500
Subject: [PATCH 2/2] Adapt to changes in GaloisInc/macaw#327
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This mostly involves consolidating various `macaw` memory model–related options
into a `MemModelConfig` value. Apart from the API changes, there should be no
user-visible changes in behavior.
---
 deps/macaw                         |  2 +-
 src/SAWScript/Crucible/LLVM/X86.hs | 15 ++++++++++-----
 src/SAWScript/X86.hs               | 12 +++++++++++-
 3 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/deps/macaw b/deps/macaw
index 97c61e471a..88d024990b 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit 97c61e471aa60a48393bb6496260db416c4dca55
+Subproject commit 88d024990b97292f4d3d0fe0bf9c08e75c12c3ce
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index 76c15dd351..5c2e738a84 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -475,13 +475,18 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
         archEvalFns = Macaw.x86_64MacawEvalFn sfs Macaw.defaultMacawArchStmtExtensionOverride
         lookupSyscall = Macaw.unsupportedSyscalls "saw-script"
         noExtraValidityPred _ _ _ _ = return Nothing
+        mmConf = Macaw.MemModelConfig
+                   { Macaw.globalMemMap = mkGlobalMap . Map.singleton 0 $ preState ^. x86GlobalBase
+                   , Macaw.lookupFunctionHandle = funcLookup
+                   , Macaw.lookupSyscallHandle = lookupSyscall
+                   , Macaw.mkGlobalPointerValidityAssertion = noExtraValidityPred
+                   , Macaw.resolvePointer = pure
+                   , Macaw.concreteImmutableGlobalRead = \_ _ -> pure Nothing
+                   , Macaw.lazilyPopulateGlobalMem = \_ _ -> pure
+                   }
         defaultMacawExtensions_x86_64 =
           Macaw.macawExtensions
-          archEvalFns mvar
-          (mkGlobalMap . Map.singleton 0 $ preState ^. x86GlobalBase)
-          funcLookup
-          lookupSyscall
-          noExtraValidityPred
+          archEvalFns mvar mmConf
         sawMacawExtensions = defaultMacawExtensions_x86_64
           { C.extensionExec = \s0 st -> case s0 of
               Macaw.PtrLt w x y -> doPtrCmp W4.bvUlt st mvar w x y
diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
index 0718323463..e61a44b0dd 100644
--- a/src/SAWScript/X86.hs
+++ b/src/SAWScript/X86.hs
@@ -106,6 +106,7 @@ import Data.Macaw.Symbolic( ArchRegStruct
                           , GlobalMap
                           , MacawSimulatorState(..)
                           , macawExtensions
+                          , MemModelConfig(..)
                           , unsupportedSyscalls
                           , defaultMacawArchStmtExtensionOverride
                           )
@@ -491,13 +492,22 @@ doSim opts elf sfs name (globs,overs) st checkPost =
        let noExtraValidityPred _ _ _ _ = return Nothing
        let archEvalFns = x86_64MacawEvalFn sfs defaultMacawArchStmtExtensionOverride
        let lookupSyscall = unsupportedSyscalls "saw-script"
+       let mmConf = MemModelConfig
+                      { globalMemMap = globs
+                      , lookupFunctionHandle = callHandler overs sym
+                      , lookupSyscallHandle = lookupSyscall
+                      , mkGlobalPointerValidityAssertion = noExtraValidityPred
+                      , resolvePointer = pure
+                      , concreteImmutableGlobalRead = \_ _ -> pure Nothing
+                      , lazilyPopulateGlobalMem = \_ _ -> pure
+                      }
        let ctx :: SimContext (MacawSimulatorState Sym) Sym (MacawExt X86_64)
            ctx = SimContext { _ctxBackend = backend opts
                               , ctxSolverProof = \a -> a
                               , ctxIntrinsicTypes = llvmIntrinsicTypes
                               , simHandleAllocator = allocator opts
                               , printHandle = stdout
-                              , extensionImpl = macawExtensions archEvalFns mvar globs (callHandler overs sym) lookupSyscall noExtraValidityPred
+                              , extensionImpl = macawExtensions archEvalFns mvar mmConf
                               , _functionBindings = FnBindings $
                                 insertHandleMap (cfgHandle cfg) (UseCFG cfg (postdomInfo cfg)) emptyHandleMap
                               , _cruciblePersonality = MacawSimulatorState