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
Prev Previous commit
Next Next commit
symbolic: Factor out fresh register assignment generator
langston-barrett committed Sep 4, 2024
commit 820401d12e59e3bf166864823dd5ba9690f85cfb
14 changes: 13 additions & 1 deletion symbolic/src/Data/Macaw/Symbolic/Testing.hs
Original file line number Diff line number Diff line change
@@ -302,6 +302,18 @@ 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)

-- | Create a name for the given 'MD.DiscoveryFunInfo'
--
-- If the function has no name, just use its address
@@ -581,7 +593,7 @@ simulateFunction binfo bak execFeatures archInfo archVals halloc mmPreset g = do
-- 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)
initialRegs <- freshRegs symArchFns sym
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