Merge branch 'main' into kani-vscode-0.0.6

README.md

@@ -1,6 +1,6 @@
 # Kani Visual Studio Code Extension
 
-A [Visual Studio Code](https://code.visualstudio.com/) extension that allows users to run and debug their [Kani Rust Verifier](https://github.com/model-checking/kani) harnesses in vscode.
+A [Visual Studio Code](https://code.visualstudio.com/) extension that allows users to run and debug their [Kani Rust Verifier](https://github.com/model-checking/kani) harnesses in VS Code.
 
 ## Usage
 
@@ -22,7 +22,7 @@ Check [user guide](docs/user-guide.md) for more detailed information.
 ## Requirements
 
 -   [Visual Studio Code](https://code.visualstudio.com/) 1.50 or newer
--   [Kani](https://github.com/model-checking/kani) 0.29 or newer
+-   [Kani](https://github.com/model-checking/kani) 0.34 or newer
 
 NOTE: The extension only works on Cargo packages. For standalone Rust files, Kani is only available on the command line.
 

docs/user-guide.md

@@ -16,6 +16,8 @@ This guide provides the various workflows that you can use to verify and debug y
   - [View trace report in window](#view-trace-report-in-window)
 - [Kani output logging](#kani-output-logging)
   - [View full Kani output](#view-full-kani-output)
+- [Coverage information](#coverage-information)
+  - [View coverage information](#view-coverage-information)
 
 ### Verify Kani harnesses
 
@@ -81,7 +83,7 @@ By clicking the `Generate report for (your harness)` option in the error banner,
 You can click on the `Preview in Editor` button to view the HTML trace within VSCode.
 It should look like this:
 
-![Generate Report](../resources/screenshots/view-report.png)
+![View Report](../resources/screenshots/view-report.png)
 
 
 ### Kani output logging
@@ -91,3 +93,23 @@ 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): ...`
 
 ![Generate Report](../resources/screenshots/view-output.png)
+
+### Coverage information
+
+Line-based coverage information can be displayed for any harness as in:
+
+![Coverage information](../resources/screenshots/coverage-info.png)
+
+To enable the coverage feature in the extension, toggle on the `Codelens-kani: Highlight Coverage` setting in `Settings > Extensions > Kani`.
+
+#### View coverage information
+
+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](https://model-checking.github.io/kani/rfc/rfcs/0008-line-coverage.html#postprocessing-coverage-checks))  is represented with three colors:
+ - **Green:** Indicates `FULL` coverage.
+ - **Yellow:** Indicates `PARTIAL` coverage.
+ - **Red:** Indicates `NONE` coverage.
+
+**NOTE**: Line-based coverage information is an unstable feature.

resources/test-crates/simple-test/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "simple-test"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

resources/test-crates/simple-test/src/funs.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn estimate_size(x: u32) -> u32 {
+    assert!(x < 4096);
+
+    if x < 256 {
+        if x < 128 {
+            return 1;
+        } else {
+            return 3;
+        }
+    } else if x < 1024 {
+        if x > 1022 {
+            return 4;
+        } else {
+            return 5;
+        }
+    } else {
+        if x < 2048 {
+            return 7;
+        } else {
+            return 9;
+        }
+    }
+}
+
+pub fn find_index(nums: &[i32], target: i32) -> Option<usize> {
+    for (index, &num) in nums.iter().enumerate() { // coverage should be yellow
+        if num == target { // coverage should be green
+            return Some(index); // coverage should be green
+        }
+    }
+    None // coverage should be red
+} // coverage should be yellow

resources/test-crates/simple-test/src/lib.rs

@@ -0,0 +1,57 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This package is intended to assist in manually testing the features of the
+//! extension. The tests to be performed are the following:
+//!
+//! 1. Run verification for `test_success` and check that it passes.
+//! 2. Run verification for `test_failure` and check that it fails with
+//!    "assertion failed: x < 4096".
+//! 3. Click on "Generate concrete test for test_failure" and check that a new
+//!    Rust unit test is added after "test_failure".
+//! 4. Check that the actions "Run Test (Kani)" and "Debug Harness (Kani)"
+//!    appear above the Rust unit test that was generated in the previous step.
+//! 5. Click on the "Run Test (Kani)" action. Check that the test runs on a
+//!    terminal and it panics as expected.
+//! 6. Click on the "Debug Harness (Kani)" action. Check that the debugging mode
+//!    is started (debugging controls should appear on the top) and stop it by
+//!    clicking on the red square button.
+//! 7. Toggle on the "Codelens-kani: Highlight" option in "Settings > Kani".
+//! 8. Check that the "Get coverage info" action appears for the "test_success"
+//!    and "test_failure" harnesses.
+//! 9. Run the "Get coverage info" action for "test_coverage". Check that all
+//!    lines in "test_coverage" are green. In addition, check that in
+//!    "funs::find_index":
+//!     - The first and last highlighted lines are yellow.
+//!     - The second and third highlighted lines are green.
+//!     - The remaining highlighted line is red.
+//!    Comments indicating the correct colors are available in "funs::find_index".
+mod funs;
+
+#[cfg(kani)]
+mod verify {
+    use super::*;
+
+    #[kani::proof]
+    fn test_success() {
+        let x: u32 = kani::any();
+        kani::assume(x < 4096);
+        let y = funs::estimate_size(x);
+        assert!(y < 10);
+    }
+
+    #[kani::proof]
+    fn test_failure() {
+        let x: u32 = kani::any();
+        let y = funs::estimate_size(x);
+        assert!(y < 10);
+    }
+
+    #[kani::proof]
+    fn test_coverage() {
+        let numbers = [10, 20, 30, 40, 50];
+        let target = 30;
+        let result = funs::find_index(&numbers, target);
+        assert_eq!(result, Some(2));
+    }
+}