symbolic: Factor stack setup code into its own module

symbolic/macaw-symbolic.cabal

@@ -39,6 +39,7 @@ library
     Data.Macaw.Symbolic.Memory
     Data.Macaw.Symbolic.Memory.Lazy
     Data.Macaw.Symbolic.MemOps
+    Data.Macaw.Symbolic.Stack
     Data.Macaw.Symbolic.Testing
   other-modules:
     Data.Macaw.Symbolic.Bitcast

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

@@ -0,0 +1,113 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Macaw.Symbolic.Stack
+  ( stackArray
+  , mallocStack
+  , ExtraStackSlots(..)
+  , ArrayStack(..)
+  , createArrayStack
+  ) where
+
+import Data.BitVector.Sized qualified as BVS
+import Data.Parameterized.Context as Ctx
+import Lang.Crucible.Backend 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
+stackAlign = CLD.noAlignment
+
+-- | Create an SMT array representing the program stack.
+stackArray ::
+  (1 WI.<= w) =>
+  CLM.HasPtrWidth w =>
+  WI.IsSymExprBuilder sym =>
+  sym ->
+  IO (WI.SymArray sym (Ctx.SingleCtx (WI.BaseBVType w)) (WI.BaseBVType 8))
+stackArray sym =
+  WI.freshConstant
+    sym
+    (WSym.safeSymbol "stack_array")
+    (WI.BaseArrayRepr (Ctx.singleton (WI.BaseBVRepr ?ptrWidth)) WI.knownRepr)
+
+-- | Create an allocation representing the program stack, using 'CLM.doMalloc'.
+--
+-- This allocation is:
+--
+-- * mutable, because the program must write to the stack
+-- * of kind 'CLM.StackAlloc'
+-- * without alignment ('CLD.noAlignment')
+mallocStack ::
+  C.IsSymBackend sym bak =>
+  CLM.HasPtrWidth w =>
+  (?memOpts :: CLM.MemOptions) =>
+  CLM.HasLLVMAnn sym =>
+  bak ->
+  CLM.MemImpl sym ->
+  -- | Size of stack allocation
+  WI.SymExpr sym (WI.BaseBVType w) ->
+  IO (CLM.LLVMPtr sym w, CLM.MemImpl sym)
+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
+    { -- | Pointer to the base of the stack array
+      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)
+    }
+
+-- | Create an SMT-array-backed stack allocation
+--
+-- * 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
+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
+  let sym = C.backendGetSym bak
+  arr <- stackArray sym
+  (base, mem1) <- mallocStack bak mem sz
+  mem2 <- CLM.doArrayStore bak mem1 base stackAlign arr sz
+
+  end <- CLM.doPtrAddOffset bak mem2 base sz
+  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
+
+  pure (ArrayStack base top arr, mem2)

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

@@ -62,6 +62,7 @@ import qualified Data.Macaw.Memory.LoadCommon as MML
 import qualified Data.Macaw.Symbolic as MS
 import qualified Data.Macaw.Symbolic.Memory as MSM
 import qualified Data.Macaw.Symbolic.Memory.Lazy as MSMLazy
+import qualified Data.Macaw.Symbolic.Stack as MSS
 import qualified Data.Macaw.Types as MT
 import qualified Data.Map as Map
 import           Data.Maybe ( fromMaybe, listToMaybe )
@@ -83,7 +84,6 @@ import qualified Lang.Crucible.Backend.Prove as Prove
 import qualified Lang.Crucible.CFG.Core as CCC
 import qualified Lang.Crucible.CFG.Extension as CCE
 import qualified Lang.Crucible.FunctionHandle as CFH
-import qualified Lang.Crucible.LLVM.DataLayout as CLD
 import qualified Lang.Crucible.LLVM.Intrinsics as CLI
 import qualified Lang.Crucible.LLVM.MemModel as CLM
 import qualified Lang.Crucible.Simulator as CS
@@ -103,7 +103,6 @@ import qualified What4.ProgramLoc as WPL
 import qualified What4.Protocol.Online as WPO
 import qualified What4.SatResult as WSR
 import qualified What4.Solver as WS
-import qualified What4.Symbol as WSym
 
 data TestingException = ELFResolutionError String
   deriving (Show)
@@ -498,12 +497,6 @@ simulateFunction binfo bak execFeatures archInfo archVals halloc mmPreset g = do
   -- This includes both global static memory (taken from the data segment
   -- initial contents) and a totally symbolic stack
 
-  -- Allocate a stack and insert it into memory
-  --
-  -- The stack allocation uses the SMT array backed memory model (rather than
-  -- the Haskell-level memory model)
-  stackArrayStorage <- WI.freshConstant sym (WSym.safeSymbol "stack_array") WI.knownRepr
-  stackSize <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr (2 * 1024 * 1024))
   let ?ptrWidth = WI.knownRepr
   (initMem, mmConf) <-
     case mmPreset of
@@ -527,21 +520,40 @@ simulateFunction binfo bak execFeatures archInfo archVals halloc mmPreset g = do
                        , MS.mkGlobalPointerValidityAssertion = validityCheck
                        }
         pure (initMem, mmConf)
-  (stackBasePtr, mem1) <- CLM.doMalloc bak CLM.StackAlloc CLM.Mutable "stack_alloc" initMem stackSize CLD.noAlignment
-  mem2 <- CLM.doArrayStore bak mem1 stackBasePtr CLD.noAlignment stackArrayStorage 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)
+  -- Allocate a stack and insert it into memory
+  --
+  -- The stack allocation uses the SMT array backed memory model (rather than
+  -- the Haskell-level memory model)
+  let kib = 1024
+  let mib = 1024 * kib
+  stackSize <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr (2 * mib))
+  (MSS.ArrayStack stackBasePtr _stackTopPtr _stackArrayStorage, mem1) <-
+    MSS.createArrayStack bak initMem (MSS.ExtraStackSlots 0) stackSize
+
+  -- 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 (1024 * 1024))
+  stackInitialOffset <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr mib)
   sp <- CLM.ptrAdd sym WI.knownRepr stackBasePtr stackInitialOffset
   let initialRegsEntry = CS.RegEntry regsRepr initialRegs
   let regsWithStack = MS.updateReg archVals initialRegsEntry MC.sp_reg sp
 
   memVar <- CLM.mkMemVar "macaw-symbolic:test-harness:llvm_memory" halloc
   let lazySimSt = MS.emptyMacawLazySimulatorState
-  let initGlobals = CSG.insertGlobal memVar mem2 CS.emptyGlobals
+  let initGlobals = CSG.insertGlobal memVar mem1 CS.emptyGlobals
   let arguments = CS.RegMap (Ctx.singleton regsWithStack)
   let simAction = CS.runOverrideSim regsRepr (CS.regValue <$> CS.callCFG g arguments)