mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-23 16:35:02 +03:00
dbb4c83f08
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).
63 lines
1.4 KiB
Plaintext
63 lines
1.4 KiB
Plaintext
name: macaw-x86-symbolic
|
|
version: 0.0.1
|
|
author: Galois, Inc.
|
|
maintainer: jhendrix@galois.com
|
|
build-type: Simple
|
|
cabal-version: >= 1.10
|
|
license: BSD3
|
|
license-file: LICENSE
|
|
|
|
library
|
|
build-depends: base >= 4,
|
|
bv-sized >= 1.0.0,
|
|
crucible >= 0.4,
|
|
crucible-llvm,
|
|
flexdis86 >= 0.1.2,
|
|
lens,
|
|
macaw-base,
|
|
macaw-symbolic,
|
|
macaw-x86 >= 0.3.1,
|
|
mtl,
|
|
parameterized-utils,
|
|
prettyprinter >= 1.7.0,
|
|
vector,
|
|
what4 >= 0.4
|
|
hs-source-dirs: src
|
|
default-language: Haskell2010
|
|
|
|
exposed-modules:
|
|
Data.Macaw.X86.Symbolic
|
|
Data.Macaw.X86.Crucible
|
|
|
|
ghc-options: -Wall -Wcompat
|
|
ghc-prof-options: -O2 -fprof-auto-top
|
|
if impl(ghc >= 8.6)
|
|
default-extensions: NoStarIsType
|
|
|
|
test-suite macaw-x86-symbolic-tests
|
|
type: exitcode-stdio-1.0
|
|
default-language: Haskell2010
|
|
ghc-options: -Wall -Wcompat
|
|
main-is: Main.hs
|
|
hs-source-dirs: tests
|
|
build-depends:
|
|
base >= 4,
|
|
bytestring,
|
|
containers,
|
|
crucible,
|
|
crucible-llvm,
|
|
elf-edit,
|
|
filepath,
|
|
Glob >= 0.9 && < 0.11,
|
|
macaw-base,
|
|
macaw-symbolic,
|
|
macaw-x86,
|
|
macaw-x86-symbolic,
|
|
parameterized-utils,
|
|
prettyprinter,
|
|
tasty,
|
|
tasty-hunit,
|
|
text,
|
|
what4,
|
|
vector
|