The goal is to support a jumptable testcase that is not supported by
the current jump bounds check. The jump bounds check needs to be
augmented so that it understands equality relationships between stack
values and registers, and bounds on both.
This patch tracks when a register points to a concrete stack offset.
As part of this, we droped the AbsDomain instance for AbsBlockState.
Clients should now likely use `fnStartAbsBlockState` in lieu of `top`.
The other client visible change is that the ClassifyFailure
constructor now has an extra argument with details about why
classification failure occured.
This introduces a new datatype CValue for representing constants
in Macaw programs, modifies the existing Value datatype to use then,
and introduces patterns for compatibility with existing datatypes.
The patch also updates the function argument analysis to use more
explicit argument passing rather than monadic updates. The intent is
to help clarify when data is initialized rather than updated.
Finally this updates a README and does some minor updates.
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.
`MonadFail` being a forward-compatibility measure, overriding
`Control.Monad.Fail.fail` in GHC versions <= 8.6 doesn't do anything
unless `Control.Monad.Fail.fail` is invoked explicitly (or the importing
module happens to have `-XMonadFailDesugaring` on).
These `getCallTarget` and `doJump` were calling `fail` if they saw an argument
type that we hadn't thought to handle yet. This change turns those errors into
TranslationError statements, allowing macaw to continue exploring code.
This came up recently in a glibc-based example where macaw ended up exploring
unaligned code and creating a strange jump to a far pointer, which doesn't make
much sense in x86_64 mode.
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.
