Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

x86-symbolic: Setting up a SysV-compatible stack #433

Merged
merged 22 commits into from
Sep 17, 2024
Merged
Changes from 1 commit
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
9955200
x86-symbolic: Setting up a SysV-compatible stack
langston-barrett Sep 3, 2024
ffcab1c
x86-symbolic: A module for SysV stack manipulation
langston-barrett Sep 4, 2024
e947585
x86-symbolic: More SysV stack setup and manipulation
langston-barrett Sep 4, 2024
145e005
x86-symbolic: Sort imports
langston-barrett Sep 4, 2024
c68cda0
symbolic: Remove unused LANGUAGE pragmas
langston-barrett Sep 4, 2024
f3fd0e0
symbolic: Small refactoring in `Testing` module
langston-barrett Sep 4, 2024
0c5ed97
symbolic: Rename and move a helper function in `Testing`
langston-barrett Sep 4, 2024
820401d
symbolic: Factor out fresh register assignment generator
langston-barrett Sep 4, 2024
c65ad34
symbolic: Data type for `(mem, mmConf)` tuple
langston-barrett Sep 4, 2024
6fcdb93
symbolic: Pass initial memory into `simulateFunction` as an argument
langston-barrett Sep 4, 2024
2372f69
symbolic: Factor out construction of initial registers and stack
langston-barrett Sep 4, 2024
2033a7d
symbolic: Further split up `simulateFunction`
langston-barrett Sep 4, 2024
be0a57f
symbolic: Don't feed the stack pointer to the `ResultExtractor`
langston-barrett Sep 5, 2024
ec0b522
symbolic: Further split up `simulateAndVerify`
langston-barrett Sep 6, 2024
9f2da79
symbolic: Try proving *all* safety conditions
langston-barrett Sep 6, 2024
ce96ba9
symbolic: Factor out simulation of discovered functions
langston-barrett Sep 11, 2024
672e0c5
symbolic: Generalize and simplify `simMacawCfg`
langston-barrett Sep 11, 2024
d005b9c
symbolic: More refactoring of testing code
langston-barrett Sep 11, 2024
b37e907
symbolic: Remove redundant constraints in testing code
langston-barrett Sep 11, 2024
edc9635
x86-symbolic: Use SysV-compatible stack setup in test suite
langston-barrett Sep 11, 2024
f80b275
symbolic: Sort imports
langston-barrett Sep 11, 2024
e1886a8
symbolic: Address review comments
langston-barrett Sep 12, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
x86-symbolic: Setting up a SysV-compatible stack
  • Loading branch information
langston-barrett committed Sep 3, 2024
commit 99552008379c09a84e35c22ad7ad7ec069af63ca
1 change: 1 addition & 0 deletions x86_symbolic/macaw-x86-symbolic.cabal
Original file line number Diff line number Diff line change
@@ -9,6 +9,7 @@ license-file: LICENSE

library
build-depends: base >= 4.13,
containers,
bv-sized >= 1.0.0,
crucible >= 0.4,
crucible-llvm,
104 changes: 104 additions & 0 deletions x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
Original file line number Diff line number Diff line change
@@ -44,22 +44,28 @@ module Data.Macaw.X86.Symbolic
, r15
, getReg
, IP, GP, Flag, X87Status, X87Top, X87Tag, FPReg, YMM
, x86SysvStack
) where

import Control.Lens ((^.),(%~),(&))
import qualified Control.Monad as Monad
import Control.Monad ( void )
import Control.Monad.IO.Class ( liftIO )
import qualified Data.BitVector.Sized as BVS
import Data.Functor.Identity (Identity(..))
import Data.Kind
import Data.Parameterized.Context as Ctx
import Data.Parameterized.Map as MapF
import Data.Parameterized.TraversableF
import Data.Parameterized.TraversableFC
import qualified Data.Sequence as Seq
import Data.Word (Word8)
import GHC.TypeLits

import qualified Data.Macaw.CFG as M
import Data.Macaw.Symbolic
import Data.Macaw.Symbolic.Backend
import qualified Data.Macaw.Symbolic.Stack as MSS
import qualified Data.Macaw.Types as M
import qualified Data.Macaw.X86 as M
import qualified Data.Macaw.X86.X86Reg as M
@@ -77,6 +83,8 @@ import qualified Lang.Crucible.CFG.Reg as C
import qualified Lang.Crucible.CFG.Expr as CE
import qualified Lang.Crucible.Simulator as C
import qualified Lang.Crucible.Types as C
import qualified Lang.Crucible.LLVM.Bytes as Bytes
import qualified Lang.Crucible.LLVM.DataLayout as CLD
import qualified Lang.Crucible.LLVM.MemModel as MM

------------------------------------------------------------------------
@@ -472,6 +480,102 @@ instance GenArchInfo LLVMMemory M.X86_64 where
, updateReg = x86UpdateReg
}

-- | Helper, not exported
writeBytesBackwards ::
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
MM.HasPtrWidth w =>
C.IsSymBackend sym bak =>
(?memOpts :: MM.MemOptions) =>
MM.HasLLVMAnn sym =>
bak ->
MM.MemImpl sym ->
MM.LLVMPtr sym w ->
Seq.Seq Word8 ->
IO (MM.LLVMPtr sym w, MM.MemImpl sym)
writeBytesBackwards bak mem ptr bytes = do
let sym = C.backendGetSym bak
let i8 = MM.bitvectorType (Bytes.toBytes (1 :: Int))
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
z <- WI.natLit sym 0
one <- WI.bvOne sym ?ptrWidth
let writeByte (p, m) byte = do
p' <- MM.ptrSub sym ?ptrWidth p one
bv <- WI.bvLit sym (C.knownNat @8) (BVS.mkBV C.knownNat (fromIntegral byte))
m' <- MM.storeRaw bak m p' i8 CLD.noAlignment (MM.LLVMValInt z bv)
pure (p', m')
Monad.foldM writeByte (ptr, mem) (Seq.reverse bytes)

-- | Create an allocation for the stack for x86_64 with the SysV ABI.
--
-- On x86_64 with the SysV ABI, 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 @rsp@):
--
-- * Their stack-spilled arguments
-- * The return address
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
--
-- To model this behavior, this function:
--
-- 1. Uses 'MSS.createArrayStack' to allocate the stack, which returns a stack
-- allocation and a pointer to its end, minus the space for stack-spilled
-- arguments (see its Haddocks for details)
-- 2. Decrements the pointer to the top of the stack ('MSS.arrayStackTopPtr') by
-- 8 bytes (i.e., the size of a pointer)
-- 3. Writes a symbolic return address to the top of the stack
--
-- (Unless a concrete list of bytes is passed, in which case the decrement (2)
-- is by the length of that list, and the write (3) is of those bytes.)
--
-- This setup should enable calling most functions without incident, after the
-- returned pointer is put in @rsp@. Those that expect stack-spilled arguments
-- may end up reading from the (uninitialized) stack slots.
--
-- Notably, the Microsoft x86_64 ABI differs in the stack setup. See
-- [this link](https://learn.microsoft.com/en-us/cpp/build/stack-usage)
-- for more detailson that ABI.
x86SysvStack ::
C.IsSymBackend sym bak =>
(?memOpts :: MM.MemOptions) =>
MM.HasLLVMAnn sym =>
bak ->
MM.MemImpl sym ->
-- | Initialize the end of the stack to a concrete sequence of bytes if the
-- value is @Just@, otherwise initialize the end of the stack to 8 fresh,
-- symbolic bytes.
Maybe (Seq.Seq Word8) ->
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
-- | The caller must ensure the size of these is less than the allocation size
MSS.ExtraStackSlots ->
-- | Size of stack allocation
WI.SymExpr sym (WI.BaseBVType 64) ->
IO (MSS.ArrayStack sym 64, MM.MemImpl sym)
x86SysvStack bak mem topBytes slots sz = do
let ptrBytes = 8
let ?ptrWidth = C.knownNat @64

(arrayStack, mem') <- MSS.createArrayStack bak mem slots sz
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
MSS.ArrayStack _base top _array <- pure arrayStack
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved

let i8 = MM.bitvectorType (Bytes.toBytes (1 :: Int))
(top', mem'') <-
case topBytes of
Nothing -> do
-- (2)
let sym = C.backendGetSym bak
ptrSzBv <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth ptrBytes)
top' <- MM.ptrSub sym ?ptrWidth top ptrSzBv

-- (3)
z <- WI.natLit sym 0
bv <- WI.freshConstant sym (WI.safeSymbol "x86_64_ret_addr") (WI.BaseBVRepr ?ptrWidth)
let val = MM.LLVMValInt z bv
let storTy = MM.arrayType (fromIntegral ptrBytes) i8
mem'' <- MM.storeRaw bak mem' top' storTy CLD.noAlignment val
pure (top', mem'')

Just bytes -> writeBytesBackwards bak mem' top bytes

let arrayStack' = arrayStack { MSS.arrayStackTopPtr = top' }
return (arrayStack', mem'')

{- Note [Syscalls]

While most of the extension functions can be translated directly by embedding them in