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>
Some important simplifications for classification were failing to fire because
other simplifications fired first, short circuiting the search. It turns out
that more than one rule may apply at any given step (and it is important to
apply all of the rules that can be applied). This commit modifies the
simplifier to apply rules until saturation.
The previous implementation used all of the registers defined in ASL translator.
It turns out that we don't actually use all of them in macaw; the significant
difference is that the `__memory` pseudo-location is used by asl-translator, but
not macaw (as macaw handles memory through implicit context). This change
modifies the register assignment to include everything except memory (which
requires an update to the asl-translator submodule).
* reify block exit in macaw extension
* add return address to block end classification
* use global variable to retain block endings
* update to mkBlockSliceCFG signature
* add haddocks for MacawBlockEnd
Co-authored-by: Tristan Ravitch <tristan@galois.com>
- Use an explicit package-level build step for each architecture, which will
build utility binaries and not just the tests/libraries
- Enable builds/tests for the PowerPC backend
- Build macaw-aarch32-symbolic
