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.
The use of `Data.Parameterized.Map.fromList` in `mkRegStateM` was
showing up in profiling as a huge time sink. We don't actually need to
build the map from scratch there, though, since the keys are known ahead
of time. Adding an `archRegSet` variable to the `RegisterInfo` class
(with the obvious default implementation) ensures that a `MapF` with the
right keys will be built once and then reused.
This mostly affects x86. Previously, we threw away the write of the return
address to the stack when identifying calls for macaw-x86. This was partly for
hygiene and partly to support the "addresses written to memory are function
pointers" heuristic. Treating the return address as a potential function
pointer breaks function identification, so that is important.
The problem comes in the translation of macaw into crucible - we never write the
return address to the stack, but returns still read the return address from the
stack. If it wasn't written in the first place, this leads to a read
from (potentially) uninitialized memory, which causes errors in the symbolic
simulator. There are two solutions:
1. Make returns not read from the stack
2. Keep the write of the return address to the stack
Solution 1 is a problem, as we have a data dependency on the read. Eliding it
breaks Crucible generation later and produces an invalid CFG.
Solution 2 works well. The implementation is actually simple. We can keep
identifyCall the same for x86 and just construct the basic block not from the
return value but from the original list of statements (unaltered). We do need
to have identifyCall still give us the reduced statement list, which we use for
identifying possible function pointers written onto the stack (but not the
return address, which we do not want to treat as a function pointer).
