Introducing the Kani VS Code Extension
Kani is a verification tool that can help you systematically test properties about your Rust code. To learn more about Kani, check out the Kani tutorial and our previous blog posts.
We are delighted to introduce the Kani VS Code Extension, which is now available on the VS Code marketplace.
The extension integrates the Kani verifier into the VS Code UI.
As you write Kani harnesses, the extension detects them and conveniently displays them within your testing panel.
The extension offers detailed diagnostics, feedback about verification failures, error messages, and stack traces.
This empowers you to find bugs and verify your code quicker.
You can install the extension from the webpage on VS Code marketplace or by searching for Kani in the extensions tab of your VS Code window.
Working through a simple example
To show some of the features in the extension, we will work through a familiar example, the rectangle example that we introduced in our first blog post.
#[derive(Debug, Copy, Clone)]
struct Rectangle {
width: u64,
height: u64,
}
impl Rectangle {
fn can_hold(&self, other: &Rectangle) -> bool {
self.width > other.width && self.height > other.height
}
fn stretch(&self, factor: u64) -> Option<Self> {
let w = self.width.checked_mul(factor)?;
let h = self.height.checked_mul(factor)?;
Some(Rectangle { width: w, height: h })
}
}
In order to verify properties about the rectangle, we wrote a verification harness. The harness postulates that when the rectangle is stretched, it can hold another rectangle of its original size (dimensions). If verified succesfully, this means that for any given stretch factor and any height and width of the original rectangle, this property holds true.
#[kani::proof]
pub fn stretched_rectangle_can_hold_original() {
let original = Rectangle { width: kani::any(), height: kani::any() };
let factor = kani::any();
if let Some(larger) = original.stretch(factor) {
assert!(larger.can_hold(&original));
}
}
Using the VS Code extension on the example
With the extension, running Kani on a verification harness, is as simple as clicking a button. In the following sections, we’ll walk you through using the extension’s core features to debug and finally verify the rectangle example mentioned above.
View Kani harnesses
As soon as your Rust package is opened using the Kani extension in a VS Code instance, you should see the Kani harnesses loaded as regular unit tests in the Testing Panel on the primary side bar of VS Code. This is how the testing page looks like when you click on the panel.
Run Kani harnesses
You can then run your harnesses using the tree view by clicking the play button beside the harness that was automatically picked up by the Kani Extension. Once you run the harness using the extension, you are shown a green check mark if verification succeeded, or a failure banner if it failed.
In our example, as with the command line, we can see through visual markers such as the failure banner pop-up and the red failure marker, that verification failed.
You are then presented with two options:
Kani’s concrete playback feature allows you to generate unit tests that call a function with the exact arguments that caused the assertion violation. The VS Code extension makes using concrete playback easy. You can read more about concrete playback in our documentation.
Generate a counterexample unit test
Next, we’ll generate the unit test by clicking on the Run Concrete Playback for stretched_rectangle_can_hold_original link that appears through a blue link on the error banner.
By clicking on the link, we have our counterexample unit test pasted directly below the harness. This is what the unit test looks like:
#[test]
fn kani_concrete_playback_stretched_rectangle_can_hold_original() {
let concrete_vals: Vec<Vec<u8>> = vec![
// 4611686018427387904ul
vec![0, 0, 0, 0, 0, 0, 0, 64],
// 0ul
vec![0, 0, 0, 0, 0, 0, 0, 0],
// 2ul
vec![2, 0, 0, 0, 0, 0, 0, 0],
];
kani::concrete_playback_run(concrete_vals, stretched_rectangle_can_hold_original);
}
You can see in the GIF above that the source code is now annotated with two options on top of the generated unit test, Run Test (Kani) and Debug Test (Kani), which allow you to run and debug the test just like any other Rust unit test.
Run Kani-generated test
Running the unit test using the Run Test (Kani) button shows us what we were expecting – that the unit test is failing.
This is because the unit test is using the counterexample to invoke the function stretched_rectangle_can_hold_original.
Debug Kani unit test
In order to peek under the hood to find out the missing assumptions that lead to unexpected behavior, it is really important to look at the concrete counterexamples for which our assertions fail.
By setting breakpoints and clicking the Debug Test (Kani) button, you are taken into the debugger which allows you to inspect the specific values for which the assertion fails.
In our case, we can see that for original.height = 0 , the larger rectangle’s height or larger.height also stays 0, which shows that for that counterexample, the property can_hold does not hold.
And finally, verify the harness with the right assumptions
Now that we know that for original.width = 0, our assertion fails, we can repeat the experiment with explicit assumptions.
The experiments should reveal that for all parameters, having a 0 value will cause the assertion to fail.
Additionally, there is a problem if factor is 1 because in this case stretch will return Some(...), but the stretched rectangle will be the same size as the original.
We missed these cases in our unit and property-based tests.
We will now add these assumptions through kani::assume and re-run the verification in the extension.
And with that green check mark, you can be assured that the harness has been verified!
Wrapping up
You can use Kani through VS Code using the Kani VS Code extension, available on the marketplace now. With this new extension you can now iteratively verify your code directly in the VS Code UI. It lets you verify harnesses with a simple click, highlights property violations, lets you generate unit tests and debug them.
The Kani extension has more features which weren’t mentioned in the blog, which you can read about in our user guide documentation.
Please go ahead and try the extension yourself!
If you are running into issues with the Kani extension or have feature requests or suggestions, we’d love to hear from you.