From 0d26e4a656176d47dcc9fba9503de3c0d8a0219f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 8 Nov 2023 14:57:57 -0500 Subject: [PATCH] crucible-cli: Library for sharing code between Crucible CLI frontends (#1123) * crucible-cli: Library for sharing code between Crucible CLI frontends Previously, `crucible-syntax` had some code for setting up and executing the Crucible symbolic simulator. This functionality is very useful for testing and interactive experimentation via a CLI, but is not necessary for most library clients of `crucible-syntax`. Furthermore, creating additional CLI frontends entailed copy-pasting a lot of `optparse-applicative`-related code from `crucible-syntax`'s' `crucibler` executable. Now, both these issues are addressed by factoring this code into a separate `crucible-cli` package. * crucible-llvm-cli: CLI for executing crucible-llvm CFGs * crucible-{,llvm-}cli: Fix hlint lints, trailing whitespace * ci: Fix executable name * crucible-cli: Haddocks * crucible-llvm-cli: Haddocks * crucible-llvm-cli: Fix build on GHC 8.10.7 by enabling GADTs --- .github/workflows/crux-llvm-build.yml | 13 + .github/workflows/uc-crux-llvm-lint.yaml | 2 + README.md | 23 +- cabal.project | 2 + crucible-cli/.hlint.yaml | 13 + crucible-cli/LICENSE | 30 ++ crucible-cli/app/Main.hs | 21 ++ crucible-cli/crucible-cli.cabal | 145 +++++++++ crucible-cli/src/Lang/Crucible/CLI.hs | 280 ++++++++++++++++++ .../src/Lang/Crucible/CLI/Options.hs | 43 +-- crucible-cli/test-data/.gitignore | 1 + .../test-data/declare}/main.cbl | 0 .../test-data/declare}/main.out.good | 0 .../test-data/extern}/main.cbl | 0 .../test-data/extern}/main.out.good | 0 .../test-data/simulate}/assert.cbl | 0 .../test-data/simulate}/assert.out.good | 2 +- .../test-data/simulate}/assume-merge.cbl | 0 .../test-data/simulate/assume-merge.out.good | 24 ++ .../test-data/simulate}/assume-merge2.cbl | 0 .../simulate}/assume-merge2.out.good | 6 +- .../test-data/simulate}/assume.cbl | 0 .../test-data/simulate}/assume.out.good | 4 +- .../test-data/simulate}/bool-expr.cbl | 0 .../test-data/simulate}/bool-expr.out.good | 0 .../test-data/simulate}/branch.cbl | 0 .../test-data/simulate}/branch.out.good | 2 +- .../test-data/simulate}/bv-expr.cbl | 0 .../test-data/simulate}/bv-expr.out.good | 8 +- .../test-data/simulate}/calls.cbl | 0 .../test-data/simulate}/calls.out.good | 2 +- .../test-data/simulate}/double-branch.cbl | 0 .../test-data/simulate/double-branch.out.good | 14 + .../test-data/simulate}/float-cast.cbl | 0 .../test-data/simulate}/float-cast.out.good | 4 +- .../test-data/simulate}/from-maybe.cbl | 0 .../test-data/simulate}/from-maybe.out.good | 4 +- .../test-data/simulate}/hello.cbl | 0 .../test-data/simulate}/hello.out.good | 0 .../test-data/simulate}/loop-err.cbl | 0 .../test-data/simulate/loop-err.out.good | 54 ++++ .../test-data/simulate}/loop.cbl | 0 .../test-data/simulate}/loop.out.good | 4 +- .../test-data/simulate}/mjrty.cbl | 0 .../test-data/simulate}/mjrty.out.good | 2 +- .../simulate}/override-nondet-test-0.cbl | 0 .../simulate}/override-nondet-test-0.out.good | 0 .../simulate}/override-nondet-test-1.cbl | 0 .../simulate}/override-nondet-test-1.out.good | 0 .../simulate}/override-nondet-test-both.cbl | 0 .../override-nondet-test-both.out.good | 42 +-- .../override-nondet-test-neither.cbl | 0 .../override-nondet-test-neither.out.good | 6 +- .../test-data/simulate}/override-test.cbl | 0 .../simulate}/override-test.out.good | 2 +- .../test-data/simulate}/override-test2.cbl | 0 .../simulate}/override-test2.out.good | 6 +- .../test-data/simulate}/seq-test1.cbl | 0 .../test-data/simulate}/seq-test1.out.good | 0 .../test-data/simulate}/seq-test2.cbl | 0 .../test-data/simulate/seq-test2.out.good | 26 ++ .../test-data/simulate}/seq-test3.cbl | 0 .../test-data/simulate}/seq-test3.out.good | 16 +- .../test/Overrides.hs | 9 - crucible-cli/test/Test.hs | 146 +++++++++ crucible-llvm-cli/.hlint.yaml | 13 + crucible-llvm-cli/LICENSE | 30 ++ crucible-llvm-cli/app/Main.hs | 8 + crucible-llvm-cli/crucible-llvm-cli.cabal | 140 +++++++++ .../src/Lang/Crucible/LLVM/CLI.hs | 57 ++++ crucible-llvm-cli/test-data/.gitignore | 1 + .../test-data}/ptr.cbl | 0 .../test-data}/ptr.out.good | 0 crucible-llvm-cli/test/Test.hs | 51 ++++ crucible-llvm-syntax/app/Main.hs | 82 ----- .../crucible-llvm-syntax.cabal | 16 - .../test-data/{parse => }/ptr.cbl | 0 .../test-data/{parse => }/ptr.out.good | 2 +- .../test-data/{parse => }/type.cbl | 0 .../test-data/{parse => }/type.out.good | 0 crucible-llvm-syntax/test/Test.hs | 37 +-- crucible-syntax/crucible-syntax.cabal | 101 +++++-- .../src/Lang/Crucible/Syntax/Prog.hs | 250 +--------------- .../{parser-tests => }/all-term-stmt.cbl | 0 .../{parser-tests => }/all-term-stmt.out.good | 0 .../test-data/{parser-tests => }/assert.cbl | 0 .../{parser-tests => }/assert.out.good | 0 .../test-data/{parser-tests => }/bool.cbl | 0 .../{parser-tests => }/bool.out.good | 0 .../{parser-tests => }/breakpoints.cbl | 0 .../{parser-tests => }/breakpoints.out.good | 0 .../test-data/{parser-tests => }/busted.cbl | 0 crucible-syntax/test-data/busted.out.good | 4 + .../test-data/{parser-tests => }/bv.cbl | 0 .../test-data/{parser-tests => }/bv.out.good | 0 .../test-data/{parser-tests => }/cfg.cbl | 0 .../test-data/{parser-tests => }/cfg.out.good | 0 .../test-data/{parser-tests => }/empty.cbl | 0 .../{parser-tests => }/empty.out.good | 0 .../test-data/{parser-tests => }/floats.cbl | 0 .../{parser-tests => }/floats.out.good | 0 .../test-data/{parser-tests => }/fun-type.cbl | 0 .../{parser-tests => }/fun-type.out.good | 0 .../test-data/{parser-tests => }/globals.cbl | 0 .../{parser-tests => }/globals.out.good | 0 .../test-data/{parser-tests => }/integer.cbl | 0 .../{parser-tests => }/integer.out.good | 0 .../test-data/{parser-tests => }/mutual.cbl | 0 .../{parser-tests => }/mutual.out.good | 0 .../test-data/{parser-tests => }/natural.cbl | 0 .../{parser-tests => }/natural.out.good | 0 .../test-data/parser-tests/busted.out.good | 4 - .../test-data/{parser-tests => }/rational.cbl | 0 .../{parser-tests => }/rational.out.good | 0 .../test-data/{parser-tests => }/recur.cbl | 0 .../{parser-tests => }/recur.out.good | 0 .../test-data/{parser-tests => }/refs.cbl | 0 .../{parser-tests => }/refs.out.good | 0 .../test-data/{parser-tests => }/regs.cbl | 0 .../{parser-tests => }/regs.out.good | 0 .../test-data/{parser-tests => }/shower.cbl | 0 .../{parser-tests => }/shower.out.good | 0 .../simulator-tests/assume-merge.out.good | 24 -- .../simulator-tests/double-branch.out.good | 14 - .../simulator-tests/loop-err.out.good | 54 ---- .../simulator-tests/seq-test2.out.good | 26 -- .../test-data/{parser-tests => }/strings.cbl | 0 .../{parser-tests => }/strings.out.good | 0 .../test-data/{parser-tests => }/structs.cbl | 0 .../{parser-tests => }/structs.out.good | 0 .../test-data/{parser-tests => }/variants.cbl | 0 .../{parser-tests => }/variants.out.good | 0 .../test-data/{parser-tests => }/vecs.cbl | 0 .../{parser-tests => }/vecs.out.good | 0 crucible-syntax/test/Tests.hs | 137 +-------- 135 files changed, 1278 insertions(+), 729 deletions(-) create mode 100644 crucible-cli/.hlint.yaml create mode 100644 crucible-cli/LICENSE create mode 100644 crucible-cli/app/Main.hs create mode 100644 crucible-cli/crucible-cli.cabal create mode 100644 crucible-cli/src/Lang/Crucible/CLI.hs rename crucible-syntax/crucible-syntax/Main.hs => crucible-cli/src/Lang/Crucible/CLI/Options.hs (63%) create mode 100644 crucible-cli/test-data/.gitignore rename {crucible-syntax/test-data/declare-tests => crucible-cli/test-data/declare}/main.cbl (100%) rename {crucible-syntax/test-data/declare-tests => crucible-cli/test-data/declare}/main.out.good (100%) rename {crucible-syntax/test-data/extern-tests => crucible-cli/test-data/extern}/main.cbl (100%) rename {crucible-syntax/test-data/extern-tests => crucible-cli/test-data/extern}/main.out.good (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/assert.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/assert.out.good (68%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/assume-merge.cbl (100%) create mode 100644 crucible-cli/test-data/simulate/assume-merge.out.good rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/assume-merge2.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/assume-merge2.out.good (57%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/assume.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/assume.out.good (55%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/bool-expr.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/bool-expr.out.good (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/branch.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/branch.out.good (71%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/bv-expr.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/bv-expr.out.good (82%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/calls.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/calls.out.good (71%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/double-branch.cbl (100%) create mode 100644 crucible-cli/test-data/simulate/double-branch.out.good rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/float-cast.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/float-cast.out.good (76%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/from-maybe.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/from-maybe.out.good (59%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/hello.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/hello.out.good (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/loop-err.cbl (100%) create mode 100644 crucible-cli/test-data/simulate/loop-err.out.good rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/loop.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/loop.out.good (59%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/mjrty.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/mjrty.out.good (76%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-0.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-0.out.good (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-1.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-1.out.good (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-both.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-both.out.good (53%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-neither.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-nondet-test-neither.out.good (68%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-test.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-test.out.good (72%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-test2.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/override-test2.out.good (77%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/seq-test1.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/seq-test1.out.good (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/seq-test2.cbl (100%) create mode 100644 crucible-cli/test-data/simulate/seq-test2.out.good rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/seq-test3.cbl (100%) rename {crucible-syntax/test-data/simulator-tests => crucible-cli/test-data/simulate}/seq-test3.out.good (62%) rename {crucible-syntax => crucible-cli}/test/Overrides.hs (92%) create mode 100644 crucible-cli/test/Test.hs create mode 100644 crucible-llvm-cli/.hlint.yaml create mode 100644 crucible-llvm-cli/LICENSE create mode 100644 crucible-llvm-cli/app/Main.hs create mode 100644 crucible-llvm-cli/crucible-llvm-cli.cabal create mode 100644 crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs create mode 100644 crucible-llvm-cli/test-data/.gitignore rename {crucible-llvm-syntax/test-data/simulate => crucible-llvm-cli/test-data}/ptr.cbl (100%) rename {crucible-llvm-syntax/test-data/simulate => crucible-llvm-cli/test-data}/ptr.out.good (100%) create mode 100644 crucible-llvm-cli/test/Test.hs delete mode 100644 crucible-llvm-syntax/app/Main.hs rename crucible-llvm-syntax/test-data/{parse => }/ptr.cbl (100%) rename crucible-llvm-syntax/test-data/{parse => }/ptr.out.good (98%) rename crucible-llvm-syntax/test-data/{parse => }/type.cbl (100%) rename crucible-llvm-syntax/test-data/{parse => }/type.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/all-term-stmt.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/all-term-stmt.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/assert.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/assert.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/bool.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/bool.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/breakpoints.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/breakpoints.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/busted.cbl (100%) create mode 100644 crucible-syntax/test-data/busted.out.good rename crucible-syntax/test-data/{parser-tests => }/bv.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/bv.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/cfg.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/cfg.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/empty.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/empty.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/floats.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/floats.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/fun-type.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/fun-type.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/globals.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/globals.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/integer.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/integer.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/mutual.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/mutual.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/natural.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/natural.out.good (100%) delete mode 100644 crucible-syntax/test-data/parser-tests/busted.out.good rename crucible-syntax/test-data/{parser-tests => }/rational.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/rational.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/recur.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/recur.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/refs.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/refs.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/regs.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/regs.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/shower.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/shower.out.good (100%) delete mode 100644 crucible-syntax/test-data/simulator-tests/assume-merge.out.good delete mode 100644 crucible-syntax/test-data/simulator-tests/double-branch.out.good delete mode 100644 crucible-syntax/test-data/simulator-tests/loop-err.out.good delete mode 100644 crucible-syntax/test-data/simulator-tests/seq-test2.out.good rename crucible-syntax/test-data/{parser-tests => }/strings.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/strings.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/structs.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/structs.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/variants.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/variants.out.good (100%) rename crucible-syntax/test-data/{parser-tests => }/vecs.cbl (100%) rename crucible-syntax/test-data/{parser-tests => }/vecs.out.good (100%) diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml index c51a1f7a8..724317f46 100644 --- a/.github/workflows/crux-llvm-build.yml +++ b/.github/workflows/crux-llvm-build.yml @@ -151,7 +151,9 @@ jobs: setup_bin() { echo setup.${{ matrix.ghc }}; } with_ghc() { $NS -c ${@}; } (cd crucible; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd crucible-cli; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) (cd crucible-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd crucible-llvm-cli; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) (cd crucible-llvm-syntax; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) (cd crux; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) (cd crux-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) @@ -163,7 +165,9 @@ jobs: - shell: bash run: | + .github/ci.sh build exe:crucible .github/ci.sh build lib:crucible-llvm-syntax + .github/ci.sh build exe:crucible-llvm .github/ci.sh build exe:crux-llvm .github/ci.sh build exe:crux-llvm-for-ide .github/ci.sh build exe:crux-llvm-svcomp @@ -177,6 +181,10 @@ jobs: name: Test crucible run: .github/ci.sh test crucible + - shell: bash + name: Test crucible-cli + run: .github/ci.sh test crucible-cli + - shell: bash name: Test crucible-symio (Linux) run: cabal test pkg:crucible-symio @@ -196,6 +204,11 @@ jobs: run: .github/ci.sh test crucible-llvm-syntax if: runner.os == 'Linux' + - shell: bash + name: Test crucible-llvm-cli (Linux) + run: .github/ci.sh test crucible-llvm-cli + if: runner.os == 'Linux' + - shell: bash name: Test crux-llvm (Linux) run: .github/ci.sh test crux-llvm diff --git a/.github/workflows/uc-crux-llvm-lint.yaml b/.github/workflows/uc-crux-llvm-lint.yaml index 437fb3951..6e8e4cae4 100644 --- a/.github/workflows/uc-crux-llvm-lint.yaml +++ b/.github/workflows/uc-crux-llvm-lint.yaml @@ -20,6 +20,8 @@ jobs: https://github.com/ndmitchell/hlint/releases/download/v3.3/hlint-3.3-x86_64-linux.tar.gz tar xvf hlint.tar.gz + (cd crucible-cli/; ../hlint-3.3/hlint app src test) + (cd crucible-llvm-cli/; ../hlint-3.3/hlint app src test) (cd crucible-llvm-syntax/; ../hlint-3.3/hlint src test) cd uc-crux-llvm/ diff --git a/README.md b/README.md index b2cc116d9..d4b0be2ee 100644 --- a/README.md +++ b/README.md @@ -26,12 +26,6 @@ Currently, the repository consists of the following Haskell packages: executing JVM bytecode programs in the Crucible symbolic simulator. * **`crucible-saw`** provides functionality for generating SAW Core terms from Crucible Control-Flow-Graphs. - * **`crucible-syntax`** provides a native S-Expression based concrete - syntax for crucible programs. It is useful for being able to - directly interact with the core Crucible simulator without bringing - in issues related to the translation of other front-ends (e.g. the - LLVM translation). It is primarily intended for the purpose of - writing test cases. * **`crux`** provides common support libraries for running the crucible simulator in a basic "all-at-once" use mode for simulation and verification. This includes most of the setup steps required @@ -69,6 +63,23 @@ In addition, there are the following library/executable packages: false positives and is less useful for full verification than `crux-llvm`. See [the README](./uc-crux-llvm/README.md) for details. +Finally, the following packages are intended primarily for use by Crucible +developers: + + * **`crucible-cli`** provides a CLI for interacting with the Crucible + simulator, via programs written in `crucible-syntax`. + + * **`crucible-llvm-cli`** provides a CLI for interacting with the Crucible + simulator, via programs written in `crucible-syntax` with the extensions + provided by `crucible-llvm{,-syntax}`. + + * **`crucible-syntax`** provides a native S-Expression based concrete + syntax for crucible programs. It is useful for being able to + directly interact with the core Crucible simulator without bringing + in issues related to the translation of other front-ends (e.g. the + LLVM translation). It is primarily intended for the purpose of + writing test cases. + The development of major features and additions to `crucible` is done in separate branches of the repository, all of which are based off `master` and merge back into it when completed. Minor features and bug diff --git a/cabal.project b/cabal.project index 4fe55bd54..0cfa9bba9 100644 --- a/cabal.project +++ b/cabal.project @@ -6,9 +6,11 @@ packages: crucible/ + crucible-cli/ crucible-go/ crucible-jvm/ crucible-llvm/ + crucible-llvm-cli/ crucible-llvm-syntax/ crucible-mir/ crucible-wasm/ diff --git a/crucible-cli/.hlint.yaml b/crucible-cli/.hlint.yaml new file mode 100644 index 000000000..1f24bbe93 --- /dev/null +++ b/crucible-cli/.hlint.yaml @@ -0,0 +1,13 @@ +# HLint's default suggestions are opinionated, so we disable all of them by +# default and enable just a small subset we can agree on. + +- ignore: {} # ignore all +- error: { name: "Fix pragma markup" } +- error: { name: "Redundant as-pattern" } +- error: { name: "Redundant do" } +- error: { name: "Unused LANGUAGE pragma" } +- error: { name: "Used otherwise as a pattern" } +- error: { name: "Use explicit module export list" } +- error: { name: "Use pragma syntax" } +- error: { name: "Use unless" } +- error: { name: "Use when" } diff --git a/crucible-cli/LICENSE b/crucible-cli/LICENSE new file mode 100644 index 000000000..f01e82c96 --- /dev/null +++ b/crucible-cli/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2023 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/crucible-cli/app/Main.hs b/crucible-cli/app/Main.hs new file mode 100644 index 000000000..d2a47b423 --- /dev/null +++ b/crucible-cli/app/Main.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE ImplicitParams #-} + +module Main (main) where + +import Lang.Crucible.Simulator.ExecutionTree (emptyExtensionImpl) + +import Lang.Crucible.Syntax.Concrete (defaultParserHooks) +import Lang.Crucible.Syntax.Overrides (setupOverrides) + +import Lang.Crucible.CLI (SimulateProgramHooks(..), defaultSimulateProgramHooks) +import qualified Lang.Crucible.CLI.Options as Opts + +main :: IO () +main = + do let ?parserHooks = defaultParserHooks + Opts.main "crucible" (\_ -> emptyExtensionImpl) simulationHooks + where + simulationHooks = + defaultSimulateProgramHooks + { setupOverridesHook = setupOverrides + } diff --git a/crucible-cli/crucible-cli.cabal b/crucible-cli/crucible-cli.cabal new file mode 100644 index 000000000..3ed59bd14 --- /dev/null +++ b/crucible-cli/crucible-cli.cabal @@ -0,0 +1,145 @@ +Cabal-version: 2.2 +Name: crucible-cli +Version: 0.1 +Author: Galois Inc. +Maintainer: langston@galois.com +Build-type: Simple +License: BSD-3-Clause +License-file: LICENSE +Category: Language +Synopsis: A library for sharing code between Crucible CLI frontends +-- Description: + +extra-doc-files: README.md +extra-source-files: + test-data/**/*.cbl + test-data/**/*.out.good + +common shared + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 8.10 or earlier: + ghc-options: + -Wall + -Werror=compat-unqualified-imports + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=typed-holes + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unticked-promoted-constructors + -Werror=unused-imports + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc >= 9.2) + ghc-options: + -Werror=ambiguous-fields + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=redundant-bang-patterns + + if impl(ghc >= 9.4) + ghc-options: + -Werror=forall-identifier + -Werror=misplaced-pragmas + -Werror=redundant-strictness-flags + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + + ghc-prof-options: -O2 -fprof-auto-top + default-language: Haskell2010 + +library + import: shared + + build-depends: + base >= 4.13, + containers, + crucible >= 0.1, + crucible-syntax, + lens, + megaparsec >= 7.0 && < 9.7, + mtl, + optparse-applicative, + parameterized-utils >= 0.1.7, + prettyprinter, + text, + what4, + + hs-source-dirs: src + + exposed-modules: + Lang.Crucible.CLI + Lang.Crucible.CLI.Options + +test-suite crucible-cli-tests + import: shared + type: exitcode-stdio-1.0 + main-is: Test.hs + hs-source-dirs: test + other-modules: + Overrides + build-depends: + base, + containers, + crucible >= 0.1, + crucible-cli, + crucible-syntax, + directory, + filepath, + lens, + parameterized-utils >= 0.1.7, + tasty, + tasty-hunit, + tasty-golden, + text, + what4, + +executable crucible + import: shared + hs-source-dirs: app + main-is: Main.hs + build-depends: + base >= 4.13, + crucible, + crucible-cli, + crucible-syntax, diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs new file mode 100644 index 000000000..62c62cdc7 --- /dev/null +++ b/crucible-cli/src/Lang/Crucible/CLI.hs @@ -0,0 +1,280 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.CLI + ( simulateProgramWithExtension + , simulateProgram + , SimulateProgramHooks(..) + , defaultSimulateProgramHooks + , repl + -- * CLI helpers + , CheckCmd(..) + , SimCmd(..) + , ProfCmd(..) + , Command(..) + , execCommand + ) where + +import Control.Lens (view) +import Control.Monad + +import Data.Foldable +import Data.Map (Map) +import Data.Text (Text) +import Data.String (IsString(..)) +import qualified Data.Text.IO as T +import System.IO +import System.Exit +import Text.Megaparsec as MP + +import Data.Parameterized.Nonce +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Some (Some(Some)) + +import qualified Lang.Crucible.CFG.Core as C +import Lang.Crucible.CFG.Extension (IsSyntaxExtension) +import Lang.Crucible.CFG.Reg +import Lang.Crucible.CFG.SSAConversion + +import Lang.Crucible.Syntax.Atoms +import Lang.Crucible.Syntax.Concrete +import Lang.Crucible.Syntax.ExprParse (printSyntaxError) +import Lang.Crucible.Syntax.Prog (doParseCheck, assertNoExterns, assertNoForwardDecs) +import Lang.Crucible.Syntax.SExpr + +import Lang.Crucible.Analysis.Postdom +import Lang.Crucible.Backend +import Lang.Crucible.Backend.Simple +import Lang.Crucible.FunctionHandle +import Lang.Crucible.Simulator +import Lang.Crucible.Simulator.Profiling + +import What4.Config +import What4.Interface (getConfiguration,notPred) +import What4.Expr (ExprBuilder, newExprBuilder, EmptyExprBuilderState(..)) +import What4.FunctionName +import What4.ProgramLoc +import What4.SatResult +import What4.Solver (defaultLogData, runZ3InOverride, z3Options) + +-- | Allows users to hook into the various stages of 'simulateProgram'. +data SimulateProgramHooks ext = SimulateProgramHooks + { setupHook :: + forall p sym rtp a r t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => + sym -> + HandleAllocator -> + OverrideSim p sym ext rtp a r () + -- ^ Override action to execute before simulation. Used by the LLVM + -- frontend to set up the LLVM global memory variable. + , setupOverridesHook :: + forall p sym t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => + sym -> HandleAllocator -> IO [(FnBinding p sym ext,Position)] + -- ^ Action to set up overrides before parsing a program. + , resolveExternsHook :: + forall sym t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => + sym -> Map GlobalName (Some GlobalVar) -> SymGlobalState sym -> IO (SymGlobalState sym) + -- ^ Action to resolve externs before simulating a program. If you do not + -- intend to support externs, this is an appropriate place to error if a + -- program contains one or more externs. + , resolveForwardDeclarationsHook :: + forall p sym t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => + Map FunctionName SomeHandle -> IO (FunctionBindings p sym ext) + -- ^ Action to resolve forward declarations before simulating a program. + -- If you do not intend to support forward declarations, this is an + -- appropriate place to error if a program contains one or more forward + -- declarations. + } + +-- | A sensible default set of hooks for 'simulateProgram' that: +-- +-- * Does nothing before simulation begins (has a no-op 'setupHook'). +-- +-- * Sets up no additional overrides. +-- +-- * Errors out if a program contains one or more forward declarations. +defaultSimulateProgramHooks :: SimulateProgramHooks ext +defaultSimulateProgramHooks = SimulateProgramHooks + { setupHook = \_sym _ha -> pure () + , setupOverridesHook = \_sym _ha -> pure [] + , resolveExternsHook = \_sym externs gst -> + do assertNoExterns externs + pure gst + , resolveForwardDeclarationsHook = \fds -> + do assertNoForwardDecs fds + pure $ FnBindings emptyHandleMap + } + +simulateProgramWithExtension + :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) + => (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) + -> FilePath -- ^ The name of the input (appears in source locations) + -> Text -- ^ The contents of the input + -> Handle -- ^ A handle that will receive the output + -> Maybe Handle -- ^ A handle to receive profiling data output + -> [ConfigDesc] -- ^ Options to install + -> SimulateProgramHooks ext -- ^ Hooks into various parts of the function + -> IO () +simulateProgramWithExtension mkExt fn theInput outh profh opts hooks = + do Some ng <- newIONonceGenerator + ha <- newHandleAllocator + case MP.parse (skipWhitespace *> many (sexp atom) <* eof) fn theInput of + Left err -> + do putStrLn $ errorBundlePretty err + exitFailure + Right v -> + withIONonceGenerator $ \nonceGen -> + do sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonceGen + bak <- newSimpleBackend sym + extendConfig opts (getConfiguration sym) + ovrs <- setupOverridesHook hooks @() sym ha + let hdls = [ (SomeHandle h, p) | (FnBinding h _,p) <- ovrs ] + parseResult <- top ng ha hdls $ prog v + case parseResult of + Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e + Left err -> hPutStrLn outh $ show err + Right (ParsedProgram{ parsedProgCFGs = cs + , parsedProgExterns = externs + , parsedProgForwardDecs = fds + }) -> do + case find isMain cs of + Just (ACFG Ctx.Empty retType mn) -> + do gst <- resolveExternsHook hooks sym externs emptyGlobals + fwdDecFnBindings <- resolveForwardDeclarationsHook hooks fds + let mainHdl = cfgHandle mn + let fns = foldl' (\(FnBindings m) (ACFG _ _ g) -> + case toSSA g of + C.SomeCFG ssa -> + FnBindings $ + insertHandleMap + (cfgHandle g) + (UseCFG ssa (postdomInfo ssa)) + m) + fwdDecFnBindings cs + let ext = mkExt sym + let simCtx = initSimContext bak emptyIntrinsicTypes ha outh fns ext () + let simSt = InitialState simCtx gst defaultAbortHandler retType $ + runOverrideSim retType $ + do mapM_ (registerFnBinding . fst) ovrs + setupHook hooks sym ha + regValue <$> callFnVal (HandleFnVal mainHdl) emptyRegMap + + hPutStrLn outh "==== Begin Simulation ====" + + case profh of + Nothing -> + void $ executeCrucible [] simSt + Just ph -> + do proftab <- newProfilingTable + pf <- profilingFeature proftab profilingEventFilter Nothing + void $ executeCrucible [genericToExecutionFeature pf] simSt + hPutStrLn ph =<< symProUIString "crucibler-prof" fn proftab + + hPutStrLn outh "\n==== Finish Simulation ====" + + getProofObligations bak >>= \case + Nothing -> hPutStrLn outh "==== No proof obligations ====" + Just gs -> + do hPutStrLn outh "==== Proof obligations ====" + forM_ (goalsToList gs) (\g -> + do hPrint outh =<< ppProofObligation sym g + neggoal <- notPred sym (view labeledPred (proofGoal g)) + asms <- assumptionsPred sym (proofAssumptions g) + let bs = [neggoal, asms] + runZ3InOverride sym defaultLogData bs (\case + Sat _ -> hPutStrLn outh "COUNTEREXAMPLE" + Unsat _ -> hPutStrLn outh "PROVED" + Unknown -> hPutStrLn outh "UNKNOWN" + ) + ) + + _ -> hPutStrLn outh "No suitable main function found" + + where + isMain (ACFG _ _ g) = handleName (cfgHandle g) == fromString "main" + +simulateProgram + :: FilePath -- ^ The name of the input (appears in source locations) + -> Text -- ^ The contents of the input + -> Handle -- ^ A handle that will receive the output + -> Maybe Handle -- ^ A handle to receive profiling data output + -> [ConfigDesc] -- ^ Options to install + -> SimulateProgramHooks () -- ^ Hooks into various parts of the function + -> IO () +simulateProgram fn theInput outh profh opts hooks = do + let ?parserHooks = defaultParserHooks + let ext = const emptyExtensionImpl + simulateProgramWithExtension ext fn theInput outh profh opts hooks + +repl :: + (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => + FilePath -> + IO () +repl f = + do putStr "> " + l <- T.getLine + doParseCheck f l True stdout + repl f + +data CheckCmd + = CheckCmd { chkInFile :: FilePath + , chkOutFile :: Maybe FilePath + , chkPrettyPrint :: Bool + } + +data SimCmd + = SimCmd { _simInFile :: FilePath + , _simOutFile :: Maybe FilePath + } + +data ProfCmd + = ProfCmd { _profInFile :: FilePath + , _profOutFile :: FilePath + } + +-- | The 'Command' datatype represents the top-level functionalities of a +-- Crucible CLI frontend. +data Command + = CheckCommand CheckCmd + | SimulateCommand SimCmd + | ProfileCommand ProfCmd + | ReplCommand + +-- | Main entry point for Crucible CLI frontends: the frontends provide +-- language-specific hooks and a 'Command' (usually parsed from the command +-- line), and this function takes care of the rest. +execCommand :: + (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => + (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) -> + SimulateProgramHooks ext -> + Command -> + IO () +execCommand ext simulationHooks = + \case + ReplCommand -> hSetBuffering stdout NoBuffering >> repl "stdin" + + CheckCommand (CheckCmd inputFile out pp) -> + do contents <- T.readFile inputFile + case out of + Nothing -> + doParseCheck inputFile contents pp stdout + Just outputFile -> + withFile outputFile WriteMode (doParseCheck inputFile contents pp) + + SimulateCommand (SimCmd inputFile out) -> + do contents <- T.readFile inputFile + case out of + Nothing -> sim inputFile contents stdout Nothing configOptions simulationHooks + Just outputFile -> + withFile outputFile WriteMode + (\outh -> sim inputFile contents outh Nothing configOptions simulationHooks) + + ProfileCommand (ProfCmd inputFile outputFile) -> + do contents <- T.readFile inputFile + withFile outputFile WriteMode + (\outh -> sim inputFile contents stdout (Just outh) configOptions simulationHooks) + where configOptions = z3Options + sim = simulateProgramWithExtension ext diff --git a/crucible-syntax/crucible-syntax/Main.hs b/crucible-cli/src/Lang/Crucible/CLI/Options.hs similarity index 63% rename from crucible-syntax/crucible-syntax/Main.hs rename to crucible-cli/src/Lang/Crucible/CLI/Options.hs index 11dfb28bb..e178b3b01 100644 --- a/crucible-syntax/crucible-syntax/Main.hs +++ b/crucible-cli/src/Lang/Crucible/CLI/Options.hs @@ -1,16 +1,19 @@ -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ImplicitParams #-} -module Main where +{-# LANGUAGE RankNTypes #-} -import Lang.Crucible.Simulator.ExecutionTree (emptyExtensionImpl) +module Lang.Crucible.CLI.Options (main) where -import Lang.Crucible.Syntax.Concrete (defaultParserHooks) -import Lang.Crucible.Syntax.Prog -import Lang.Crucible.Syntax.Overrides (setupOverrides) +import Lang.Crucible.Backend (IsSymInterface) +import Lang.Crucible.CFG.Extension (IsSyntaxExtension) +import Lang.Crucible.Simulator.ExecutionTree (ExtensionImpl) + +import Lang.Crucible.Syntax.Concrete (ParserHooks) import qualified Options.Applicative as Opt import Options.Applicative ( (<**>) ) +import Lang.Crucible.CLI + file :: String -> Opt.Parser FilePath file which = Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file")) @@ -20,18 +23,18 @@ input = file "input" output :: Opt.Parser FilePath output = file "output" -command :: Opt.Parser Command -command = +command :: String -> Opt.Parser Command +command name = Opt.subparser $ (Opt.command "check" (Opt.info (CheckCommand <$> parseCheck) - (Opt.fullDesc <> Opt.progDesc "Check a file" <> Opt.header "crucibler"))) + (Opt.fullDesc <> Opt.progDesc "Check a file" <> Opt.header name))) <> (Opt.command "simulate" (Opt.info (SimulateCommand <$> simFile) - (Opt.fullDesc <> Opt.progDesc "Simulate a file" <> Opt.header "crucibler"))) + (Opt.fullDesc <> Opt.progDesc "Simulate a file" <> Opt.header name))) <> (Opt.command "profile" (Opt.info (ProfileCommand <$> profFile) - (Opt.fullDesc <> Opt.progDesc "Simulate a file, with profiling" <> Opt.header "crucibler"))) + (Opt.fullDesc <> Opt.progDesc "Simulate a file, with profiling" <> Opt.header name))) <> (Opt.command "repl" (Opt.info (pure ReplCommand) (Opt.fullDesc <> Opt.progDesc "Open a REPL"))) @@ -47,14 +50,14 @@ parseCheck :: Opt.Parser CheckCmd parseCheck = CheckCmd <$> input <*> Opt.optional output <*> Opt.switch (Opt.help "Pretty-print the source file") -main :: IO () -main = +main :: + (?parserHooks :: ParserHooks ext, IsSyntaxExtension ext) => + String -> + (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) -> + SimulateProgramHooks ext -> + IO () +main name ext simulationHooks = do cmd <- Opt.customExecParser prefs info - let ?parserHooks = defaultParserHooks - execCommand (\_ -> emptyExtensionImpl) simulationHooks cmd - where info = Opt.info (command <**> Opt.helper) (Opt.fullDesc) + execCommand ext simulationHooks cmd + where info = Opt.info (command name <**> Opt.helper) (Opt.fullDesc) prefs = Opt.prefs $ Opt.showHelpOnError <> Opt.showHelpOnEmpty - simulationHooks = - defaultSimulateProgramHooks - { setupOverridesHook = setupOverrides - } diff --git a/crucible-cli/test-data/.gitignore b/crucible-cli/test-data/.gitignore new file mode 100644 index 000000000..c08a15c10 --- /dev/null +++ b/crucible-cli/test-data/.gitignore @@ -0,0 +1 @@ +**/*.out diff --git a/crucible-syntax/test-data/declare-tests/main.cbl b/crucible-cli/test-data/declare/main.cbl similarity index 100% rename from crucible-syntax/test-data/declare-tests/main.cbl rename to crucible-cli/test-data/declare/main.cbl diff --git a/crucible-syntax/test-data/declare-tests/main.out.good b/crucible-cli/test-data/declare/main.out.good similarity index 100% rename from crucible-syntax/test-data/declare-tests/main.out.good rename to crucible-cli/test-data/declare/main.out.good diff --git a/crucible-syntax/test-data/extern-tests/main.cbl b/crucible-cli/test-data/extern/main.cbl similarity index 100% rename from crucible-syntax/test-data/extern-tests/main.cbl rename to crucible-cli/test-data/extern/main.cbl diff --git a/crucible-syntax/test-data/extern-tests/main.out.good b/crucible-cli/test-data/extern/main.out.good similarity index 100% rename from crucible-syntax/test-data/extern-tests/main.out.good rename to crucible-cli/test-data/extern/main.out.good diff --git a/crucible-syntax/test-data/simulator-tests/assert.cbl b/crucible-cli/test-data/simulate/assert.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/assert.cbl rename to crucible-cli/test-data/simulate/assert.cbl diff --git a/crucible-syntax/test-data/simulator-tests/assert.out.good b/crucible-cli/test-data/simulate/assert.out.good similarity index 68% rename from crucible-syntax/test-data/simulator-tests/assert.out.good rename to crucible-cli/test-data/simulate/assert.out.good index f1ec06191..59c641f96 100644 --- a/crucible-syntax/test-data/simulator-tests/assert.out.good +++ b/crucible-cli/test-data/simulate/assert.out.good @@ -4,7 +4,7 @@ ==== Proof obligations ==== Prove: - test-data/simulator-tests/assert.cbl:4:5: error: in main + test-data/simulate/assert.cbl:4:5: error: in main x is true cx@0:b COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/assume-merge.cbl b/crucible-cli/test-data/simulate/assume-merge.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/assume-merge.cbl rename to crucible-cli/test-data/simulate/assume-merge.cbl diff --git a/crucible-cli/test-data/simulate/assume-merge.out.good b/crucible-cli/test-data/simulate/assume-merge.out.good new file mode 100644 index 000000000..bee815a53 --- /dev/null +++ b/crucible-cli/test-data/simulate/assume-merge.out.good @@ -0,0 +1,24 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== Proof obligations ==== +Assuming: +* The branch in main from test-data/simulate/assume-merge.cbl:4:5 to test-data/simulate/assume-merge.cbl:6:14 + intLe 0 cx@0:i +* in main test-data/simulate/assume-merge.cbl:6:5: even + eq 0 (intMod cx@0:i 2) +Prove: + test-data/simulate/assume-merge.cbl:12:5: error: in main + oopsie! + false +COUNTEREXAMPLE +Assuming: +* The branch in main from test-data/simulate/assume-merge.cbl:4:5 to test-data/simulate/assume-merge.cbl:9:14 + not (intLe 0 cx@0:i) +* in main test-data/simulate/assume-merge.cbl:9:5: odd + eq 1 (intMod cx@0:i 2) +Prove: + test-data/simulate/assume-merge.cbl:12:5: error: in main + oopsie! + false +COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/assume-merge2.cbl b/crucible-cli/test-data/simulate/assume-merge2.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/assume-merge2.cbl rename to crucible-cli/test-data/simulate/assume-merge2.cbl diff --git a/crucible-syntax/test-data/simulator-tests/assume-merge2.out.good b/crucible-cli/test-data/simulate/assume-merge2.out.good similarity index 57% rename from crucible-syntax/test-data/simulator-tests/assume-merge2.out.good rename to crucible-cli/test-data/simulate/assume-merge2.out.good index 81762afdf..c1183635e 100644 --- a/crucible-syntax/test-data/simulator-tests/assume-merge2.out.good +++ b/crucible-cli/test-data/simulate/assume-merge2.out.good @@ -3,12 +3,12 @@ ==== Finish Simulation ==== ==== Proof obligations ==== Assuming: -* in main test-data/simulator-tests/assume-merge2.cbl:9:5: odd +* in main test-data/simulate/assume-merge2.cbl:9:5: odd not (and (not (intLe 0 cx@0:i)) (not (eq 1 (intMod cx@0:i 2)))) -* in main test-data/simulator-tests/assume-merge2.cbl:6:5: even +* in main test-data/simulate/assume-merge2.cbl:6:5: even not (and (intLe 0 cx@0:i) (not (eq 0 (intMod cx@0:i 2)))) Prove: - test-data/simulator-tests/assume-merge2.cbl:12:5: error: in main + test-data/simulate/assume-merge2.cbl:12:5: error: in main oopsie! false COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/assume.cbl b/crucible-cli/test-data/simulate/assume.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/assume.cbl rename to crucible-cli/test-data/simulate/assume.cbl diff --git a/crucible-syntax/test-data/simulator-tests/assume.out.good b/crucible-cli/test-data/simulate/assume.out.good similarity index 55% rename from crucible-syntax/test-data/simulator-tests/assume.out.good rename to crucible-cli/test-data/simulate/assume.out.good index 4035444c3..1b3076be7 100644 --- a/crucible-syntax/test-data/simulator-tests/assume.out.good +++ b/crucible-cli/test-data/simulate/assume.out.good @@ -3,10 +3,10 @@ ==== Finish Simulation ==== ==== Proof obligations ==== Assuming: -* in main test-data/simulator-tests/assume.cbl:4:5: x is true +* in main test-data/simulate/assume.cbl:4:5: x is true cx@0:b Prove: - test-data/simulator-tests/assume.cbl:5:5: error: in main + test-data/simulate/assume.cbl:5:5: error: in main error statement false COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/bool-expr.cbl b/crucible-cli/test-data/simulate/bool-expr.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/bool-expr.cbl rename to crucible-cli/test-data/simulate/bool-expr.cbl diff --git a/crucible-syntax/test-data/simulator-tests/bool-expr.out.good b/crucible-cli/test-data/simulate/bool-expr.out.good similarity index 100% rename from crucible-syntax/test-data/simulator-tests/bool-expr.out.good rename to crucible-cli/test-data/simulate/bool-expr.out.good diff --git a/crucible-syntax/test-data/simulator-tests/branch.cbl b/crucible-cli/test-data/simulate/branch.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/branch.cbl rename to crucible-cli/test-data/simulate/branch.cbl diff --git a/crucible-syntax/test-data/simulator-tests/branch.out.good b/crucible-cli/test-data/simulate/branch.out.good similarity index 71% rename from crucible-syntax/test-data/simulator-tests/branch.out.good rename to crucible-cli/test-data/simulate/branch.out.good index 7e0d4efd1..f129b0f2d 100644 --- a/crucible-syntax/test-data/simulator-tests/branch.out.good +++ b/crucible-cli/test-data/simulate/branch.out.good @@ -4,7 +4,7 @@ ==== Proof obligations ==== Prove: - test-data/simulator-tests/branch.cbl:11:5: error: in main + test-data/simulate/branch.cbl:11:5: error: in main bogus condition and (eq 42 cx@1:i) cp@0:b COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/bv-expr.cbl b/crucible-cli/test-data/simulate/bv-expr.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/bv-expr.cbl rename to crucible-cli/test-data/simulate/bv-expr.cbl diff --git a/crucible-syntax/test-data/simulator-tests/bv-expr.out.good b/crucible-cli/test-data/simulate/bv-expr.out.good similarity index 82% rename from crucible-syntax/test-data/simulator-tests/bv-expr.out.good rename to crucible-cli/test-data/simulate/bv-expr.out.good index 21ef8c52e..80cfa0b48 100644 --- a/crucible-syntax/test-data/simulator-tests/bv-expr.out.good +++ b/crucible-cli/test-data/simulate/bv-expr.out.good @@ -1,22 +1,22 @@ ==== Begin Simulation ==== === q1 === -let -- test-data/simulator-tests/bv-expr.cbl:11:9 +let -- test-data/simulate/bv-expr.cbl:11:9 v13 = bvAnd cx@0:bv cy@1:bv cz@2:bv in bvSum (bvMul 0x2:[16] cy@1:bv) (bvMul 0x5:[16] cx@0:bv) v13 0xf0:[16] === q2 === bvSum (bvMul 0x3:[16] cz@2:bv) cy@1:bv cx@0:bv === (+ q1 q2) === -let -- test-data/simulator-tests/bv-expr.cbl:11:9 +let -- test-data/simulate/bv-expr.cbl:11:9 v13 = bvAnd cx@0:bv cy@1:bv cz@2:bv in bvSum (bvMul 0x3:[16] cz@2:bv) (bvMul 0x3:[16] cy@1:bv) (bvMul 0x6:[16] cx@0:bv) v13 0xf0:[16] === r1 === -let -- test-data/simulator-tests/bv-expr.cbl:27:8 +let -- test-data/simulate/bv-expr.cbl:27:8 v29 = bvProd cx@0:bv cy@1:bv cz@2:bv in bvXor (bvAnd 0xfff7:[16] cx@0:bv) v29 (bvAnd 0x1:[16] (bvSum (bvMul 0xffff:[16] cx@0:bv))) 0xff0e:[16] === r2 === bvXor cz@2:bv cy@1:bv cx@0:bv === (bv-xor r1 r2) === -let -- test-data/simulator-tests/bv-expr.cbl:27:8 +let -- test-data/simulate/bv-expr.cbl:27:8 v29 = bvProd cx@0:bv cy@1:bv cz@2:bv in bvXor cz@2:bv cy@1:bv (bvAnd 0x8:[16] cx@0:bv) v29 (bvAnd 0x1:[16] (bvSum (bvMul 0xffff:[16] cx@0:bv))) 0xff0e:[16] ====== diff --git a/crucible-syntax/test-data/simulator-tests/calls.cbl b/crucible-cli/test-data/simulate/calls.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/calls.cbl rename to crucible-cli/test-data/simulate/calls.cbl diff --git a/crucible-syntax/test-data/simulator-tests/calls.out.good b/crucible-cli/test-data/simulate/calls.out.good similarity index 71% rename from crucible-syntax/test-data/simulator-tests/calls.out.good rename to crucible-cli/test-data/simulate/calls.out.good index 0616e089e..8387be052 100644 --- a/crucible-syntax/test-data/simulator-tests/calls.out.good +++ b/crucible-cli/test-data/simulate/calls.out.good @@ -6,7 +6,7 @@ intSum cx@0:i 42 ==== Proof obligations ==== Prove: - test-data/simulator-tests/calls.cbl:7:5: error: in main + test-data/simulate/calls.cbl:7:5: error: in main bogus false COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/double-branch.cbl b/crucible-cli/test-data/simulate/double-branch.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/double-branch.cbl rename to crucible-cli/test-data/simulate/double-branch.cbl diff --git a/crucible-cli/test-data/simulate/double-branch.out.good b/crucible-cli/test-data/simulate/double-branch.out.good new file mode 100644 index 000000000..d9c4a9c49 --- /dev/null +++ b/crucible-cli/test-data/simulate/double-branch.out.good @@ -0,0 +1,14 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== Proof obligations ==== +Assuming: +* The branch in main from test-data/simulate/double-branch.cbl:5:5 to test-data/simulate/double-branch.cbl:7:13 + eq 5 ca@0:i +* The branch in main from test-data/simulate/double-branch.cbl:7:5 to test-data/simulate/double-branch.cbl:9:14 + intLe 0 cb@1:i +Prove: + test-data/simulate/double-branch.cbl:9:5: error: in main + assert + eq 5 ca@0:i +PROVED diff --git a/crucible-syntax/test-data/simulator-tests/float-cast.cbl b/crucible-cli/test-data/simulate/float-cast.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/float-cast.cbl rename to crucible-cli/test-data/simulate/float-cast.cbl diff --git a/crucible-syntax/test-data/simulator-tests/float-cast.out.good b/crucible-cli/test-data/simulate/float-cast.out.good similarity index 76% rename from crucible-syntax/test-data/simulator-tests/float-cast.out.good rename to crucible-cli/test-data/simulate/float-cast.out.good index 9457276c4..f8ded6f24 100644 --- a/crucible-syntax/test-data/simulator-tests/float-cast.out.good +++ b/crucible-cli/test-data/simulate/float-cast.out.good @@ -10,13 +10,13 @@ floatToSBV RNE ca@0:f ==== Proof obligations ==== Prove: - test-data/simulator-tests/float-cast.cbl:20:5: error: in main + test-data/simulate/float-cast.cbl:20:5: error: in main bad unsigned round trip eq ca@0:f (bvToFloat RNE (floatToBV RNE ca@0:f)) COUNTEREXAMPLE Prove: - test-data/simulator-tests/float-cast.cbl:24:5: error: in main + test-data/simulate/float-cast.cbl:24:5: error: in main bad signed round trip eq ca@0:f (sbvToFloat RNE (floatToSBV RNE ca@0:f)) COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/from-maybe.cbl b/crucible-cli/test-data/simulate/from-maybe.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/from-maybe.cbl rename to crucible-cli/test-data/simulate/from-maybe.cbl diff --git a/crucible-syntax/test-data/simulator-tests/from-maybe.out.good b/crucible-cli/test-data/simulate/from-maybe.out.good similarity index 59% rename from crucible-syntax/test-data/simulator-tests/from-maybe.out.good rename to crucible-cli/test-data/simulate/from-maybe.out.good index 62875c22c..54ce0cc4e 100644 --- a/crucible-syntax/test-data/simulator-tests/from-maybe.out.good +++ b/crucible-cli/test-data/simulate/from-maybe.out.good @@ -4,13 +4,13 @@ ==== Proof obligations ==== Prove: - test-data/simulator-tests/from-maybe.cbl:11:12: error: in main + test-data/simulate/from-maybe.cbl:11:12: error: in main OK to project z cp@0:b COUNTEREXAMPLE Prove: - test-data/simulator-tests/from-maybe.cbl:12:5: error: in main + test-data/simulate/from-maybe.cbl:12:5: error: in main from-just eq (bogus) false COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/hello.cbl b/crucible-cli/test-data/simulate/hello.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/hello.cbl rename to crucible-cli/test-data/simulate/hello.cbl diff --git a/crucible-syntax/test-data/simulator-tests/hello.out.good b/crucible-cli/test-data/simulate/hello.out.good similarity index 100% rename from crucible-syntax/test-data/simulator-tests/hello.out.good rename to crucible-cli/test-data/simulate/hello.out.good diff --git a/crucible-syntax/test-data/simulator-tests/loop-err.cbl b/crucible-cli/test-data/simulate/loop-err.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/loop-err.cbl rename to crucible-cli/test-data/simulate/loop-err.cbl diff --git a/crucible-cli/test-data/simulate/loop-err.out.good b/crucible-cli/test-data/simulate/loop-err.out.good new file mode 100644 index 000000000..a20940faf --- /dev/null +++ b/crucible-cli/test-data/simulate/loop-err.out.good @@ -0,0 +1,54 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== Proof obligations ==== +Assuming: +* in main test-data/simulate/loop-err.cbl:10:5: nonzero start + not (eq 0 cx@0:i) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:27:12 + eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6) +Prove: + test-data/simulate/loop-err.cbl:27:5: error: in main + oopsie! + false +COUNTEREXAMPLE +Assuming: +* in main test-data/simulate/loop-err.cbl:10:5: nonzero start + not (eq 0 cx@0:i) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:20:13 + not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:27:12 + eq 0 (intMod (intSum (intMul 4 cx@0:i)) 6) +Prove: + test-data/simulate/loop-err.cbl:27:5: error: in main + oopsie! + false +PROVED +Assuming: +* in main test-data/simulate/loop-err.cbl:10:5: nonzero start + not (eq 0 cx@0:i) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:20:13 + not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:20:13 + not (eq 0 (intMod (intSum (intMul 4 cx@0:i)) 6)) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:27:12 + eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6) +Prove: + test-data/simulate/loop-err.cbl:27:5: error: in main + oopsie! + false +PROVED +Assuming: +* in main test-data/simulate/loop-err.cbl:10:5: nonzero start + not (eq 0 cx@0:i) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:20:13 + not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:20:13 + not (eq 0 (intMod (intSum (intMul 4 cx@0:i)) 6)) +* The branch in main from test-data/simulate/loop-err.cbl:17:5 to test-data/simulate/loop-err.cbl:20:13 + not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) +Prove: + test-data/simulate/loop-err.cbl:23:5: error: in main + nonzero + not (intLe (intSum (intMul 8 cx@0:i)) 0) +PROVED diff --git a/crucible-syntax/test-data/simulator-tests/loop.cbl b/crucible-cli/test-data/simulate/loop.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/loop.cbl rename to crucible-cli/test-data/simulate/loop.cbl diff --git a/crucible-syntax/test-data/simulator-tests/loop.out.good b/crucible-cli/test-data/simulate/loop.out.good similarity index 59% rename from crucible-syntax/test-data/simulator-tests/loop.out.good rename to crucible-cli/test-data/simulate/loop.out.good index 4849c0974..5c27a5e15 100644 --- a/crucible-syntax/test-data/simulator-tests/loop.out.good +++ b/crucible-cli/test-data/simulate/loop.out.good @@ -3,10 +3,10 @@ ==== Finish Simulation ==== ==== Proof obligations ==== Assuming: -* in main test-data/simulator-tests/loop.cbl:10:5: nonzero start +* in main test-data/simulate/loop.cbl:10:5: nonzero start not (eq 0 cx@0:i) Prove: - test-data/simulator-tests/loop.cbl:19:5: error: in main + test-data/simulate/loop.cbl:19:5: error: in main nonzero not (intLe (intSum (intMul 8 cx@0:i)) 0) PROVED diff --git a/crucible-syntax/test-data/simulator-tests/mjrty.cbl b/crucible-cli/test-data/simulate/mjrty.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/mjrty.cbl rename to crucible-cli/test-data/simulate/mjrty.cbl diff --git a/crucible-syntax/test-data/simulator-tests/mjrty.out.good b/crucible-cli/test-data/simulate/mjrty.out.good similarity index 76% rename from crucible-syntax/test-data/simulator-tests/mjrty.out.good rename to crucible-cli/test-data/simulate/mjrty.out.good index 284462f06..49dfe9376 100644 --- a/crucible-syntax/test-data/simulator-tests/mjrty.out.good +++ b/crucible-cli/test-data/simulate/mjrty.out.good @@ -3,7 +3,7 @@ Hello! Attempting to prove all outstanding obligations! Proof Succeeded! -test-data/simulator-tests/mjrty.cbl:15:5: error: in main +test-data/simulate/mjrty.cbl:15:5: error: in main MJRTY postcondition diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl b/crucible-cli/test-data/simulate/override-nondet-test-0.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl rename to crucible-cli/test-data/simulate/override-nondet-test-0.cbl diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-0.out.good b/crucible-cli/test-data/simulate/override-nondet-test-0.out.good similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-0.out.good rename to crucible-cli/test-data/simulate/override-nondet-test-0.out.good diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl b/crucible-cli/test-data/simulate/override-nondet-test-1.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl rename to crucible-cli/test-data/simulate/override-nondet-test-1.cbl diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-1.out.good b/crucible-cli/test-data/simulate/override-nondet-test-1.out.good similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-1.out.good rename to crucible-cli/test-data/simulate/override-nondet-test-1.out.good diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl b/crucible-cli/test-data/simulate/override-nondet-test-both.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl rename to crucible-cli/test-data/simulate/override-nondet-test-both.cbl diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good b/crucible-cli/test-data/simulate/override-nondet-test-both.out.good similarity index 53% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good rename to crucible-cli/test-data/simulate/override-nondet-test-both.out.good index 8154b4293..03a2abe54 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good +++ b/crucible-cli/test-data/simulate/override-nondet-test-both.out.good @@ -3,14 +3,14 @@ ==== Finish Simulation ==== ==== Proof obligations ==== Assuming: -* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1 +* in main test-data/simulate/override-nondet-test-both.cbl:6:5: w is 0 or 1 not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))) -* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0 +* The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to after branch 0 not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) * The branch in nondetBranchesTest from after branch 0 to after branch 1 not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)) * The branch in nondetBranchesTest from after branch 1 to default branch - let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + let -- test-data/simulate/override-nondet-test-both.cbl:7:12 v16 = eq 2 cnondetBranchesZ@11:i in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v16 Prove: @@ -19,52 +19,52 @@ Prove: false PROVED Assuming: -* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1 +* in main test-data/simulate/override-nondet-test-both.cbl:6:5: w is 0 or 1 not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))) -* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0 - let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 +* The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to after branch 0 + let -- test-data/simulate/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i - -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + -- test-data/simulate/override-nondet-test-both.cbl:7:12 v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) * The branch in nondetBranchesTest from after branch 0 to second branch - let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5 + let -- test-data/simulate/override-nondet-test-both.cbl:10:5 v43 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) in not v43 -* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch - let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 +* The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to first branch + let -- test-data/simulate/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i - -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + -- test-data/simulate/override-nondet-test-both.cbl:7:12 v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) Prove: - test-data/simulator-tests/override-nondet-test-both.cbl:8:5: error: in main + test-data/simulate/override-nondet-test-both.cbl:8:5: error: in main should be true! let -- after branch 2 v28 = ite (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) cx@1:i cy@2:i in not (and (not (eq v28 cx@1:i)) (not (eq v28 cy@2:i))) PROVED Assuming: -* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1 +* in main test-data/simulate/override-nondet-test-both.cbl:6:5: w is 0 or 1 not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))) -* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0 - let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 +* The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to after branch 0 + let -- test-data/simulate/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i - -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + -- test-data/simulate/override-nondet-test-both.cbl:7:12 v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) * The branch in nondetBranchesTest from after branch 0 to second branch - let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5 + let -- test-data/simulate/override-nondet-test-both.cbl:10:5 v54 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))) in not v54 -* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch - let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 +* The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to first branch + let -- test-data/simulate/override-nondet-test-both.cbl:7:12 v7 = eq 0 cw@0:i - -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12 + -- test-data/simulate/override-nondet-test-both.cbl:7:12 v12 = eq 0 cnondetBranchesZ@11:i in not (and v7 v12 (not (and v7 v12))) Prove: - test-data/simulator-tests/override-nondet-test-both.cbl:9:5: error: in main + test-data/simulate/override-nondet-test-both.cbl:9:5: error: in main should be true! let -- after branch 2 v28 = ite (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) cx@1:i cy@2:i diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl b/crucible-cli/test-data/simulate/override-nondet-test-neither.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl rename to crucible-cli/test-data/simulate/override-nondet-test-neither.cbl diff --git a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good b/crucible-cli/test-data/simulate/override-nondet-test-neither.out.good similarity index 68% rename from crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good rename to crucible-cli/test-data/simulate/override-nondet-test-neither.out.good index 0fc875c03..6892d9f3b 100644 --- a/crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good +++ b/crucible-cli/test-data/simulate/override-nondet-test-neither.out.good @@ -3,14 +3,14 @@ ==== Finish Simulation ==== ==== Proof obligations ==== Assuming: -* in main test-data/simulator-tests/override-nondet-test-neither.cbl:6:5: w is not 0 or 1 +* in main test-data/simulate/override-nondet-test-neither.cbl:6:5: w is not 0 or 1 and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) -* The branch in main from test-data/simulator-tests/override-nondet-test-neither.cbl:7:12 to after branch 0 +* The branch in main from test-data/simulate/override-nondet-test-neither.cbl:7:12 to after branch 0 not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@12:i)) * The branch in nondetBranchesTest from after branch 0 to after branch 1 not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@12:i)) * The branch in nondetBranchesTest from after branch 1 to default branch - let -- test-data/simulator-tests/override-nondet-test-neither.cbl:7:12 + let -- test-data/simulate/override-nondet-test-neither.cbl:7:12 v17 = eq 2 cnondetBranchesZ@12:i in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v17 Prove: diff --git a/crucible-syntax/test-data/simulator-tests/override-test.cbl b/crucible-cli/test-data/simulate/override-test.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-test.cbl rename to crucible-cli/test-data/simulate/override-test.cbl diff --git a/crucible-syntax/test-data/simulator-tests/override-test.out.good b/crucible-cli/test-data/simulate/override-test.out.good similarity index 72% rename from crucible-syntax/test-data/simulator-tests/override-test.out.good rename to crucible-cli/test-data/simulate/override-test.out.good index 550e0fafb..373ffbe22 100644 --- a/crucible-syntax/test-data/simulator-tests/override-test.out.good +++ b/crucible-cli/test-data/simulate/override-test.out.good @@ -4,7 +4,7 @@ ==== Proof obligations ==== Prove: - test-data/simulator-tests/override-test.cbl:7:5: error: in main + test-data/simulate/override-test.cbl:7:5: error: in main should be true! eq (ite cp@0:b cx@1:i cy@2:i) (ite cp@0:b cx@1:i cy@2:i) PROVED diff --git a/crucible-syntax/test-data/simulator-tests/override-test2.cbl b/crucible-cli/test-data/simulate/override-test2.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/override-test2.cbl rename to crucible-cli/test-data/simulate/override-test2.cbl diff --git a/crucible-syntax/test-data/simulator-tests/override-test2.out.good b/crucible-cli/test-data/simulate/override-test2.out.good similarity index 77% rename from crucible-syntax/test-data/simulator-tests/override-test2.out.good rename to crucible-cli/test-data/simulate/override-test2.out.good index 4beed736f..da5a28651 100644 --- a/crucible-syntax/test-data/simulator-tests/override-test2.out.good +++ b/crucible-cli/test-data/simulate/override-test2.out.good @@ -3,7 +3,7 @@ ==== Finish Simulation ==== ==== Proof obligations ==== Assuming: -* The branch in main from test-data/simulator-tests/override-test2.cbl:5:12 to after branch 0 +* The branch in main from test-data/simulate/override-test2.cbl:5:12 to after branch 0 not (eq 1 cx@0:i) * The branch in symbolicBranchesTest from after branch 0 to after branch 1 not (eq 2 cx@0:i) @@ -16,11 +16,11 @@ Prove: COUNTEREXAMPLE Assuming: * The branch in symbolicBranchesTest from after branch 1 to third branch - let -- test-data/simulator-tests/override-test2.cbl:7:5 + let -- test-data/simulate/override-test2.cbl:7:5 v30 = and (not (eq 1 cx@0:i)) (not (eq 2 cx@0:i)) (not (eq 3 cx@0:i)) in not v30 Prove: - test-data/simulator-tests/override-test2.cbl:6:5: error: in main + test-data/simulate/override-test2.cbl:6:5: error: in main bogus! let -- default branch v19 = intSum (intMul 2 cx@0:i) (ite (eq 2 cx@0:i) 0 cy@1:i) diff --git a/crucible-syntax/test-data/simulator-tests/seq-test1.cbl b/crucible-cli/test-data/simulate/seq-test1.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/seq-test1.cbl rename to crucible-cli/test-data/simulate/seq-test1.cbl diff --git a/crucible-syntax/test-data/simulator-tests/seq-test1.out.good b/crucible-cli/test-data/simulate/seq-test1.out.good similarity index 100% rename from crucible-syntax/test-data/simulator-tests/seq-test1.out.good rename to crucible-cli/test-data/simulate/seq-test1.out.good diff --git a/crucible-syntax/test-data/simulator-tests/seq-test2.cbl b/crucible-cli/test-data/simulate/seq-test2.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/seq-test2.cbl rename to crucible-cli/test-data/simulate/seq-test2.cbl diff --git a/crucible-cli/test-data/simulate/seq-test2.out.good b/crucible-cli/test-data/simulate/seq-test2.out.good new file mode 100644 index 000000000..b6f1e062d --- /dev/null +++ b/crucible-cli/test-data/simulate/seq-test2.out.good @@ -0,0 +1,26 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== Proof obligations ==== + +Prove: + test-data/simulate/seq-test2.cbl:29:5: error: in main + head check + eq (ite cb@0:b cx@1:i cz@3:i) (ite cb@0:b cx@1:i cz@3:i) +PROVED +Assuming: +* The branch in main from test-data/simulate/seq-test2.cbl:33:5 to test-data/simulate/seq-test2.cbl:36:13 + cb@0:b +Prove: + test-data/simulate/seq-test2.cbl:38:5: error: in main + tail 2 condition check + cb@0:b +PROVED +Assuming: +* The branch in main from test-data/simulate/seq-test2.cbl:33:5 to test-data/simulate/seq-test2.cbl:45:14 + not cb@0:b +Prove: + test-data/simulate/seq-test2.cbl:45:5: error: in main + tail 2 none check + not cb@0:b +PROVED diff --git a/crucible-syntax/test-data/simulator-tests/seq-test3.cbl b/crucible-cli/test-data/simulate/seq-test3.cbl similarity index 100% rename from crucible-syntax/test-data/simulator-tests/seq-test3.cbl rename to crucible-cli/test-data/simulate/seq-test3.cbl diff --git a/crucible-syntax/test-data/simulator-tests/seq-test3.out.good b/crucible-cli/test-data/simulate/seq-test3.out.good similarity index 62% rename from crucible-syntax/test-data/simulator-tests/seq-test3.out.good rename to crucible-cli/test-data/simulate/seq-test3.out.good index 3b573b12b..2118753b2 100644 --- a/crucible-syntax/test-data/simulator-tests/seq-test3.out.good +++ b/crucible-cli/test-data/simulate/seq-test3.out.good @@ -4,49 +4,49 @@ ==== Proof obligations ==== Prove: - test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq + test-data/simulate/seq-test3.cbl:95:5: error: in eqseq value mismatch! eq (ite cb1@0:b cx@2:i cy@3:i) (ite cb1@0:b cx@2:i cy@3:i) PROVED Prove: - test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq + test-data/simulate/seq-test3.cbl:95:5: error: in eqseq value mismatch! eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i) PROVED Prove: - test-data/simulator-tests/seq-test3.cbl:56:5: error: in main + test-data/simulate/seq-test3.cbl:56:5: error: in main head 1 eq check eq (ite cb1@0:b cx@2:i cy@3:i) (ite cb1@0:b cx@2:i cy@3:i) PROVED Prove: - test-data/simulator-tests/seq-test3.cbl:57:5: error: in main + test-data/simulate/seq-test3.cbl:57:5: error: in main head 1 check eq (ite cb1@0:b cx@2:i cy@3:i) (ite cb1@0:b cx@2:i cy@3:i) PROVED Prove: - test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq + test-data/simulate/seq-test3.cbl:95:5: error: in eqseq value mismatch! eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i) PROVED Prove: - test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq + test-data/simulate/seq-test3.cbl:95:5: error: in eqseq value mismatch! eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i) PROVED Prove: - test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq + test-data/simulate/seq-test3.cbl:95:5: error: in eqseq value mismatch! eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i) PROVED Prove: - test-data/simulator-tests/seq-test3.cbl:95:5: error: in eqseq + test-data/simulate/seq-test3.cbl:95:5: error: in eqseq value mismatch! eq (ite cb2@1:b cz@4:i cw@5:i) (ite cb2@1:b cz@4:i cw@5:i) PROVED diff --git a/crucible-syntax/test/Overrides.hs b/crucible-cli/test/Overrides.hs similarity index 92% rename from crucible-syntax/test/Overrides.hs rename to crucible-cli/test/Overrides.hs index 41e3d1cb0..8175250a3 100644 --- a/crucible-syntax/test/Overrides.hs +++ b/crucible-cli/test/Overrides.hs @@ -1,33 +1,24 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternGuards #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} module Overrides where -import Control.Lens hiding ((:>), Empty) -import Control.Monad (forM_) import Control.Monad.IO.Class -import Control.Monad.ST -import System.IO import Data.Parameterized.Context hiding (view) import What4.Expr.Builder import What4.Interface import What4.ProgramLoc -import What4.SatResult -import What4.Solver.Z3 (runZ3InOverride, z3Options, z3Path) import Lang.Crucible.Backend import Lang.Crucible.Types import Lang.Crucible.FunctionHandle import Lang.Crucible.Simulator -import Lang.Crucible.Simulator.SimError (ppSimError) -- Some overrides for testing purposes. diff --git a/crucible-cli/test/Test.hs b/crucible-cli/test/Test.hs new file mode 100644 index 000000000..dcb9a0d8c --- /dev/null +++ b/crucible-cli/test/Test.hs @@ -0,0 +1,146 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RankNTypes #-} + +module Main (main) where + +import Control.Lens (use) +import Control.Monad.IO.Class (MonadIO(..)) + +import qualified Data.List as List (sort) +import qualified Data.Map as Map +import Data.Map (Map) +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Some (Some(..)) +import qualified Data.Text.IO as T + +import qualified System.FilePath as Path +import qualified System.IO as IO + +import Lang.Crucible.Backend (IsSymInterface) +import Lang.Crucible.FunctionHandle +import Lang.Crucible.Simulator.ExecutionTree +import Lang.Crucible.Simulator.GlobalState (SymGlobalState, insertGlobal) +import Lang.Crucible.Simulator.OverrideSim +import Lang.Crucible.Syntax.Atoms (GlobalName(..)) +import Lang.Crucible.Syntax.Overrides as SyntaxOvrs +import Lang.Crucible.Types +import Lang.Crucible.CFG.Common (GlobalVar(..)) + +import Test.Tasty (defaultMain, TestTree, testGroup) +import Test.Tasty.HUnit (assertFailure) +import Test.Tasty.Golden + +import What4.Config +import What4.FunctionName +import What4.Interface (intLit) +import What4.Solver.Z3 (z3Options) + +import Lang.Crucible.CLI + +import Overrides as TestOvrs + +main :: IO () +main = do + simTests <- findTests "Simulation" "test-data/simulate" testSimulator + let allTests = testGroup "Tests" [resolvedExternTest, resolvedForwardDecTest, simTests] + defaultMain allTests + +findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree +findTests group_name test_dir test_action = + do inputs <- findByExtension [".cbl"] test_dir + return $ testGroup group_name + [ goldenFileTestCase input test_action + | input <- List.sort inputs + ] + +goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree +goldenFileTestCase input test_action = + goldenVsFileDiff + (Path.takeBaseName input) -- test name + (\x y -> ["diff", "-u", x, y]) + goodFile -- golden file path + outFile + (test_action input outFile) -- action whose result is tested + where + outFile = Path.replaceExtension input ".out" + goodFile = Path.replaceExtension input ".out.good" + +testOptions :: [ConfigDesc] +testOptions = z3Options + +testSimulator :: FilePath -> FilePath -> IO () +testSimulator inFile outFile = + do contents <- T.readFile inFile + IO.withFile outFile IO.WriteMode $ \outh -> + simulateProgram inFile contents outh Nothing testOptions $ + defaultSimulateProgramHooks + { setupOverridesHook = \sym ha -> + do os1 <- SyntaxOvrs.setupOverrides sym ha + os2 <- TestOvrs.setupOverrides sym ha + return $ concat [os1,os2] + } + +-- | A basic test that ensures a forward declaration behaves as expected when +-- invoked with an override that is assigned to it after parsing. +resolvedForwardDecTest :: TestTree +resolvedForwardDecTest = + testGroup "Forward declarations" + [ goldenFileTestCase ("test-data" Path. "declare" Path. "main.cbl") $ \mainCbl mainOut -> + IO.withFile mainOut IO.WriteMode $ \outh -> + do mainContents <- T.readFile mainCbl + simulateProgram mainCbl mainContents outh Nothing testOptions $ + defaultSimulateProgramHooks + { resolveForwardDeclarationsHook = resolveForwardDecs + } + ] + where + resolveForwardDecs :: + IsSymInterface sym => + Map FunctionName SomeHandle -> + IO (FunctionBindings p sym ext) + resolveForwardDecs fds + | Just (SomeHandle hdl) <- Map.lookup "foo" fds + , Just Refl <- testEquality (handleArgTypes hdl) Ctx.empty + , Just Refl <- testEquality (handleReturnType hdl) IntegerRepr + = pure $ fnBindingsFromList [FnBinding hdl (UseOverride fooOv)] + + | otherwise + = assertFailure "Could not find @foo function of the appropriate type" + + fooOv :: + IsSymInterface sym => + Override p sym ext EmptyCtx IntegerType + fooOv = mkOverride "foo" $ do + sym <- use (stateContext.ctxSymInterface) + liftIO $ intLit sym 42 + +-- | A basic test that ensures an extern behaves as expected after assigning a +-- value to it after parsing. +resolvedExternTest :: TestTree +resolvedExternTest = + testGroup "Externs" + [ goldenFileTestCase ("test-data" Path. "extern" Path. "main.cbl") $ \mainCbl mainOut -> + IO.withFile mainOut IO.WriteMode $ \outh -> + do mainContents <- T.readFile mainCbl + simulateProgram mainCbl mainContents outh Nothing testOptions $ + defaultSimulateProgramHooks + { resolveExternsHook = resolveExterns + } + ] + where + resolveExterns :: + IsSymInterface sym => + sym -> + Map GlobalName (Some GlobalVar) -> + SymGlobalState sym -> + IO (SymGlobalState sym) + resolveExterns sym externs gst + | Just (Some gv) <- Map.lookup (GlobalName "foo") externs + , Just Refl <- testEquality (globalType gv) IntegerRepr + = do fooVal <- intLit sym 42 + pure $ insertGlobal gv fooVal gst + + | otherwise + = assertFailure "Could not find $$foo extern of the appropriate type" diff --git a/crucible-llvm-cli/.hlint.yaml b/crucible-llvm-cli/.hlint.yaml new file mode 100644 index 000000000..1f24bbe93 --- /dev/null +++ b/crucible-llvm-cli/.hlint.yaml @@ -0,0 +1,13 @@ +# HLint's default suggestions are opinionated, so we disable all of them by +# default and enable just a small subset we can agree on. + +- ignore: {} # ignore all +- error: { name: "Fix pragma markup" } +- error: { name: "Redundant as-pattern" } +- error: { name: "Redundant do" } +- error: { name: "Unused LANGUAGE pragma" } +- error: { name: "Used otherwise as a pattern" } +- error: { name: "Use explicit module export list" } +- error: { name: "Use pragma syntax" } +- error: { name: "Use unless" } +- error: { name: "Use when" } diff --git a/crucible-llvm-cli/LICENSE b/crucible-llvm-cli/LICENSE new file mode 100644 index 000000000..f01e82c96 --- /dev/null +++ b/crucible-llvm-cli/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2023 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/crucible-llvm-cli/app/Main.hs b/crucible-llvm-cli/app/Main.hs new file mode 100644 index 000000000..007d2b3f2 --- /dev/null +++ b/crucible-llvm-cli/app/Main.hs @@ -0,0 +1,8 @@ +module Main (main) where + +import qualified Lang.Crucible.CLI.Options as Opts + +import Lang.Crucible.LLVM.CLI (withLlvmHooks) + +main :: IO () +main = withLlvmHooks (Opts.main "crucible-llvm") diff --git a/crucible-llvm-cli/crucible-llvm-cli.cabal b/crucible-llvm-cli/crucible-llvm-cli.cabal new file mode 100644 index 000000000..53c282bab --- /dev/null +++ b/crucible-llvm-cli/crucible-llvm-cli.cabal @@ -0,0 +1,140 @@ +Cabal-version: 2.2 +Name: crucible-llvm-cli +Version: 0.1 +Author: Galois Inc. +Maintainer: langston@galois.com +Build-type: Simple +License: BSD-3-Clause +License-file: LICENSE +Category: Language +Synopsis: A Crucible CLI frontend for the LLVM language extension +-- Description: + +extra-doc-files: README.md +extra-source-files: + test-data/*.cbl + test-data/*.out.good + +common shared + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 8.10 or earlier: + ghc-options: + -Wall + -Werror=compat-unqualified-imports + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=typed-holes + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unticked-promoted-constructors + -Werror=unused-imports + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc >= 9.2) + ghc-options: + -Werror=ambiguous-fields + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=redundant-bang-patterns + + if impl(ghc >= 9.4) + ghc-options: + -Werror=forall-identifier + -Werror=misplaced-pragmas + -Werror=redundant-strictness-flags + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + + ghc-prof-options: -O2 -fprof-auto-top + default-language: Haskell2010 + +library + import: shared + + build-depends: + base >= 4.13, + containers, + crucible >= 0.1, + crucible-cli, + crucible-llvm, + crucible-llvm-syntax, + crucible-syntax, + mtl, + parameterized-utils >= 0.1.7, + prettyprinter, + text, + what4, + + hs-source-dirs: src + + exposed-modules: + Lang.Crucible.LLVM.CLI + +test-suite crucible-llvm-cli-tests + import: shared + type: exitcode-stdio-1.0 + main-is: Test.hs + hs-source-dirs: test + build-depends: + base, + containers, + crucible >= 0.1, + crucible-cli, + crucible-llvm-cli, + crucible-llvm-syntax, + crucible-syntax, + filepath, + parameterized-utils >= 0.1.7, + tasty, + tasty-golden, + text, + what4 + +executable crucible-llvm + import: shared + hs-source-dirs: app + main-is: Main.hs + build-depends: + base >= 4.13, + crucible-cli, + crucible-llvm-cli, diff --git a/crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs b/crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs new file mode 100644 index 000000000..83dd23358 --- /dev/null +++ b/crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} + +module Lang.Crucible.LLVM.CLI + ( withLlvmHooks + ) where + +import Control.Monad.IO.Class (liftIO) + +import Data.Parameterized.NatRepr (knownNat) + +import Lang.Crucible.Backend (IsSymInterface) +import Lang.Crucible.FunctionHandle (newHandleAllocator) +import Lang.Crucible.Simulator.ExecutionTree (ExtensionImpl) +import Lang.Crucible.Simulator.OverrideSim (writeGlobal) + +import Lang.Crucible.CLI (SimulateProgramHooks(..), defaultSimulateProgramHooks) + +import Lang.Crucible.Syntax.Concrete (ParserHooks) +import Lang.Crucible.Syntax.Overrides (setupOverrides) + +import Lang.Crucible.LLVM (llvmExtensionImpl) +import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian)) +import Lang.Crucible.LLVM.Extension (LLVM) +import Lang.Crucible.LLVM.MemModel (HasPtrWidth, defaultMemOptions, emptyMem, mkMemVar) + +import Lang.Crucible.LLVM.Syntax (llvmParserHooks) +import Lang.Crucible.LLVM.Syntax.TypeAlias (typeAliasParserHooks, x86_64LinuxTypes) + +-- | Small helper for providing LLVM language-specific hooks, e.g., for use with +-- 'Lang.Crucible.CLI.execCommand'. +withLlvmHooks :: + (forall w. + (HasPtrWidth w, ?parserHooks :: ParserHooks LLVM) => + (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym LLVM) -> + SimulateProgramHooks LLVM -> + IO a) -> + IO a +withLlvmHooks k = do + ha <- newHandleAllocator + mvar <- mkMemVar "llvm_memory" ha + let ?ptrWidth = knownNat @64 + let ?parserHooks = llvmParserHooks (typeAliasParserHooks x86_64LinuxTypes) mvar + let simulationHooks = + defaultSimulateProgramHooks + { setupHook = \_sym _ha -> do + mem <- liftIO (emptyMem LittleEndian) + writeGlobal mvar mem + , setupOverridesHook = setupOverrides + } + let ext _ = let ?recordLLVMAnnotation = \_ _ _ -> pure () + in llvmExtensionImpl defaultMemOptions + k ext simulationHooks \ No newline at end of file diff --git a/crucible-llvm-cli/test-data/.gitignore b/crucible-llvm-cli/test-data/.gitignore new file mode 100644 index 000000000..f47cb2045 --- /dev/null +++ b/crucible-llvm-cli/test-data/.gitignore @@ -0,0 +1 @@ +*.out diff --git a/crucible-llvm-syntax/test-data/simulate/ptr.cbl b/crucible-llvm-cli/test-data/ptr.cbl similarity index 100% rename from crucible-llvm-syntax/test-data/simulate/ptr.cbl rename to crucible-llvm-cli/test-data/ptr.cbl diff --git a/crucible-llvm-syntax/test-data/simulate/ptr.out.good b/crucible-llvm-cli/test-data/ptr.out.good similarity index 100% rename from crucible-llvm-syntax/test-data/simulate/ptr.out.good rename to crucible-llvm-cli/test-data/ptr.out.good diff --git a/crucible-llvm-cli/test/Test.hs b/crucible-llvm-cli/test/Test.hs new file mode 100644 index 000000000..27f5b774e --- /dev/null +++ b/crucible-llvm-cli/test/Test.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} + +module Main (main) where + +import Data.List (sort) +import Data.Text.IO qualified as T +import System.FilePath +import System.IO + +import Test.Tasty (defaultMain, TestTree, testGroup) +import Test.Tasty.Golden + +import What4.Solver.Z3 (z3Options) + +import Lang.Crucible.CLI (simulateProgramWithExtension) + +import Lang.Crucible.LLVM.CLI (withLlvmHooks) + +main :: IO () +main = do + simTests <- findTests "LLVM simulation" "test-data" testSimulator + defaultMain simTests + +findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree +findTests groupName testDir testAction = + do inputs <- findByExtension [".cbl"] testDir + return $ testGroup groupName + [ goldenFileTestCase input testAction + | input <- sort inputs + ] + +goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree +goldenFileTestCase input testAction = + goldenVsFileDiff + (takeBaseName input) -- test name + (\x y -> ["diff", "-u", x, y]) + goodFile -- golden file path + outFile + (testAction input outFile) -- action whose result is tested + where + outFile = replaceExtension input ".out" + goodFile = replaceExtension input ".out.good" + +testSimulator :: FilePath -> FilePath -> IO () +testSimulator inFile outFile = + do contents <- T.readFile inFile + withFile outFile WriteMode $ \outh -> + withLlvmHooks $ \ext hooks -> + simulateProgramWithExtension ext inFile contents outh Nothing z3Options hooks diff --git a/crucible-llvm-syntax/app/Main.hs b/crucible-llvm-syntax/app/Main.hs deleted file mode 100644 index 4aaf559b6..000000000 --- a/crucible-llvm-syntax/app/Main.hs +++ /dev/null @@ -1,82 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TypeApplications #-} - -module Main (main) where - -import Control.Monad.IO.Class (liftIO) - -import Data.Parameterized.NatRepr (knownNat) - -import Lang.Crucible.Simulator.OverrideSim (writeGlobal) -import Lang.Crucible.FunctionHandle (newHandleAllocator) - -import Lang.Crucible.Syntax.Prog -import Lang.Crucible.Syntax.Overrides (setupOverrides) - -import Lang.Crucible.LLVM (llvmExtensionImpl) -import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian)) -import Lang.Crucible.LLVM.MemModel (defaultMemOptions, emptyMem, mkMemVar) - -import Lang.Crucible.LLVM.Syntax (emptyParserHooks, llvmParserHooks) - -import qualified Options.Applicative as Opt -import Options.Applicative ( (<**>) ) - -file :: String -> Opt.Parser FilePath -file which = Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file")) - -input :: Opt.Parser FilePath -input = file "input" - -output :: Opt.Parser FilePath -output = file "output" - -command :: Opt.Parser Command -command = - Opt.subparser $ - (Opt.command "check" - (Opt.info (CheckCommand <$> parseCheck) - (Opt.fullDesc <> Opt.progDesc "Check a file" <> Opt.header "crucibler"))) - <> (Opt.command "simulate" - (Opt.info (SimulateCommand <$> simFile) - (Opt.fullDesc <> Opt.progDesc "Simulate a file" <> Opt.header "crucibler"))) - <> (Opt.command "profile" - (Opt.info (ProfileCommand <$> profFile) - (Opt.fullDesc <> Opt.progDesc "Simulate a file, with profiling" <> Opt.header "crucibler"))) - <> (Opt.command "repl" - (Opt.info (pure ReplCommand) (Opt.fullDesc <> Opt.progDesc "Open a REPL"))) - -profFile :: Opt.Parser ProfCmd -profFile = - ProfCmd <$> input <*> output - -simFile :: Opt.Parser SimCmd -simFile = - SimCmd <$> input <*> Opt.optional output - -parseCheck :: Opt.Parser CheckCmd -parseCheck = - CheckCmd <$> input <*> Opt.optional output <*> Opt.switch (Opt.help "Pretty-print the source file") - -main :: IO () -main = - do cmd <- Opt.customExecParser prefs info - ha <- newHandleAllocator - mvar <- mkMemVar "llvm_memory" ha - let ?ptrWidth = knownNat @64 - let ?parserHooks = llvmParserHooks emptyParserHooks mvar - let simulationHooks = - defaultSimulateProgramHooks - { setupHook = \_sym _ha -> do - mem <- liftIO (emptyMem LittleEndian) - writeGlobal mvar mem - , setupOverridesHook = setupOverrides - } - let ext _ = let ?recordLLVMAnnotation = \_ _ _ -> pure () - in llvmExtensionImpl defaultMemOptions - execCommand ext simulationHooks cmd - where info = Opt.info (command <**> Opt.helper) (Opt.fullDesc) - prefs = Opt.prefs $ Opt.showHelpOnError <> Opt.showHelpOnEmpty diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal index dfc8ea5b2..e5fa453b0 100644 --- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal +++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal @@ -126,19 +126,3 @@ test-suite crucible-llvm-syntax-tests tasty, tasty-golden, text, - what4 - -executable exec-crucible-llvm - import: shared - hs-source-dirs: app - main-is: Main.hs - build-depends: - base >= 4.13, - crucible, - crucible-syntax, - crucible-llvm, - crucible-llvm-syntax, - optparse-applicative, - parameterized-utils, - text, - what4 diff --git a/crucible-llvm-syntax/test-data/parse/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl similarity index 100% rename from crucible-llvm-syntax/test-data/parse/ptr.cbl rename to crucible-llvm-syntax/test-data/ptr.cbl diff --git a/crucible-llvm-syntax/test-data/parse/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good similarity index 98% rename from crucible-llvm-syntax/test-data/parse/ptr.out.good rename to crucible-llvm-syntax/test-data/ptr.out.good index 1aaf92ffa..691192e90 100644 --- a/crucible-llvm-syntax/test-data/parse/ptr.out.good +++ b/crucible-llvm-syntax/test-data/ptr.out.good @@ -52,7 +52,7 @@ test-ptr % 12:13 $11 = bVLit(64, BV 1) % 13:12 - $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/parse/ptr.cbl:13:12 + $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/ptr.cbl:13:12 % 15:16 $13 = bVLit(8, BV 255) % 16:13 diff --git a/crucible-llvm-syntax/test-data/parse/type.cbl b/crucible-llvm-syntax/test-data/type.cbl similarity index 100% rename from crucible-llvm-syntax/test-data/parse/type.cbl rename to crucible-llvm-syntax/test-data/type.cbl diff --git a/crucible-llvm-syntax/test-data/parse/type.out.good b/crucible-llvm-syntax/test-data/type.out.good similarity index 100% rename from crucible-llvm-syntax/test-data/parse/type.out.good rename to crucible-llvm-syntax/test-data/type.out.good diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs index 6ec85c4a5..bcefa92c1 100644 --- a/crucible-llvm-syntax/test/Test.hs +++ b/crucible-llvm-syntax/test/Test.hs @@ -6,7 +6,6 @@ module Main (main) where -import Control.Monad.IO.Class (liftIO) import Data.List (sort) import Data.Text.IO qualified as T import System.FilePath @@ -17,27 +16,21 @@ import Test.Tasty.Golden import Data.Parameterized.NatRepr (knownNat) -import What4.Solver.Z3 (z3Options) - -import Lang.Crucible.Simulator.OverrideSim (writeGlobal) import Lang.Crucible.FunctionHandle (newHandleAllocator) -import Lang.Crucible.LLVM (llvmExtensionImpl) -import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian)) import Lang.Crucible.LLVM.Extension (LLVM) -import Lang.Crucible.LLVM.MemModel (defaultMemOptions, emptyMem, mkMemVar) +import Lang.Crucible.LLVM.MemModel (mkMemVar) import Lang.Crucible.Syntax.Concrete (ParserHooks) -import Lang.Crucible.Syntax.Prog (SimulateProgramHooks(setupHook), defaultSimulateProgramHooks, doParseCheck, simulateProgramWithExtension) +import Lang.Crucible.Syntax.Prog (doParseCheck) -import Lang.Crucible.LLVM.Syntax (emptyParserHooks, llvmParserHooks) +import Lang.Crucible.LLVM.Syntax (llvmParserHooks) import Lang.Crucible.LLVM.Syntax.TypeAlias (typeAliasParserHooks, x86_64LinuxTypes) main :: IO () main = do - parseTests <- findTests "Parse tests" "test-data/parse" testParser - simTests <- findTests "LLVM simulation" "test-data/simulate" testSimulator - defaultMain $ testGroup "Tests" [parseTests, simTests] + parseTests <- findTests "Parse tests" "test-data" testParser + defaultMain parseTests findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree findTests groupName testDir testAction = @@ -73,23 +66,3 @@ testParser inFile outFile = hooks <- parserHooks let ?parserHooks = hooks withFile outFile WriteMode $ doParseCheck inFile contents True - -testSimulator :: FilePath -> FilePath -> IO () -testSimulator inFile outFile = - do contents <- T.readFile inFile - ha <- newHandleAllocator - mvar <- mkMemVar "llvm_memory" ha - let ?ptrWidth = knownNat @64 - let ?parserHooks = llvmParserHooks emptyParserHooks mvar - withFile outFile WriteMode $ \outh -> do - let ext _ = - let ?recordLLVMAnnotation = \_ _ _ -> pure () - in llvmExtensionImpl defaultMemOptions - simulateProgramWithExtension ext inFile contents outh Nothing z3Options $ - defaultSimulateProgramHooks - { setupHook = \_sym _ha -> do - mem <- liftIO (emptyMem LittleEndian) - writeGlobal mvar mem - } - - diff --git a/crucible-syntax/crucible-syntax.cabal b/crucible-syntax/crucible-syntax.cabal index 5094c3cc7..78463b867 100644 --- a/crucible-syntax/crucible-syntax.cabal +++ b/crucible-syntax/crucible-syntax.cabal @@ -1,19 +1,93 @@ +Cabal-version: 2.2 Name: crucible-syntax Version: 0.3 Author: Galois Inc. Maintainer: dtc@galois.com Build-type: Simple -License: BSD3 +License: BSD-3-Clause License-file: LICENSE -Cabal-version: >= 1.9.2 Category: Language Synopsis: A syntax for reading and writing Crucible control-flow graphs Description: This package provides a syntax for directly constructing Crucible control-flow graphs, as well as for observing them. +extra-doc-files: README.txt extra-source-files: +common shared + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 8.10 or earlier: + ghc-options: + -Wall + -Werror=compat-unqualified-imports + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=typed-holes + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unticked-promoted-constructors + -Werror=unused-imports + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc >= 9.2) + ghc-options: + -Werror=ambiguous-fields + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=redundant-bang-patterns + + if impl(ghc >= 9.4) + ghc-options: + -Werror=forall-identifier + -Werror=misplaced-pragmas + -Werror=redundant-strictness-flags + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + + ghc-prof-options: -O2 -fprof-auto-top + default-language: Haskell2010 + library build-depends: base >= 4.9, @@ -37,35 +111,17 @@ library Lang.Crucible.Syntax.Concrete Lang.Crucible.Syntax.SExpr Lang.Crucible.Syntax.Overrides - Lang.Crucible.Syntax.Prog Lang.Crucible.Syntax.ExprParse + Lang.Crucible.Syntax.Prog ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns ghc-prof-options: -O2 -fprof-auto-top - -executable crucibler - build-depends: - base >= 4.9 && < 4.19, - crucible, - crucible-syntax, - optparse-applicative, - text, - what4 - - ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns - - main-is: Main.hs - hs-source-dirs: - crucible-syntax - - test-suite crucible-syntax-tests + import: shared type: exitcode-stdio-1.0 main-is: Tests.hs hs-source-dirs: test - other-modules: - Overrides build-depends: base, containers, @@ -73,7 +129,6 @@ test-suite crucible-syntax-tests crucible-syntax, directory, filepath, - lens, megaparsec, parameterized-utils, tasty, diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs index 6d68eb462..1d76bd6eb 100644 --- a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs +++ b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs @@ -6,18 +6,9 @@ {-# LANGUAGE TypeOperators #-} module Lang.Crucible.Syntax.Prog - ( doParseCheck - , simulateProgramWithExtension - , simulateProgram - , SimulateProgramHooks(..) - , defaultSimulateProgramHooks - , repl - -- * CLI helpers - , CheckCmd(..) - , SimCmd(..) - , ProfCmd(..) - , Command(..) - , execCommand + ( assertNoExterns + , assertNoForwardDecs + , doParseCheck ) where import Control.Lens (view) @@ -62,6 +53,17 @@ import What4.ProgramLoc import What4.SatResult import What4.Solver (defaultLogData, runZ3InOverride, z3Options) +assertNoExterns :: Map GlobalName (Some GlobalVar) -> IO () +assertNoExterns externs = + unless (Map.null externs) $ + do putStrLn "Externs not currently supported" + exitFailure + +assertNoForwardDecs :: Map FunctionName SomeHandle -> IO () +assertNoForwardDecs fds = + unless (Map.null fds) $ + do putStrLn "Forward declarations not currently supported" + exitFailure -- | The main loop body, useful for both the program and for testing. doParseCheck @@ -98,227 +100,3 @@ doParseCheck fn theInput pprint outh = hPutStrLn outh $ show $ cfgHandle theCfg hPutStrLn outh $ show $ C.ppCFG' True (postdomInfo ssa) ssa --- | Allows users to hook into the various stages of 'simulateProgram'. -data SimulateProgramHooks ext = SimulateProgramHooks - { setupHook :: - forall p sym rtp a r t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => - sym -> - HandleAllocator -> - OverrideSim p sym ext rtp a r () - -- ^ Override action to execute before simulation. Used by the LLVM - -- frontend to set up the LLVM global memory variable. - , setupOverridesHook :: - forall p sym t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => - sym -> HandleAllocator -> IO [(FnBinding p sym ext,Position)] - -- ^ Action to set up overrides before parsing a program. - , resolveExternsHook :: - forall sym t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => - sym -> Map GlobalName (Some GlobalVar) -> SymGlobalState sym -> IO (SymGlobalState sym) - -- ^ Action to resolve externs before simulating a program. If you do not - -- intend to support externs, this is an appropriate place to error if a - -- program contains one or more externs. - , resolveForwardDeclarationsHook :: - forall p sym t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) => - Map FunctionName SomeHandle -> IO (FunctionBindings p sym ext) - -- ^ Action to resolve forward declarations before simulating a program. - -- If you do not intend to support forward declarations, this is an - -- appropriate place to error if a program contains one or more forward - -- declarations. - } - --- | A sensible default set of hooks for 'simulateProgram' that: --- --- * Does nothing before simulation begins (has a no-op 'setupHook'). --- --- * Sets up no additional overrides. --- --- * Errors out if a program contains one or more forward declarations. -defaultSimulateProgramHooks :: SimulateProgramHooks ext -defaultSimulateProgramHooks = SimulateProgramHooks - { setupHook = \_sym _ha -> pure () - , setupOverridesHook = \_sym _ha -> pure [] - , resolveExternsHook = \_sym externs gst -> - do assertNoExterns externs - pure gst - , resolveForwardDeclarationsHook = \fds -> - do assertNoForwardDecs fds - pure $ FnBindings emptyHandleMap - } - -assertNoExterns :: Map GlobalName (Some GlobalVar) -> IO () -assertNoExterns externs = - unless (Map.null externs) $ - do putStrLn "Externs not currently supported" - exitFailure - -assertNoForwardDecs :: Map FunctionName SomeHandle -> IO () -assertNoForwardDecs fds = - unless (Map.null fds) $ - do putStrLn "Forward declarations not currently supported" - exitFailure - -simulateProgramWithExtension - :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) - => (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) - -> FilePath -- ^ The name of the input (appears in source locations) - -> Text -- ^ The contents of the input - -> Handle -- ^ A handle that will receive the output - -> Maybe Handle -- ^ A handle to receive profiling data output - -> [ConfigDesc] -- ^ Options to install - -> SimulateProgramHooks ext -- ^ Hooks into various parts of the function - -> IO () -simulateProgramWithExtension mkExt fn theInput outh profh opts hooks = - do Some ng <- newIONonceGenerator - ha <- newHandleAllocator - case MP.parse (skipWhitespace *> many (sexp atom) <* eof) fn theInput of - Left err -> - do putStrLn $ errorBundlePretty err - exitFailure - Right v -> - withIONonceGenerator $ \nonceGen -> - do sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonceGen - bak <- newSimpleBackend sym - extendConfig opts (getConfiguration sym) - ovrs <- setupOverridesHook hooks @() sym ha - let hdls = [ (SomeHandle h, p) | (FnBinding h _,p) <- ovrs ] - parseResult <- top ng ha hdls $ prog v - case parseResult of - Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e - Left err -> hPutStrLn outh $ show err - Right (ParsedProgram{ parsedProgCFGs = cs - , parsedProgExterns = externs - , parsedProgForwardDecs = fds - }) -> do - case find isMain cs of - Just (ACFG Ctx.Empty retType mn) -> - do gst <- resolveExternsHook hooks sym externs emptyGlobals - fwdDecFnBindings <- resolveForwardDeclarationsHook hooks fds - let mainHdl = cfgHandle mn - let fns = foldl' (\(FnBindings m) (ACFG _ _ g) -> - case toSSA g of - C.SomeCFG ssa -> - FnBindings $ - insertHandleMap - (cfgHandle g) - (UseCFG ssa (postdomInfo ssa)) - m) - fwdDecFnBindings cs - let ext = mkExt sym - let simCtx = initSimContext bak emptyIntrinsicTypes ha outh fns ext () - let simSt = InitialState simCtx gst defaultAbortHandler retType $ - runOverrideSim retType $ - do mapM_ (registerFnBinding . fst) ovrs - setupHook hooks sym ha - regValue <$> callFnVal (HandleFnVal mainHdl) emptyRegMap - - hPutStrLn outh "==== Begin Simulation ====" - - case profh of - Nothing -> - void $ executeCrucible [] simSt - Just ph -> - do proftab <- newProfilingTable - pf <- profilingFeature proftab profilingEventFilter Nothing - void $ executeCrucible [genericToExecutionFeature pf] simSt - hPutStrLn ph =<< symProUIString "crucibler-prof" fn proftab - - hPutStrLn outh "\n==== Finish Simulation ====" - - getProofObligations bak >>= \case - Nothing -> hPutStrLn outh "==== No proof obligations ====" - Just gs -> - do hPutStrLn outh "==== Proof obligations ====" - forM_ (goalsToList gs) (\g -> - do hPrint outh =<< ppProofObligation sym g - neggoal <- notPred sym (view labeledPred (proofGoal g)) - asms <- assumptionsPred sym (proofAssumptions g) - let bs = [neggoal, asms] - runZ3InOverride sym defaultLogData bs (\case - Sat _ -> hPutStrLn outh "COUNTEREXAMPLE" - Unsat _ -> hPutStrLn outh "PROVED" - Unknown -> hPutStrLn outh "UNKNOWN" - ) - ) - - _ -> hPutStrLn outh "No suitable main function found" - - where - isMain (ACFG _ _ g) = handleName (cfgHandle g) == fromString "main" - -simulateProgram - :: FilePath -- ^ The name of the input (appears in source locations) - -> Text -- ^ The contents of the input - -> Handle -- ^ A handle that will receive the output - -> Maybe Handle -- ^ A handle to receive profiling data output - -> [ConfigDesc] -- ^ Options to install - -> SimulateProgramHooks () -- ^ Hooks into various parts of the function - -> IO () -simulateProgram fn theInput outh profh opts hooks = do - let ?parserHooks = defaultParserHooks - let ext = const emptyExtensionImpl - simulateProgramWithExtension ext fn theInput outh profh opts hooks - -repl :: - (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => - FilePath -> - IO () -repl f = - do putStr "> " - l <- T.getLine - doParseCheck f l True stdout - repl f - -data CheckCmd - = CheckCmd { chkInFile :: FilePath - , chkOutFile :: Maybe FilePath - , chkPrettyPrint :: Bool - } - -data SimCmd - = SimCmd { _simInFile :: FilePath - , _simOutFile :: Maybe FilePath - } - -data ProfCmd - = ProfCmd { _profInFile :: FilePath - , _profOutFile :: FilePath - } - -data Command - = CheckCommand CheckCmd - | SimulateCommand SimCmd - | ProfileCommand ProfCmd - | ReplCommand - -execCommand :: - (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => - (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) -> - SimulateProgramHooks ext -> - Command -> - IO () -execCommand ext simulationHooks = - \case - ReplCommand -> hSetBuffering stdout NoBuffering >> repl "stdin" - - CheckCommand (CheckCmd inputFile out pp) -> - do contents <- T.readFile inputFile - case out of - Nothing -> - doParseCheck inputFile contents pp stdout - Just outputFile -> - withFile outputFile WriteMode (doParseCheck inputFile contents pp) - - SimulateCommand (SimCmd inputFile out) -> - do contents <- T.readFile inputFile - case out of - Nothing -> sim inputFile contents stdout Nothing configOptions simulationHooks - Just outputFile -> - withFile outputFile WriteMode - (\outh -> sim inputFile contents outh Nothing configOptions simulationHooks) - - ProfileCommand (ProfCmd inputFile outputFile) -> - do contents <- T.readFile inputFile - withFile outputFile WriteMode - (\outh -> sim inputFile contents stdout (Just outh) configOptions simulationHooks) - where configOptions = z3Options - sim = simulateProgramWithExtension ext diff --git a/crucible-syntax/test-data/parser-tests/all-term-stmt.cbl b/crucible-syntax/test-data/all-term-stmt.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/all-term-stmt.cbl rename to crucible-syntax/test-data/all-term-stmt.cbl diff --git a/crucible-syntax/test-data/parser-tests/all-term-stmt.out.good b/crucible-syntax/test-data/all-term-stmt.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/all-term-stmt.out.good rename to crucible-syntax/test-data/all-term-stmt.out.good diff --git a/crucible-syntax/test-data/parser-tests/assert.cbl b/crucible-syntax/test-data/assert.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/assert.cbl rename to crucible-syntax/test-data/assert.cbl diff --git a/crucible-syntax/test-data/parser-tests/assert.out.good b/crucible-syntax/test-data/assert.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/assert.out.good rename to crucible-syntax/test-data/assert.out.good diff --git a/crucible-syntax/test-data/parser-tests/bool.cbl b/crucible-syntax/test-data/bool.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/bool.cbl rename to crucible-syntax/test-data/bool.cbl diff --git a/crucible-syntax/test-data/parser-tests/bool.out.good b/crucible-syntax/test-data/bool.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/bool.out.good rename to crucible-syntax/test-data/bool.out.good diff --git a/crucible-syntax/test-data/parser-tests/breakpoints.cbl b/crucible-syntax/test-data/breakpoints.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/breakpoints.cbl rename to crucible-syntax/test-data/breakpoints.cbl diff --git a/crucible-syntax/test-data/parser-tests/breakpoints.out.good b/crucible-syntax/test-data/breakpoints.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/breakpoints.out.good rename to crucible-syntax/test-data/breakpoints.out.good diff --git a/crucible-syntax/test-data/parser-tests/busted.cbl b/crucible-syntax/test-data/busted.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/busted.cbl rename to crucible-syntax/test-data/busted.cbl diff --git a/crucible-syntax/test-data/busted.out.good b/crucible-syntax/test-data/busted.out.good new file mode 100644 index 000000000..d24c63f35 --- /dev/null +++ b/crucible-syntax/test-data/busted.out.good @@ -0,0 +1,4 @@ +(defun @f () Unit + (start foo: (let foo (the Integer #f)) (let x ()) (return x))) + +At test-data/busted.cbl:3:27, expected a IntegerRepr rather than a BoolRepr but got #f diff --git a/crucible-syntax/test-data/parser-tests/bv.cbl b/crucible-syntax/test-data/bv.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/bv.cbl rename to crucible-syntax/test-data/bv.cbl diff --git a/crucible-syntax/test-data/parser-tests/bv.out.good b/crucible-syntax/test-data/bv.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/bv.out.good rename to crucible-syntax/test-data/bv.out.good diff --git a/crucible-syntax/test-data/parser-tests/cfg.cbl b/crucible-syntax/test-data/cfg.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/cfg.cbl rename to crucible-syntax/test-data/cfg.cbl diff --git a/crucible-syntax/test-data/parser-tests/cfg.out.good b/crucible-syntax/test-data/cfg.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/cfg.out.good rename to crucible-syntax/test-data/cfg.out.good diff --git a/crucible-syntax/test-data/parser-tests/empty.cbl b/crucible-syntax/test-data/empty.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/empty.cbl rename to crucible-syntax/test-data/empty.cbl diff --git a/crucible-syntax/test-data/parser-tests/empty.out.good b/crucible-syntax/test-data/empty.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/empty.out.good rename to crucible-syntax/test-data/empty.out.good diff --git a/crucible-syntax/test-data/parser-tests/floats.cbl b/crucible-syntax/test-data/floats.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/floats.cbl rename to crucible-syntax/test-data/floats.cbl diff --git a/crucible-syntax/test-data/parser-tests/floats.out.good b/crucible-syntax/test-data/floats.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/floats.out.good rename to crucible-syntax/test-data/floats.out.good diff --git a/crucible-syntax/test-data/parser-tests/fun-type.cbl b/crucible-syntax/test-data/fun-type.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/fun-type.cbl rename to crucible-syntax/test-data/fun-type.cbl diff --git a/crucible-syntax/test-data/parser-tests/fun-type.out.good b/crucible-syntax/test-data/fun-type.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/fun-type.out.good rename to crucible-syntax/test-data/fun-type.out.good diff --git a/crucible-syntax/test-data/parser-tests/globals.cbl b/crucible-syntax/test-data/globals.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/globals.cbl rename to crucible-syntax/test-data/globals.cbl diff --git a/crucible-syntax/test-data/parser-tests/globals.out.good b/crucible-syntax/test-data/globals.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/globals.out.good rename to crucible-syntax/test-data/globals.out.good diff --git a/crucible-syntax/test-data/parser-tests/integer.cbl b/crucible-syntax/test-data/integer.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/integer.cbl rename to crucible-syntax/test-data/integer.cbl diff --git a/crucible-syntax/test-data/parser-tests/integer.out.good b/crucible-syntax/test-data/integer.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/integer.out.good rename to crucible-syntax/test-data/integer.out.good diff --git a/crucible-syntax/test-data/parser-tests/mutual.cbl b/crucible-syntax/test-data/mutual.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/mutual.cbl rename to crucible-syntax/test-data/mutual.cbl diff --git a/crucible-syntax/test-data/parser-tests/mutual.out.good b/crucible-syntax/test-data/mutual.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/mutual.out.good rename to crucible-syntax/test-data/mutual.out.good diff --git a/crucible-syntax/test-data/parser-tests/natural.cbl b/crucible-syntax/test-data/natural.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/natural.cbl rename to crucible-syntax/test-data/natural.cbl diff --git a/crucible-syntax/test-data/parser-tests/natural.out.good b/crucible-syntax/test-data/natural.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/natural.out.good rename to crucible-syntax/test-data/natural.out.good diff --git a/crucible-syntax/test-data/parser-tests/busted.out.good b/crucible-syntax/test-data/parser-tests/busted.out.good deleted file mode 100644 index 8f2eac703..000000000 --- a/crucible-syntax/test-data/parser-tests/busted.out.good +++ /dev/null @@ -1,4 +0,0 @@ -(defun @f () Unit - (start foo: (let foo (the Integer #f)) (let x ()) (return x))) - -At test-data/parser-tests/busted.cbl:3:27, expected a IntegerRepr rather than a BoolRepr but got #f diff --git a/crucible-syntax/test-data/parser-tests/rational.cbl b/crucible-syntax/test-data/rational.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/rational.cbl rename to crucible-syntax/test-data/rational.cbl diff --git a/crucible-syntax/test-data/parser-tests/rational.out.good b/crucible-syntax/test-data/rational.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/rational.out.good rename to crucible-syntax/test-data/rational.out.good diff --git a/crucible-syntax/test-data/parser-tests/recur.cbl b/crucible-syntax/test-data/recur.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/recur.cbl rename to crucible-syntax/test-data/recur.cbl diff --git a/crucible-syntax/test-data/parser-tests/recur.out.good b/crucible-syntax/test-data/recur.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/recur.out.good rename to crucible-syntax/test-data/recur.out.good diff --git a/crucible-syntax/test-data/parser-tests/refs.cbl b/crucible-syntax/test-data/refs.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/refs.cbl rename to crucible-syntax/test-data/refs.cbl diff --git a/crucible-syntax/test-data/parser-tests/refs.out.good b/crucible-syntax/test-data/refs.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/refs.out.good rename to crucible-syntax/test-data/refs.out.good diff --git a/crucible-syntax/test-data/parser-tests/regs.cbl b/crucible-syntax/test-data/regs.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/regs.cbl rename to crucible-syntax/test-data/regs.cbl diff --git a/crucible-syntax/test-data/parser-tests/regs.out.good b/crucible-syntax/test-data/regs.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/regs.out.good rename to crucible-syntax/test-data/regs.out.good diff --git a/crucible-syntax/test-data/parser-tests/shower.cbl b/crucible-syntax/test-data/shower.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/shower.cbl rename to crucible-syntax/test-data/shower.cbl diff --git a/crucible-syntax/test-data/parser-tests/shower.out.good b/crucible-syntax/test-data/shower.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/shower.out.good rename to crucible-syntax/test-data/shower.out.good diff --git a/crucible-syntax/test-data/simulator-tests/assume-merge.out.good b/crucible-syntax/test-data/simulator-tests/assume-merge.out.good deleted file mode 100644 index ba2185a59..000000000 --- a/crucible-syntax/test-data/simulator-tests/assume-merge.out.good +++ /dev/null @@ -1,24 +0,0 @@ -==== Begin Simulation ==== - -==== Finish Simulation ==== -==== Proof obligations ==== -Assuming: -* The branch in main from test-data/simulator-tests/assume-merge.cbl:4:5 to test-data/simulator-tests/assume-merge.cbl:6:14 - intLe 0 cx@0:i -* in main test-data/simulator-tests/assume-merge.cbl:6:5: even - eq 0 (intMod cx@0:i 2) -Prove: - test-data/simulator-tests/assume-merge.cbl:12:5: error: in main - oopsie! - false -COUNTEREXAMPLE -Assuming: -* The branch in main from test-data/simulator-tests/assume-merge.cbl:4:5 to test-data/simulator-tests/assume-merge.cbl:9:14 - not (intLe 0 cx@0:i) -* in main test-data/simulator-tests/assume-merge.cbl:9:5: odd - eq 1 (intMod cx@0:i 2) -Prove: - test-data/simulator-tests/assume-merge.cbl:12:5: error: in main - oopsie! - false -COUNTEREXAMPLE diff --git a/crucible-syntax/test-data/simulator-tests/double-branch.out.good b/crucible-syntax/test-data/simulator-tests/double-branch.out.good deleted file mode 100644 index 829bfc6a6..000000000 --- a/crucible-syntax/test-data/simulator-tests/double-branch.out.good +++ /dev/null @@ -1,14 +0,0 @@ -==== Begin Simulation ==== - -==== Finish Simulation ==== -==== Proof obligations ==== -Assuming: -* The branch in main from test-data/simulator-tests/double-branch.cbl:5:5 to test-data/simulator-tests/double-branch.cbl:7:13 - eq 5 ca@0:i -* The branch in main from test-data/simulator-tests/double-branch.cbl:7:5 to test-data/simulator-tests/double-branch.cbl:9:14 - intLe 0 cb@1:i -Prove: - test-data/simulator-tests/double-branch.cbl:9:5: error: in main - assert - eq 5 ca@0:i -PROVED diff --git a/crucible-syntax/test-data/simulator-tests/loop-err.out.good b/crucible-syntax/test-data/simulator-tests/loop-err.out.good deleted file mode 100644 index 8df1dc9b4..000000000 --- a/crucible-syntax/test-data/simulator-tests/loop-err.out.good +++ /dev/null @@ -1,54 +0,0 @@ -==== Begin Simulation ==== - -==== Finish Simulation ==== -==== Proof obligations ==== -Assuming: -* in main test-data/simulator-tests/loop-err.cbl:10:5: nonzero start - not (eq 0 cx@0:i) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:27:12 - eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6) -Prove: - test-data/simulator-tests/loop-err.cbl:27:5: error: in main - oopsie! - false -COUNTEREXAMPLE -Assuming: -* in main test-data/simulator-tests/loop-err.cbl:10:5: nonzero start - not (eq 0 cx@0:i) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:20:13 - not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:27:12 - eq 0 (intMod (intSum (intMul 4 cx@0:i)) 6) -Prove: - test-data/simulator-tests/loop-err.cbl:27:5: error: in main - oopsie! - false -PROVED -Assuming: -* in main test-data/simulator-tests/loop-err.cbl:10:5: nonzero start - not (eq 0 cx@0:i) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:20:13 - not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:20:13 - not (eq 0 (intMod (intSum (intMul 4 cx@0:i)) 6)) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:27:12 - eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6) -Prove: - test-data/simulator-tests/loop-err.cbl:27:5: error: in main - oopsie! - false -PROVED -Assuming: -* in main test-data/simulator-tests/loop-err.cbl:10:5: nonzero start - not (eq 0 cx@0:i) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:20:13 - not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:20:13 - not (eq 0 (intMod (intSum (intMul 4 cx@0:i)) 6)) -* The branch in main from test-data/simulator-tests/loop-err.cbl:17:5 to test-data/simulator-tests/loop-err.cbl:20:13 - not (eq 0 (intMod (intSum (intMul 2 cx@0:i)) 6)) -Prove: - test-data/simulator-tests/loop-err.cbl:23:5: error: in main - nonzero - not (intLe (intSum (intMul 8 cx@0:i)) 0) -PROVED diff --git a/crucible-syntax/test-data/simulator-tests/seq-test2.out.good b/crucible-syntax/test-data/simulator-tests/seq-test2.out.good deleted file mode 100644 index ca82ee72e..000000000 --- a/crucible-syntax/test-data/simulator-tests/seq-test2.out.good +++ /dev/null @@ -1,26 +0,0 @@ -==== Begin Simulation ==== - -==== Finish Simulation ==== -==== Proof obligations ==== - -Prove: - test-data/simulator-tests/seq-test2.cbl:29:5: error: in main - head check - eq (ite cb@0:b cx@1:i cz@3:i) (ite cb@0:b cx@1:i cz@3:i) -PROVED -Assuming: -* The branch in main from test-data/simulator-tests/seq-test2.cbl:33:5 to test-data/simulator-tests/seq-test2.cbl:36:13 - cb@0:b -Prove: - test-data/simulator-tests/seq-test2.cbl:38:5: error: in main - tail 2 condition check - cb@0:b -PROVED -Assuming: -* The branch in main from test-data/simulator-tests/seq-test2.cbl:33:5 to test-data/simulator-tests/seq-test2.cbl:45:14 - not cb@0:b -Prove: - test-data/simulator-tests/seq-test2.cbl:45:5: error: in main - tail 2 none check - not cb@0:b -PROVED diff --git a/crucible-syntax/test-data/parser-tests/strings.cbl b/crucible-syntax/test-data/strings.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/strings.cbl rename to crucible-syntax/test-data/strings.cbl diff --git a/crucible-syntax/test-data/parser-tests/strings.out.good b/crucible-syntax/test-data/strings.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/strings.out.good rename to crucible-syntax/test-data/strings.out.good diff --git a/crucible-syntax/test-data/parser-tests/structs.cbl b/crucible-syntax/test-data/structs.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/structs.cbl rename to crucible-syntax/test-data/structs.cbl diff --git a/crucible-syntax/test-data/parser-tests/structs.out.good b/crucible-syntax/test-data/structs.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/structs.out.good rename to crucible-syntax/test-data/structs.out.good diff --git a/crucible-syntax/test-data/parser-tests/variants.cbl b/crucible-syntax/test-data/variants.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/variants.cbl rename to crucible-syntax/test-data/variants.cbl diff --git a/crucible-syntax/test-data/parser-tests/variants.out.good b/crucible-syntax/test-data/variants.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/variants.out.good rename to crucible-syntax/test-data/variants.out.good diff --git a/crucible-syntax/test-data/parser-tests/vecs.cbl b/crucible-syntax/test-data/vecs.cbl similarity index 100% rename from crucible-syntax/test-data/parser-tests/vecs.cbl rename to crucible-syntax/test-data/vecs.cbl diff --git a/crucible-syntax/test-data/parser-tests/vecs.out.good b/crucible-syntax/test-data/vecs.out.good similarity index 100% rename from crucible-syntax/test-data/parser-tests/vecs.out.good rename to crucible-syntax/test-data/vecs.out.good diff --git a/crucible-syntax/test/Tests.hs b/crucible-syntax/test/Tests.hs index 77c57c351..f5a96309b 100644 --- a/crucible-syntax/test/Tests.hs +++ b/crucible-syntax/test/Tests.hs @@ -4,41 +4,19 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RankNTypes #-} -module Main where +module Main (main) where -import Control.Applicative -import Control.Lens (use) -import Control.Monad.IO.Class (MonadIO(..)) -import Control.Monad.ST - -import Data.List -import qualified Data.Map as Map -import Data.Map (Map) -import Data.Monoid -import qualified Data.Parameterized.Context as Ctx -import Data.Parameterized.Some (Some(..)) +import qualified Data.List as List import Data.Text (Text) -import Data.Type.Equality (TestEquality(..), (:~:)(..)) import qualified Data.Text as T import qualified Data.Text.IO as T import System.IO -import Lang.Crucible.Syntax.Concrete hiding (SyntaxError) - -import Lang.Crucible.Backend (IsSymInterface) -import Lang.Crucible.FunctionHandle -import Lang.Crucible.Simulator.ExecutionTree -import Lang.Crucible.Simulator.GlobalState (SymGlobalState, insertGlobal) -import Lang.Crucible.Simulator.OverrideSim -import Lang.Crucible.Syntax.Atoms (GlobalName(..)) -import Lang.Crucible.Syntax.Prog -import Lang.Crucible.Syntax.SExpr +import Lang.Crucible.Syntax.Concrete (defaultParserHooks) import Lang.Crucible.Syntax.ExprParse -import Lang.Crucible.Syntax.Overrides as SyntaxOvrs -import Lang.Crucible.Types -import Lang.Crucible.CFG.Common (GlobalVar(..)) -import Lang.Crucible.CFG.SSAConversion +import Lang.Crucible.Syntax.Prog (doParseCheck) +import Lang.Crucible.Syntax.SExpr import Test.Tasty (defaultMain, TestTree, testGroup) import Test.Tasty.Golden @@ -47,30 +25,13 @@ import qualified Text.Megaparsec as MP import System.FilePath import System.Directory -import What4.Config -import What4.FunctionName -import What4.Interface (intLit) -import What4.ProgramLoc -import What4.Solver.Z3 (z3Options) - - - -import Overrides as TestOvrs - -for = flip map +import What4.ProgramLoc (Position(SourcePos), Posd(..)) main :: IO () main = do wd <- getCurrentDirectory putStrLn $ "Looking for tests in " ++ wd - parseTests <- findTests - "Crucible parsing round-trips" - "test-data/parser-tests" - testParser - simTests <- findTests - "Crucible simulation" - "test-data/simulator-tests" - testSimulator - let allTests = testGroup "Tests" [syntaxParsing, resolvedForwardDecTest, parseTests, simTests] + parseTests <- findTests "Parsing round-trips" "test-data" testParser + let allTests = testGroup "Tests" [syntaxParsing, parseTests] defaultMain allTests findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree @@ -78,7 +39,7 @@ findTests group_name test_dir test_action = do inputs <- findByExtension [".cbl"] test_dir return $ testGroup group_name [ goldenFileTestCase input test_action - | input <- sort inputs + | input <- List.sort inputs ] goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree @@ -99,22 +60,6 @@ testParser inFile outFile = let ?parserHooks = defaultParserHooks withFile outFile WriteMode $ doParseCheck inFile contents True -testOptions :: [ConfigDesc] -testOptions = z3Options - -testSimulator :: FilePath -> FilePath -> IO () -testSimulator inFile outFile = - do contents <- T.readFile inFile - withFile outFile WriteMode $ \outh -> - simulateProgram inFile contents outh Nothing testOptions $ - defaultSimulateProgramHooks - { setupOverridesHook = \sym ha -> - do os1 <- SyntaxOvrs.setupOverrides sym ha - os2 <- TestOvrs.setupOverrides sym ha - return $ concat [os1,os2] - } - - data Lam = Lam [Text] (Datum TrivialAtom) deriving (Eq, Show) syntaxParsing :: TestTree @@ -125,7 +70,7 @@ syntaxParsing = vars :: SyntaxParse TrivialAtom [TrivialAtom] vars = describe "sequence of variable bindings" $ rep atomic distinctVars :: SyntaxParse TrivialAtom [TrivialAtom] - distinctVars = sideCondition' "sequence of distinct variable bindings" (\xs -> nub xs == xs) vars + distinctVars = sideCondition' "sequence of distinct variable bindings" (\xs -> List.nub xs == xs) vars lambda = fmap (\(_, (xs, (body, ()))) -> Lam [x | TrivialAtom x <- xs] (syntaxToDatum body)) (cons (atom "lambda") $ @@ -251,65 +196,3 @@ syntaxTest txt p = Left err -> error $ "Reader error: " ++ MP.errorBundlePretty err Right sexpr -> syntaxParseIO p sexpr --- | A basic test that ensures a forward declaration behaves as expected when --- invoked with an override that is assigned to it after parsing. -resolvedForwardDecTest :: TestTree -resolvedForwardDecTest = - testGroup "Forward declarations" - [ goldenFileTestCase ("test-data" "declare-tests" "main.cbl") $ \mainCbl mainOut -> - withFile mainOut WriteMode $ \outh -> - do mainContents <- T.readFile mainCbl - simulateProgram mainCbl mainContents outh Nothing testOptions $ - defaultSimulateProgramHooks - { resolveForwardDeclarationsHook = resolveForwardDecs - } - ] - where - resolveForwardDecs :: - IsSymInterface sym => - Map FunctionName SomeHandle -> - IO (FunctionBindings p sym ext) - resolveForwardDecs fds - | Just (SomeHandle hdl) <- Map.lookup "foo" fds - , Just Refl <- testEquality (handleArgTypes hdl) Ctx.empty - , Just Refl <- testEquality (handleReturnType hdl) IntegerRepr - = pure $ fnBindingsFromList [FnBinding hdl (UseOverride fooOv)] - - | otherwise - = assertFailure "Could not find @foo function of the appropriate type" - - fooOv :: - IsSymInterface sym => - Override p sym ext EmptyCtx IntegerType - fooOv = mkOverride "foo" $ do - sym <- use (stateContext.ctxSymInterface) - liftIO $ intLit sym 42 - --- | A basic test that ensures an extern behaves as expected after assigning a --- value to it after parsing. -resolvedExternTest :: TestTree -resolvedExternTest = - testGroup "Externs" - [ goldenFileTestCase ("test-data" "extern-tests" "main.cbl") $ \mainCbl mainOut -> - withFile mainOut WriteMode $ \outh -> - do mainContents <- T.readFile mainCbl - simulateProgram mainCbl mainContents outh Nothing testOptions $ - defaultSimulateProgramHooks - { resolveExternsHook = resolveExterns - } - ] - where - resolveExterns :: - IsSymInterface sym => - sym -> - Map GlobalName (Some GlobalVar) -> - SymGlobalState sym -> - IO (SymGlobalState sym) - resolveExterns sym externs gst - | Just (Some gv) <- Map.lookup (GlobalName "foo") externs - , Just Refl <- testEquality (globalType gv) IntegerRepr - = do fooVal <- intLit sym 42 - pure $ insertGlobal gv fooVal gst - - | otherwise - = assertFailure "Could not find $$foo extern of the appropriate type"