This bumps the `what4` submodule to the 1.6.* version series and updates the
`.cabal` files in the `macaw` repo accordingly.
Bumping the `what4` submodule also requires bringing in corresponding changes
in the `crucible`, `llvm-pretty`, and `llvm-pretty-bc-parser` submodules, so I
have done that as well.
This introduces a `HasMacawLazySimulatorState` data type, which provides a
"classy lens" for accessing a `MacawLazySimulatorState` within some Crucible
personality type. It also generalizes the lazy `macaw-symbolic` memory model in
`Data.Macaw.Symbolic.Memory.Lazy` to be polymorphic over
`HasMacawLazySimulatorState` instances. The upside is that it is now possible
to use the lazy memory model at other personality types besides just
`MacawLazySimulatorState`, making it much easier to extend the memory model.
Because there is a `HasMacawLazySimulatorState` instance for
`MacawLazySimulatorState`, existing code that uses `MacawLazySimulatorState`
should continue to compile without changes.
Fixes#357.
Rather than `error`ing, we now generate fresh constants for all possible
`macaw` `Type`s that are supplied to the `MacawFreshSymbolic` operation.
Fixes#301.
This patch contains a handful of tweaks needed to make the libraries in the
`macaw` repo build with GHC 9.6:
* GHC 9.6 bundles `mtl-2.3.*`, which no longer re-exports `Control.Monad`,
`Control.Monad.Trans`, and similar modules from `mtl`-related modules. To
accommodate this, various imports have been made more explicit.
* I have disambiguated a use of `Data.Parameterized.NatRepr.withKnownNat` in
`macaw-aarch32` to avoid clashing with a newly exported function of the same
name in `GHC.TypeNats`.
* I have bumped various upper version bounds on `doctest`,
`optparse-applicative`, and `what4` to allow building these libraries with
GHC 9.6.
* I have bumped the following submodules to bring in GHC 9.6–related changes:
* `asl-translator`: GaloisInc/asl-translator#53
* `crucible`: GaloisInc/crucible#1102
* `dwarf`: GaloisInc/dwarf#6
* `elf-edit`: GaloisInc/elf-edit#38
* `flexdis86`: GaloisInc/flexdis86#54
* `grift`: GaloisInc/grift#9
* `llvm-pretty`: elliottt/llvm-pretty#112
* `llvm-pretty-bc-parser`: GaloisInc/llvm-pretty-bc-parser#225
* `semmc`: GaloisInc/semmc#80
* `what4`: GaloisInc/what4#235
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.
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.
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.
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.
The core of macaw cannot represent conditional calls because the existing block terminators are not sufficiently expressive and it doesn't support creating synthetic blocks to represent control flow not directly tied to machine addresses.
To work around this, we introduce ARM-specific block terminators for conditional calls and plumb them through up to macaw-aarch32-symbolic.
Fixes#288
The tail call classifier came after the jump classifier, which was a problem because it is less strict than the tail call classifier, meaning it would always fire. This commit moves direct jump to be the last classifier applied, giving the others a chance.
Includes a test case in the ARM backend.
This requires some updates to some of the expected test results, as a few blocks are now classified as tail calls that were
plain jumps before. They really could be considered either. I think it would be nice if these could be classified as jumps instead, but the reason they are flagged as tail calls is mostly down to the fact that their surrounding context is so simple that either interpretation works.
Correcting this would require some heuristics based on additional analysis passes.
The test harness for macaw symbolic required a few changes because the new detection of some jumps as tail calls introduces new calls into the symbolic test suites. However, the symbolic testing harness did not support calls before. Adding support required a bit of plumbing, including a more extensive code discovery pass.
Fixes#285
* remove/generalize MacawBlockEnd from CFG slicing
* expose functions in symbolic backend
* hide bvLit from Backend import
* add CI version to workflow
This would come in handy for an application where I wish to pass a
`NonEmptyVector` to `newMergedGlobalMemoryWith`. Currently, I have to convert
the `NonEmptyVector` to a `NonEmpty` list to accomplish this, wish seems
wasteful given that `newMergedGlobalMemoryWith` only needs to use the
`Foldable` interface.
This change adds a function `newMergedGlobalMemoryWith`, which acts like
`newGlobalMemoryWith` but takes a list of macaw memories and merges them
into a flat address space. This aids in reasoning dynamically linked
programs.
Before, the API provided by macaw-symbolic asserted the initial value of each byte of memory individually. This was fairly expensive for large binaries, as each such assertion flushed the solver pipe.
This change generates a large conjunction of assertions and sends them all at once. In unscientific testing, this saved half an hour on a large binary.
API Changes:
- Note that it introduces a minor API change. The optimization required that the `sym` parameter be concretely an `ExprBuilder`.
* Translate PLTStubs as tail calls
This change modifies `addMacawParsedTermStmt` to translate `PLTStub`s as
tail calls.
* Replace CR.Call + CR.Return with CR.TailCall
* Add support for standalone PIEs
This changeset adds support for standalone position independent
executables (PIEs) that do not make use of procedure linkage tables. It
does so by adding relative address support to `populateSegmentChunk` and
adding an additional simplification rule for Aarch32.
This covers part of the work for #234.
* Remove NoOp + replace mult with left shift
This mostly deals with the splitting of the old `sym` type into
two: one for dealing with expression creation, and a new simulator
backend type for dealing with control-flow and assertions.
See the writeup in Crucible.hs in this commit for details. In short, the recent
changes to generalize `PtrAdd` triggered a failing proof obligation due to a use
of `llvmPointer_bv`. The new implementation is as sound as the previous one,
but more general.
Fixes#260
This contains a variety of fixes needed to make the packages in the `macaw`
repo compile with GHC 9.0:
* GHC 9.0 implements simplified subsumption (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#simplified-subsumption)).
In most cases, adapting to this is a matter of manually eta expanding
definitions, such as in `base:Data.Macaw.Analysis.RegisterUse`. In the case
of `macaw-x86-symbolic:Data.Macaw.X86.Crucible`, the type signature of
`evalExt` had to be made more specific to adapt to the loss of contravariance
when typechecking `(->)`.
* GHC's constraint solver now solves constraints in each top-level group
sooner (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#the-order-of-th-splices-is-more-important)).
This affects `macaw-aarch32` and `macaw-symbolic`, as they separate top-level
groups with `$(return [])` Template Haskell splices. The previous locations
of these splices made it so that the TH-generated instances in that package
were not available to any code before the splice, resulting in type errors
when compiled with GHC 9.0.
To overcome this, I rearranged the TH-generated instances so that they appear
before the top-level groups that make use of them.
* GHC 9.0 now enables `-Wstar-is-type` in `-Wall`, so this patch replaces some
uses of `*` with `Data.Kind.Type`. `Data.Kind` requires the use of GHC 8.0 or
later, so this patch also updates thes lower bounds on `base` to `>= 4.9` in
the appropriate `.cabal` files. (I'm fairly certain that this requirement was
already present implicity, but better to be explicit about it.)
* The `asl-translator`, `crucible`, and `semmc` submodules were updated to
allow them to build with GHC 9.0. The `llvm-pretty` and
`llvm-pretty-bc-parser` submodules were also bumped to accommodate unrelated
changes in `crucible` that were brought in.
* The upper version bounds on `doctest` in `macaw-symbolic`'s test suite were
raised to allow it to build with GHC 9.0.
There were two identical definitions of `toCrucibleEndian`, one in
`D.M.S.Memory` and another in `D.M.S.Testing`. This commit removes the
latter in favor of the former, which is actually exported.
Have all additions (at any bit width) go through the special PtrAdd
handler (rather than BVAdd). Also add special handlers for truncation and
extension.
These changes support architectures that do pointer operations at non-pointer
widths (e.g., to detect overflow). These new operations apply the named
operations over just the offset of pointers, preserving the block id.
The `Data.Macaw.Symbolic.Memory` module provides a default memory model and
initial memory setup that is suitable for many symbolic execution
workloads. However, the defaults cannot handle dynamically-linked programs, as
it calls `error` when it attempts to determine an initial value for relocations
it finds in memory.
There are no good defaults for this, as what those values should be depend a lot
on what the verifier wants to prove.
This commit adds some hooks to configure this behavior in the verifier, and is
designed to be extensible and enable other configuration choices where
reasonable.
The original API is unchanged, as it calls the added `newGlobalMemoryWith`
function with a default set of hooks. Callers with special memory handling
needs are directed to use that function.
This updates the `crucible` submodule to include GaloisInc/crucible#906
(`Control granularity of reading uninitialized memory`), as well as the
`semmc` submodule to bring in corresponding changes on its side
(GaloisInc/semmc#69). Some additional `?memOpts :: MemOptions` constraints
needed to be added to some functions in `macaw-symbolic` and
`macaw-refinement` as a result.
Adds support in macaw-aarch32 for conditional returns. These are not supported in core macaw, and are thus architecture-specific block terminators.
This required changes to the type of arch-specific block terminators. Before, `ArchTermStmt` was only parameterized by a state thread (`ids`). This meant that they could not contain macaw (or crucible) values. Some work on. AArch32 requires being able to store condition values in arch terminators (to support conditional returns). This change modifies the `ArchTermStmt` to enable this, which requires a bit of plumbing through various definitions and some extra instances.
In support of actually using this, it also became necessary to plumb fallthrough block labels through the architecture-specific terminator translation in macaw-symbolic.
Note that this change was overdue, as the PowerPC backend was storing macaw values in a way that would have rendered them unusable in the macaw-ppc-symbolic translation, had any interpretation been provided. These new changes will enable a handler to be written for the conditional PowerPC trap instructions.
PowerPC, x86, and ARM have been updated.
Improves the macaw-aarch32 tests. There is now a command line option to save the generated macaw IR for each
discovered function to /tmp. Note that this reuses some infrastructure from the macaw-symbolic tests. This
shared functionality should be extracted into a macaw-testing library.
