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.
GaloisInc · Mar 10, 2023 · 89a0ae7 · 89a0ae7
1 parent 03cd2fb
commit 89a0ae7
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 7 deletions.
diff --git a/deps/macaw b/deps/macaw
diff --git 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
@@ -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
+6 −6		refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+6 −2		refinement/tests/RefinementTests.hs
+32 −0		symbolic/ChangeLog.md
+5 −0		symbolic/macaw-symbolic.cabal
+132 −52		symbolic/src/Data/Macaw/Symbolic.hs
+221 −0		symbolic/src/Data/Macaw/Symbolic/Concretize.hs
+33 −3		symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+86 −242		symbolic/src/Data/Macaw/Symbolic/Memory.hs
+320 −0		symbolic/src/Data/Macaw/Symbolic/Memory/Common.hs
+826 −0		symbolic/src/Data/Macaw/Symbolic/Memory/Lazy.hs
+26 −15		symbolic/src/Data/Macaw/Symbolic/Testing.hs