Kani relies on a quite extensive range of tests to perform regression testing. Regression testing can be executed by running the command:
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.
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
kanibut contains tests inspired by Firecracker code.
prusti: Works like
kanibut contains tests from the Prusti tool.
smack: Works like
kanibut contains tests from the SMACK tool.
kani-fixme: Similar to
kani, but runs ignored tests from the
kanitesting suite (i.e., tests with
ignorein their name). Allows us to detect when a previously not supported test becomes supported. More details in "Fixme" tests.
expected: Similar to
kanibut with an additional check which ensures that lines appearing in
*.expectedfiles appear in the output generated by
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-kanicommand. As such, this suite works with packages instead of single Rust files. Arguments can be specified in the
Cargo.tomlconfiguration file. Similar to the
expectedsuite, we look for
*.expectedfiles for each harness in the package.
cargo-ui: Similar to
cargo-kani, but focuses on the user interface like the
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
execmode, described in more detail here.
Rust compiler testing framework) to work with these suites. That way, we take
advantage of all
compiletest features (e.g., parallel execution).
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
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
included in the Kani library. The
kani::expect_fail is a condition
that you expect not to hold during verification. The testing framework expects
EXPECTED FAIL message in the verification output for each use of the
kani::expect_failis only useful to indicate failure in the
verifystage, errors in other stages will be considered testing failures.
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
cargo-kani tests, the preferred way to pass command-line options is adding
Usage on a package for more details.
Any test containing
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 works on test files from
- Only runs tests whose name contains
ignore(ignoring the rest).
- 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
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
These tests follow the Rust unit testing style.
At present, Kani runs unit tests from the following packages:
We use the Python unit testing framework to test the CBMC JSON parser.
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
compiletest(described below), we'll be migrating these script-based tests to other suites using the
execmode allows us to take advantage of
compiletestfeatures while executing script-based tests (e.g., parallel execution).
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
script-based-pre) in a directory with a
config.yml file, which
script: The path to the script to be executed.
expected(optional): The path to the
.expectedfile 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
echo "Exiting with code 1!" exit 1
In this case, we'll create a folder that contains the
script: exit-one.sh expected: exit-one.expected exit_code: 1
exit-one.expected is simply a text file such as:
Exiting with code 1!
expected isn't specified, the output won't be checked. If
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.