Adapt to changes in GaloisInc/macaw#327

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.

Author: RyanGlScott

deps/macaw

@@ -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

src/SAWScript/Crucible/LLVM/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