symbolic: Refine discussion about the placement of the stack pointer

dbb4c83 introduced this stack-pointer-in-the-middle approach, but
the commit message has no further commentary on why it was seen as
necessary. I've written up why *I* believe it to be necessary, and
removed what I see as a misleading comment.

Also, return a pointer to the end of the stack, because that's what
most clients will want.

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

@@ -1,5 +1,7 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE TypeOperators #-}
 
 module Data.Macaw.Symbolic.Stack
@@ -9,15 +11,15 @@ module Data.Macaw.Symbolic.Stack
   , createArrayStack
   ) where
 
+import Data.Macaw.CFG qualified as MC
+import Data.Macaw.Symbolic qualified as MS
 import Data.Parameterized.Context as Ctx
-
-import qualified What4.Interface as WI
-import qualified What4.Symbol as WSym
-
-import qualified Lang.Crucible.Backend as C
-
-import qualified Lang.Crucible.LLVM.DataLayout as CLD
-import qualified Lang.Crucible.LLVM.MemModel as CLM
+import Lang.Crucible.Backend qualified as C
+import Lang.Crucible.Simulator qualified as C
+import Lang.Crucible.LLVM.DataLayout qualified as CLD
+import Lang.Crucible.LLVM.MemModel qualified as CLM
+import What4.Interface qualified as WI
+import What4.Symbol qualified as WSym
 
 -- | Helper, not exported
 stackAlign :: CLD.Alignment
@@ -61,7 +63,9 @@ mallocStack bak mem sz =
 data ArrayStack sym w
   = ArrayStack
     { -- | Pointer to the base of the stack array
-      arrayStackPtr :: CLM.LLVMPtr sym w
+      arrayStackBasePtr :: CLM.LLVMPtr sym w
+      -- | Pointer to the top (end) of the stack array
+    , arrayStackTopPtr :: CLM.LLVMPtr sym w
       -- | SMT array backing the stack allocation
     , arrayStackVal :: WI.SymArray sym (Ctx.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8)
     }
@@ -84,6 +88,18 @@ createArrayStack ::
 createArrayStack bak mem sz = do
   let sym = C.backendGetSym bak
   arr <- stackArray sym
-  (ptr, mem1) <- mallocStack bak mem sz
-  mem2 <- CLM.doArrayStore bak mem1 ptr stackAlign arr sz
-  pure (ArrayStack ptr arr, mem2)
+  (base, mem1) <- mallocStack bak mem sz
+  mem2 <- CLM.doArrayStore bak mem1 base stackAlign arr sz
+  top <- CLM.ptrAdd sym ?ptrWidth base sz
+  pure (ArrayStack base top arr, mem2)
+
+-- | Set the stack pointer register.
+_setStackPointerReg ::
+  1 WI.<= MC.ArchAddrWidth arch =>
+  MS.SymArchConstraints arch =>
+  C.IsSymInterface sym =>
+  MS.ArchVals arch ->
+  C.RegEntry sym (MS.ArchRegStruct arch) ->
+  CLM.LLVMPtr sym (MC.ArchAddrWidth arch) ->
+  C.RegEntry sym (MS.ArchRegStruct arch)
+_setStackPointerReg archVals regs = MS.updateReg archVals regs MC.sp_reg

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

@@ -528,12 +528,23 @@ simulateFunction binfo bak execFeatures archInfo archVals halloc mmPreset g = do
   let kib = 1024
   let mib = 1024 * kib
   stackSize <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr (2 * mib))
-  (MSS.ArrayStack stackBasePtr _stackArrayStorage, mem1) <-
+  (MSS.ArrayStack stackBasePtr _stackTopPtr _stackArrayStorage, mem1) <-
     MSS.createArrayStack bak initMem stackSize
 
-  -- Make initial registers, including setting up a stack pointer (which points
-  -- into the middle of the stack allocation, to allow accesses into the caller
-  -- frame if needed (though it generally should not be)
+  -- Make initial registers, including setting up a stack pointer.
+  --
+  -- The stack pointer points to the middle of the stack allocation. This is a
+  -- hack. We do this because each architecture has some expected stack layout
+  -- (e.g., x86_64 expects a return address just above the stack pointer;
+  -- PPC expects a "back chain"; and AArch32, PPC, and x86_64 all expect
+  -- stack-spilled arguments above everything else). Setting the stack pointer
+  -- to the middle of the allocation allows reads of fully symbolic data from
+  -- above the stack pointer, and this seems to be good enough to make our tests
+  -- pass.
+  --
+  -- The functions in the test-suite do not (and should not) rely on accessing
+  -- data in their caller's stack frames, even though that wouldn't cause test
+  -- failures with this setup.
   initialRegs <- MS.macawAssignToCrucM (mkInitialRegVal symArchFns sym) (MS.crucGenRegAssignment symArchFns)
   stackInitialOffset <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr mib)
   sp <- CLM.ptrAdd sym WI.knownRepr stackBasePtr stackInitialOffset