Merge branch 'main' of https://github.com/model-checking/kani-vscode-…

…extension into add-qna-link

.github/workflows/format-check.yml

@@ -20,7 +20,6 @@ jobs:
 
       - name: Check TS linting
         run: |
-          npm install -g npm@latest
           npm install
           npm run lint
 

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
 
@@ -18,11 +18,12 @@ Check [user guide](docs/user-guide.md) for more detailed information.
 -   One-click button for verifying Kani harnesses.
 -   Generate counterexamples as Rust unit tests.
 -   Debug counterexamples using a standard debugger.
+-   View coverage information inline using VS Code source highlighting.
 
 ## 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.
 
@@ -32,7 +33,7 @@ NOTE: The extension only works on Cargo packages. For standalone Rust files, Kan
 | :-------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | :------------------------------------------------------------- |
 | `kani.enable-codelens` | Enable Codelens actions for `Run Test (Kani)` & `Debug Test (Kani)`.                                                                                                      | `true`                                                         |
 | `kani.show-output-window`     | Toggle to show the output terminal window containing the full output from Kani.                                                                  | `false`                                                     |
-
+| `kani.highlight-coverage` | Toggle to enable the codelens button for `Generage Coverage` by default.  | `false`
 
 ## Installation
 

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,30 @@ 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.
+
+
+#### De-highlight coverage information
+
+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).
+
+![De-highlight command](../resources/screenshots/de-highlight.png)

package.json

@@ -15,7 +15,7 @@
     "url": "https://github.com/model-checking/kani-vscode-extension/issues"
   },
   "qna": "https://github.com/model-checking/kani-vscode-extension/blob/main/docs/troubleshooting.md",
-  "version": "0.0.5",
+  "version": "0.0.6",
   "engines": {
     "vscode": "^1.70.0"
   },
@@ -53,6 +53,14 @@
         "title": "Disable Codelens",
         "command": "codelens-kani.disableCodeLens",
         "category": "CodeLens Sample"
+      },
+      {
+        "command": "codelens-kani.highlightCoverage",
+        "title": "Highlight Coverage"
+      },
+      {
+        "command": "codelens-kani.dehighlightCoverage",
+        "title": "De-Highlight Coverage"
       }
     ],
     "configuration": {
@@ -62,6 +70,11 @@
           "type": "boolean",
           "default": true
         },
+        "codelens-kani.highlightCoverage": {
+          "type": "boolean",
+          "default": false,
+          "description": "Controls the visibility of the `generate coverage` button by default."
+        },
         "Kani.showOutputWindow": {
           "type": "boolean",
           "default": false,

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));
+    }
+}

src/constants.ts

@@ -17,5 +17,5 @@ export namespace KaniArguments {
 	export const testsFlag: string = `--tests`;
 	export const outputFormatFlag: string = `--output-format`;
 	export const unstableFormatFlag: string = `--enable-unstable`;
-	export const stubbingFlag: string = `--enable-stubbing`;
+	export const stubbingFlag: string = `-Z=stubbing`;
 }

src/debugger/debugger.ts

@@ -44,8 +44,12 @@ async function getBinaryPath(): Promise<string | undefined> {
 
 		const output = execFileSync(kaniBinaryPath, commandSplit.args, options);
 		const outputString = output.toString();
-
 		const lines = outputString.trim().split('\n');
+		// Remove version string before JSON parsing
+		// NOTE: This is a temporary patch till <https://github.com/model-checking/kani/issues/2649> is fixed.
+		lines.shift();
+
+		// Parse JSON objects from response
 		const jsonMessages = lines.map((line: string) => JSON.parse(line));
 
 		/*

src/extension.ts

@@ -19,6 +19,8 @@ import {
 import { CodelensProvider } from './ui/CodeLensProvider';
 import { callConcretePlayback } from './ui/concrete-playback/concretePlayback';
 import { runKaniPlayback } from './ui/concrete-playback/kaniPlayback';
+import CoverageConfig from './ui/coverage/config';
+import { CoverageRenderer, runCodeCoverageAction } from './ui/coverage/coverageInfo';
 import { callViewerReport } from './ui/reportView/callReport';
 import { showInformationMessage } from './ui/showMessage';
 import { SourceCodeParser } from './ui/sourceCodeParser';
@@ -64,6 +66,9 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
 
 	// create a uri for the root folder
 	context.subscriptions.push(controller);
+	// Store coverage objects in a global cache when highlighting. When de-highlighting, the same objects need to be disposed
+	const coverageConfig = new CoverageConfig(context);
+	const globalConfig = GlobalConfig.getInstance();
 	const crateURI: Uri = getRootDirURI();
 	const treeRoot: vscode.TestItem = controller.createTestItem(
 		'Kani proofs',
@@ -225,20 +230,49 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
 		vscode.workspace.getConfiguration('codelens-kani').update('enableCodeLens', true, true);
 	});
 
-	// Allows VSCode to disable VSCode globally
+	// Allows VSCode to disable code lens globally
 	vscode.commands.registerCommand('codelens-kani.disableCodeLens', () => {
 		vscode.workspace.getConfiguration('codelens-kani').update('enableCodeLens', false, true);
 	});
 
+	// Allows VSCode to enable highlighting globally
+	vscode.commands.registerCommand('codelens-kani.enableCoverage', () => {
+		vscode.workspace.getConfiguration('codelens-kani').update('highlightCoverage', true, true);
+	});
+
+	// Allows VSCode to disable highlighting globally
+	vscode.commands.registerCommand('codelens-kani.disableCoverage', () => {
+		vscode.workspace.getConfiguration('codelens-kani').update('highlightCoverage', false, true);
+	});
+
 	// Register the command for the code lens Kani test runner function
 	vscode.commands.registerCommand('codelens-kani.codelensAction', (args: any) => {
 		runKaniPlayback(args);
 	});
 
+	// Separate rendering logic and re-use everywhere to highlight and de-highlight
+	const renderer = new CoverageRenderer(coverageConfig);
+
+	// Register a command to de-highlight the coverage in the active editor
+	const dehighlightCoverageCommand = vscode.commands.registerCommand(
+		'codelens-kani.dehighlightCoverage',
+		() => {
+			globalConfig.setCoverage(new Map());
+			renderer.renderInterface(vscode.window.visibleTextEditors, new Map());
+		},
+	);
+
 	// Update the test tree with proofs whenever a test case is opened
 	context.subscriptions.push(
 		vscode.workspace.onDidOpenTextDocument(updateNodeForDocument),
 		vscode.workspace.onDidSaveTextDocument(async (e) => await updateNodeForDocument(e)),
+		vscode.window.onDidChangeActiveTextEditor((editor) => {
+			// VS Code resets highlighting whenever a document is changed or switched.
+			// In order to work around this issue, the highlighting needs to be rendered each time.
+			// To keep the rendering time short, we store the coverage metadata as a global cache.
+			const cache = globalConfig.getCoverage();
+			renderer.renderInterfaceForFile(editor!, cache);
+		}),
 	);
 
 	context.subscriptions.push(runKani);
@@ -251,4 +285,13 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
 			connectToDebugger(programName),
 		),
 	);
+	// Register the command for running the coverage action on a harness
+	context.subscriptions.push(
+		vscode.commands.registerCommand('codelens-kani.highlightCoverage', (args: any) => {
+			runCodeCoverageAction(renderer, args);
+		}),
+	);
+
+	// Register the command for de-highlighting kani's coverage action on a harness
+	context.subscriptions.push(dehighlightCoverageCommand);
 }

src/globalConfig.ts

@@ -3,6 +3,7 @@
 class GlobalConfig {
 	private static instance: GlobalConfig;
 	private filePath: string;
+	public coverageMap: any;
 
 	private constructor() {
 		this.filePath = '';
@@ -15,6 +16,16 @@ class GlobalConfig {
 		return GlobalConfig.instance;
 	}
 
+	// Store coverage as a cache to be accessed whenever a new text page is opened or switched
+	public setCoverage(coverageMap: any): void {
+		this.coverageMap = coverageMap;
+	}
+
+	// Retrieve coverage as a cache to be accessed whenever a new text page is opened or switched
+	public getCoverage(): any {
+		return this.coverageMap;
+	}
+
 	public setFilePath(filePath: string): void {
 		this.filePath = filePath;
 	}