Regression testing

Kani relies on a quite extensive range of tests to perform regression testing. Regression testing can be executed by running the command:

./scripts/kani-regression.sh

The kani-regression.sh script executes different testing commands, which we classify into:

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:

kani file.rs <options>

Command-line options can be passed to the test by adding a special comment to the file. See 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 code.
  • prusti: Works like kani but contains tests from the Prusti tool.
  • smack: Works like kani but contains tests from the 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.
  • 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.

We've extended compiletest (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

// kani-<stage>-fail

at the top of the test file, where <stage> 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:

// kani-flags: <options>

For example, to use an unwinding value of 4 in a test, we can write:

// 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 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 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 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:

echo "Exiting with code 1!"
exit 1

In this case, we'll create a folder that contains the config.yml file:

script: exit-one.sh
expected: exit-one.expected
exit_code: 1

where exit-one.expected is simply a text file such as:

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.