diff --git a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal b/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal index 439f9efc..5ee7bd4e 100644 --- a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal +++ b/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, diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs new file mode 100644 index 00000000..fbbe0d72 --- /dev/null +++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs @@ -0,0 +1,187 @@ +{-| +Copyright : (c) Galois, Inc 2024 +Maintainer : Langston Barrett + +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: + +* +* + +(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') diff --git a/macaw-aarch32-symbolic/tests/Main.hs b/macaw-aarch32-symbolic/tests/Main.hs index f3a75c59..4b6a907e 100644 --- a/macaw-aarch32-symbolic/tests/Main.hs +++ b/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 diff --git a/symbolic/src/Data/Macaw/Symbolic/Stack.hs b/symbolic/src/Data/Macaw/Symbolic/Stack.hs index 18a17148..8708be30 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Stack.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Stack.hs @@ -12,11 +12,18 @@ module Data.Macaw.Symbolic.Stack , ExtraStackSlots(..) , ArrayStack(..) , createArrayStack + , allocStackSpace + , alignStackPointer + , writeSpilledArgs ) where +import Control.Monad qualified as Monad import Data.BitVector.Sized qualified as BVS import Data.Parameterized.Context as Ctx +import Data.Sequence qualified as Seq +import GHC.Natural (naturalToInteger) import Lang.Crucible.Backend qualified as C +import Lang.Crucible.LLVM.Bytes qualified as Bytes import Lang.Crucible.LLVM.DataLayout qualified as CLD import Lang.Crucible.LLVM.MemModel qualified as CLM import What4.Interface qualified as WI @@ -103,7 +110,11 @@ createArrayStack bak mem slots sz = do (base, mem1) <- mallocStack bak mem sz mem2 <- CLM.doArrayStore bak mem1 base stackAlign arr sz - end <- CLM.doPtrAddOffset bak mem2 base sz + -- 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 @@ -111,3 +122,118 @@ createArrayStack bak mem slots sz = do top <- CLM.ptrSub sym ?ptrWidth end slotsBytesBv pure (ArrayStack base top arr, mem2) + +-- | Allocate stack space by subtracting from the stack pointer +-- +-- This is only suitable for use with architectures/ABIs where the stack grows +-- down. +allocStackSpace :: + C.IsSymInterface sym => + CLM.HasPtrWidth w => + sym -> + CLM.LLVMPtr sym w -> + WI.SymBV sym w -> + IO (CLM.LLVMPtr sym w) +allocStackSpace sym = CLM.ptrSub sym ?ptrWidth + +-- | Align the stack pointer to a particular 'CLD.Alignment'. +-- +-- This is only suitable for use with architectures/ABIs where the stack grows +-- down. +alignStackPointer :: + C.IsSymInterface sym => + CLM.HasPtrWidth w => + sym -> + CLD.Alignment -> + CLM.LLVMPtr sym w -> + IO (CLM.LLVMPtr sym w) +alignStackPointer sym align orig@(CLM.LLVMPointer blk off) = do + let alignInt = 2 ^ naturalToInteger (CLD.alignmentToExponent align) + if alignInt == 1 + then pure orig + else do + -- Because the stack grows down, we can align it by simply ANDing the stack + -- pointer with a mask with some amount of 1s followed by some amount of 0s. + let mask = BVS.complement ?ptrWidth (BVS.mkBV ?ptrWidth (alignInt - 1)) + maskBv <- WI.bvLit sym ?ptrWidth mask + off' <- WI.bvAndBits sym off maskBv + pure (CLM.LLVMPointer blk off') + +-- | Write pointer-sized stack-spilled arguments to the stack. +-- +-- This function: +-- +-- * Aligns the stack to the minimum provided 'CLD.Alignment', call this M. +-- * Potentially adds padding to ensure that after writing the arguments to the +-- stack, the resulting stack pointer will be 2M-aligned. +-- * Writes the stack-spilled arguments, in reverse order. +-- +-- It is suitable for use with architectures/ABIs where the above is +-- the desired behavior, e.g., AArch32 and SysV on x86_64. However, +-- macaw-symbolic-{aarch32,x86} provide higher-level wrappers around this +-- function, so its direct use is discouraged. +-- +-- Asserts that the stack allocation is writable and large enough to contain the +-- spilled arguments. +writeSpilledArgs :: + C.IsSymBackend sym bak => + (?memOpts :: CLM.MemOptions) => + CLM.HasPtrWidth w => + CLM.HasLLVMAnn sym => + bak -> + CLM.MemImpl sym -> + -- | Minimum stack alignment + CLD.Alignment -> + CLM.LLVMPtr sym w -> + -- | Stack spilled arguments, in normal left-to-right order + Seq.Seq (CLM.LLVMPtr sym w) -> + IO (CLM.LLVMPtr sym w, CLM.MemImpl sym) +writeSpilledArgs bak mem minAlign sp spilledArgs = do + let sym = C.backendGetSym bak + + -- M is the minimum alignment, as an integer + let m = 2 ^ CLD.alignmentToExponent minAlign + + -- First, align to M bytes. In all probability, this is a no-op. + spAlignedMin <- alignStackPointer sym minAlign sp + + -- At this point, exactly one of `spAlignedMin` or `spAlignedMin +/- M` is + -- 2M-byte aligned. We need to ensure that, after writing the argument list, + -- the stack pointer will be 2M-byte aligned. + -- + -- If `sp` is already 2M-byte aligned and there are an even number of spilled + -- arguments, we're good. If `sp + M` is already 2M-byte aligned and there + -- are an odd number of arguments, we're good. In the other cases, we need to + -- subtract M from `sp`. As a table: + -- + -- +----------------------+------+------+ + -- | | even | odd | + -- |----------------------+------+------+ + -- | 16-byte aligned | noop | -M | + -- +----------------------+-------------+ + -- | not 16-byte aligned | -M | noop | + -- +----------------------+-------------+ + -- + let alignMore = CLD.exponentToAlignment (CLD.alignmentToExponent minAlign + 1) + spAlignedMore <- alignStackPointer sym alignMore sp + isAlignedMore <- CLM.ptrEq sym ?ptrWidth spAlignedMin spAlignedMore + sp' <- + if even (Seq.length spilledArgs) + then + -- In this case, either the stack pointer is *already* 2M-byte aligned, or + -- it *needs to be* 2M-byte aligned (which is equivalent to subtracting M, + -- as it is already M-byte aligned). In either case, this value suffices. + pure spAlignedMore + else do + mBv <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth m) + spSubMore <- allocStackSpace sym spAlignedMore mBv + CLM.muxLLVMPtr sym isAlignedMore spSubMore spAlignedMin + + let ptrBytes = WI.natValue ?ptrWidth `div` 8 + ptrBytesBv <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth (fromIntegral ptrBytes)) + let ptrSz = CLM.bitvectorType (Bytes.toBytes ptrBytes) + let writeWord (p, mi) arg = do + p' <- CLM.ptrSub sym ?ptrWidth p ptrBytesBv + mi' <- CLM.storeRaw bak mi p' ptrSz CLD.noAlignment (CLM.ptrToPtrVal arg) + pure (p', mi') + Monad.foldM writeWord (sp', mem) (Seq.reverse spilledArgs) diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs index 9f893657..d9deb234 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs @@ -76,8 +76,8 @@ module Data.Macaw.X86.Symbolic.ABI.SysV ) where import Control.Lens qualified as Lens -import Control.Monad qualified as Monad import Data.BitVector.Sized qualified as BVS +import Data.Coerce (coerce) import Data.Macaw.Symbolic qualified as MS import Data.Macaw.Symbolic.Stack qualified as MSS import Data.Macaw.X86 qualified as X86 @@ -85,7 +85,6 @@ import Data.Macaw.X86.Symbolic qualified as X86S import Data.Parameterized.Classes (ixF') import Data.Parameterized.Context qualified as Ctx import Data.Sequence qualified as Seq -import GHC.Natural (naturalToInteger) import Lang.Crucible.Backend qualified as C import Lang.Crucible.LLVM.Bytes qualified as Bytes import Lang.Crucible.LLVM.DataLayout qualified as CLD @@ -113,16 +112,6 @@ stackPointerReg = (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' X86S.rsp))) (\regs v -> regs Lens.& ixF' X86S.rsp Lens..~ C.RV (getStackPointer v)) --- | Allocate stack space by subtracting from the stack pointer -allocStackSpace :: - C.IsSymInterface sym => - sym -> - StackPointer sym -> - WI.SymBV sym 64 -> - IO (StackPointer sym) -allocStackSpace sym (StackPointer sp) amount = - StackPointer <$> MM.ptrSub sym ptrRepr sp amount - -- | A return address newtype RetAddr sym = RetAddr { getRetAddr :: MM.LLVMPtr sym 64 } @@ -140,17 +129,7 @@ alignStackPointer :: CLD.Alignment -> StackPointer sym -> IO (StackPointer sym) -alignStackPointer sym align orig@(StackPointer (MM.LLVMPointer blk off)) = do - let alignInt = 2 ^ naturalToInteger (CLD.alignmentToExponent align) - if alignInt == 1 - then pure orig - else do - -- Because the stack grows down, we can align it by simply ANDing the stack - -- pointer with a mask with some amount of 1s followed by some amount of 0s. - let mask = BVS.complement ptrRepr (BVS.mkBV ptrRepr (alignInt - 1)) - maskBv <- WI.bvLit sym ptrRepr mask - off' <- WI.bvAndBits sym off maskBv - pure (StackPointer (MM.LLVMPointer blk off')) +alignStackPointer = let ?ptrWidth = ptrRepr in coerce MSS.alignStackPointer -- | Stack-spilled arguments, in normal order newtype SpilledArgs sym @@ -176,51 +155,9 @@ writeSpilledArgs :: SpilledArgs sym -> IO (StackPointer sym, MM.MemImpl sym) writeSpilledArgs bak mem sp spilledArgs = do - let sym = C.backendGetSym bak - eight <- WI.bvLit sym ptrRepr (BVS.mkBV WI.knownNat 8) - let i64 = MM.bitvectorType (Bytes.toBytes (64 :: Int)) let ?ptrWidth = ptrRepr - - -- First, align to 8 bytes. In all probability, this is a no-op. let align8 = CLD.exponentToAlignment 3 -- 2^3 = 8 - StackPointer spAligned8 <- alignStackPointer sym align8 sp - - -- At this point, exactly one of `spAligned8` or `spAligned8 +/- 8` is 16-byte - -- aligned. We need to ensure that, after writing the argument list, the stack - -- pointer will be 16-byte aligned. - -- - -- If `rsp` is already 16-byte aligned and there are an even number of spilled - -- arguments, we're good. If `rsp + 8` is already 16-byte aligned and there - -- are an odd number of arguments, we're good. In the other cases, we need to - -- subtract 8 from `rsp`. As a table: - -- - -- +----------------------+------+------+ - -- | | even | odd | - -- |----------------------+------+------+ - -- | 16-byte aligned | noop | -8 | - -- +----------------------+-------------+ - -- | not 16-byte aligned | -8 | noop | - -- +----------------------+-------------+ - -- - let align16 = CLD.exponentToAlignment 4 -- 2^4 = 16 - sp16@(StackPointer spAligned16) <- alignStackPointer sym align16 sp - isAligned16 <- MM.ptrEq sym ptrRepr spAligned8 spAligned16 - sp' <- - if even (Seq.length (getSpilledArgs spilledArgs)) - then - -- In this case, either the stack pointer is *already* 16-byte aligned, or - -- it *needs to be* 16-byte aligned (which is equivalent to subtracting 8, - -- as it is already 8-byte aligned). In either case, this value suffices. - pure sp16 - else do - StackPointer spAdd8 <- allocStackSpace sym sp16 eight - StackPointer <$> MM.muxLLVMPtr sym isAligned16 spAdd8 spAligned8 - - let writeWord (StackPointer p, m) arg = do - p' <- MM.ptrSub sym ?ptrWidth p eight - m' <- MM.storeRaw bak m p' i64 CLD.noAlignment (MM.ptrToPtrVal arg) - pure (StackPointer p', m') - Monad.foldM writeWord (sp', mem) (Seq.reverse (getSpilledArgs spilledArgs)) + coerce (MSS.writeSpilledArgs bak) mem align8 sp spilledArgs -- | Write the return address to the stack. -- diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs index f92bcdb7..99d0a167 100644 --- a/x86_symbolic/tests/Main.hs +++ b/x86_symbolic/tests/Main.hs @@ -185,7 +185,6 @@ setupRegsAndMem bak archVals mmPreset binariesInfo = do 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