symbolic: Remove support for stack-spilled arguments

Many ABIs impose some kind of alignment constraints on the stack
pointer. For example, both the AArch32 and x86_64 SysV ABIs specify
that the end of the spilled argument list is aligned to 2*w where w
is the number of bytes in a word. Since macaw-symbolic has no notion
of the ABI in use, its ABI-agnostic code could only ever satisfy such
alignment constraints accidentally. Clients wishing to spill arguments
to the stack should do so with ABI-specific functionality.

macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs

@@ -163,8 +163,6 @@ pushStackFrame bak mem regs spilledArgs = do
   pure (regs', mem')
 
 -- | Like 'MSS.createArrayStack', but puts the stack pointer in @sp@ directly.
---
--- Does not allow allocating stack slots, use 'pushStackFrame' for that.
 allocStack ::
   C.IsSymBackend sym bak =>
   (?memOpts :: MM.MemOptions) =>
@@ -181,7 +179,6 @@ allocStack ::
     )
 allocStack bak mem regs sz = do
   let ?ptrWidth = ptrRepr
-  let slots = MSS.ExtraStackSlots 0
-  (MSS.ArrayStack _base top _arr, mem') <- MSS.createArrayStack bak mem slots sz
+  (MSS.ArrayStack _base top _arr, mem') <- MSS.createArrayStack bak mem sz
   let regs' = regs Lens.& stackPointerReg Lens..~ StackPointer top
   pure (regs', mem')

symbolic/src/Data/Macaw/Symbolic/Stack.hs

@@ -9,7 +9,6 @@
 module Data.Macaw.Symbolic.Stack
   ( stackArray
   , mallocStack
-  , ExtraStackSlots(..)
   , ArrayStack(..)
   , createArrayStack
   , allocStackSpace
@@ -66,14 +65,6 @@ mallocStack ::
 mallocStack bak mem sz =
   CLM.doMalloc bak CLM.StackAlloc CLM.Mutable "stack_alloc" mem sz stackAlign
 
--- | Allocate this many pointer-sized stack slots, which are reserved for
--- stack-spilled arguments.
-newtype ExtraStackSlots = ExtraStackSlots { getExtraStackSlots :: Int }
-  -- Derive the Read instance using the `newtype` strategy, not the
-  -- `stock` strategy. This allows parsing ExtraStackSlots values in
-  -- optparse-applicative-based command-line parsers using the `Read` instance.
-  deriving newtype (Enum, Eq, Integral, Num, Ord, Read, Real, Show)
-
 -- | An allocation representing the program stack, backed by an SMT array
 data ArrayStack sym w
   = ArrayStack
@@ -90,21 +81,18 @@ data ArrayStack sym w
 -- * Creates a stack array with 'stackArray'
 -- * Allocates space for the stack with 'mallocStack'
 -- * Writes the stack array to the allocation
--- * Creates a pointer to the top of the stack, which is the end minus the extra
---   stack slots
+-- * Creates a pointer to the end of the stack
 createArrayStack ::
   C.IsSymBackend sym bak =>
   CLM.HasPtrWidth w =>
   (?memOpts :: CLM.MemOptions) =>
   CLM.HasLLVMAnn sym =>
   bak ->
   CLM.MemImpl sym ->
-  -- | The caller must ensure the size of these is less than the allocation size
-  ExtraStackSlots ->
   -- | Size of stack allocation
   WI.SymExpr sym (WI.BaseBVType w) ->
   IO (ArrayStack sym w, CLM.MemImpl sym)
-createArrayStack bak mem slots sz = do
+createArrayStack bak mem sz = do
   let sym = C.backendGetSym bak
   arr <- stackArray sym
   (base, mem1) <- mallocStack bak mem sz
@@ -113,14 +101,7 @@ createArrayStack bak mem slots sz = do
   -- Put the stack pointer at the end of the stack allocation, i.e., an offset
   -- that is one less than the allocation's size.
   off <- WI.bvSub sym sz =<< WI.bvOne sym ?ptrWidth
-  end <- CLM.doPtrAddOffset bak mem2 base off
-
-  let ptrBytes = WI.intValue ?ptrWidth `div` 8
-  let slots' = fromIntegral (getExtraStackSlots slots)
-  let slotsBytes = slots' * ptrBytes
-  slotsBytesBv <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth slotsBytes)
-  top <- CLM.ptrSub sym ?ptrWidth end slotsBytesBv
-
+  top <- CLM.doPtrAddOffset bak mem2 base off
   pure (ArrayStack base top arr, mem2)
 
 -- | Allocate stack space by subtracting from the stack pointer

symbolic/src/Data/Macaw/Symbolic/Testing.hs

@@ -351,7 +351,7 @@ defaultRegs bak archVals mem = do
   let mib = 1024 * kib
   stackSize <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth (2 * mib))
   (MSS.ArrayStack stackBasePtr _stackTopPtr _stackArrayStorage, mem') <-
-    MSS.createArrayStack bak mem (MSS.ExtraStackSlots 0) stackSize
+    MSS.createArrayStack bak mem stackSize
   stackInitialOffset <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth mib)
   sp <- CLM.ptrAdd sym ?ptrWidth stackBasePtr stackInitialOffset
 

x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs

@@ -231,9 +231,6 @@ pushStackFrame bak mem regs spilledArgs retAddr = do
   pure (regs', mem')
 
 -- | Like 'MSS.createArrayStack', but puts the stack pointer in @rsp@ directly.
---
--- Does not allow allocating stack slots, use 'allocStackFrame' or
--- 'pushStackFrame' for that.
 allocStack ::
   C.IsSymBackend sym bak =>
   (?memOpts :: MM.MemOptions) =>
@@ -250,7 +247,6 @@ allocStack ::
     )
 allocStack bak mem regs sz = do
   let ?ptrWidth = ptrRepr
-  let slots = MSS.ExtraStackSlots 0
-  (MSS.ArrayStack _base top _arr, mem') <- MSS.createArrayStack bak mem slots sz
+  (MSS.ArrayStack _base top _arr, mem') <- MSS.createArrayStack bak mem sz
   let regs' = regs Lens.& stackPointerReg Lens..~ StackPointer top
   pure (regs', mem')