Skip to content

Commit

Permalink
x86-symbolic: Use SysV-compatible stack setup in test suite
Browse files Browse the repository at this point in the history
  • Loading branch information
langston-barrett committed Sep 11, 2024
1 parent b37e907 commit b39ef9b
Show file tree
Hide file tree
Showing 3 changed files with 42 additions and 4 deletions.
10 changes: 8 additions & 2 deletions symbolic/src/Data/Macaw/Symbolic/Testing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,12 @@ module Data.Macaw.Symbolic.Testing (
MemModelPreset(..),
describeMemModelPreset,
toAddrSymMap,
freshRegs,
InitialMem(..),
initialMem,
lazyInitialMem,
simDiscoveredFunction,
summarizeExecution,
-- * Execution features
SomeBackend(..),
defaultExecFeatures,
Expand Down Expand Up @@ -583,8 +589,8 @@ lazyInitialMem binfo bak archInfo archVals = do

data InitialMem p sym arch
= InitialMem
{ _initMemMem :: CLM.MemImpl sym
, _initMemMmConf :: MS.MemModelConfig p sym arch CLM.Mem
{ initMemMem :: CLM.MemImpl sym
, initMemMmConf :: MS.MemModelConfig p sym arch CLM.Mem
}

-- | Set up the symbolic execution engine with initial states and execute
Expand Down
1 change: 1 addition & 0 deletions x86_symbolic/macaw-x86-symbolic.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ test-suite macaw-x86-symbolic-tests
hs-source-dirs: tests
build-depends:
base >= 4,
bv-sized,
bytestring,
containers,
crucible,
Expand Down
35 changes: 33 additions & 2 deletions x86_symbolic/tests/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,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
Expand All @@ -18,6 +19,7 @@ import qualified Data.Parameterized.Classes as PC
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
Expand All @@ -34,14 +36,17 @@ import qualified Data.Macaw.Symbolic.Testing as MST
import qualified Data.Macaw.X86 as MX
import Data.Macaw.X86.Symbolic ()
import qualified Data.Macaw.X86.Symbolic as MXS
import qualified Data.Macaw.X86.Symbolic.ABI.SysV as SysV
import qualified What4.Config as WC
import qualified What4.Interface as WI
import qualified What4.ProblemFeatures as WPF
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.Types as CT
import qualified Lang.Crucible.LLVM.MemModel as LLVM

import qualified What4.FloatMode as W4
Expand Down Expand Up @@ -171,8 +176,34 @@ mkSymExTest expected mmPreset exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> T
let extract = x86ResultExtractor archVals
logger <- makeGoalLogger saveSMT solver name exePath
let ?memOpts = LLVM.defaultMemOptions
simRes <- MST.simulateAndVerify solver logger bak execFeatures MX.x86_64_linux_info archVals binariesInfo mmPreset extract dfi
TTH.assertEqual "AssertionResult" expected simRes

MS.withArchConstraints archVals $ do
halloc <- CFH.newHandleAllocator
let ?recordLLVMAnnotation = \_ _ _ -> return ()

MST.InitialMem initMem mmConf <-
case mmPreset of
MST.DefaultMemModel -> MST.initialMem binariesInfo bak MX.x86_64_linux_info archVals
MST.LazyMemModel -> MST.lazyInitialMem binariesInfo bak MX.x86_64_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) <- SysV.allocStack bak initMem initRegs stackSize
retAddr <- SysV.freshRetAddr sym
let spilled = SysV.SpilledArgs Seq.Empty
(regs', mem') <- SysV.pushStackFrame bak mem regs spilled retAddr
let crucRegTypes = MS.crucArchRegTypes symArchFns
let regsEntry = CS.RegEntry (CT.StructRepr crucRegTypes) regs'

let iMem = MST.InitialMem mem' mmConf
(memVar, execResult) <-
MST.simDiscoveredFunction bak execFeatures archVals halloc iMem regsEntry binariesInfo 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
Expand Down

0 comments on commit b39ef9b

Please sign in to comment.