The new registerUse analysis uses a three phase process:
Phase 1 computes invariants about the start state of each block. It
will indicate when registers/stack locations store stack offsets, and
where callee saved registers are stashed. It also memoizes
information about stack reads and writes to simplify later passes.
Phase 2 is a demand analysis that computes which registers and stack
locations must be available to execute the program. It then
propagates those constraints across blocks in the function.
Phase 3 combines the information into a form relevant for function
recovery.
The only real code change required is that simulation failure messages have an
extra argument. The goal with this update is to pull in some fixes to the
solver feature detection for yices in the latest crucible.
This version constructs a Crucible CFG for a collection of blocks while
preserving control flow between them. It allows the caller to specify blocks
that are considered "terminal": those blocks return the current register state.
Control flow to blocks no included in the "slice" are directed to synthetic
blocks that assume False in order to stop the symbolic simulator from exploring
those branches.
The improved string support in Crucible adds a parameter to string reprs; this
change accommodates that. Earlier changes added the necessary support in the
rest of macaw.
This was an artifact of merging macaw-semmc into macaw. This commit unifies the
two directories. There are some remaining submodules in the old directory:
these are obsolete and will be removed in a separate commit.
The main changes are:
- `postCallAbsState` was removed from the architecture info
- `mkInitialRegsForBlock` was renamed to `initialBlockRegs` and takes slightly
different parameters
- There is a new type family and some new functions in the architecture info
relating to post-block/terminator abstract state construction
PowerPC doesn't need any extra information to compute post-block abstract
states, so we use () as the ArchBlockPrecond type.
