# Regression testing Kani relies on a quite extensive range of tests to perform regression testing. Regression testing can be executed by running the command: ```bash ./scripts/kani-regression.sh ``` The `kani-regression.sh` script executes different testing commands, which we classify into: * [Kani testing suites](#kani-testing-suites) * [Rust unit tests](#rust-unit-tests) * [Python unit tests](#python-unit-tests) * [Script-based tests](#script-based-tests) See below for a description of each one. Note that regression testing is run whenever a Pull Request is opened, updated or merged into the main branch. Therefore, it's a good idea to run regression testing locally before submitting a Pull Request for Kani. ## Kani testing suites The Kani testing suites are the main testing resource for Kani. In most cases, the tests contained in the Kani testing suites are single Rust files that are run using the following command: ```bash kani file.rs ``` Command-line options can be passed to the test by adding a special comment to the file. See [testing options](#testing-options) for more details. In particular, the Kani testing suites are composed of: * `kani`: The main testing suite for Kani. The test is a single Rust file that's run through Kani. In general, the test passes if verification with Kani is successful, otherwise it fails. * `firecracker`: Works like `kani` but contains tests inspired by [Firecracker](https://github.com/firecracker-microvm/firecracker) code. * `prusti`: Works like `kani` but contains tests from the [Prusti](https://github.com/viperproject/prusti-dev) tool. * `smack`: Works like `kani` but contains tests from the [SMACK](https://github.com/smackers/smack) tool. * `kani-fixme`: Similar to `kani`, but runs ignored tests from the `kani` testing suite (i.e., tests with `fixme` or `ignore` in their name). Allows us to detect when a previously not supported test becomes supported. More details in ["Fixme" tests](#fixme-tests). * `expected`: Similar to `kani` but with an additional check which ensures that lines appearing in `*.expected` files appear in the output generated by `kani`. * `ui`: Works like `expected`, but focuses on the user interface (e.g., warnings) instead of the verification output. * `cargo-kani`: This suite is designed to test the `cargo-kani` command. As such, this suite works with packages instead of single Rust files. Arguments can be specified in the `Cargo.toml` configuration file. Similar to the `expected` suite, we look for `*.expected` files for each harness in the package. * `cargo-ui`: Similar to `cargo-kani`, but focuses on the user interface like the `ui` test suite. * `script-based-pre`: This suite is useful to execute script-based tests, and also allows checking expected output and exit codes after running them. The suite uses the `exec` mode, described in more detail [here](#the-exec-mode). We've extended [`compiletest`](https://rustc-dev-guide.rust-lang.org/tests/intro.html) (the Rust compiler testing framework) to work with these suites. That way, we take advantage of all `compiletest` features (e.g., parallel execution). ### Testing stages The process of running single-file tests is split into three stages: * `check`: This stage uses the Rust front-end to detect if the example is valid Rust code. * `codegen`: This stage uses the Kani back-end to determine if we can generate GotoC code. * `verify`: This stage uses CBMC to obtain a verification result. If a test fails, the error message will include the stage where it failed: ``` error: test failed: expected check success, got failure ``` When working on a test that's expected to fail, there are two options to indicate an expected failure. The first one is to add a comment ```rust // kani--fail ``` at the top of the test file, where `` is the stage where the test is expected to fail. The other option is to use the predicate `kani::expect_fail(cond, message)` included in the Kani library. The `cond` in `kani::expect_fail` is a condition that you expect not to hold during verification. The testing framework expects one `EXPECTED FAIL` message in the verification output for each use of the predicate. > **NOTE**: `kani::expect_fail` is only useful to indicate failure in the > `verify` stage, errors in other stages will be considered testing failures. ### Testing options Many tests will require passing command-line options to Kani. These options can be specified in single Rust files by adding a comment at the top of the file: ```rust // kani-flags: ``` For example, to use an unwinding value of 4 in a test, we can write: ```rust // kani-flags: --default-unwind 4 ``` For `cargo-kani` tests, the preferred way to pass command-line options is adding them to `Cargo.toml`. See [`Usage on a package`](./usage.md#usage-on-a-package) for more details. ### "Fixme" tests Any test containing `fixme` or `ignore` in its name is considered a test not supported for some reason (i.e., they return an unexpected verification result). However, "fixme" tests included in the `kani` folder are run via the `kani-fixme` testing suite. `kani-fixme` works on test files from `kani` but: 1. Only runs tests whose name contains `fixme` or `ignore` (ignoring the rest). 2. The expected outcome is failure. In other words, a test is successful if it fails. We welcome contributions with "fixme" tests which demonstrate a bug or unsupported feature in Kani. Ideally, the test should include some comments regarding: * The expected result of the test. * The actual result of the test (e.g., interesting parts of the output). * Links to related issues. To include a new "fixme" test in `kani` you only need to ensure its name contains `fixme` or `ignore`. If your changes to Kani cause a "fixme" test to become supported, you only need to rename it so the name does not contain `fixme` nor `ignore`. ## Rust unit tests These tests follow the [Rust unit testing](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html) style. At present, Kani runs unit tests from the following packages: * `cprover_bindings` * `kani-compiler` * `cargo-kani` ## Python unit tests We use the Python [unit testing framework](https://docs.python.org/3/library/unittest.html) to test the CBMC JSON parser. ## Script-based tests These are tests which are run using scripts. Scripting gives us the ability to perform ad-hoc checks that cannot be done otherwise. They are currently used for: * Standard library codegen * Firecracker virtio codegen * Diamond dependency In fact, most of them are equivalent to running `cargo kani` and performing checks on the output. The downside to scripting is that these tests will always be run, even if there have not been any changes since the last time the regression was run. > **NOTE**: With the addition of the `exec` mode for `compiletest` (described > below), we'll be migrating these script-based tests to other suites using the > `exec` mode. The `exec` mode allows us to take advantage of `compiletest` > features while executing script-based tests (e.g., parallel execution). ### The `exec` mode The `exec` mode in `compiletest` allows us to execute script-based tests, in addition to checking expected output and exit codes after running them. In particular, tests are expected to be placed directly under the test directory (e.g., `script-based-pre`) in a directory with a `config.yml` file, which should contain: * `script`: The path to the script to be executed. * `expected` (optional): The path to the `.expected` file to use for output comparison. * `exit_code` (optional): The exit code to be returned by executing the script (a zero exit code is expected if not specified). For example, let's say want to test the script `exit-one.sh`: ```bash echo "Exiting with code 1!" exit 1 ``` In this case, we'll create a folder that contains the `config.yml` file: ```yml script: exit-one.sh expected: exit-one.expected exit_code: 1 ``` where `exit-one.expected` is simply a text file such as: ```text Exiting with code 1! ``` If `expected` isn't specified, the output won't be checked. If `exit_code` isn't specified, the `exec` mode will check the exit code was zero. Note that all paths specified in the `config.yml` file are local to the test directory, which is the working directory assumed when executing the test. This is meant to avoid problems when executing the test manually.