Create coverage UI (#122)

Author: jaisnan

package.json

@@ -52,6 +52,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": {
@@ -61,6 +69,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,

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

src/ui/CodeLensProvider.ts

@@ -44,7 +44,7 @@ export class CodelensProvider implements vscode.CodeLensProvider {
 				const function_item_name = item.at(0);
 
 				if (function_item_name === undefined) {
-					return [];
+					continue;
 				}
 
 				const startPosition = item.at(1);
@@ -77,6 +77,43 @@ export class CodelensProvider implements vscode.CodeLensProvider {
 					this.codeLenses.push(debugTestCodelens);
 				}
 			}
+
+			// The setting for the coverage code lens needs to be switched on for the mechanism
+			// to be enabled
+			if (vscode.workspace.getConfiguration('codelens-kani').get('highlightCoverage', true)) {
+				// Retrieve harness metadata from the tree-sitter which will be used to place the
+				// `Get coverage info` code lens button.
+				const kani_harnesses = await SourceCodeParser.getAttributeFromRustFile(text);
+
+				for (const harness of kani_harnesses) {
+					const harness_name = harness.harnessName;
+
+					// If the harness is empty or undefined, skip to the next iteration
+					if (harness_name === undefined || harness_name === '') {
+						continue;
+					}
+
+					const startPosition = harness.endPosition;
+
+					// This is the metadata that VSCode needs to place the codelens button
+					const line = document.lineAt(startPosition.row);
+					const indexOf = line.text.indexOf(harness_name);
+					const position = new vscode.Position(line.lineNumber, indexOf);
+					const range = document.getWordRangeAtPosition(position);
+
+					const codeCoverageAction = {
+						title: '$(play) Get coverage info',
+						tooltip: 'Highlight code with coverage information generated by Kani',
+						command: 'codelens-kani.highlightCoverage',
+						arguments: [harness_name],
+					};
+
+					if (range) {
+						const codeCoverageCodelens = new vscode.CodeLens(range, codeCoverageAction);
+						this.codeLenses.push(codeCoverageCodelens);
+					}
+				}
+			}
 			return this.codeLenses;
 		}
 

src/ui/coverage/config.ts

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+import { DecorationRenderOptions, ExtensionContext, TextEditorDecorationType, window } from "vscode";
+
+// Takes the extension context and stores the specified decoration (VS Code highliging API) values for that context
+// By storing the decoration values per context, we allow users to de-highlight the same contexts.
+// Without caching these values as a global cache, VS Code does not de-highlight.
+class CoverageConfig {
+    public covered!: TextEditorDecorationType;
+    public partialcovered!: TextEditorDecorationType;
+    public uncovered!: TextEditorDecorationType;
+
+    private context: ExtensionContext;
+
+    constructor(context: ExtensionContext) {
+        this.context = context;
+        this.setup();
+    }
+
+    private setup(): void {
+        const fullDecoration: DecorationRenderOptions = {
+            backgroundColor: 'rgba(0, 255, 0, 0.2)', // Green background
+            isWholeLine: false
+        };
+
+        const partialDecoration: DecorationRenderOptions = {
+            backgroundColor: 'rgba(255, 255, 0, 0.2)', // Yellow background
+            isWholeLine: false
+        };
+
+        const noDecoration: DecorationRenderOptions = {
+            backgroundColor: 'rgba(255, 0, 0, 0.2)', // Red background
+            isWholeLine: false
+        };
+
+        this.covered = window.createTextEditorDecorationType(fullDecoration);
+        this.partialcovered = window.createTextEditorDecorationType(partialDecoration);
+        this.uncovered = window.createTextEditorDecorationType(noDecoration);
+    }
+}
+
+export default CoverageConfig;