diff --git a/macaw-aarch32-symbolic/tests/Main.hs b/macaw-aarch32-symbolic/tests/Main.hs index 9abe7ecc..ca86be36 100644 --- a/macaw-aarch32-symbolic/tests/Main.hs +++ b/macaw-aarch32-symbolic/tests/Main.hs @@ -106,7 +106,7 @@ armResultExtractor :: ( CB.IsSymInterface sym ) => MS.ArchVals MA.ARM -> MST.ResultExtractor sym MA.ARM -armResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do +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) diff --git a/macaw-aarch32-symbolic/tests/README.org b/macaw-aarch32-symbolic/tests/README.org index e9312e6c..7e90f490 100644 --- a/macaw-aarch32-symbolic/tests/README.org +++ b/macaw-aarch32-symbolic/tests/README.org @@ -1,7 +1,7 @@ * Overview This test suite tests that symbolic execution of AArch32 programs works. It is also a convenient place to test the semantics. The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories. In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states. It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion). Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected). The test harness uses yices for path satisfiability checking and z3 to prove goals. Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate. -In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). +In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). * Usage diff --git a/macaw-ppc-symbolic/tests/Main.hs b/macaw-ppc-symbolic/tests/Main.hs index 4142b6d1..27f6f85c 100644 --- a/macaw-ppc-symbolic/tests/Main.hs +++ b/macaw-ppc-symbolic/tests/Main.hs @@ -118,7 +118,7 @@ ppcResultExtractor :: ( arch ~ MP.AnyPPC v ) => MS.ArchVals arch -> MST.ResultExtractor sym arch -ppcResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do +ppcResultExtractor archVals = MST.ResultExtractor $ \regs _mem k -> do let re = MS.lookupReg archVals regs (MP.PPC_GP (DP.GPR 3)) k PC.knownRepr (CS.regValue re) diff --git a/macaw-ppc-symbolic/tests/README.org b/macaw-ppc-symbolic/tests/README.org index 5ba19d3e..a8ec97dd 100644 --- a/macaw-ppc-symbolic/tests/README.org +++ b/macaw-ppc-symbolic/tests/README.org @@ -1,7 +1,7 @@ * Overview This test suite tests that symbolic execution of PowerPC programs works. It is also a convenient place to test the semantics. The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories. In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states. It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion). Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected). The test harness uses yices for path satisfiability checking and z3 to prove goals. Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate. -In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). +In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). * Usage diff --git a/macaw-riscv-symbolic/tests/Main.hs b/macaw-riscv-symbolic/tests/Main.hs index cb62f6cc..0034d97a 100644 --- a/macaw-riscv-symbolic/tests/Main.hs +++ b/macaw-riscv-symbolic/tests/Main.hs @@ -109,7 +109,7 @@ riscvResultExtractor :: ( arch ~ MR.RISCV rv ) => MS.ArchVals arch -> MST.ResultExtractor sym arch -riscvResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do +riscvResultExtractor archVals = MST.ResultExtractor $ \regs _mem k -> do let re = MS.lookupReg archVals regs MR.GPR_A0 k PC.knownRepr (CS.regValue re) diff --git a/macaw-riscv-symbolic/tests/README.org b/macaw-riscv-symbolic/tests/README.org index 836a5a7b..b74329ac 100644 --- a/macaw-riscv-symbolic/tests/README.org +++ b/macaw-riscv-symbolic/tests/README.org @@ -1,7 +1,7 @@ * Overview This test suite tests that symbolic execution of RISC-V programs works. It is also a convenient place to test the semantics. The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories. In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states. It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion). Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected). The test harness uses yices for path satisfiability checking and z3 to prove goals. Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate. -In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). +In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). * Usage diff --git a/symbolic/src/Data/Macaw/Symbolic/Testing.hs b/symbolic/src/Data/Macaw/Symbolic/Testing.hs index 077c8cca..3f33ffc5 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Testing.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Testing.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} @@ -8,9 +7,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} + -- | This module defines common test harness code that can be used in each of the -- architecture-specific backends. -- @@ -31,6 +29,12 @@ module Data.Macaw.Symbolic.Testing ( MemModelPreset(..), describeMemModelPreset, toAddrSymMap, + freshRegs, + InitialMem(..), + initialMem, + lazyInitialMem, + simDiscoveredFunction, + summarizeExecution, -- * Execution features SomeBackend(..), defaultExecFeatures, @@ -44,7 +48,6 @@ module Data.Macaw.Symbolic.Testing ( import qualified Control.Exception as X import qualified Control.Lens as L import Control.Lens ( (&), (%~) ) -import Control.Monad ( when ) import Control.Monad.Except ( runExceptT ) import qualified Data.Bits as Bits import qualified Data.BitVector.Sized as BVS @@ -70,7 +73,6 @@ import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.List as PL import qualified Data.Parameterized.NatRepr as PN import Data.Parameterized.Some ( Some(..) ) -import Data.Proxy ( Proxy(..) ) import qualified Data.Text as Text import qualified Data.Text.Encoding as Text import qualified Data.Text.Encoding.Error as Text @@ -305,6 +307,63 @@ mkInitialRegVal archFns sym r = do MT.FloatTypeRepr {} -> error ("Float-typed registers are not supported in the macaw-symbolic test harness: " ++ show regName) MT.VecTypeRepr {} -> error ("Vector-typed registers are not supported in the macaw-symbolic test harness: " ++ show regName) + +freshRegs :: + CB.IsSymInterface sym => + MT.HasRepr (MC.ArchReg arch) MT.TypeRepr => + MS.MacawSymbolicArchFunctions arch -> + sym -> + IO (Ctx.Assignment (CS.RegValue' sym) (MS.CtxToCrucibleType (MS.ArchRegContext arch))) +freshRegs symArchFns sym = + MS.macawAssignToCrucM + (mkInitialRegVal symArchFns sym) + (MS.crucGenRegAssignment symArchFns) + +-- | Make initial registers, including setting up a stack pointer. +-- +-- The stack pointer points to the middle of the stack allocation. This is a +-- hack. We do this because each architecture has some expected stack layout +-- (e.g., x86_64 expects a return address just above the stack pointer; +-- PPC expects a "back chain"; and AArch32, PPC, and x86_64 all expect +-- stack-spilled arguments above everything else). Setting the stack pointer +-- to the middle of the allocation allows reads of fully symbolic data from +-- above the stack pointer, and this seems to be good enough to make our tests +-- pass. +-- +-- The functions in the test-suite do not (and should not) rely on accessing +-- data in their caller's stack frames, even though that wouldn't cause test +-- failures with this setup. +defaultRegs :: + CB.IsSymBackend sym bak => + CLM.HasPtrWidth (MC.ArchAddrWidth arch) => + (?memOpts :: CLM.MemOptions) => + MS.SymArchConstraints arch => + CLM.HasLLVMAnn sym => + MT.HasRepr (MC.ArchReg arch) MT.TypeRepr => + bak -> + MS.ArchVals arch -> + CLM.MemImpl sym -> + IO (CS.RegEntry sym (MS.ArchRegStruct arch), CLM.MemImpl sym) +defaultRegs bak archVals mem = do + let sym = CB.backendGetSym bak + + let kib = 1024 + let mib = 1024 * kib + stackSize <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth (2 * mib)) + (MSS.ArrayStack stackBasePtr _stackTopPtr _stackArrayStorage, mem') <- + MSS.createArrayStack bak mem (MSS.ExtraStackSlots 0) stackSize + stackInitialOffset <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth mib) + sp <- CLM.ptrAdd sym ?ptrWidth stackBasePtr stackInitialOffset + + let symArchFns = MS.archFunctions archVals + initialRegs <- freshRegs symArchFns sym + + let crucRegTypes = MS.crucArchRegTypes symArchFns + let regsRepr = CT.StructRepr crucRegTypes + let initialRegsEntry = CS.RegEntry regsRepr initialRegs + let regs = MS.updateReg archVals initialRegsEntry MC.sp_reg sp + pure (regs, mem') + -- | Create a name for the given 'MD.DiscoveryFunInfo' -- -- If the function has no name, just use its address @@ -361,11 +420,7 @@ proveGoals bak goalSolver = do -- architecture-specific primitives). -- -- In addition to symbolically executing the function to produce a Sat/Unsat --- result, this function will attempt to verify all generate side conditions if --- the name of the function being simulated begins with @test_and_verify_@ (as --- opposed to just @test@). This is necessary for testing aspects of the --- semantics that involve the generated side conditions, rather than just the --- final result. +-- result, this function will attempt to verify all generated side conditions. simulateAndVerify :: forall arch sym bak ids w solver scope st fs . ( CB.IsSymBackend sym bak , CCE.IsSyntaxExtension (MS.MacawExt arch) @@ -401,46 +456,152 @@ simulateAndVerify :: forall arch sym bak ids w solver scope st fs -> MD.DiscoveryFunInfo arch ids -- ^ The function to simulate and verify -> IO SimulationResult -simulateAndVerify goalSolver logger bak execFeatures archInfo archVals binfo mmPreset (ResultExtractor withResult) dfi = - let sym = CB.backendGetSym bak in +simulateAndVerify goalSolver logger bak execFeatures archInfo archVals binfo mmPreset extractor dfi = MS.withArchConstraints archVals $ do - let funName = functionName dfi - let mainInfo = mainBinaryInfo binfo halloc <- CFH.newHandleAllocator - CCC.SomeCFG g <- - MS.mkFunCFG (MS.archFunctions archVals) halloc funName (posFn (binaryPath mainInfo)) dfi - let ?recordLLVMAnnotation = \_ _ _ -> return () - (memVar, stackPointer, execResult) <- - simulateFunction binfo bak execFeatures archInfo archVals halloc mmPreset g - case execResult of - CS.TimeoutResult {} -> return SimulationTimeout - CS.AbortedResult {} -> return SimulationAborted - CS.FinishedResult _simCtx partialRes -> - case partialRes of - CS.PartialRes {} -> return SimulationPartial - CS.TotalRes gp -> do - when ("test_and_verify_" `Text.isPrefixOf` WF.functionName funName) $ - proveGoals bak goalSolver - - postMem <- case CSG.lookupGlobal memVar (gp L.^. CS.gpGlobals) of - Just postMem -> pure postMem - Nothing -> error $ "simulateAndVerify: Could not find global variable: " - ++ Text.unpack (CS.globalName memVar) - withResult (gp L.^. CS.gpValue) stackPointer postMem $ \resRepr val -> do - -- The function is assumed to return a value that is intended to be - -- True. Try to prove that (by checking the negation for unsat) - -- - -- The result is treated as true if it is not equal to zero - zero <- WI.bvLit sym resRepr (BVS.mkBV resRepr 0) - bv_val <- CLM.projectLLVM_bv bak val - notZero <- WI.bvNe sym bv_val zero - goal <- WI.notPred sym notZero - WS.solver_adapter_check_sat goalSolver sym logger [goal] $ \satRes -> - case satRes of - WSR.Sat {} -> return (SimulationResult Sat) - WSR.Unsat {} -> return (SimulationResult Unsat) - WSR.Unknown -> return (SimulationResult Unknown) + + -- Initialize memory + -- + -- This includes both global static memory (taken from the data segment + -- initial contents) and a totally symbolic stack + iMem <- + case mmPreset of + DefaultMemModel -> initialMem binfo bak archInfo archVals + LazyMemModel -> lazyInitialMem binfo bak archInfo archVals + + (memVar, execResult) <- + simulateFunction bak execFeatures archVals halloc iMem binfo dfi + + summarizeExecution goalSolver logger bak memVar extractor execResult + +-- | Post-process the results of symbolic execution +-- +-- In particular, turn a 'CS.ExecResult' into a 'SimulationResult'. If +-- simulation succeeded, uses the 'ResultExtractor' to assert that the executed +-- function returned a nonzero value. +summarizeExecution :: + ( CB.IsSymBackend sym bak + , CCE.IsSyntaxExtension (MS.MacawExt arch) + , MM.MemWidth (MC.ArchAddrWidth arch) + , w ~ MC.ArchAddrWidth arch + , 16 <= w + , MT.KnownNat w + , sym ~ WE.ExprBuilder scope st fs + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + ) => + -- | The solver adapter to use to discharge assertions + WS.SolverAdapter st -> + -- | A logger to (optionally) record solver interaction (for the goal solver) + WS.LogData -> + bak -> + CS.GlobalVar CLM.Mem -> + -- | A function to extract the return value of a function from its post-state + ResultExtractor sym arch -> + CS.ExecResult (MS.MacawLazySimulatorState sym w) sym ext (CS.RegEntry sym (MS.ArchRegStruct arch)) -> + IO SimulationResult +summarizeExecution goalSolver logger bak memVar (ResultExtractor withResult) = + \case + CS.TimeoutResult {} -> return SimulationTimeout + CS.AbortedResult {} -> return SimulationAborted + CS.FinishedResult _simCtx partialRes -> + case partialRes of + CS.PartialRes {} -> return SimulationPartial + CS.TotalRes gp -> do + proveGoals bak goalSolver + + postMem <- case CSG.lookupGlobal memVar (gp L.^. CS.gpGlobals) of + Just postMem -> pure postMem + Nothing -> error $ "simulateAndVerify: Could not find global variable: " + ++ Text.unpack (CS.globalName memVar) + withResult (gp L.^. CS.gpValue) postMem $ \resRepr val -> do + let sym = CB.backendGetSym bak + -- The function is assumed to return a value that is intended to be + -- True. Try to prove that (by checking the negation for unsat) + -- + -- The result is treated as true if it is not equal to zero + zero <- WI.bvLit sym resRepr (BVS.mkBV resRepr 0) + bv_val <- CLM.projectLLVM_bv bak val + notZero <- WI.bvNe sym bv_val zero + goal <- WI.notPred sym notZero + WS.solver_adapter_check_sat goalSolver sym logger [goal] $ + \case + WSR.Sat {} -> return (SimulationResult Sat) + WSR.Unsat {} -> return (SimulationResult Unsat) + WSR.Unknown -> return (SimulationResult Unknown) + +initialMem :: + ( ext ~ MS.MacawExt arch + , CCE.IsSyntaxExtension ext + , CB.IsSymBackend sym bak + , CLM.HasLLVMAnn sym + , MS.SymArchConstraints arch + , w ~ MC.ArchAddrWidth arch + , 16 <= w + , sym ~ WE.ExprBuilder scope st fs + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + , ?memOpts :: CLM.MemOptions + ) => + BinariesInfo arch -> + bak -> + MAI.ArchitectureInfo arch -> + MS.ArchVals arch -> + IO (InitialMem p sym arch) +initialMem binfo bak archInfo archVals = do + let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo) + (mem, memPtrTbl) <- + MSM.newMergedGlobalMemoryWith populateRelocation archInfo bak + endianness MSM.ConcreteMutable (binariesMems binfo) + let mmConf = (MSM.memModelConfig bak memPtrTbl) + { MS.lookupFunctionHandle = lookupFunction archVals binfo + , MS.lookupSyscallHandle = lookupSyscall + , MS.mkGlobalPointerValidityAssertion = validityCheck + } + pure (InitialMem mem mmConf) + +lazyInitialMem :: + ( ext ~ MS.MacawExt arch + , CCE.IsSyntaxExtension ext + , CB.IsSymBackend sym bak + , CLM.HasLLVMAnn sym + , MS.SymArchConstraints arch + , w ~ MC.ArchAddrWidth arch + , 16 <= w + , sym ~ WE.ExprBuilder scope st fs + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + , ?memOpts :: CLM.MemOptions + , MS.HasMacawLazySimulatorState p sym w + ) => + BinariesInfo arch -> + bak -> + MAI.ArchitectureInfo arch -> + MS.ArchVals arch -> + IO (InitialMem p sym arch) +lazyInitialMem binfo bak archInfo archVals = do + let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo) + (mem, memPtrTbl) <- + MSMLazy.newMergedGlobalMemoryWith populateRelocation archInfo bak + endianness MSMLazy.ConcreteMutable (binariesMems binfo) + let mmConf = (MSMLazy.memModelConfig bak memPtrTbl) + { MS.lookupFunctionHandle = lookupFunction archVals binfo + , MS.lookupSyscallHandle = lookupSyscall + , MS.mkGlobalPointerValidityAssertion = validityCheck + } + pure (InitialMem mem mmConf) + +-- | Initial program memory and memory configuration +-- +-- Returned by 'initialMem' and 'lazyInitialMem'. +data InitialMem p sym arch + = InitialMem + { -- | Initial contents of memory, before symbolic execution + initMemMem :: CLM.MemImpl sym + -- | Memory model configuration + , initMemMmConf :: MS.MemModelConfig p sym arch CLM.Mem + } -- | Set up the symbolic execution engine with initial states and execute -- @@ -449,15 +610,13 @@ simulateAndVerify goalSolver logger bak execFeatures archInfo archVals binfo mmP -- 1. The global variable that holds the memory state (allowing for -- inspecting the post-state, which is extracted from the 'CS.ExecResult') -- --- 2. The stack pointer for the function --- --- 3. The result of symbolic execution +-- 2. The result of symbolic execution -- -- Note that the provided 'CLM.MemImpl' is expected to have its global state -- populated as desired. The default loader populates it with concrete (and -- mutable) values taken from the data segment of the binary (as well as the -- immutable contents of the text segment). -simulateFunction :: forall arch sym bak w solver scope st fs ext blocks +simulateFunction :: forall arch sym bak w ext ids . ( ext ~ MS.MacawExt arch , CCE.IsSyntaxExtension ext , CB.IsSymBackend sym bak @@ -465,105 +624,86 @@ simulateFunction :: forall arch sym bak w solver scope st fs ext blocks , MS.SymArchConstraints arch , w ~ MC.ArchAddrWidth arch , 16 <= w - , sym ~ WE.ExprBuilder scope st fs - , bak ~ CBO.OnlineBackend solver scope st fs - , WPO.OnlineSolver solver , ?memOpts :: CLM.MemOptions ) - => BinariesInfo arch - -> bak + => bak -> [CS.GenericExecutionFeature sym] - -> MAI.ArchitectureInfo arch -> MS.ArchVals arch -> CFH.HandleAllocator - -> MemModelPreset - -> CCC.CFG ext blocks (Ctx.EmptyCtx Ctx.::> MS.ArchRegStruct arch) (MS.ArchRegStruct arch) + -> InitialMem (MS.MacawLazySimulatorState sym w) sym arch + -> BinariesInfo arch + -> MD.DiscoveryFunInfo arch ids -> IO ( CS.GlobalVar CLM.Mem - , CLM.LLVMPtr sym w , CS.ExecResult (MS.MacawLazySimulatorState sym w) sym ext (CS.RegEntry sym (MS.ArchRegStruct arch)) ) -simulateFunction binfo bak execFeatures archInfo archVals halloc mmPreset g = do - let sym = CB.backendGetSym bak - let symArchFns = MS.archFunctions archVals - let crucRegTypes = MS.crucArchRegTypes symArchFns - let regsRepr = CT.StructRepr crucRegTypes - let mainInfo = mainBinaryInfo binfo - let soInfos = sharedLibraryInfos binfo - let endianness = MSMLazy.toCrucibleEndian (MAI.archEndianness archInfo) - let mems = V.map (MD.memory . binaryDiscState) (V.cons mainInfo soInfos) - - -- Initialize memory - -- - -- This includes both global static memory (taken from the data segment - -- initial contents) and a totally symbolic stack - +simulateFunction bak execFeatures archVals halloc iMem binfo dfi = do let ?ptrWidth = WI.knownRepr - (initMem, mmConf) <- - case mmPreset of - DefaultMemModel -> do - (initMem, memPtrTbl) <- - MSM.newMergedGlobalMemoryWith populateRelocation (Proxy @arch) bak - endianness MSM.ConcreteMutable mems - let mmConf = (MSM.memModelConfig bak memPtrTbl) - { MS.lookupFunctionHandle = lookupFunction archVals binfo - , MS.lookupSyscallHandle = lookupSyscall - , MS.mkGlobalPointerValidityAssertion = validityCheck - } - pure (initMem, mmConf) - LazyMemModel -> do - (initMem, memPtrTbl) <- - MSMLazy.newMergedGlobalMemoryWith populateRelocation (Proxy @arch) bak - endianness MSMLazy.ConcreteMutable mems - let mmConf = (MSMLazy.memModelConfig bak memPtrTbl) - { MS.lookupFunctionHandle = lookupFunction archVals binfo - , MS.lookupSyscallHandle = lookupSyscall - , MS.mkGlobalPointerValidityAssertion = validityCheck - } - pure (initMem, mmConf) - - -- Allocate a stack and insert it into memory - -- - -- The stack allocation uses the SMT array backed memory model (rather than - -- the Haskell-level memory model) - let kib = 1024 - let mib = 1024 * kib - stackSize <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr (2 * mib)) - (MSS.ArrayStack stackBasePtr _stackTopPtr _stackArrayStorage, mem1) <- - MSS.createArrayStack bak initMem (MSS.ExtraStackSlots 0) stackSize - - -- Make initial registers, including setting up a stack pointer. - -- - -- The stack pointer points to the middle of the stack allocation. This is a - -- hack. We do this because each architecture has some expected stack layout - -- (e.g., x86_64 expects a return address just above the stack pointer; - -- PPC expects a "back chain"; and AArch32, PPC, and x86_64 all expect - -- stack-spilled arguments above everything else). Setting the stack pointer - -- to the middle of the allocation allows reads of fully symbolic data from - -- above the stack pointer, and this seems to be good enough to make our tests - -- pass. - -- - -- The functions in the test-suite do not (and should not) rely on accessing - -- data in their caller's stack frames, even though that wouldn't cause test - -- failures with this setup. - initialRegs <- MS.macawAssignToCrucM (mkInitialRegVal symArchFns sym) (MS.crucGenRegAssignment symArchFns) - stackInitialOffset <- WI.bvLit sym WI.knownRepr (BVS.mkBV WI.knownRepr mib) - sp <- CLM.ptrAdd sym WI.knownRepr stackBasePtr stackInitialOffset - let initialRegsEntry = CS.RegEntry regsRepr initialRegs - let regsWithStack = MS.updateReg archVals initialRegsEntry MC.sp_reg sp - + let InitialMem initMem mmConf = iMem + (regs, mem) <- defaultRegs bak archVals initMem + let iMem' = InitialMem mem mmConf + simDiscoveredFunction bak execFeatures archVals halloc iMem' regs binfo dfi + +-- | Simulate a discovered Macaw function, given initial registers and memory +simDiscoveredFunction :: + ( ext ~ MS.MacawExt arch + , CCE.IsSyntaxExtension ext + , CB.IsSymBackend sym bak + , CLM.HasLLVMAnn sym + , MS.SymArchConstraints arch + , ?memOpts :: CLM.MemOptions + ) => + bak -> + [CS.GenericExecutionFeature sym] -> + MS.ArchVals arch -> + CFH.HandleAllocator -> + InitialMem (MS.MacawLazySimulatorState sym w) sym arch -> + CS.RegEntry sym (MS.ArchRegStruct arch) -> + BinariesInfo arch -> + MD.DiscoveryFunInfo arch ids -> + -- ^ The function to simulate + IO ( CS.GlobalVar CLM.Mem + , CS.ExecResult (MS.MacawLazySimulatorState sym w) sym ext (CS.RegEntry sym (MS.ArchRegStruct arch)) + ) +simDiscoveredFunction bak execFeatures archVals halloc iMem regs binfo dfi = do + let sym = CB.backendGetSym bak + let InitialMem mem mmConf = iMem memVar <- CLM.mkMemVar "macaw-symbolic:test-harness:llvm_memory" halloc - let lazySimSt = MS.emptyMacawLazySimulatorState - let initGlobals = CSG.insertGlobal memVar mem1 CS.emptyGlobals - let arguments = CS.RegMap (Ctx.singleton regsWithStack) - let simAction = CS.runOverrideSim regsRepr (CS.regValue <$> CS.callCFG g arguments) + extImpl <- + MS.withArchEval archVals sym $ \archEvalFn -> + pure (MS.macawExtensions archEvalFn memVar mmConf) + let funName = functionName dfi + let mainInfo = mainBinaryInfo binfo + let pos = posFn (binaryPath mainInfo) + CCC.SomeCFG g <- + MS.mkFunCFG (MS.archFunctions archVals) halloc funName pos dfi + let regMap = CS.RegMap (Ctx.singleton regs) + res <- simMacawCfg bak execFeatures halloc extImpl memVar mem regMap g + pure (memVar, res) + +-- | Simulate a Macaw CFG, given initial registers and memory +simMacawCfg :: + ( ext ~ MS.MacawExt arch + , CCE.IsSyntaxExtension ext + , CB.IsSymBackend sym bak + ) => + bak -> + [CS.GenericExecutionFeature sym] -> + CFH.HandleAllocator -> + CS.ExtensionImpl (MS.MacawLazySimulatorState sym w) sym (MS.MacawExt arch) -> + CS.GlobalVar CLM.Mem -> + CLM.MemImpl sym -> + CS.RegMap sym argTys -> + CCC.CFG ext blocks argTys retTy -> + IO (CS.ExecResult (MS.MacawLazySimulatorState sym w) sym ext (CS.RegEntry sym retTy)) +simMacawCfg bak execFeatures halloc extImpl memVar mem args g = do + let lazySimSt = MS.emptyMacawLazySimulatorState let fnBindings = CFH.insertHandleMap (CCC.cfgHandle g) (CS.UseCFG g (CAP.postdomInfo g)) CFH.emptyHandleMap - MS.withArchEval archVals sym $ \archEvalFn -> do - let extImpl = MS.macawExtensions archEvalFn memVar mmConf - let ctx = CS.initSimContext bak CLI.llvmIntrinsicTypes halloc IO.stdout (CS.FnBindings fnBindings) extImpl lazySimSt - let s0 = CS.InitialState ctx initGlobals CS.defaultAbortHandler regsRepr simAction - res <- CS.executeCrucible (fmap CS.genericToExecutionFeature execFeatures) s0 - return (memVar, sp, res) + let ctx = CS.initSimContext bak CLI.llvmIntrinsicTypes halloc IO.stdout (CS.FnBindings fnBindings) extImpl lazySimSt + let initGlobals = CSG.insertGlobal memVar mem CS.emptyGlobals + let simAction = CS.runOverrideSim (CCC.cfgReturnType g) (CS.regValue <$> CS.callCFG g args) + let s0 = CS.InitialState ctx initGlobals CS.defaultAbortHandler (CCC.cfgReturnType g) simAction + CS.executeCrucible (fmap CS.genericToExecutionFeature execFeatures) s0 -- | A wrapper around the symbolic backend that allows us to recover the online -- constraints when they are available @@ -592,10 +732,8 @@ defaultExecFeatures backend = -- | This type wraps up a function that takes the post-state of a symbolic -- execution and extracts the return value from executing that function -- --- The details are architecture specific. Some architectures return values via --- dedicated registers, while others return values on the stack. --- --- This function takes the final register state and the post-state of memory, +-- Which register stores the return value is architecture-specific. This +-- function takes the final register state and the post-state of memory, -- allowing arbitrary access. -- -- Note that the function that clients provide could return any arbitrary @@ -607,7 +745,6 @@ defaultExecFeatures backend = data ResultExtractor sym arch where ResultExtractor :: (forall a . CS.RegEntry sym (MS.ArchRegStruct arch) - -> CLM.LLVMPtr sym (MC.ArchAddrWidth arch) -> CLM.MemImpl sym -> (forall n . (1 <= n) => PN.NatRepr n -> CLM.LLVMPtr sym n -> IO a) -> IO a) @@ -822,6 +959,14 @@ data BinariesInfo arch = BinariesInfo -- revisited. } +binariesMems :: + BinariesInfo arch -> + V.Vector (MEL.Memory (MC.ArchAddrWidth arch)) +binariesMems binfo = + let mainInfo = mainBinaryInfo binfo in + let soInfos = sharedLibraryInfos binfo in + V.map (MD.memory . binaryDiscState) (V.cons mainInfo soInfos) + -- | Information about an individual binary. data BinaryInfo arch = BinaryInfo { binaryDiscState :: MD.DiscoveryState arch diff --git a/x86_symbolic/macaw-x86-symbolic.cabal b/x86_symbolic/macaw-x86-symbolic.cabal index 91b0b5a8..89397ce6 100644 --- a/x86_symbolic/macaw-x86-symbolic.cabal +++ b/x86_symbolic/macaw-x86-symbolic.cabal @@ -9,6 +9,7 @@ license-file: LICENSE library build-depends: base >= 4.13, + containers, bv-sized >= 1.0.0, crucible >= 0.4, crucible-llvm, @@ -29,6 +30,7 @@ library exposed-modules: Data.Macaw.X86.Symbolic Data.Macaw.X86.Crucible + Data.Macaw.X86.Symbolic.ABI.SysV other-modules: Data.Macaw.X86.Symbolic.Panic @@ -44,6 +46,7 @@ test-suite macaw-x86-symbolic-tests hs-source-dirs: tests build-depends: base >= 4, + bv-sized, bytestring, containers, crucible, diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs new file mode 100644 index 00000000..65655054 --- /dev/null +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs @@ -0,0 +1,219 @@ +{-| +Copyright : (c) Galois, Inc 2024 +Maintainer : Langston Barrett + +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@), from high addresses +to low: + +* Their stack-spilled arguments +* The return address + +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: + +* +* + +TODO: The stack is supposed to be 16-byte aligned before a @call@. + +This module is meant to be imported qualified. +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} + +module Data.Macaw.X86.Symbolic.ABI.SysV + ( StackPointer + , getStackPointer + , stackPointerReg + , RetAddr(..) + , freshRetAddr + , SpilledArgs(..) + , writeSpilledArgs + , writeRetAddr + , allocStackFrame + , 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.Symbolic qualified as MS +import Data.Macaw.Symbolic.Stack qualified as MSS +import Data.Macaw.X86 qualified as X86 +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 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 +ptrBytes :: Integer +ptrBytes = 8 + +ptrRepr :: WI.NatRepr 64 +ptrRepr = WI.knownNat + +-- | A pointer to a SysV-compatible x86_64 stack +newtype StackPointer sym = StackPointer { getStackPointer :: MM.LLVMPtr sym 64 } + +-- | A lens for accessing the stack pointer register as a 'StackPointer' +stackPointerReg :: + Lens.Lens' + (Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes X86.X86_64)) + (StackPointer sym) +stackPointerReg = + Lens.lens + (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' X86S.rsp))) + (\regs v -> regs Lens.& ixF' X86S.rsp Lens..~ C.RV (getStackPointer v)) + +-- | A return address +newtype RetAddr sym = RetAddr { getRetAddr :: MM.LLVMPtr sym 64 } + +-- | Create a fresh, symbolic return address. +freshRetAddr :: C.IsSymInterface sym => sym -> IO (RetAddr sym) +freshRetAddr sym = do + bv <- WI.freshConstant sym (WI.safeSymbol "x86_64_ret_addr") (WI.BaseBVRepr ptrRepr) + ptr <- MM.llvmPointer_bv sym bv + pure (RetAddr ptr) + +-- | Stack-spilled arguments, in normal order +newtype SpilledArgs sym + = SpilledArgs { getSpilledArgs :: Seq.Seq (MM.LLVMPtr sym 64) } + +-- | 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. +-- +-- 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 + eight <- WI.bvLit sym ptrRepr (BVS.mkBV WI.knownNat 8) + let i64 = MM.bitvectorType (Bytes.toBytes (64 :: Int)) + let ?ptrWidth = ptrRepr + 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)) + +-- | Write the return address to the stack. +-- +-- Asserts that the stack allocation is writable and large enough to contain the +-- return address. +writeRetAddr :: + C.IsSymBackend sym bak => + (?memOpts :: MM.MemOptions) => + MM.HasLLVMAnn sym => + bak -> + MM.MemImpl sym -> + StackPointer sym -> + RetAddr sym -> + IO (StackPointer sym, MM.MemImpl sym) +writeRetAddr bak mem sp retAddr = do + let sym = C.backendGetSym bak + let ?ptrWidth = MM.ptrWidth (getRetAddr retAddr) + ptrSzBv <- WI.bvLit sym ?ptrWidth (BVS.mkBV ?ptrWidth ptrBytes) + top <- MM.ptrSub sym ?ptrWidth (getStackPointer sp) ptrSzBv + let i64 = MM.bitvectorType (Bytes.toBytes (8 :: Int)) + let val = MM.ptrToPtrVal (getRetAddr retAddr) + mem' <- MM.storeRaw bak mem top i64 CLD.noAlignment val + pure (StackPointer top, mem') + +-- | Allocate a single stack frame by decrementing the stack pointer. +-- +-- From high to low addresses: +-- +-- * First, write stack-spilled arguments in reverse order +-- * Then, write the return address +-- +-- Asserts that the stack allocation is writable and large enough to contain the +-- spilled arguments and return address. +allocStackFrame :: + C.IsSymBackend sym bak => + (?memOpts :: MM.MemOptions) => + MM.HasLLVMAnn sym => + bak -> + MM.MemImpl sym -> + StackPointer sym -> + SpilledArgs sym -> + RetAddr sym -> + IO (StackPointer sym, MM.MemImpl sym) +allocStackFrame bak mem sp spilledArgs retAddr = do + let ?ptrWidth = ptrRepr + (sp', mem') <- writeSpilledArgs bak mem sp spilledArgs + writeRetAddr bak mem' sp' retAddr + +-- | Like 'allocStackFrame', but manipulates @rsp@ 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 X86.X86_64) -> + SpilledArgs sym -> + RetAddr sym -> + IO + ( Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes X86.X86_64) + , MM.MemImpl sym + ) +pushStackFrame bak mem regs spilledArgs retAddr = do + let sp = regs Lens.^. stackPointerReg + (sp', mem') <- allocStackFrame bak mem sp spilledArgs retAddr + let regs' = regs Lens.& stackPointerReg Lens..~ sp' + pure (regs', mem') + +-- | Like 'MSS.createArrayStack', but puts the stack pointer in @rsp@ directly. +-- +-- Does not allow allocating stack slots, use 'allocStackFrame' or +-- '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 X86.X86_64) -> + -- | Size of stack allocation + WI.SymExpr sym (WI.BaseBVType 64) -> + IO + ( Ctx.Assignment (C.RegValue' sym) (MS.MacawCrucibleRegTypes X86.X86_64) + , 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/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs index a165b3f1..f92bcdb7 100644 --- a/x86_symbolic/tests/Main.hs +++ b/x86_symbolic/tests/Main.hs @@ -5,9 +5,11 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} 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 @@ -15,9 +17,11 @@ import qualified Data.Foldable as F import qualified Data.Map as Map import Data.Maybe ( mapMaybe ) import qualified Data.Parameterized.Classes as PC +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 @@ -34,20 +38,22 @@ 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.Expr.Builder as W4 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.CFG.Extension as CCE +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 -import qualified What4.Expr.Builder as W4 -import qualified Data.Parameterized.Context as Ctx - -- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes data SaveSMT = SaveSMT Bool deriving (Eq, Show) @@ -134,12 +140,52 @@ hasTestPrefix (Some dfi) = do -- Since all test functions must return a value to assert as true, this is -- straightforward to extract x86ResultExtractor :: (CB.IsSymInterface sym) => MS.ArchVals MX.X86_64 -> MST.ResultExtractor sym MX.X86_64 -x86ResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do +x86ResultExtractor archVals = MST.ResultExtractor $ \regs _mem k -> do let re = MS.lookupReg archVals regs MX.RAX k PC.knownRepr (CS.regValue re) data MacawX86SymbolicTest t = MacawX86SymbolicTest +setupRegsAndMem :: + ( ext ~ MS.MacawExt MX.X86_64 + , CCE.IsSyntaxExtension ext + , CB.IsSymBackend sym bak + , LLVM.HasLLVMAnn sym + , sym ~ W4.ExprBuilder scope st fs + , bak ~ CBO.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver + , ?memOpts :: LLVM.MemOptions + , MS.HasMacawLazySimulatorState p sym 64 + ) => + bak -> + MS.GenArchVals MS.LLVMMemory MX.X86_64 -> + MST.MemModelPreset -> + MST.BinariesInfo MX.X86_64 -> + IO ( CS.RegEntry sym (MS.ArchRegStruct MX.X86_64) + , MST.InitialMem p sym MX.X86_64 + ) +setupRegsAndMem bak archVals mmPreset binariesInfo = do + let sym = CB.backendGetSym bak + 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 + 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 @@ -171,8 +217,17 @@ 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 () + + (regs, iMem) <- setupRegsAndMem bak archVals mmPreset binariesInfo + (memVar, execResult) <- + MST.simDiscoveredFunction bak execFeatures archVals halloc iMem regs 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 diff --git a/x86_symbolic/tests/README.org b/x86_symbolic/tests/README.org index c8b73bf2..1d46a150 100644 --- a/x86_symbolic/tests/README.org +++ b/x86_symbolic/tests/README.org @@ -1,7 +1,7 @@ * Overview This test suite tests that symbolic execution of x86_64 programs works. It is also a convenient place to test the semantics. The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories. In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states. It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion). Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected). The test harness uses yices for path satisfiability checking and z3 to prove goals. Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate. -In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). +In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). * Usage