macaw-symbolic: newGlobalMemory doesn't need to know about the architecture

[RyanGlScott]

The type of the newGlobalMemory function is:

macaw/symbolic/src/Data/Macaw/Symbolic/Memory.hs

Lines 329 to 348 in df74837

	newGlobalMemory :: ( 16 <= MC.ArchAddrWidth arch
	, MC.MemWidth (MC.ArchAddrWidth arch)
	, KnownNat (MC.ArchAddrWidth arch)
	, CB.IsSymBackend sym bak
	, CL.HasLLVMAnn sym
	, MonadIO m
	, sym ~ WEB.ExprBuilder t st fs
	, ?memOpts :: CL.MemOptions
	)
	=> proxy arch
	-- ^ A proxy to fix the architecture
	-> bak
	-- ^ The symbolic backend used to construct terms
	-> CLD.EndianForm
	-- ^ The endianness of values in memory
	-> MemoryModelContents
	-- ^ A configuration option controlling how mutable memory should be represented (concrete or symbolic)
	-> MC.Memory (MC.ArchAddrWidth arch)
	-- ^ The macaw memory
	-> m (CL.MemImpl sym, MemPtrTable sym (MC.ArchAddrWidth arch))

Notably, this takes in a proxy arch argument, presumably for the purpose of fixing the type of the architecture being used. It turns out, however, that nothing in the implementation of newGlobalMemory actually makes use of this arch! Sure, the type signature mentions ArchAddrWith arch in various places, but those are the only uses of arch, and every occurrence of ArchAddrWidth arch could just as well be replaced with an arbitrary width w. As a proof of concept, I wrote a quick patch that removes the proxy arch arguments entirely:

diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
index 21af7d48..2e8f3402 100644
--- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
@@ -493,7 +493,7 @@ initializeSimulator ctx bak archVals halloc cfg entryBlock =
   MS.withArchEval archVals (CB.backendGetSym bak) $ \archEvalFns -> do
   memVar <- liftIO $ LLVM.mkMemVar "macaw-refinement:llvm_memory" halloc
   let end = MS.toCrucibleEndian (binaryEndianness ctx)
-  (memory0, memPtrTable) <- liftIO $ MS.newGlobalMemory (Proxy @arch) bak end MS.ConcreteMutable (binaryMemory ctx)
+  (memory0, memPtrTable) <- liftIO $ MS.newGlobalMemory bak end MS.ConcreteMutable (binaryMemory ctx)
   (memory1, initSPVal) <- initializeMemory (Proxy @arch) bak memory0
   -- FIXME: Capture output somewhere besides stderr
   let globalMappingFn = MS.mapRegionPointers memPtrTable
diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs
index dd0e58bd..25fe9fdc 100644
--- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs
@@ -230,30 +230,28 @@ defaultGlobalMemoryHooks =
 -- This version enables callers to control behaviors for which there is no good
 -- default behavior (and that must be otherwise treated as an error).
 newGlobalMemoryWith
- :: ( 16 <= MC.ArchAddrWidth arch
-    , MC.MemWidth (MC.ArchAddrWidth arch)
-    , KnownNat (MC.ArchAddrWidth arch)
+ :: ( 16 <= w
+    , MC.MemWidth w
+    , KnownNat w
     , CB.IsSymBackend sym bak
     , CL.HasLLVMAnn sym
     , MonadIO m
     , sym ~ WEB.ExprBuilder t st fs
     , ?memOpts :: CL.MemOptions
     )
- => GlobalMemoryHooks (MC.ArchAddrWidth arch)
+ => GlobalMemoryHooks w
  -- ^ Hooks customizing the memory setup
- -> proxy arch
- -- ^ A proxy to fix the architecture
  -> bak
  -- ^ The symbolic backend used to construct terms
  -> CLD.EndianForm
  -- ^ The endianness of values in memory
  -> MemoryModelContents
  -- ^ A configuration option controlling how mutable memory should be represented (concrete or symbolic)
- -> MC.Memory (MC.ArchAddrWidth arch)
+ -> MC.Memory w
  -- ^ The macaw memory
- -> m (CL.MemImpl sym, MemPtrTable sym (MC.ArchAddrWidth arch))
-newGlobalMemoryWith hooks proxy bak endian mmc mem =
-  newMergedGlobalMemoryWith hooks proxy bak endian mmc (Identity mem)
+ -> m (CL.MemImpl sym, MemPtrTable sym w)
+newGlobalMemoryWith hooks bak endian mmc mem =
+  newMergedGlobalMemoryWith hooks bak endian mmc (Identity mem)
 
 -- | A version of 'newGlobalMemoryWith' that takes a 'Foldable' collection of
 -- memories and merges them into a flat addresses space.  The address spaces of
@@ -263,10 +261,10 @@ newGlobalMemoryWith hooks proxy bak endian mmc mem =
 -- strategies by adding additional configuration options to
 -- 'GlobalMemoryHooks'.
 newMergedGlobalMemoryWith
- :: forall arch sym bak m t st fs proxy t'
-  . ( 16 <= MC.ArchAddrWidth arch
-    , MC.MemWidth (MC.ArchAddrWidth arch)
-    , KnownNat (MC.ArchAddrWidth arch)
+ :: forall w sym bak m t st fs t'
+  . ( 16 <= w
+    , MC.MemWidth w
+    , KnownNat w
     , CB.IsSymBackend sym bak
     , CL.HasLLVMAnn sym
     , MonadIO m
@@ -274,22 +272,20 @@ newMergedGlobalMemoryWith
     , ?memOpts :: CL.MemOptions
     , Foldable t'
     )
- => GlobalMemoryHooks (MC.ArchAddrWidth arch)
+ => GlobalMemoryHooks w
  -- ^ Hooks customizing the memory setup
- -> proxy arch
- -- ^ A proxy to fix the architecture
  -> bak
  -- ^ The symbolic backend used to construct terms
  -> CLD.EndianForm
  -- ^ The endianness of values in memory
  -> MemoryModelContents
  -- ^ A configuration option controlling how mutable memory should be represented (concrete or symbolic)
- -> t' (MC.Memory (MC.ArchAddrWidth arch))
+ -> t' (MC.Memory w)
  -- ^ The macaw memories
- -> m (CL.MemImpl sym, MemPtrTable sym (MC.ArchAddrWidth arch))
-newMergedGlobalMemoryWith hooks proxy bak endian mmc mems = do
+ -> m (CL.MemImpl sym, MemPtrTable sym w)
+newMergedGlobalMemoryWith hooks bak endian mmc mems = do
   let sym = CB.backendGetSym bak
-  let ?ptrWidth = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)
+  let ?ptrWidth = MC.memWidthNatRepr @w
 
   memImpl1 <- liftIO $ CL.emptyMem endian
 
@@ -300,7 +296,7 @@ newMergedGlobalMemoryWith hooks proxy bak endian mmc mems = do
                          "Global memory for macaw-symbolic"
                          memImpl1 sizeBV CLD.noAlignment
 
-  (symArray2, tbl) <- populateMemory proxy hooks bak mmc mems symArray1
+  (symArray2, tbl) <- populateMemory hooks bak mmc mems symArray1
   memImpl3 <- liftIO $ CL.doArrayStore bak memImpl2 ptr CLD.noAlignment symArray2 sizeBV
   let ptrTable = MemPtrTable { memPtrTable = tbl, memPtr = ptr, memRepr = ?ptrWidth }
 
@@ -326,53 +322,49 @@ newMergedGlobalMemoryWith hooks proxy bak endian mmc mems = do
 -- Note that this default setup is not suitable for dynamically linked binaries
 -- with relocations in the data section, as it will call 'error' if it
 -- encounters one. To handle dynamically linked binaries, see 'newGlobalMemoryWith'.
-newGlobalMemory :: ( 16 <= MC.ArchAddrWidth arch
-                   , MC.MemWidth (MC.ArchAddrWidth arch)
-                   , KnownNat (MC.ArchAddrWidth arch)
+newGlobalMemory :: ( 16 <= w
+                   , MC.MemWidth w
+                   , KnownNat w
                    , CB.IsSymBackend sym bak
                    , CL.HasLLVMAnn sym
                    , MonadIO m
                    , sym ~ WEB.ExprBuilder t st fs
                    , ?memOpts :: CL.MemOptions
                    )
-                => proxy arch
-                -- ^ A proxy to fix the architecture
-                -> bak
+                => bak
                 -- ^ The symbolic backend used to construct terms
                 -> CLD.EndianForm
                 -- ^ The endianness of values in memory
                 -> MemoryModelContents
                 -- ^ A configuration option controlling how mutable memory should be represented (concrete or symbolic)
-                -> MC.Memory (MC.ArchAddrWidth arch)
+                -> MC.Memory w
                 -- ^ The macaw memory
-                -> m (CL.MemImpl sym, MemPtrTable sym (MC.ArchAddrWidth arch))
+                -> m (CL.MemImpl sym, MemPtrTable sym w)
 newGlobalMemory = newGlobalMemoryWith defaultGlobalMemoryHooks
 
 -- | Copy memory from the 'MC.Memory' into the LLVM memory model allocation as
 -- directed by the 'MemoryModelContents' selection
 populateMemory :: ( CB.IsSymBackend sym bak
-                  , 16 <= MC.ArchAddrWidth arch
-                  , MC.MemWidth (MC.ArchAddrWidth arch)
-                  , KnownNat (MC.ArchAddrWidth arch)
+                  , 16 <= w
+                  , MC.MemWidth w
+                  , KnownNat w
                   , MonadIO m
                   , sym ~ WEB.ExprBuilder t st fs
                   , Foldable t'
                   )
-               => proxy arch
-               -- ^ A proxy to fix the architecture
-               -> GlobalMemoryHooks (MC.ArchAddrWidth arch)
+               => GlobalMemoryHooks w
                -- ^ Hooks controlling how memory should be initialized
                -> bak
                -- ^ The symbolic backend
                -> MemoryModelContents
                -- ^ A flag to indicate how to populate the memory model based on the memory image
-               -> t' (MC.Memory (MC.ArchAddrWidth arch))
+               -> t' (MC.Memory w)
                -- ^ The initial memory images for the binaries, which contain static data to populate the memory model
-               -> WI.SymArray sym (CT.SingleCtx (WI.BaseBVType (MC.ArchAddrWidth arch))) (WI.BaseBVType 8)
-               -> m ( WI.SymArray sym (CT.SingleCtx (WI.BaseBVType (MC.ArchAddrWidth arch))) (WI.BaseBVType 8)
-                    , IM.IntervalMap (MC.MemWord (MC.ArchAddrWidth arch)) CL.Mutability
+               -> WI.SymArray sym (CT.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8)
+               -> m ( WI.SymArray sym (CT.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8)
+                    , IM.IntervalMap (MC.MemWord w) CL.Mutability
                     )
-populateMemory proxy hooks bak mmc mems symArray0 =
+populateMemory hooks bak mmc mems symArray0 =
   let sym = CB.backendGetSym bak in
   pleatM (symArray0, IM.empty) mems $ \allocs0 mem ->
     pleatM allocs0 (MC.memSegments mem) $ \allocs1 seg -> do
@@ -383,7 +375,7 @@ populateMemory proxy hooks bak mmc mems symArray0 =
             liftIO $ replicate (fromIntegral sz) <$> WI.bvLit sym PN.knownNat (BV.zero PN.knownNat)
           MC.ByteRegion bytes ->
             liftIO $ mapM (WI.bvLit sym PN.knownNat . BV.word8) $ BS.unpack bytes
-        populateSegmentChunk proxy bak mmc mem symArray seg addr concreteBytes allocs2
+        populateSegmentChunk bak mmc mem symArray seg addr concreteBytes allocs2
 
 -- | If we want to treat the contents of this chunk of memory (the bytes at the
 -- 'MemAddr') as concrete, assert that the bytes from the symbolic array backing
@@ -397,16 +389,14 @@ populateSegmentChunk :: ( 16 <= w
                       , KnownNat w
                       , CB.IsSymBackend sym bak
                       , MonadIO m
-                      , MC.ArchAddrWidth arch ~ w
                       , sym ~ WEB.ExprBuilder t st fs
                       )
-                   => proxy arch
-                   -> bak
+                   => bak
                    -> MemoryModelContents
                    -- ^ The interpretation of mutable memory that we want to use
                    -> MC.Memory w
                    -- ^ The contents of memory
-                   -> WI.SymArray sym (CT.SingleCtx (WI.BaseBVType (MC.ArchAddrWidth arch))) (WI.BaseBVType 8)
+                   -> WI.SymArray sym (CT.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8)
                    -- ^ The symbolic array backing memory
                    -> MC.MemSegment w
                    -- ^ The segment containing this chunk
@@ -415,10 +405,10 @@ populateSegmentChunk :: ( 16 <= w
                    -> [WI.SymBV sym 8]
                    -- ^ The concrete values in this chunk (which may or may not be used)
                    -> IM.IntervalMap (MC.MemWord w) CL.Mutability
-                   -> m ( WI.SymArray sym (CT.SingleCtx (WI.BaseBVType (MC.ArchAddrWidth arch))) (WI.BaseBVType 8)
+                   -> m ( WI.SymArray sym (CT.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8)
                         , IM.IntervalMap (MC.MemWord w) CL.Mutability
                         )
-populateSegmentChunk _ bak mmc mem symArray seg addr bytes ptrtable = do
+populateSegmentChunk bak mmc mem symArray seg addr bytes ptrtable = do
   let sym = CB.backendGetSym bak
   let ?ptrWidth = MC.memWidth mem
   let abs_addr = toAbsoluteAddr addr
diff --git a/symbolic/src/Data/Macaw/Symbolic/Testing.hs b/symbolic/src/Data/Macaw/Symbolic/Testing.hs
index dc35d376..53d5e7b4 100644
--- a/symbolic/src/Data/Macaw/Symbolic/Testing.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Testing.hs
@@ -54,7 +54,6 @@ import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.List as PL
 import qualified Data.Parameterized.NatRepr as PN
 import           Data.Parameterized.Some ( Some(..) )
-import           Data.Proxy ( Proxy(..) )
 import qualified Data.Text as Text
 import qualified Data.Text.Encoding as Text
 import qualified Data.Text.Encoding.Error as Text
@@ -275,7 +274,7 @@ simulateAndVerify goalSolver logger bak execFeatures archInfo archVals mem (Resu
 
     let endianness = MSM.toCrucibleEndian (MAI.archEndianness archInfo)
     let ?recordLLVMAnnotation = \_ _ _ -> return ()
-    (initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @arch) bak endianness MSM.ConcreteMutable mem
+    (initMem, memPtrTbl) <- MSM.newGlobalMemory bak endianness MSM.ConcreteMutable mem
     let globalMap = MSM.mapRegionPointers memPtrTbl
     (memVar, stackPointer, execResult) <- simulateFunction discState bak execFeatures archVals halloc initMem globalMap g
     case execResult of

This isn't a huge issue in practice, since newGlobalMemory and friends are usually called in places that bind an arch anyway. As a result, I'm not inclined to address this issue right now, especially considering that fixing it would require a breaking API change.