* 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.
Attempting to refine the switching test for PPC executables ends up
with a non-terminating Z3 process, so this test is disabled until this
is diagnosed.
For each discovered transfer refinement, the Discovery process must be
re-started from scratch for the particular target function in
question. The implication is that subsequent refinements for the same
nominal function must use the newer version, and that all previous
refinements must be re-applied each time the function Discovery
process is repeated.
These changes ensure that both of these occur during the refinement
iterations.
After the SMT evaluation has identified possible targets for a
previously unknown transfer TermStmt, the updateDiscovery will update
the DiscoveryState (using a locally-supplied TermStmt rewriter) to
resolve the transfer targets.
Currently smt solving just uses the first block of the first path,
which is not correct, but the framework for providing the list of
paths is now present.
The previous implementation invoked the SMT solver at the top level
for prototyping. This version moves the SMT solver invocation to the
intended location in the algorithm where the path is successively
extended and solutions are compared to identify the "best" refinement
solution.
