The PPC return sequence (from the PPC semantics)
implicitly wraps the address in shift left/shift right to mask
the lower two bits, e.g.:
r15 := (bv_shr r13 (0x2 :: [32]))
r16 := (trunc r15 30)
r17 := (uext r16 32)
r18 := (bv_shl r17 (0x2 :: [32]))
Prior to this patch, this was the only pattern that was
handled by matchReturn, and thus considered a valid return
address.
We observed in some cases that binaries compiled with -O2
would have the following expression appear in the link
register prior to a tail function call:
r8 := (bv_add r1_0 (0x14 :: [32]))
r9 := read_mem r8 (bvbe4)
Where r9 is read directly off the stack without any
additional shifting.
This second pattern causes the tail call classifier to fail,
because matchReturn did not recognize this sequence.
This change allows matchReturn to succeed on the latter case,
and therefore causes the tail call classifier to succeed as
expected.
This is cargo-culted from the `*.Panic` module of a similar name in
`macaw-aarch32`. This will be useful in a subsequent commit in which we replace
some unreachable calls to `fail` with `panic`.
The only other changes required are (1) deleting an unused dependency on
`what4-serialize`, and (2) raising upper version bounds on `what4`.
This brings in submodule changes from the following:
* GaloisInc/asl-translator#48, which performed a similar `what4` adaptation.
* GaloisInc/semmc#78, which performed a similar `what4` adaptation.
* GaloisIns/crucible#1068, which ensures that everything can build against
`tasty-sugar >= 2.0` (the version of the library that `what4-1.4` depends on).
This folds the menagerie of various configuration option arguments to
`macawExtensions` into the `MemModelConfig` data type. The advantage to doing
this is that is will make it easier to extend the memory model configuration
options in the future without needlessly foisting breaking changes on all
`macaw-symbolic` users.
Unfortunately, it does require a breaking change to get to this point, but the
migration path is straightforward for existing code. I have included this
migration story in the `macaw-symbolic` changelog.
The current `macaw-symbolic` memory model has issues when scaling up to
binaries that have several megabytes or more in size. This patch introduces a
new memory model (in `Data.Macaw.Symbolic.Memory.Lazy`) that serves as a mostly
drop-in replacement for the existing memory model (which I now refer to as the
"default" memoy model). The lazy memory model scales better by incrementally
populating the SMT array backing global memory over the course of a run of the
simulator. For the full details, see `Note [Lazy memory model]`.
I performed some refactoring to share common bits between the default and lazy
memory models.
Fixes#282.
This patch introduces a `MemModelConfig` data type for configuring the finer
details of `macaw-symbolic`'s memory model. For now, there is a single option,
which configures whether the memory model should attempt to concretize pointers
during a read or write, which can sometimes be beneficial for performance
reasons. The details of how concretization work can be found in the new
`Data.Macaw.Symbolic.Concretize` module.
Subsequent commits will add more configurable knobs to `MemModelConfig`.
Fixes#323.
This extends `Data.Macaw.Symbolic.Testing` in `macaw-symbolic` to be able to
handle binaries that depend on shared libraries. This is fully functional for
the x86-64 and AArch32 symbolic backends, and I have added test cases to the
respective repos demonstrating that it works. (The PowerPC backend is not yet
supported. At a minimum, this is blocked on GaloisInc/elf-edit#35.)
To implement this, I also needed to add some additional infrastructure to
`macaw-base` (I put this infrastructure here as it doesn't depend on any
Crucible-specific functionality):
* `Data.Macaw.Memory.ElfLoader.DynamicDependencies`: a basic ELF dynamic
loader that performs a breadth-first search over all `DT_NEEDED` entries
that an ELF binary depends on (both directly and indirectly).
* `Data.Macaw.Memory.ElfLoader.PLTStubs`: a collection of heuristics for
detecting the addresses of PLT stubs in a dynamically linked binary.
It is worth noting that shared libraries are rife with nuance and subtlety,
and the way `macaw` models shared libraries is not 100% accurate. I have
written a length `Note [Shared libraries]` in `Data.Macaw.Symbolic.Testing`
to describe where corners had to be cut.
Fixes#318.
This:
* Bumps the `elf-edit` submodule to bring in the changes from
GaloisInc/elf-edit#34.
* Updates `Data.Macaw.Memory.ElfLoader` to consolidate the symbol table logic
with the corresponding functions from `elf-edit`.
Fixes#277.
This is needed to bring in the changes from #77, which adds support for
`hashable-1.4.*`. With this change, everything in the `macaw` repo now
builds with `hashable-1.4.*`.
This requires bumping the `asl-translator` submodule to bring the changes from
GaloisInc/asl-translator#47, which are necessary for the test case to work.
When populating `COPY` relocations, it is helpful to know the address of the
relocation so that it can be related back to the name of the global symbol
whose value it is copying. Unfortunately, the type of `populateRelocation` does
not make it straightforward to compute this address. This patch includes three
additional arguments to `populateRelocation` (the relocation's `Memory`, its
`MemSegment`, and its `MemAddr`) to more easily facilitate computing the
address.
This is a breaking API change, albet it is a fairly straightforward change to
adapt to for most consumers.
This is related to #47, although this is not a full fix for the issue.
We already have support for `R_X86_64_COPY` relocations, so adding support
for `R_ARM_COPY` on the AArch32 side is straightforward.
This is related to #47, although this is not a full fix for the issue.
This patch was motivated by the need to call `doGetGlobal` from a Crucible
override, where the `SimState` is instantiated with `OverrideLang` rather than
`CrucibleLang`, the latter of which is used in the `CrucibleState` type
synonym. While I was in town, I generalized the types of other operations in
`Data.Macaw.Symbolic.MemOps` where it was reasonable.
This bumps the `crucible` submodule to bring in the changes from
GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to
a handful of additional functions. This requires adding constraints to
some functions in `macaw-symbolic` to accommodate, as well as bumping the
`semmc` submodule to bring in analogous changes from GaloisInc/semmc#76.
It turns out that we have to be more conservative with tail call identification,
as incorrectly identifying a block as the target of a tail call (instead of a
branch) can cause other branch classifiers to fail if that block is the target
of another jump.
Ultimately, we will need to give up some tail call recognition (since they are
in general indistinguishable from jumps), and instead only identify known call
targets as tail call candidates.
With additional global analysis we could do better.
Fixes#294
The bug arose in the handling of `StackOffsetAbsVal`, which track an abstraction
of references relative to the stack pointer. The offsets in `StackOffsetAbsVal`
are `Int64`; they are signed because references are both above and below the
stack pointer. The code constructing new values of this type was incorrectly
zero-extending new offsets instead of sign extending them. This did not matter
on 64 bit architectures, as it happened to result in the same values. It
substantially corrupted the abstract stack on PowerPC 32. It did not seem to
affect AArch32, but that is likely just due to luck in compiler code generation
that does not require this level of precision in the abstract stack.
The resulting errors manifest in the `absEvalCall` function. Because of the lack
of sign extension in `StackOffsetAbsVal`s, it made the current stack pointer
look like a huge number, which caused *all* stack entries to be dropped after
function calls.
This fix simplifies the stack offset abstract value computation substantially
and ensures that signs are extended correctly. The commit adds a PowerPC32 test
case that only passes with this fix.
GHC 9.2 adds `-Wincomplete-uni-patterns` to `-Wall`, which uncovers a slew of
previously unnoticed warnings in `macaw`. This patch fixes them, mostly by
adding explicit fall-through cases.
