* update to bv-sized branch of what4 and other things
* removed parameterized-utils submodule completely
* Updates submodules
* Fixes macaw-symbolic w.r.t. crucible-llvm changes
Co-authored-by: Ben Selfridge <ben@000548-benselfridge.local>
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.
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.
