aarch32-symbolic: Setting up an ABI-compatible stack

macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal

@@ -19,11 +19,13 @@ extra-source-files:  CHANGELOG.md
 
 library
   exposed-modules:     Data.Macaw.AArch32.Symbolic
+                       Data.Macaw.AArch32.Symbolic.ABI
   other-modules:       Data.Macaw.AArch32.Symbolic.AtomWrapper
                        Data.Macaw.AArch32.Symbolic.Functions
                        Data.Macaw.AArch32.Symbolic.Panic
   -- other-extensions:
   build-depends:       base >=4.10 && <5,
+                       bv-sized,
                        containers,
                        lens,
                        panic,
@@ -51,6 +53,7 @@ test-suite macaw-aarch32-symbolic-tests
   hs-source-dirs: tests
   build-depends:
     base >= 4,
+    bv-sized,
     bytestring,
     containers,
     crucible,

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

@@ -0,0 +1,187 @@
+{-|
+Copyright        : (c) Galois, Inc 2024
+Maintainer       : Langston Barrett <langston@galois.com>
+
+On AArch32, the stack grows \"downwards\" from high addresses to low. The end
+of the stack is initialized with the ELF auxiliary vector (not modelled here),
+and functions expect the following data to be available above their stack frame
+(i.e., just above the address in @sp@/@r13@), from high addresses to low:
+
+* Padding (if necessary)
+* Their stack-spilled arguments
+
+The stack is always 4-byte aligned, and must be 8-byte aligned \"at any public
+interface\", i.e., at function calls.
+
+Unlike x86_64, the return address is not stored on the stack.
+
+The following diagram summarizes the stack frame layout:
+
+@
+High addresses
+
+|---------------------|
+| Caller's frame      |
+|---------------------|
+| Padding (if needed) |
+|---------------------|
+| Spilled argument n  |
+|---------------------|
+| ...                 |
+|---------------------|
+| Spilled argument 2  |
+|---------------------|
+| Spilled argument 1  |
+|---------------------| <- sp
+| Callee's frame      |
+|---------------------|
+
+Low addresses
+@
+
+The functions in this module support manipulation of a stack under these
+constraints. ABI-compatible machine code translated by Macaw manages the stack
+for itself, so this module is primarily helpful for initial setup of the stack,
+before starting symbolic execution.
+
+Helpful links:
+
+* <https://github.com/ARM-software/abi-aa/blob/a82eef0433556b30539c0d4463768d9feb8cfd0b/aapcs32/aapcs32.rst#621the-stack>
+* <https://learn.microsoft.com/en-us/cpp/build/overview-of-arm-abi-conventions?view=msvc-170>
+
+(The latter describes the Microsoft ARM ABI which is slightly different from the
+standard ARM ABI, but most of the content still applies.)
+
+This module is meant to be imported qualified.
+-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+
+module Data.Macaw.AArch32.Symbolic.ABI
+  ( StackPointer
+  , getStackPointer
+  , stackPointerReg
+  , alignStackPointer
+  , SpilledArgs(..)
+  , writeSpilledArgs
+  , pushStackFrame
+  , allocStack
+  ) where
+
+import Control.Lens qualified as Lens
+import Data.Coerce (coerce)
+import Data.Macaw.AArch32.Symbolic qualified as AArch32S
+import Data.Macaw.ARM qualified as AArch32
+import Data.Macaw.Symbolic qualified as MS
+import Data.Macaw.Symbolic.Stack qualified as MSS
+import Data.Parameterized.Classes (ixF')
+import Data.Parameterized.Context qualified as Ctx
+import Data.Sequence qualified as Seq
+import Lang.Crucible.Backend qualified as C
+import Lang.Crucible.LLVM.DataLayout qualified as CLD
+import Lang.Crucible.LLVM.MemModel qualified as MM
+import Lang.Crucible.Simulator qualified as C
+import What4.Interface qualified as WI
+
+-- | Helper, not exported
+ptrRepr :: WI.NatRepr 32
+ptrRepr = WI.knownNat
+
+-- | A pointer to an AArch32 stack
+newtype StackPointer sym = StackPointer { getStackPointer :: MM.LLVMPtr sym 32 }
+
+-- | A lens for accessing the stack pointer register as a 'StackPointer'
+stackPointerReg ::
+  Lens.Lens'
+    (Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes AArch32.ARM))
+    (StackPointer sym)
+stackPointerReg =
+  Lens.lens
+    (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' AArch32S.sp)))
+    (\regs v -> regs Lens.& ixF' AArch32S.sp Lens..~ C.RV (getStackPointer v))
+
+-- | Align the stack pointer to a particular 'CLD.Alignment'.
+alignStackPointer ::
+  C.IsSymInterface sym =>
+  sym ->
+  CLD.Alignment ->
+  StackPointer sym ->
+  IO (StackPointer sym)
+alignStackPointer = let ?ptrWidth = ptrRepr in coerce MSS.alignStackPointer
+
+-- | Stack-spilled arguments, in normal order
+newtype SpilledArgs sym
+  = SpilledArgs { getSpilledArgs :: Seq.Seq (MM.LLVMPtr sym 32) }
+
+-- | Write pointer-sized stack-spilled arguments to the stack.
+--
+-- The ABI specifies that they will be written in reverse order, i.e., the last
+-- element of the 'Seq.Seq' will be written to the highest address. It further
+-- specifies that the end of the argument list will be 8-byte aligned. This
+-- function will allocate additional stack space before the spilled arguments if
+-- necessary to establish this constraint.
+--
+-- Asserts that the stack allocation is writable and large enough to contain the
+-- spilled arguments.
+writeSpilledArgs ::
+  C.IsSymBackend sym bak =>
+  (?memOpts :: MM.MemOptions) =>
+  MM.HasLLVMAnn sym =>
+  bak ->
+  MM.MemImpl sym ->
+  StackPointer sym ->
+  SpilledArgs sym ->
+  IO (StackPointer sym, MM.MemImpl sym)
+writeSpilledArgs bak mem sp spilledArgs = do
+  let ?ptrWidth = ptrRepr
+  let align4 = CLD.exponentToAlignment 2  -- 2^2 = 4
+  coerce (MSS.writeSpilledArgs bak) mem align4 sp spilledArgs
+
+-- | Like 'writeSpilledArgs', but manipulates @sp@ directly.
+--
+-- Asserts that the stack allocation is writable and large enough to contain the
+-- spilled arguments.
+pushStackFrame ::
+  C.IsSymBackend sym bak =>
+  (?memOpts :: MM.MemOptions) =>
+  MM.HasLLVMAnn sym =>
+  bak ->
+  MM.MemImpl sym ->
+  -- | Assignment of values to registers
+  Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes AArch32.ARM) ->
+  SpilledArgs sym ->
+  IO
+    ( Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes AArch32.ARM)
+    , MM.MemImpl sym
+    )
+pushStackFrame bak mem regs spilledArgs = do
+  let sp = regs Lens.^. stackPointerReg
+  (sp', mem') <- writeSpilledArgs bak mem sp spilledArgs
+  let regs' = regs Lens.& stackPointerReg Lens..~ sp'
+  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) =>
+  MM.HasLLVMAnn sym =>
+  bak ->
+  MM.MemImpl sym ->
+  -- | Assignment of values to registers
+  Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes AArch32.ARM) ->
+  -- | Size of stack allocation
+  WI.SymExpr sym (WI.BaseBVType 32) ->
+  IO
+    ( Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes AArch32.ARM)
+    , MM.MemImpl sym
+    )
+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
+  let regs' = regs Lens.& stackPointerReg Lens..~ StackPointer top
+  pure (regs', mem')

macaw-aarch32-symbolic/tests/Main.hs

@@ -9,6 +9,7 @@
 module Main (main) where
 
 import           Control.Lens ( (^.) )
+import qualified Data.BitVector.Sized as BVS
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BS8
 import qualified Data.ElfEdit as Elf
@@ -20,6 +21,7 @@ import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.Nonce as PN
 import           Data.Parameterized.Some ( Some(..) )
 import           Data.Proxy ( Proxy(..) )
+import qualified Data.Sequence as Seq
 import qualified Prettyprinter as PP
 import           System.FilePath ( (</>), (<.>) )
 import qualified System.FilePath.Glob as SFG
@@ -33,6 +35,7 @@ import qualified Language.ASL.Globals as ASL
 import qualified Data.Macaw.Architecture.Info as MAI
 
 import qualified Data.Macaw.AArch32.Symbolic as MAS
+import qualified Data.Macaw.AArch32.Symbolic.ABI as ABI
 import qualified Data.Macaw.ARM as MA
 import qualified Data.Macaw.ARM.ARMReg as MAR
 import qualified Data.Macaw.CFG as MC
@@ -43,12 +46,16 @@ import qualified What4.Config as WC
 import qualified What4.Expr.Builder as WEB
 import qualified What4.Interface as WI
 import qualified What4.ProblemFeatures as WPF
+import qualified What4.Protocol.Online as WPO
 import qualified What4.Solver as WS
 
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.Backend.Online as CBO
+import qualified Lang.Crucible.FunctionHandle as CFH
 import qualified Lang.Crucible.Simulator as CS
 import qualified Lang.Crucible.LLVM.MemModel as LLVM
+import qualified Lang.Crucible.CFG.Extension as CCE
+import qualified Lang.Crucible.Types as CT
 
 -- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes
 data SaveSMT = SaveSMT Bool
@@ -146,6 +153,44 @@ armResultExtractor archVals = MST.ResultExtractor $ \regs _mem k -> do
   let re = MS.lookupReg archVals regs (MAR.ARMGlobalBV (ASL.knownGlobalRef @"_R0"))
   k PC.knownRepr (CS.regValue re)
 
+setupRegsAndMem ::
+  ( ext ~ MS.MacawExt MA.ARM
+  , CCE.IsSyntaxExtension ext
+  , CB.IsSymBackend sym bak
+  , LLVM.HasLLVMAnn sym
+  , sym ~ WEB.ExprBuilder scope st fs
+  , bak ~ CBO.OnlineBackend solver scope st fs
+  , WPO.OnlineSolver solver
+  , ?memOpts :: LLVM.MemOptions
+  , MS.HasMacawLazySimulatorState p sym 32
+  ) =>
+  bak ->
+  MS.GenArchVals MS.LLVMMemory MA.ARM ->
+  MST.MemModelPreset ->
+  MST.BinariesInfo MA.ARM ->
+  IO ( CS.RegEntry sym (MS.ArchRegStruct MA.ARM)
+     , MST.InitialMem p sym MA.ARM
+     )
+setupRegsAndMem bak archVals mmPreset binariesInfo = do
+  let sym = CB.backendGetSym bak
+  MST.InitialMem initMem mmConf <-
+    case mmPreset of
+      MST.DefaultMemModel -> MST.initialMem binariesInfo bak MA.arm_linux_info archVals
+      MST.LazyMemModel -> MST.lazyInitialMem binariesInfo bak MA.arm_linux_info archVals
+
+  let symArchFns = MS.archFunctions archVals
+  initRegs <- MST.freshRegs symArchFns sym
+  let kib = 1024
+  let mib = 1024 * kib
+  stackSize <- WI.bvLit sym CT.knownNat (BVS.mkBV CT.knownNat mib)
+  (regs, mem) <- ABI.allocStack bak initMem initRegs stackSize
+  let spilled = ABI.SpilledArgs Seq.Empty
+  (regs', mem') <- ABI.pushStackFrame bak mem regs spilled
+  let crucRegTypes = MS.crucArchRegTypes symArchFns
+  let regsEntry = CS.RegEntry (CT.StructRepr crucRegTypes) regs'
+  let iMem = MST.InitialMem mem' mmConf
+  pure (regsEntry, iMem)
+
 mkSymExTest :: MST.SimulationResult -> MST.MemModelPreset -> FilePath -> TT.TestTree
 mkSymExTest expected mmPreset exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> TT.askOption $ \saveMacaw@(SaveMacaw _) -> TTH.testCaseSteps exePath $ \step -> do
   bytes <- BS.readFile exePath
@@ -191,8 +236,17 @@ symExTestSized expected mmPreset exePath saveSMT saveMacaw step ehi archInfo = d
        let extract = armResultExtractor archVals
        logger <- makeGoalLogger saveSMT solver name exePath
        let ?memOpts = LLVM.defaultMemOptions
-       simRes <- MST.simulateAndVerify solver logger bak execFeatures archInfo archVals binfo mmPreset extract dfi
-       TTH.assertEqual "AssertionResult" expected simRes
+
+       MS.withArchConstraints archVals $ do
+         halloc <- CFH.newHandleAllocator
+         let ?recordLLVMAnnotation = \_ _ _ -> return ()
+
+         (regs, iMem) <- setupRegsAndMem bak archVals mmPreset binfo
+         (memVar, execResult) <-
+           MST.simDiscoveredFunction bak execFeatures archVals halloc iMem regs binfo dfi
+
+         simRes <- MST.summarizeExecution solver logger bak memVar extract execResult
+         TTH.assertEqual "AssertionResult" expected simRes
 
 writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO ()
 writeMacawIR (SaveMacaw sm) name dfi