a6ff58f473
When converting a Macaw value with the Macaw type `TupleType [x_1, ..., x_n]` to Crucible, the resulting Crucible value will have the Crucible type `StructType (EmptyCtx ::> ToCrucibleType x_n ::> ... ::> ToCrucibleType x_1)`. (See `macawListToCrucible(M)` in `Data.Macaw.Symbolic.PersistentState` for where this is implemented.) Note that the order of the tuple's fields is reversed in the process of converting it to a Crucible struct. This is a convention that one must keep in mind when dealing with Macaw tuples at the Crucible level. As it turns out, the part of `macaw-x86-symbolic` reponsible for interpreting the semantics of the `idiv` instruction (for signed quotient/remainder) and the `div` instruction (for unsigned quotient/remainder) were _not_ respecting this convention. This is because the `macaw-x86-symbolic` semantics were returning a Crucible struct consisting of `Empty :> quotient :> remainder)`, but at the Macaw level, this was interpreted as the tuple `(remainder, quotient)`, which is the opposite of the intended order. This led to subtle bugs such as those observed in #393. The solution is straightforward: have the `macaw-x86-symbolic` semantics compute `Empty :> remainder :> quotient` instead. Somewhat counterintuitive, but it does work. Fixes #393. |
||
|---|---|---|
| .. | ||
| fail | ||
| pass | ||
| Main.hs | ||
| README.org | ||
Overview
This test suite tests that symbolic execution of x86_64 programs works. It is also a convenient place to test the semantics. The test harness looks for binaries in the pass and fail subdirectories. In both cases, it enumerates the functions whose names are prefixed by test_, each of which are symbolically executed with fully symbolic initial states. It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion). Test cases in pass are expected to return a value that is always true, while the test cases in fail are expected to not always be true (but note that the precise models are not inspected). The test harness uses yices for path satisfiability checking and z3 to prove goals. Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate.
In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by test_and_verify_. In both the pass and fail directories, these side conditions are expected to pass (or they will cause test failures).
Usage
The test runner has two command line options (beyond the defaults for tasty):
--save-macaw: Saves the Macaw IR for each test case to /tmp for debugging purposes--save-smt: Saves the generated SMTLib for each test to /tmp for debugging purposes
Limitations
- It currently tests both optimized an unoptimized binaries. It is intended that this set will expand and that a wide variety of compilers will be tested.
- Only two solvers are involved in the test, rather than a whole matrix
- Function calls are not supported in test cases
- There are no facilities for generating symbolic data beyond the initial symbolic arguments to each function