* Fix block size accounting in the disassembler
The value in the early failure combinator is used as the *block size* in the
resulting macaw block. The code was actually using the offset from the
beginning of the segment, which is wrong. This produced very large blocks that
didn't reflect the results of code discovery and led to decode errors later in
the pipeline.
* Do not throw an error if concreteIte has a symbolic argument
The `concreteIte` combinator turns formula conditionals with concrete operands
into Haskell-level conditional execution. It would fail because we believed
that there were no cases that could fail to satisfy that condition. That
assumption was not true - we need to fall back to generating a mux when we have
a symbolic condition.
Under GHC8.4, a let binding is independent of the surrounding context,
so the let statements encountered errors related to type matching on
synthesized internal type parameters that could not be identified as
the same due to rigid skolem type binding inside the let.
Improve the TH codegen for macaw-semmc
This change lazily translates as much as possible. It also generates somewhat more compact code. This change also finishes implementing primitives for the aarch32 backend. Complementing the aarch32 changes, the macaw-semmc interface has been modified to allow macaw-aarch32 to avoid a redundant serialize-deserialize round.
Co-authored-by: Kevin Quick <kquick@galois.com>
These are currently broken. If someone is actively interested in
using stack to build then the files could be re-instated from this
position and updated, but it's better to not have them if they are not
used or maintained.
This code was confusing what "offset" to pass to the `failAt` function. Some
sites were passing the offset from the beginning of the block (correct), while
others passed the offset from the start of the segment (incorrect). The
incorrect values were later used as block sizes, which caused some downstream
failures (in renovate).
This commit uniformly fails with the offset from the start of the block.
This change is probably due to the BitTrie modifications in
dismantle-tablegen. It's not clear whether the older or newer number
of discovered blocks is correct; testing at this point is focused more
on getting roughly the correct order of magnitude rather than being
refined enough for high precision values.
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`.
These packages replace the old macaw-arm (which has been removed). The only
change to the core macaw is to introduce a `Lift` instance for the Endianness
data type, which is used in macaw-semmc.
The macaw-aarch32 package uses the official ARM semantics (via the
asl-translator package). In its current state, macaw-aarch32 seems to handle
the common idioms of simple ARM binaries. Position independent executables have
not been tested yet. The semantics and disassemblers for Thumb are present, but
not integrated into code discovery at this time. There are some tests in
macaw-aarch32. Compile times are longer than necessarily desired.
macaw-aarch32 can be compiled in two modes: lite mode (cabal flag -fasl-lite),
which uses a restricted set of instructions for testing, and takes less time to
compile. The full instruction set is the default, though there are a few
undefined functions that are not yet handled for the full set, mostly relating
to floating point operations.
The macaw-aarch32-symbolic package is currently a stub, but is implemented to
provide a few necessary instances.
We were reading partially updated values that were committed to the register
state out-of-order, yielding some bad results.
This commit takes a snapshot of the register state before executing each
instruction and only reads register values from the snapshot.
