This is the user guide for Kani VSCode Extension. This guide provides the various workflows that you can use to verify and debug your Kani harnesses.
- Verify Kani harnesses
- Use Concrete Playback to debug a Kani harness
- View trace report
- Kani output logging
- Coverage information
As soon as the Rust package containing the harnesses is opened using the Kani extension in a VSCode instance, you should see the Kani harnesses loaded as regular unit tests in the testing panel on the left border of the VSCode window. This is how the VSCode window looks like when you click on the panel:
You can then run your harnesses using the harness tree view by clicking the play button beside the harness that was automatically picked up by the Kani VSCode Extension. Once you run the harness using the extension, you are shown an error message if the verification fails. You are then presented with two options:
We are going to describe the flows in detail in their respective sections, but explain the concrete playback feature first.
Kani can help you generate unit tests containing the counterexample (also called concrete playback). These unit tests can help you inspect the trace with the counterexamples and debug your Kani harnesses.
You can generate the unit test with the counterexample by clicking on the Run Concrete Playback for (your harness name) option that appears through a blue link on the error banner.
You can see that the source is annotated with two buttons that hover over the generated unit test called Run Test (Kani) and Debug Test (Kani) which allow you to run and debug the test just like any other Rust unit test.
Clicking the Run Test (Kani) button on top of a unit test, runs the unit test generated via concrete playback.
By setting breakpoints and clicking the Debug Test (Kani) button, you are taken into the debugger panel which allows you to inspect the trace using the counterexample.
You can then use the debugger controller to step through, into, out of, replay and also change values on the trace panel on the left for interactive debugging.
By clicking the Generate report for (your harness) option in the error banner, you can view the trace for the harness in an HTML report.
You can click on the Preview in Editor button to view the HTML trace within VSCode.
It should look like this:
For every test run, you can view the full output from Kani logged into the output channel as a text file. To view the log, open the output channel, and click on the channel drop down list to view a channel called Output (Kani): ...
Line-based coverage information can be displayed for any harness as in:
To enable the coverage feature in the extension, toggle on the Codelens-kani: Highlight Coverage setting in Settings > Extensions > Kani.
Once the coverage feature is enabled, the Get coverage info action should be visible on top of each Kani harness in the project.
Running the Get coverage info highlights all lines for which coverage information was obtained.
Coverage information (as described in the RFC for line coverage) is represented with three colors:
- Green: Indicates
FULLcoverage. - Yellow: Indicates
PARTIALcoverage. - Red: Indicates
NONEcoverage.
NOTE: Line-based coverage information is an unstable feature.
To remove or de-highlight the coverage information presented on the UI, open the command palette with Shift + Command + P (Mac) / Ctrl + Shift + P (Windows/Linux). Then, search for the command De-highlight coverage. This should revert the VS Code UI to it's normal state (pre-coverage).
