From 14f312457528f29000a9fecda500a6d27711eec2 Mon Sep 17 00:00:00 2001 From: Your Name Date: Fri, 20 Sep 2024 15:19:20 -0400 Subject: [PATCH 1/9] aarch32-symbolic: Setting up an ABI-compatible stack --- .../macaw-aarch32-symbolic.cabal | 2 + .../src/Data/Macaw/AArch32/Symbolic/ABI.hs | 249 ++++++++++++++++++ 2 files changed, 251 insertions(+) create mode 100644 macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs diff --git a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal b/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal index 439f9efc..ebff9cbe 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, 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..b8c7164e --- /dev/null +++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs @@ -0,0 +1,249 @@ +{-| +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: + +* +* + +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 Control.Monad qualified as Monad +import Data.BitVector.Sized qualified as BVS +import Data.Macaw.ARM qualified as AArch32 +import Data.Macaw.AArch32.Symbolic qualified as AArch32S +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 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 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)) + +-- | Allocate stack space by subtracting from the stack pointer +allocStackSpace :: + C.IsSymInterface sym => + sym -> + StackPointer sym -> + WI.SymBV sym 32 -> + IO (StackPointer sym) +allocStackSpace sym (StackPointer sp) amount = + StackPointer <$> MM.ptrSub sym ptrRepr sp amount + +-- | Align the stack pointer to a particular 'CLD.Alignment'. +alignStackPointer :: + C.IsSymInterface sym => + sym -> + 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')) + +-- | 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. +-- +-- SysV 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 16-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 sym = C.backendGetSym bak + four <- WI.bvLit sym ptrRepr (BVS.mkBV WI.knownNat 4) + let ?ptrWidth = ptrRepr + + -- First, align to 4 bytes. In all probability, this is a no-op. + let align4 = CLD.exponentToAlignment 2 -- 2^2 = 4 + StackPointer spAligned4 <- alignStackPointer sym align4 sp + + -- At this point, exactly one of `spAligned4` or `spAligned4 +/- 4` is 8-byte + -- aligned. We need to ensure that, after writing the argument list, the stack + -- pointer will be 8-byte aligned. + -- + -- If `sp` is already 8-byte aligned and there are an even number of spilled + -- arguments, we're good. If `sp + 4` is already 16-byte aligned and there + -- are an odd number of arguments, we're good. In the other cases, we need to + -- subtract 4 from `sp`. As a table: + -- + -- +----------------------+------+------+ + -- | | even | odd | + -- |----------------------+------+------+ + -- | 16-byte aligned | noop | -4 | + -- +----------------------+-------------+ + -- | not 16-byte aligned | -4 | noop | + -- +----------------------+-------------+ + -- + let align8 = CLD.exponentToAlignment 3 -- 2^3 = 8 + sp8@(StackPointer spAligned8) <- alignStackPointer sym align8 sp + isAligned8 <- MM.ptrEq sym ptrRepr spAligned4 spAligned8 + sp' <- + if even (Seq.length (getSpilledArgs spilledArgs)) + then + -- In this case, either the stack pointer is *already* 8-byte aligned, or + -- it *needs to be* 8-byte aligned (which is equivalent to subtracting 4, + -- as it is already 4-byte aligned). In either case, this value suffices. + pure sp8 + else do + StackPointer spAdd4 <- allocStackSpace sym sp8 four + StackPointer <$> MM.muxLLVMPtr sym isAligned8 spAdd4 spAligned4 + + let i32 = MM.bitvectorType (Bytes.toBytes (32 :: Int)) + let writeWord (StackPointer p, m) arg = do + p' <- MM.ptrSub sym ?ptrWidth p four + m' <- MM.storeRaw bak m p' i32 CLD.noAlignment (MM.ptrToPtrVal arg) + pure (StackPointer p', m') + Monad.foldM writeWord (sp', mem) (Seq.reverse (getSpilledArgs spilledArgs)) + +-- | Like 'writeSpilledArgs', but manipulates @sp@ directly. +-- +-- Asserts that the stack allocation is writable and large enough to contain the +-- spilled arguments and return address. +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') From 2398322a2c9ae123c7819ddd58aa1c2e2367f8f1 Mon Sep 17 00:00:00 2001 From: Your Name Date: Fri, 20 Sep 2024 17:29:08 -0400 Subject: [PATCH 2/9] symbolic: Upstream stack spilled argument code from x86-symbolic ...so that it can also be used by AArch32. --- symbolic/src/Data/Macaw/Symbolic/Stack.hs | 122 ++++++++++++++++++ .../src/Data/Macaw/X86/Symbolic/ABI/SysV.hs | 57 +------- 2 files changed, 125 insertions(+), 54 deletions(-) diff --git a/symbolic/src/Data/Macaw/Symbolic/Stack.hs b/symbolic/src/Data/Macaw/Symbolic/Stack.hs index 18a17148..c2ed1086 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Stack.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Stack.hs @@ -12,13 +12,20 @@ module Data.Macaw.Symbolic.Stack , ExtraStackSlots(..) , ArrayStack(..) , createArrayStack + , allocStackSpace + , alignStackPointer + , writeSpilledArgs ) where import Data.BitVector.Sized qualified as BVS import Data.Parameterized.Context as Ctx +import GHC.Natural (naturalToInteger) import Lang.Crucible.Backend qualified as C import Lang.Crucible.LLVM.DataLayout qualified as CLD import Lang.Crucible.LLVM.MemModel qualified as CLM +import qualified Control.Monad as Monad +import qualified Data.Sequence as Seq +import qualified Lang.Crucible.LLVM.Bytes as Bytes import What4.Interface qualified as WI import What4.Symbol qualified as WSym @@ -111,3 +118,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..448c33a0 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 @@ -91,6 +91,7 @@ import Lang.Crucible.LLVM.Bytes qualified as Bytes import Lang.Crucible.LLVM.DataLayout qualified as CLD import Lang.Crucible.LLVM.MemModel qualified as MM import Lang.Crucible.Simulator qualified as C +import qualified Data.Macaw.Symbolic.Stack as Stack import What4.Interface qualified as WI -- | Helper, not exported @@ -113,16 +114,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 } @@ -176,51 +167,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 (Stack.writeSpilledArgs bak) mem align8 sp spilledArgs -- | Write the return address to the stack. -- From e741905b21689fb8ba2c2c3e540668804cdf0465 Mon Sep 17 00:00:00 2001 From: Your Name Date: Fri, 20 Sep 2024 17:41:20 -0400 Subject: [PATCH 3/9] symbolic-aarch32: Use upstream code for stack-spilled arguments --- .../src/Data/Macaw/AArch32/Symbolic/ABI.hs | 63 ++----------------- .../src/Data/Macaw/X86/Symbolic/ABI/SysV.hs | 3 +- 2 files changed, 6 insertions(+), 60 deletions(-) diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs index b8c7164e..88409fd7 100644 --- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs +++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs @@ -68,10 +68,10 @@ module Data.Macaw.AArch32.Symbolic.ABI ) where import Control.Lens qualified as Lens -import Control.Monad qualified as Monad import Data.BitVector.Sized qualified as BVS -import Data.Macaw.ARM qualified as AArch32 +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') @@ -79,7 +79,6 @@ 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 import Lang.Crucible.LLVM.MemModel qualified as MM import Lang.Crucible.Simulator qualified as C @@ -102,16 +101,6 @@ stackPointerReg = (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' AArch32S.sp))) (\regs v -> regs Lens.& ixF' AArch32S.sp Lens..~ C.RV (getStackPointer v)) --- | Allocate stack space by subtracting from the stack pointer -allocStackSpace :: - C.IsSymInterface sym => - sym -> - StackPointer sym -> - WI.SymBV sym 32 -> - IO (StackPointer sym) -allocStackSpace sym (StackPointer sp) amount = - StackPointer <$> MM.ptrSub sym ptrRepr sp amount - -- | Align the stack pointer to a particular 'CLD.Alignment'. alignStackPointer :: C.IsSymInterface sym => @@ -137,9 +126,9 @@ newtype SpilledArgs sym -- | Write pointer-sized stack-spilled arguments to the stack. -- --- SysV specifies that they will be written in reverse order, i.e., the last +-- 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 16-byte aligned. This +-- 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. -- @@ -155,51 +144,9 @@ writeSpilledArgs :: SpilledArgs sym -> IO (StackPointer sym, MM.MemImpl sym) writeSpilledArgs bak mem sp spilledArgs = do - let sym = C.backendGetSym bak - four <- WI.bvLit sym ptrRepr (BVS.mkBV WI.knownNat 4) let ?ptrWidth = ptrRepr - - -- First, align to 4 bytes. In all probability, this is a no-op. let align4 = CLD.exponentToAlignment 2 -- 2^2 = 4 - StackPointer spAligned4 <- alignStackPointer sym align4 sp - - -- At this point, exactly one of `spAligned4` or `spAligned4 +/- 4` is 8-byte - -- aligned. We need to ensure that, after writing the argument list, the stack - -- pointer will be 8-byte aligned. - -- - -- If `sp` is already 8-byte aligned and there are an even number of spilled - -- arguments, we're good. If `sp + 4` is already 16-byte aligned and there - -- are an odd number of arguments, we're good. In the other cases, we need to - -- subtract 4 from `sp`. As a table: - -- - -- +----------------------+------+------+ - -- | | even | odd | - -- |----------------------+------+------+ - -- | 16-byte aligned | noop | -4 | - -- +----------------------+-------------+ - -- | not 16-byte aligned | -4 | noop | - -- +----------------------+-------------+ - -- - let align8 = CLD.exponentToAlignment 3 -- 2^3 = 8 - sp8@(StackPointer spAligned8) <- alignStackPointer sym align8 sp - isAligned8 <- MM.ptrEq sym ptrRepr spAligned4 spAligned8 - sp' <- - if even (Seq.length (getSpilledArgs spilledArgs)) - then - -- In this case, either the stack pointer is *already* 8-byte aligned, or - -- it *needs to be* 8-byte aligned (which is equivalent to subtracting 4, - -- as it is already 4-byte aligned). In either case, this value suffices. - pure sp8 - else do - StackPointer spAdd4 <- allocStackSpace sym sp8 four - StackPointer <$> MM.muxLLVMPtr sym isAligned8 spAdd4 spAligned4 - - let i32 = MM.bitvectorType (Bytes.toBytes (32 :: Int)) - let writeWord (StackPointer p, m) arg = do - p' <- MM.ptrSub sym ?ptrWidth p four - m' <- MM.storeRaw bak m p' i32 CLD.noAlignment (MM.ptrToPtrVal arg) - pure (StackPointer p', m') - Monad.foldM writeWord (sp', mem) (Seq.reverse (getSpilledArgs spilledArgs)) + coerce (MSS.writeSpilledArgs bak) mem align4 sp spilledArgs -- | Like 'writeSpilledArgs', but manipulates @sp@ directly. -- 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 448c33a0..b1003412 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs @@ -91,7 +91,6 @@ import Lang.Crucible.LLVM.Bytes qualified as Bytes import Lang.Crucible.LLVM.DataLayout qualified as CLD import Lang.Crucible.LLVM.MemModel qualified as MM import Lang.Crucible.Simulator qualified as C -import qualified Data.Macaw.Symbolic.Stack as Stack import What4.Interface qualified as WI -- | Helper, not exported @@ -169,7 +168,7 @@ writeSpilledArgs :: writeSpilledArgs bak mem sp spilledArgs = do let ?ptrWidth = ptrRepr let align8 = CLD.exponentToAlignment 3 -- 2^3 = 8 - coerce (Stack.writeSpilledArgs bak) mem align8 sp spilledArgs + coerce (MSS.writeSpilledArgs bak) mem align8 sp spilledArgs -- | Write the return address to the stack. -- From 3cdbb2c962bb98f22c4d583abbab57ce35585886 Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 23 Sep 2024 13:16:29 -0400 Subject: [PATCH 4/9] symbolic: Fix off-by-one error in stack setup code --- symbolic/src/Data/Macaw/Symbolic/Stack.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/symbolic/src/Data/Macaw/Symbolic/Stack.hs b/symbolic/src/Data/Macaw/Symbolic/Stack.hs index c2ed1086..e71a62f4 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Stack.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Stack.hs @@ -110,7 +110,8 @@ 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 + 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 From 33af2814d99068a15473e7858f15a66b765dd79f Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 23 Sep 2024 11:26:39 -0400 Subject: [PATCH 5/9] symbolic-aarch32: Use ABI-compatible stack setup code in test harness --- .../macaw-aarch32-symbolic.cabal | 1 + .../src/Data/Macaw/AArch32/Symbolic/ABI.hs | 2 +- macaw-aarch32-symbolic/tests/Main.hs | 58 ++++++++++++++++++- x86_symbolic/tests/Main.hs | 1 - 4 files changed, 58 insertions(+), 4 deletions(-) diff --git a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal b/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal index ebff9cbe..5ee7bd4e 100644 --- a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal +++ b/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal @@ -53,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 index 88409fd7..740a0894 100644 --- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs +++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs @@ -151,7 +151,7 @@ writeSpilledArgs bak mem sp spilledArgs = do -- | Like 'writeSpilledArgs', but manipulates @sp@ directly. -- -- Asserts that the stack allocation is writable and large enough to contain the --- spilled arguments and return address. +-- spilled arguments. pushStackFrame :: C.IsSymBackend sym bak => (?memOpts :: MM.MemOptions) => 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/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 From dcc87334c799ce4c72abacd37466a94cfe9e06d6 Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 23 Sep 2024 15:49:03 -0400 Subject: [PATCH 6/9] x86-symbolic: Reuse upstream implementation of `alignStackPointer` --- .../src/Data/Macaw/X86/Symbolic/ABI/SysV.hs | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) 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 b1003412..d9deb234 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs @@ -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 @@ -130,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 From c43be551df5fbf8fb7f4dcdb9a1fd8bf725d70a6 Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 23 Sep 2024 15:49:12 -0400 Subject: [PATCH 7/9] aarch32-symbolic: Reuse upstream implementation of `alignStackPointer` --- .../src/Data/Macaw/AArch32/Symbolic/ABI.hs | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs index 740a0894..74827d20 100644 --- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs +++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs @@ -68,7 +68,6 @@ module Data.Macaw.AArch32.Symbolic.ABI ) where import Control.Lens qualified as Lens -import Data.BitVector.Sized qualified as BVS import Data.Coerce (coerce) import Data.Macaw.AArch32.Symbolic qualified as AArch32S import Data.Macaw.ARM qualified as AArch32 @@ -77,7 +76,6 @@ 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 GHC.Natural (naturalToInteger) import Lang.Crucible.Backend qualified as C import Lang.Crucible.LLVM.DataLayout qualified as CLD import Lang.Crucible.LLVM.MemModel qualified as MM @@ -108,17 +106,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 From 94195b485c7f8d1489b93014b09320c63d3df71f Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 23 Sep 2024 15:50:44 -0400 Subject: [PATCH 8/9] symbolic: Sort imports --- symbolic/src/Data/Macaw/Symbolic/Stack.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/symbolic/src/Data/Macaw/Symbolic/Stack.hs b/symbolic/src/Data/Macaw/Symbolic/Stack.hs index e71a62f4..db48d8e6 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Stack.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Stack.hs @@ -17,15 +17,15 @@ module Data.Macaw.Symbolic.Stack , 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 qualified Control.Monad as Monad -import qualified Data.Sequence as Seq -import qualified Lang.Crucible.LLVM.Bytes as Bytes import What4.Interface qualified as WI import What4.Symbol qualified as WSym From e9f939a24528360db6ef4761964e1735aefa84e3 Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 23 Sep 2024 16:30:55 -0400 Subject: [PATCH 9/9] {aarch32-,}symbolic: Additional commentary --- macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs | 3 +++ symbolic/src/Data/Macaw/Symbolic/Stack.hs | 3 +++ 2 files changed, 6 insertions(+) diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs index 74827d20..fbbe0d72 100644 --- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs +++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs @@ -49,6 +49,9 @@ 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. -} diff --git a/symbolic/src/Data/Macaw/Symbolic/Stack.hs b/symbolic/src/Data/Macaw/Symbolic/Stack.hs index db48d8e6..8708be30 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Stack.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Stack.hs @@ -110,8 +110,11 @@ createArrayStack bak mem slots sz = do (base, mem1) <- mallocStack bak mem sz mem2 <- CLM.doArrayStore bak mem1 base stackAlign arr 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