stubs-common: Use the lazy macaw-symbolic memory model

Much of the memory model code that `stubs-common` sits on top of has since been upstreamed to `macaw-symbolic` as part of its lazy memory model. This patch rips out the copy that `stubs-common` uses and replaces it with equivalent functionality found in `Data.Macaw.Symbolic.Memory.Lazy`. Fixes #12.
GaloisInc · Jan 14, 2025 · 54904ac · 54904ac
1 parent 5b1d315
commit 54904ac
Show file tree

Hide file tree

Showing 7 changed files with 65 additions and 1,013 deletions.
diff --git a/stubs-common/src/Stubs/Extensions.hs b/stubs-common/src/Stubs/Extensions.hs
diff --git a/stubs-common/src/Stubs/Extensions/Memory.hs b/stubs-common/src/Stubs/Extensions/Memory.hs
diff --git a/stubs-common/src/Stubs/Memory.hs b/stubs-common/src/Stubs/Memory.hs
@@ -36,6 +36,7 @@ import qualified Text.Megaparsec as TM
 import qualified Text.Megaparsec.Char as TMC
 
 import qualified Data.Macaw.Symbolic as DMS
+import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM
 import qualified Lang.Crucible.Simulator as LCS
 import qualified Lang.Crucible.Simulator.GlobalState as LCSG
 
@@ -129,7 +130,7 @@ data (IsStubsMemoryModel mem arch) => InitialMemory sym mem arch =
                -- ^ Initial global variables
                 , imStackBasePtr :: LCS.RegValue sym (PtrType mem arch)
                -- ^ Stack memory base pointer
-                , imMemTable :: MemTable sym mem arch
+                , imMemTable :: DMSM.MemPtrTable sym (DMC.ArchAddrWidth arch)
                 , imGlobalMap :: MemMap sym arch
                 }
 

diff --git a/stubs-common/src/Stubs/Memory/AArch32/Linux.hs b/stubs-common/src/Stubs/Memory/AArch32/Linux.hs
@@ -20,6 +20,7 @@ module Stubs.Memory.AArch32.Linux (
   ) where
 
 import qualified Data.BitVector.Sized as BVS
+import           Data.Proxy (Proxy(..))
 import qualified Data.Text as DT
 
 import qualified Data.Macaw.ARM as DMA
@@ -46,7 +47,7 @@ import qualified Lang.Crucible.LLVM.MemModel.Partial as LCLMP
 import qualified Lang.Crucible.LLVM.Errors as LCLE
 import qualified Lang.Crucible.LLVM.MemModel.CallStack
 import qualified Lang.Crucible.Types as LCT
-import qualified Data.Macaw.Symbolic.Memory as DMSM
+import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM
 import qualified Data.Macaw.Architecture.Info as DMA
 import qualified Data.Parameterized.NatRepr as PN
 import qualified Stubs.Memory as SM
@@ -55,7 +56,6 @@ import Control.Monad.IO.Class (MonadIO(..))
 import Data.Macaw.AArch32.Symbolic ()
 import qualified Stubs.Extensions as SE
 import qualified Data.Macaw.Symbolic.MemOps as DMSMO
-import qualified Stubs.Extensions.Memory as AEM
 import qualified Data.Macaw.BinaryLoader as DMB
 import qualified Stubs.Loader.BinaryConfig as SLB
 import qualified Stubs.Memory.Common as SMC
@@ -64,7 +64,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where
   type instance PtrType DMS.LLVMMemory SAA.AArch32 =  LCLM.LLVMPointerType (DMC.ArchAddrWidth SAA.AArch32)
   type instance MemType DMS.LLVMMemory SAA.AArch32 = LCLM.Mem
   type instance BVToPtrTy w DMS.LLVMMemory SAA.AArch32 = LCLM.LLVMPointerType w
-  type instance MemTable sym DMS.LLVMMemory SAA.AArch32 = AEM.MemPtrTable sym SAA.AArch32
+  type instance MemTable sym DMS.LLVMMemory SAA.AArch32 = DMSM.MemPtrTable sym 32
   type instance MemMap sym SAA.AArch32 = DMSMO.GlobalMap sym LCLM.Mem (DMC.ArchAddrWidth SAA.AArch32)
 
   type instance VerifierState sym DMS.LLVMMemory SAA.AArch32 = (SE.AmbientSimulatorState sym SAA.AArch32)
@@ -115,7 +115,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where
     (recordFn, _) <- liftIO SM.buildRecordLLVMAnnotation
     let ?recordLLVMAnnotation = recordFn
     let ?memOpts = LCLM.defaultMemOptions
-    (mem, memPtrTbl) <- AEM.newMemPtrTable (SMC.globalMemoryHooks mems mempty mempty) bak endian mems
+    (mem, memPtrTbl) <- DMSM.newMergedGlobalMemoryWith (SMC.globalMemoryHooks mems mempty mempty) (Proxy @SAA.AArch32) bak endian DMSM.ConcreteMutable mems
     stackSizeBV <- liftIO $ WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr stackSize)
 
     (stackBasePtr, mem1) <- liftIO $ LCLM.doMalloc bak LCLM.StackAlloc LCLM.Mutable "stack_alloc" mem stackSizeBV LCLD.noAlignment
@@ -127,7 +127,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where
     (mem3, globals0) <- liftIO $ aarch32LinuxInitGlobals tlsvar (SC.Sym sym bak) mem2
     memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc
     let globals1 = LCSG.insertGlobal memVar mem3 globals0
-    let globalMap = AEM.mapRegionPointers memPtrTbl
+    let globalMap = DMSM.mapRegionPointers memPtrTbl
 
     return SM.InitialMemory{
       SM.imMemVar=memVar,

diff --git a/stubs-common/src/Stubs/Memory/PPC/Linux.hs b/stubs-common/src/Stubs/Memory/PPC/Linux.hs
@@ -19,6 +19,7 @@
 module Stubs.Memory.PPC.Linux (ppcLinuxStmtExtensionOverride) where
 
 import qualified Data.BitVector.Sized as BVS
+import           Data.Proxy (Proxy(..))
 import qualified Data.Text as DT
 
 import qualified Data.Macaw.Symbolic as DMS
@@ -32,7 +33,7 @@ import qualified Stubs.Memory as AM
 import qualified Stubs.Common as SC
 import qualified Lang.Crucible.FunctionHandle as LCF
 import qualified Lang.Crucible.Types as LCT
-import qualified Data.Macaw.Symbolic.Memory as DMSM
+import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM
 import qualified Data.Macaw.Architecture.Info as DMA
 import qualified Data.Parameterized.NatRepr as PN
 import qualified Stubs.Memory as SM
@@ -42,7 +43,6 @@ import qualified Data.Macaw.PPC as DMP
 import Data.Macaw.PPC.Symbolic ()
 import qualified Stubs.Extensions as SE
 import qualified Data.Macaw.Symbolic.MemOps as DMSMO
-import qualified Stubs.Extensions.Memory as AEM
 import qualified Data.Macaw.BinaryLoader as DMB
 import qualified Stubs.Loader.BinaryConfig as SLB
 import qualified Stubs.Memory.Common as SMC
@@ -52,7 +52,7 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) =>
   type instance PtrType DMS.LLVMMemory (DMP.AnyPPC v) = LCLM.LLVMPointerType (SAP.AddrWidth v)
   type instance MemType DMS.LLVMMemory (DMP.AnyPPC v) = LCLM.Mem
   type instance BVToPtrTy w DMS.LLVMMemory (DMP.AnyPPC v) = LCLM.LLVMPointerType w
-  type instance MemTable sym DMS.LLVMMemory (DMP.AnyPPC v) = AEM.MemPtrTable sym (DMP.AnyPPC v)
+  type instance MemTable sym DMS.LLVMMemory (DMP.AnyPPC v) = DMSM.MemPtrTable sym (SAP.AddrWidth v)
   type instance MemMap sym (DMP.AnyPPC v) = DMSMO.GlobalMap sym LCLM.Mem (SAP.AddrWidth v)
 
   type instance VerifierState sym DMS.LLVMMemory (DMP.AnyPPC v) = SE.AmbientSimulatorState sym (DMP.AnyPPC v)
@@ -103,7 +103,7 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) =>
     (recordFn, _) <- liftIO SM.buildRecordLLVMAnnotation
     let ?recordLLVMAnnotation = recordFn
     let ?memOpts = LCLM.defaultMemOptions
-    (mem, memPtrTbl) <- AEM.newMemPtrTable (SMC.globalMemoryHooks mems mempty mempty) bak endian mems
+    (mem, memPtrTbl) <- DMSM.newMergedGlobalMemoryWith (SMC.globalMemoryHooks mems mempty mempty) (Proxy @(DMP.AnyPPC v)) bak endian DMSM.ConcreteMutable mems
     stackSizeBV <- liftIO $ WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr stackSize)
 
     (stackBasePtr, mem1) <- liftIO $ LCLM.doMalloc bak LCLM.StackAlloc LCLM.Mutable "stack_alloc" mem stackSizeBV LCLD.noAlignment
@@ -113,7 +113,7 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) =>
 
     memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc
     let globals = LCSG.insertGlobal memVar mem2 LCSG.emptyGlobals
-    let globalMap = AEM.mapRegionPointers memPtrTbl
+    let globalMap = DMSM.mapRegionPointers memPtrTbl
 
     return SM.InitialMemory{
       SM.imMemVar=memVar,

diff --git a/stubs-common/src/Stubs/Memory/X86_64/Linux.hs b/stubs-common/src/Stubs/Memory/X86_64/Linux.hs
@@ -24,6 +24,7 @@ module Stubs.Memory.X86_64.Linux (
 
 import           Control.Lens ((^.))
 import qualified Data.BitVector.Sized as BVS
+import           Data.Proxy (Proxy(..))
 
 import qualified Data.Macaw.CFG as DMC
 import qualified Data.Macaw.Symbolic as DMS
@@ -47,7 +48,7 @@ import qualified Stubs.Panic as AP
 import qualified Stubs.Memory as SM
 import qualified Lang.Crucible.Types as LCT
 import qualified Stubs.Common as SC
-import qualified Data.Macaw.Symbolic.Memory as DMSM
+import qualified Data.Macaw.Symbolic.Memory.Lazy as DMSM
 import qualified Data.Macaw.X86 as DMA
 import qualified Data.Macaw.X86.Symbolic ()
 import Control.Monad.IO.Class (liftIO, MonadIO)
@@ -59,7 +60,6 @@ import qualified Lang.Crucible.LLVM.MemModel.Partial as LCLMP
 import qualified Stubs.Memory.Common as SMC
 import qualified Stubs.Logging as SL
 import qualified Stubs.Extensions as SE
-import qualified Stubs.Extensions.Memory as AEM
 import qualified Data.Macaw.Symbolic as DMSMO
 import qualified Stubs.Loader.BinaryConfig as SLB
 import qualified Data.Macaw.BinaryLoader as DMB
@@ -69,7 +69,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where
   type instance PtrType DMS.LLVMMemory DMX.X86_64 =  LCLM.LLVMPointerType (DMC.ArchAddrWidth DMX.X86_64)
   type instance MemType DMS.LLVMMemory DMX.X86_64 = LCLM.Mem
   type instance BVToPtrTy w DMS.LLVMMemory DMX.X86_64 = LCLM.LLVMPointerType w
-  type instance MemTable sym DMS.LLVMMemory DMX.X86_64 = AEM.MemPtrTable sym DMX.X86_64
+  type instance MemTable sym DMS.LLVMMemory DMX.X86_64 = DMSM.MemPtrTable sym 64
   type instance MemMap sym DMX.X86_64 = DMSMO.GlobalMap sym LCLM.Mem (DMC.ArchAddrWidth DMX.X86_64)
   type instance VerifierState sym DMS.LLVMMemory DMX.X86_64 = (SE.AmbientSimulatorState sym DMX.X86_64)
 
@@ -92,35 +92,13 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where
     (re, _) <- liftIO $ SM.buildRecordLLVMAnnotation @sym
     let ?recordLLVMAnnotation = re
     let mpt = SM.imMemTable initialMem
-    -- This MemModelConfig is very nearly the same as the memModelConfig that
-    -- Data.Macaw.Symbolic.Memory provides, but we have to duplicate some logic
-    -- here since `stubs` uses a different MemPtrTable data type than
-    -- `macaw-symbolic`. Note that some of these fields (e.g., the
-    -- `mkGlobalPointerValidityAssertion` field) will effectively go unused, as
-    -- `stubs-common`'s memory model overrides certain operations that would
-    -- otherwise use these fields.
-    --
-    -- In the future, it would be preferable to build on top of the
-    -- `macaw-symbolic` lazy memory model, whose functionality largely overlaps
-    -- with the `stubs-common` memory model. See
-    -- https://github.com/GaloisInc/stubs/issues/12.
     let mmConf =
-          DMS.MemModelConfig
-            { DMS.globalMemMap =
-                AEM.mapRegionPointers mpt
-            , DMS.lookupFunctionHandle =
+          (DMSM.memModelConfig bak mpt)
+            { DMS.lookupFunctionHandle =
                 SMC.symExLookupFunction SL.emptyLogger bak initialMem archVals binconf functionABI halloc archInfo Nothing
 
             , DMS.lookupSyscallHandle =
                 SMC.symExLookupSyscall bak syscallABI halloc
-            , DMS.mkGlobalPointerValidityAssertion =
-                AEM.mkGlobalPointerValidityPred mpt
-            , DMS.resolvePointer =
-                pure
-            , DMS.concreteImmutableGlobalRead =
-                \_ _ -> pure Nothing
-            , DMS.lazilyPopulateGlobalMem =
-                \_ _ -> pure
             }
     return $ SE.ambientExtensions @sym @DMX.X86_64 bak f initialMem mmConf mempty
 
@@ -178,7 +156,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where
 
     let supportedRelocs = SLB.bcSupportedRelocations binConf
     let globs = SLB.bcDynamicGlobalVarAddrs binConf
-    (mem, memPtrTbl) <- AEM.newMemPtrTable (SMC.globalMemoryHooks mems globs supportedRelocs) bak endian mems
+    (mem, memPtrTbl) <- DMSM.newMergedGlobalMemoryWith (SMC.globalMemoryHooks mems globs supportedRelocs) (Proxy @DMX.X86_64) bak endian DMSM.ConcreteMutable mems
     (stackBasePtr, mem1) <- liftIO $ LCLM.doMalloc bak LCLM.StackAlloc LCLM.Mutable "stack_alloc" mem stackSizeBV LCLD.noAlignment
     fsvar <- liftIO $ freshFSBaseGlobalVar halloc
     gsvar <- liftIO $ freshGSBaseGlobalVar halloc
@@ -188,7 +166,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where
     memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc
     let globals1 = LCSG.insertGlobal memVar mem3 globals0
 
-    let globalMap = AEM.mapRegionPointers memPtrTbl
+    let globalMap = DMSM.mapRegionPointers memPtrTbl
     return SM.InitialMemory{
       SM.imMemVar=memVar,
       SM.imGlobals=globals1,

diff --git a/stubs-common/stubs-common.cabal b/stubs-common/stubs-common.cabal
@@ -53,7 +53,6 @@ library
                       Stubs.EnvVar,
                       Stubs.Exception,
                       Stubs.Extensions,
-                      Stubs.Extensions.Memory,
                       Stubs.FunctionOverride,
                       Stubs.FunctionOverride.ArgumentMapping,
                       Stubs.FunctionOverride.Common,