This commit reduces duplication in the PowerPC backend. Instances are now in terms of the generic `AnyPPC` type, rather than having separate instances for 32 and 64 bit. Shuffling some type parameters also allows us to remove a large number of type equalities that e.g., fix the arch register type to `PPCReg`.
The main changes are:
- `postCallAbsState` was removed from the architecture info
- `mkInitialRegsForBlock` was renamed to `initialBlockRegs` and takes slightly
different parameters
- There is a new type family and some new functions in the architecture info
relating to post-block/terminator abstract state construction
PowerPC doesn't need any extra information to compute post-block abstract
states, so we use () as the ArchBlockPrecond type.
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.
Update to API changes in macaw-base in macaw-ppc and macaw-arm
The "block label" abstraction (used during arch-specific disassembly) was removed some time ago in the base macaw library. This change updates macaw-ppc and macaw-arm to remove uses of block labels. The major change is that the disassembly function only returns a single block at a time instead of a sequence of blocks.
To facilitate this, the handling of the PowerPC conditional trap instruction (trap doubleword) is now an architecture-specific terminator instruction instead of encoding the logic of conditional trapping. We will now have to encode the conditional trapping logic in macaw-ppc-symbolic. Note that we have not done so yet.
This commit also updates the expected results of the PowerPC tests; the number of discovered blocks is different, but not significantly so. It is hard to tell if this is a regression or an improvement.
Verifies that the number of blocks found matches what should generally
be expected from this particular executable.
The specific value checked for is not independently verified, it just
happens to be a reasonable-looking value that the discovery process
currently identifies, and encoding it here ensures that if discovery
ever changes that the change will be seen and explicitly accepted or
fixed as needed.
We now thread a snapshot of the register state from the beginning of the
instruction evaluation through each instruction's semantics instead of
re-fetching register values each time we need it and potentially seeing
incorrect, partially modified register values.
The field it contains is supposed to be the instruction offset in its basic
block; overflowing it can cause significant problems during symbolic simulation.
There is a new metadata statement that tracks the start address of each
instruction. This is used in the translation to Crucible to provide better
error messages. The x86 backend was already updated, this commit adds the
metadata to the ARM and PowerPC backends.
In macaw core, the type of the arch-specific 'disassemble' function changed to
no longer take a Memory, and to pass the maximum offset as an Int instead of a
MemWord. It also removed the jump table entry size (which is no longer
required).
The removal of the Memory parameter required a bit of a change in how the
instruction parsers are structured, but it isn't a huge change (the "memory
contents after an address" can be computed from a MemSegmentOff, too).
