GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-29 11:02:13 +03:00
Code Issues Projects Releases Wiki Activity
caef1d30c1
macaw/symbolic
History
Langston Barrett caef1d30c1 symbolic: Factor stack setup out of Testing into its own module 
Several Macaw-based projects use a similar stack setup:

* `pate`: c43542818b/src/Pate/Verification/InlineCallee.hs (L135-L143)
* `ambient-verifier`: https://github.com/GaloisInc/ambient-verifier/blob/open-source/src/Ambient/Verifier/SymbolicExecution.hs#L1272-L1280

We can share code by factoring it into its own module.
2024-09-03 15:35:08 -04:00
..
examples Add optional override for MacawArchStmtExtensions to genArchVals (#230) 2021-09-14 18:24:47 -07:00
src/Data/Macaw symbolic: Factor stack setup out of Testing into its own module 2024-09-03 15:35:08 -04:00
test This commit re-implements the memory model used by macaw symbolic 2020-02-11 09:58:53 -08:00
ChangeLog.md macaw-symbolic: Note lazy memory model in the changelog 2023-03-14 13:27:07 -04:00
LICENSE Update license information. 2017-09-27 15:59:06 -07:00
macaw-symbolic.cabal symbolic: Factor stack setup out of Testing into its own module 2024-09-03 15:35:08 -04:00
README.org Clean up and document the macaw-symbolic API 2019-01-10 18:20:54 -08:00

README.org

Overview

The macaw-symbolic library provides a mechanism for translating machine code functions discovered by macaw into Crucible CFGs that can then be symbolically simulated.

The core macaw-symbolic library supports translating generic macaw into crucible, but is not a standalone library. To translate actual machine code, an architecture-specific backend is required. For example, macaw-x86-symbolic can be used to translate x86_64 binaries into crucible. Examples for using macaw-symbolic (and architecture-specific backends) are available in Data.Macaw.Symbolic.

In order to avoid API bloat, the definitions required to implement a new architecture-specific backend are exported through the Data.Macaw.Symbolic.Backend module.

An additional module, Data.Macaw.Symbolic.Memory, provides an example of how to handle memory address translation in the simulator for machine code programs. There are other possible ways to translate memory addresses, but this module provides a versatile example that can serve many common use cases.