The new test suites cover x86_64, PowerPC, and ARM. They test that the semantics are actually correct (rather than just seeing if symbolic execution produces any result). The `Data.Macaw.Symbolic.Testing` module in macaw-symbolic provides some common utilities for symbolic execution engine setup, while there are tailored test harnesses for each architecture.
The semantics of the test harnesses are documented in each architecture test suite, but they:
1. Discover all of the test binaries (which are generated from the included makefiles)
2. Treat each function whose name begins with `test_` as a test entry point
3. Symbolically executes each test case with fully symbolic register states
4. Extracts the return value after symbolic execution, which is treated as the predicate to an assertion that must be proved
- If the test case is in the `pass` subdirectory, it is proved and expected to hold
- If the test case is in the `fail` subdirectory, it is proved and expected to not hold.
Each test harness supports two options for debugging:
- Dumping generated SMT queries
- Dumping generated Macaw IR for inspection
This testing uncovered a bug in the (previously untested) macaw-aarch32-symbolic code. It required a number of submodule updates to:
- Adapt to some what4 changes
- Fix a bug in the LLVM memory model that lets these tests pass
- Adapt to changes to some crucible APIs
This change also modifies the CI configuration to install SMT solvers earlier (which are now needed for all of the symbolic package tests).
Nat is no longer a what4 base type, so we have to adapt various APIs to accommodate that. The template haskell in macaw-semmc is updated to remove Nat cases. Changes to the `SymFn` type required removing a type parameter.
This commit also adds macaw-refinement to CI (which requires installing SMT solvers); that code had to be updated due to the what4 changes.
Co-authored-by: Tristan Ravitch <tristan@galois.com>
* update to bv-sized branch of what4 and other things
* removed parameterized-utils submodule completely
* Updates submodules
* Fixes macaw-symbolic w.r.t. crucible-llvm changes
Co-authored-by: Ben Selfridge <ben@000548-benselfridge.local>
There are two major changes:
- The interface to memory models in Data.Macaw.Symbolic has changed
- The suggested implementation in Data.Macaw.Symbolic.Memory has changed
The change improves performance and fixes a soundness bug.
* `macawExtensions` (Data.Macaw.Symbolic) takes a new argument: a `MkGlobalPointerValidityPred`. Use `mkGlobalPointerValidityPred` to provide one.
* `mapRegionPointers` no longer takes a default pointer argument (delete it at call sites)
* `GlobalMap` returns an `LLVMPtr sym w` instead of a `Maybe (LLVMPtr sym w)`
Users of the suggested memory model do not need to worry about the last change,
as it has been migrated. If you provided your own address mapping function, it
must now be total. This is annoying, but the old API was unsound because
macaw-symbolic did not have enough information to correctly handle the `Nothing`
case. The idea of the change is that the mapping function should translate any
concrete pointers as appropriate, while symbolic pointers should generate a mux
over all possible allocations. Unfortunately, macaw-symbolic does not have
enough information to generate the mux itself, as there may be allocations
created externally.
This interface and implementation is concerned with handling pointers to static
memory in a binary. These are distinguished from pointers to
dynamically-allocated or stack memory because many machine code instructions
compute bitvectors and treat them as pointers. In the LLVM memory model used by
macaw-symbolic, each memory allocation has a block identifier (a natural
number). The stack and each heap allocation get unique block identifiers.
However, pointers to static memory have no block identifier and must be mapped
to a block in order to fit into the LLVM memory model.
The previous implementation assigned each mapped memory segment in a binary to
its own LLVM memory allocation. This had the nice property of implicitly
proving that no memory access was touching unmapped memory. Unfortunately, it
was especially inefficient in the presence of symbolic reads and writes, as it
generated mux trees over all possible allocations and significantly slowed
symbolic execution.
The new memory model implementation (in Data.Macaw.Symbolic.Memory) instead uses
a single allocation for all static allocations. This pushes more of the logic
for resolving reads and writes into the SMT solver and the theory of arrays. In
cases where sufficient constraints exist in path conditions, this means that we
can support symbolic reads and writes. Additionally, since we have only a
single SMT array backing all allocations, mapping bitvectors to LLVM pointers in
the memory model is trivial: we just change their block identifier from zero
(denoting a bitvector) to the block identifier of the unique allocation backing
static data.
This change has to do some extra work to ensure safety (especially that unmapped
memory is never written to or read from). This is handled with the
MkGlobalPointerValidityPred interface in Data.Macaw.Symbolic. This function,
which is passed to the macaw-symbolic initialization, constructs well-formedness
predicates for all pointers used to access memory. Symbolic execution tasks
that do not need to enforce this property can simply provide a function that
never returns any predicates to check. Implementations that want a reasonable
default can use the mkGlobalPointerValidityPred from Data.Macaw.Symbolic.Memory.
The default implementation ensures that no reads or writes touch unmapped memory
and that writes to static data never write to read-only segments.
This change also converts the examples in macaw-symbolic haddocks to use doctest
to ensure that they do not get out of date. These are checked as part of CI.
This cleanup consolidates the interface to macaw symbolic into two (and a half)
modules:
- Data.Macaw.Symbolic for clients who just need to symbolically simulate
machine code
- Data.Macaw.Symbolic.Backend for clients that need to implement new
architectures
- Data.Macaw.Symbolic.Memory provides a reusable example implementation of
machine pointer to LLVM memory model pointer mapping
Most functions are now documented and are grouped by use case. There are two
worked (compiling) examples in the haddocks that show how to translate Macaw
into Crucible and then symbolically simulate the results (including setting up
all aspects of Crucible). The examples are included in the symbolic/examples
directory and can be loaded with GHCi to type check them.
The Data.Macaw.Symbolic.Memory module still needs a worked example.
There were very few changes to actual code as part of this overhaul, but there
are a few places where complicated functions were hidden behind newtypes, as
users never need to construct the values themselves (e.g., MacawArchEvalFn and
MacawSymbolicArchFunctions). There was also a slight consolidation of
constraint synonyms to reduce duplication. All callers will have to be updated.
There is also now a README for macaw-symbolic that explains its purpose and
includes pointers to the new haddocks.
This commit also fixes up the (minor) breakage in the macaw-x86-symbolic
implementation from the API changes.
