This patch focuses on function argument analysis, but includes some
other cleanups.
The main changes are to add additional comments and cleanups to the
function argument analysis code. This also extends the analysis so
that we can annotate the types of some of the functions and use those
types during analysis.
As part of this we tighten the PLTStub checking, and clean up the
elfloader in some minor ways.
WidthEqProofs are now irrelevant. Two proofs with the same
coercision source and destination will be equal. This allows us to
add a transitivity constructor without introducing spurious
inequalities, and will in the future allow us to collapse multiple
bitcasts into a single bitcast.
adjustedLoadRegionIndex is exported for reopt.
TypeRepr now has a pretty instance.
This primarily refines the abstract state propagated to branch
pairs. It was needed on the ARM platform to support the IT blocks
with the changes to the Core representation in macaw-base 0.3.6.
This also includes a few simplifications added and comment
improvements.
The caller (e.g. macaw-refinement) can provide an additional Rewriter
operation that can operate on TermStmts for blocks (typically those
for which a previous Discovery was unable to determine a transfer
target). There is an additional
entrypoint ('addDiscoveredFunctionBlockTargets') that will allow this
additional rewriter to be supplied for updating an existing
DiscoveryState.
Some of the TermStmt and other elements might generate new blocks as
part of the Rewrite operation (e.g. adding a new 'Branch' TermStmt) so
this change allows the rewrite context to update the generated block
labels and collect these newly generated blocks for inclusing in the
results passed to the parser.
Before, we just discarded them during the translation. They are useful metadata
for generating diagnostics in Crucible, so this commit translates them. They
are no-ops during symbolic evaluation.
To make them truly useful, they need to include the address of the block that
they belong to (their data payload in macaw is just an offset from the start of
a block). This information wasn't available before, so it has to be plumbed
through in macaw-x86.
