Debugging verification failures
When the result of a certain check comes back as a FAILURE
,
Kani offers different options to help debug:
--concrete-playback
. This experimental feature generates a Rust unit test case that plays back a failing proof harness using a concrete counterexample.--visualize
. This feature generates an HTML text-based trace that enumerates the execution steps leading to the check failure.
Concrete playback
This section describes the concrete playback feature in more detail.
Setup
The Kani library needs to be linked as a dev dependency to the crate you're trying to debug.
This requires adding the following lines to your Cargo.toml
file,
which differ depending on what version of the Kani library you would like to use:
- The latest version:
[dev-dependencies]
kani = { git = "https://github.com/model-checking/kani", features = ["concrete_playback"] }
- A specific version of the Kani library (v0.9+) that's already downloaded:
[dev-dependencies]
kani = { path = "{path_to_kani_root}/library/kani", features = ["concrete_playback"] }
Usage
In order to enable this feature, run Kani with the --enable-unstable --concrete-playback=[print|inplace]
flag.
After getting a verification failure, Kani will generate a Rust unit test case that plays back a failing
proof harness with a concrete counterexample.
The concrete playback modes mean the following:
print
: Kani will just print the unit test to stdout. You will then need to copy this unit test into the same module as your proof harness.inplace
: Kani will automatically copy the unit test into your source code. Before running this mode, you might find it helpful to have your existing code committed togit
. That way, you can easily remove the unit test withgit revert
. Note that Kani will not copy the unit test into your source code if it detects that the exact same test already exists.
After the unit test is in your source code, you can run it with cargo test
.
To debug it, there are a couple of options:
- If you have certain IDEs, there are extensions (e.g.,
rust-analyzer
forVS Code
) that support UI elements like aRun Test | Debug
button next to all unit tests. - Otherwise, you can debug the unit test on the command line.
To do this, you first run
cargo test {unit_test_func_name}
. The output from this will have a line in the beginning likeRunning unittests {files} ({binary})
. You can then debug the binary with tools likerust-gdb
orlldb
.
Example
Running kani --enable-unstable --concrete-playback=print
on the following source file:
#[kani::proof]
fn proof_harness() {
let a: u8 = kani::any();
let b: u16 = kani::any();
assert!(a / 2 * 2 == a &&
b / 2 * 2 == b);
}
yields this concrete playback Rust unit test:
#[test]
fn kani_concrete_playback_proof_harness_16220658101615121791() {
let concrete_vals: Vec<Vec<u8>> = vec![
// 133
vec![133],
// 35207
vec![135, 137],
];
kani::concrete_playback_run(concrete_vals, proof_harness);
}
Here, 133
and 35207
are the concrete values that, when substituted for a
and b
,
cause an assertion failure.
vec![135, 137]
is the byte array representation of 35207
.
Common issues
error[E0425]: cannot find function x in this scope
: this is usually caused by having#[cfg(kani)]
somewhere in the control flow path of the user's proof harness. To fix this, remove#[cfg(kani)]
from those paths.
Request for comments
This feature is experimental and is therefore subject to change. If you have ideas for improving the user experience of this feature, please add them to this GitHub issue. We are tracking the existing feature requests in this GitHub milestone.
Limitations
- This feature does not generate unit tests for failing non-panic checks (e.g., UB checks). This is because checks would not trigger runtime errors during concrete playback. Kani generates warning messages for this.
- This feature does not support generating unit tests for multiple assertion failures within the same harness. This limitation might be removed in the future. Kani generates warning messages for this.
- This feature requires that you do not change your code or runtime configurations between when Kani generates the unit test and when you run it. For instance, if you linked with library A during unit test generation and library B during unit test play back, that might cause unintended errors in the unit test counterexample. Kani currently has no way to detect this issue.