From b669f7c1228efb362cbb56b95090b24c0611ba7b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 12:01:31 +0200 Subject: tests: Add a README --- tests/README.md | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 tests/README.md (limited to 'tests/README.md') diff --git a/tests/README.md b/tests/README.md new file mode 100644 index 00000000..4f4f1ff5 --- /dev/null +++ b/tests/README.md @@ -0,0 +1,67 @@ +# Aeneas test suite + +This folder contains the test suite for Aeneas. It is organized as follows: +- `test_runner/`: ocaml script that orchestrates the test suite; +- `src/`: rust files and crates used as test inputs; +- `llbc/`: temporary directory (ignored by git) that stores intermediate files generated during tests; +- `coq/`, `fstar/`, `hol4/`, `lean/`: one folder per backend. Each folder contains: + - Files generated by Aeneas from our test inputs; + - Handwritten proof files. + +# Running the test suite + +Running the test suite has two parts: +- The generation of files from rust to each backend. This is done by running `make test` in the + project root. This will call the test runner on each file or crate in `tests/src`, which will call + `charon` and `aeneas` to generate the backend-specific outputs. +- The verification of proofs for each backend. This is done by running `make verify` in the project + root. It will run each verifier (`fstar`, `lean` etc) on the files in the corresponding folder to + verify the correctness of proofs. + +CI does both of these things; in particular it checks that we correctly committed the generated +files. + +Important note: at the moment we don't regenerate the `hol4` outputs. We do still check them with +hol4. This is tracked in https://github.com/AeneasVerif/aeneas/issues/62. + +# Adding a new test + +Adding a new test is easy: just add a `foo.rs` file or a `foo_crate` folder in `tests/src`. `make +test` will find the new file and call the test runner on it. + +To specify options for how your test should be run, see the next section. + +Ideally, any non-trivial change to Aeneas should have an accompanying test that exercises the new +code. The goal of this test suite is to cover a large portion of what Aeneas can do, so we can work +on it confidently. + +# Passing options to `Aeneas` and `Charon` + +The test runner supports setting several options for each test. +- For single files, it will read comments at the top of the file that start with `//@`; +- For crates, it will read the `crate_dir/aeneas-test-options` file. + +In both cases it supports the same options. Typical options are: +- `charon-args=--polonius --opaque=betree_utils`: pass these arguments to `charon`; +- `aeneas-args=-test-trans-units`: pass these arguments to `aeneas` for all backends; +- `[fstar] aeneas-args=-decreases-clauses -template-clauses`: pass these arguments to `aeneas` for + the `fstar` backend; +- `[coq,lean] skip`: skip the test for the `coq` and `lean` backends; +- `[fstar] known-failure`: see below; +- `[coq,fstar] subdir=misc`: store the output in the `misc` subdirectory for these two backends. + +For an up-to-date list of options, see comments in the test runner code. + +# `known-failure` tests + +There's a special kind of test that doesn't generate backend code: `//@ known-failure` tests. These +are meant to record: +- Cases that produce an error so we don't forget and can fix them later; +- Cases that _should_ error, to ensure we correctly raise an error and that the error output is nice. + +It is useful to add tests there whenever you find an interesting failure case. + +Note however that this is for failures of Aeneas. Tests that cause Charon errors should be submitted +to the Charon project. `known-failure` tests will not pass if the error occurs within Charon. Note +also that there is no option for tests that translate successfully but fail to be verified by the +backend. -- cgit v1.2.3 From ec03335a473ffdf9371210e8558c691ea69d212d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 12:18:52 +0200 Subject: runner: Split up into multiple files --- tests/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests/README.md') diff --git a/tests/README.md b/tests/README.md index 4f4f1ff5..f68b509f 100644 --- a/tests/README.md +++ b/tests/README.md @@ -50,7 +50,7 @@ In both cases it supports the same options. Typical options are: - `[fstar] known-failure`: see below; - `[coq,fstar] subdir=misc`: store the output in the `misc` subdirectory for these two backends. -For an up-to-date list of options, see comments in the test runner code. +For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`. # `known-failure` tests -- cgit v1.2.3 From 87d5a08f44b46657026a99c154bcec4a733f221d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 May 2024 10:37:17 +0200 Subject: Improve the tests README --- tests/README.md | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'tests/README.md') diff --git a/tests/README.md b/tests/README.md index f68b509f..c9ca0047 100644 --- a/tests/README.md +++ b/tests/README.md @@ -8,23 +8,26 @@ This folder contains the test suite for Aeneas. It is organized as follows: - Files generated by Aeneas from our test inputs; - Handwritten proof files. -# Running the test suite +## Running the test suite Running the test suite has two parts: -- The generation of files from rust to each backend. This is done by running `make test` in the +- We generate files from rust to each backend. This is done by running `make test` in the project root. This will call the test runner on each file or crate in `tests/src`, which will call `charon` and `aeneas` to generate the backend-specific outputs. -- The verification of proofs for each backend. This is done by running `make verify` in the project - root. It will run each verifier (`fstar`, `lean` etc) on the files in the corresponding folder to - verify the correctness of proofs. +- We check that the generated output is valid code by parsing it and type-checking it with the + relevant verifier (Lean, Coq, F*, etc.), and replay the hand-written proofs which use it as + a dependency. This is done by running `make verify` in the project root. -CI does both of these things; in particular it checks that we correctly committed the generated -files. +To generate the output of a single test, run `make test-`, e.g. `make test-loops.rs` or +`make test-betree`. To verify the output for a single backend, run `make verify-` inside the +`tests/` folder, e.g. `make verify-coq`. -Important note: at the moment we don't regenerate the `hol4` outputs. We do still check them with +CI does both of these things; it also checks that we committed all the generated files. + +Important note: at the moment we don't regenerate the HOL4 outputs. We do still check them with hol4. This is tracked in https://github.com/AeneasVerif/aeneas/issues/62. -# Adding a new test +## Adding a new test Adding a new test is easy: just add a `foo.rs` file or a `foo_crate` folder in `tests/src`. `make test` will find the new file and call the test runner on it. @@ -35,7 +38,7 @@ Ideally, any non-trivial change to Aeneas should have an accompanying test that code. The goal of this test suite is to cover a large portion of what Aeneas can do, so we can work on it confidently. -# Passing options to `Aeneas` and `Charon` +## Passing options to `Aeneas` and `Charon` The test runner supports setting several options for each test. - For single files, it will read comments at the top of the file that start with `//@`; @@ -52,13 +55,18 @@ In both cases it supports the same options. Typical options are: For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`. -# `known-failure` tests +## `known-failure` tests There's a special kind of test that doesn't generate backend code: `//@ known-failure` tests. These are meant to record: - Cases that produce an error so we don't forget and can fix them later; - Cases that _should_ error, to ensure we correctly raise an error and that the error output is nice. +We record the output of the `aeneas` call in `test-file.out` alongside the original `test-file.rs`. +This file must be committed like the rest of the test outputs. (Note: sometimes the output will be +different between your local machine and CI, e.g. because release build changed a stacktrace. In +that case we don't record the output, which is done with `//@ no-check-output`). + It is useful to add tests there whenever you find an interesting failure case. Note however that this is for failures of Aeneas. Tests that cause Charon errors should be submitted -- cgit v1.2.3