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. |
||
|---|---|---|
| .. | ||
| src/Data/Macaw | ||
| tests | ||
| tools | ||
| Changelog.md | ||
| LICENSE | ||
| macaw-refinement.cabal | ||
| README.md | ||
Macaw Refinement Libary
The refinement library provides supplemental functionality for discovery of elements that macaw-symbolic is not able to discover via pattern matching. This library will use crucible symbolic analysis to attempt to determine elements that could not be identified by macaw-symbolic. The identification provided by macaw-symbolic is incomplete, and so is the identification by this macaw-refinement, but macaw-refinement attempts to additionally "refine" the analysis to achieve even more information which can then be provided back to the macaw analysis.
-
Terminator effects for incomplete blocks. For example, the target IP address by symbolic evaluation (e.g. of jump tables). If the current block does not provide sufficient information to symbolically identify the target, previous blocks can be added to the analysis (back to the entry block or a loop point).
-
Argument liveness (determining which registers and memory locations are used/live by a block allows determination of ABI compliance (for transformations) and specific block requirements (which currently start with a full register state and blank memory).
-
Call graphs. Determination of targets of call instructions that cannot be identified by pattern matching via symbolic evaluation, using techniques similar to those for identifying incomplete blocks.