mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-02 10:54:04 +03:00
e024646860
This commit updates macaw-refinement to work with the latest macaw/crucible and makes a few improvements along the way. The major changes involved in this are: * Block labels were removed from macaw, so we had to come up with an alternative approach to making synthetic blocks to represent dispatch resolved by macaw-refinement that is not really a jump table. We considered adding a new terminator that encoded "computed IP-based dispatch", but there was concern about the impact on client code. Instead, we added a field to the `DiscoveryFunInfo` that records "external" resolutions to indirect control flow (e.g., as by an SMT solver in macaw-refinement). The hook by which we feed SMT-based resolutions back into macaw was modified accordingly (`addDiscoveredFunctionBlockTargets`). * Solver invocation changed to allow solver selection and parallel solver application. * Logging is now done via the `lumberjack` library. * macaw-symbolic now uses the "external" resolutions in `DiscoveryFunInfo` while building crucible CFGs. * The path creation code in macaw-refinement was simplified significantly and the approach to path creation has been documented. * The run-refinement tool is now more featureful. * The test suite is a bit more structured and no longer depends on the printed output of the discovery process.
18 lines
711 B
Org Mode
18 lines
711 B
Org Mode
The contents of this directory provide several "golden" tests: a
|
|
binary file along with a file containing the results of the base macaw
|
|
discovery and also a file containing the results of the refined
|
|
discovery are present for several architectural variants.
|
|
|
|
The test utility will perform both base discovery and discovery
|
|
refinement and compare the results obtained to the expected results
|
|
recorded in the files here to determine if both discovery and
|
|
refinement are operating as expected.
|
|
|
|
* Skipped Tests
|
|
|
|
- ~address-of-label1.ppc.gcc.pie.*.exe~
|
|
|
|
These are not tested because this test cannot be made PIE on PowerPC. The
|
|
address-of-label uses add relocations that aren't supported in static PIE
|
|
mode.
|