diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index ab9553e..2cfc3f3 100644 --- a/.github/workflows/format-check.yml +++ b/.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 diff --git a/README.md b/README.md index b542f0f..16ab67f 100644 --- a/README.md +++ b/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 diff --git a/docs/user-guide.md b/docs/user-guide.md index 87201f5..a3d62a2 100644 --- a/docs/user-guide.md +++ b/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) diff --git a/package-lock.json b/package-lock.json index b350880..457cf76 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,12 +1,12 @@ { "name": "kani-vscode-extension", - "version": "0.0.3", + "version": "0.0.6", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "kani-vscode-extension", - "version": "0.0.3", + "version": "0.0.6", "dependencies": { "esbuild": "0.16.2", "readline": "^1.3.0", @@ -3696,9 +3696,9 @@ } }, "node_modules/word-wrap": { - "version": "1.2.3", - "resolved": "https://registry.npmjs.org/word-wrap/-/word-wrap-1.2.3.tgz", - "integrity": "sha512-Hz/mrNwitNRh/HUAtM/VT/5VH+ygD6DV7mYKZAtHOrbs8U7lvPS6xf7EJKMF0uW1KJCl0H701g3ZGus+muE5vQ==", + "version": "1.2.5", + "resolved": "https://registry.npmjs.org/word-wrap/-/word-wrap-1.2.5.tgz", + "integrity": "sha512-BN22B5eaMMI9UMtjrGd5g5eCYPpCPDUy0FJXbYsaT5zYxjFOckS53SQDE3pWkVoWpHXVb3BrYcEN4Twa55B5cA==", "dev": true, "engines": { "node": ">=0.10.0" diff --git a/package.json b/package.json index 29770b5..00414cd 100644 --- a/package.json +++ b/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, diff --git a/resources/screenshots/coverage-info.png b/resources/screenshots/coverage-info.png new file mode 100644 index 0000000..f539092 Binary files /dev/null and b/resources/screenshots/coverage-info.png differ diff --git a/resources/screenshots/de-highlight.png b/resources/screenshots/de-highlight.png new file mode 100644 index 0000000..4de5298 Binary files /dev/null and b/resources/screenshots/de-highlight.png differ diff --git a/resources/test-crates/simple-test/Cargo.toml b/resources/test-crates/simple-test/Cargo.toml new file mode 100644 index 0000000..faf0c68 --- /dev/null +++ b/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] diff --git a/resources/test-crates/simple-test/src/funs.rs b/resources/test-crates/simple-test/src/funs.rs new file mode 100644 index 0000000..a8155d9 --- /dev/null +++ b/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 { + 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 diff --git a/resources/test-crates/simple-test/src/lib.rs b/resources/test-crates/simple-test/src/lib.rs new file mode 100644 index 0000000..8383971 --- /dev/null +++ b/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)); + } +} diff --git a/src/constants.ts b/src/constants.ts index 2417ac7..23f7189 100644 --- a/src/constants.ts +++ b/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`; } diff --git a/src/debugger/debugger.ts b/src/debugger/debugger.ts index cf784ad..c441e3f 100644 --- a/src/debugger/debugger.ts +++ b/src/debugger/debugger.ts @@ -44,8 +44,12 @@ async function getBinaryPath(): Promise { 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 is fixed. + lines.shift(); + + // Parse JSON objects from response const jsonMessages = lines.map((line: string) => JSON.parse(line)); /* diff --git a/src/extension.ts b/src/extension.ts index 2e5b7d7..87340f1 100644 --- a/src/extension.ts +++ b/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 // 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 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 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); } diff --git a/src/globalConfig.ts b/src/globalConfig.ts index 00270ef..b3d7cc6 100644 --- a/src/globalConfig.ts +++ b/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; } diff --git a/src/model/kaniCommandCreate.ts b/src/model/kaniCommandCreate.ts index ff7d976..897113f 100644 --- a/src/model/kaniCommandCreate.ts +++ b/src/model/kaniCommandCreate.ts @@ -72,19 +72,13 @@ function createCommand( testFlag: boolean = false, stubbing_args?: boolean, ): string { - let harnessCommand = ''; - if (!testFlag) { - if (stubbing_args === undefined || !stubbing_args) { - harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.packageFlag} ${packageName} ${KaniArguments.harnessFlag} ${harnessName}`; - } else { - harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.unstableFormatFlag} ${KaniArguments.stubbingFlag} ${KaniArguments.packageFlag} ${packageName} ${KaniArguments.harnessFlag} ${harnessName}`; - } - } else { - if (stubbing_args === undefined || !stubbing_args) { - harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.testsFlag} ${KaniArguments.packageFlag} ${packageName} ${KaniArguments.harnessFlag} ${harnessName}`; - } else { - harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.testsFlag} ${KaniArguments.unstableFormatFlag} ${KaniArguments.stubbingFlag} ${KaniArguments.packageFlag} ${packageName} ${KaniArguments.harnessFlag} ${harnessName}`; - } + let harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.packageFlag} ${packageName} ${KaniArguments.harnessFlag} ${harnessName}`; + if (testFlag) { + harnessCommand = `${harnessCommand} ${KaniArguments.testsFlag}`; + } + + if (stubbing_args !== undefined && stubbing_args) { + harnessCommand = `${harnessCommand} ${KaniArguments.stubbingFlag}`; } return harnessCommand; diff --git a/src/ui/CodeLensProvider.ts b/src/ui/CodeLensProvider.ts index 378b67e..90361dd 100644 --- a/src/ui/CodeLensProvider.ts +++ b/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; } diff --git a/src/ui/coverage/config.ts b/src/ui/coverage/config.ts new file mode 100644 index 0000000..63497a4 --- /dev/null +++ b/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; diff --git a/src/ui/coverage/coverageInfo.ts b/src/ui/coverage/coverageInfo.ts new file mode 100644 index 0000000..87ae7be --- /dev/null +++ b/src/ui/coverage/coverageInfo.ts @@ -0,0 +1,294 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +import * as path from 'path'; + +import * as vscode from 'vscode'; + +import GlobalConfig from '../../globalConfig'; +import { getKaniPath } from '../../model/kaniRunner'; +import { CommandArgs, getRootDir, splitCommand } from '../../utils'; +import Config from './config'; + +const { execFile } = require('child_process'); + +// Interface for parsing Kani's output and storing as an object +interface CoverageEntry { + filePath: string; + lineNumber: number; + coverageStatus: string; +} + +// Interface for storing the coverage status for each line of a document. +export interface CoverageLines { + full: vscode.Range[]; + partial: vscode.Range[]; + none: vscode.Range[]; +} + +enum CoverageStatus { + Full = "FULL", + Partial = "PARTIAL", + None = "NONE" +} + +const warningMessage = `Line coverage is an unstable feature.`; + +// Callback function for the coverage code lens action +export async function runCodeCoverageAction(renderer: CoverageRenderer, functionName: string): Promise { + const globalConfig = GlobalConfig.getInstance(); + const kaniBinaryPath = globalConfig.getFilePath(); + + vscode.window.showWarningMessage(warningMessage); + + const activeEditor = vscode.window.activeTextEditor; + const currentFileUri = activeEditor?.document.uri.fsPath; + + const playbackCommand: string = `${kaniBinaryPath} --coverage -Z line-coverage --harness ${functionName}`; + const processOutput = await runCoverageCommand(playbackCommand, functionName); + + + if(processOutput.statusCode == 0) { + const coverageOutputArray = processOutput.result; + + // Convert the array of (file, line, status) objects into Map> + // since we need to cache this globally + const coverageGlobalMap = parseCoverageFormatted(coverageOutputArray); + globalConfig.setCoverage(coverageGlobalMap); + + renderer.renderInterface(vscode.window.visibleTextEditors, coverageGlobalMap); + } +} + +/** + * Run the --coverage command (with -Z line-coverage) to generate the coverage output, parse the output and return the result + * + * @param command - the kani command to run along with the harness name + * @param harnessName - name of the harness + * @returns - the result of executing the --coverage command and parsing the output + */ +async function runCoverageCommand(command: string, harnessName: string): Promise { + // Get the full resolved path for the root directory of the crate + const directory = path.resolve(getRootDir()); + const commmandSplit = command.split(' '); + + // Get args for the command to be executed + const args = commmandSplit.slice(1); + + const options = { + shell: false, + cwd: directory, + }; + + const globalConfig = GlobalConfig.getInstance(); + const kaniBinaryPath = globalConfig.getFilePath(); + + vscode.window.showInformationMessage(`Generating coverage for ${harnessName}`); + return new Promise((resolve, _reject) => { + execFile(kaniBinaryPath, args, options, async (_error: any, stdout: any, _stderr: any) => { + if (stdout) { + const parseResult = await parseKaniCoverageOutput(stdout); + resolve({ statusCode: 0, result: parseResult }); + } + }); + }); +} + +/** + * Search for the path to the report printed in Kani's output, and detect if we are in a remote + * enviroment before returning the result. + * + * @param stdout - Kani's standard output after running the visualize command + * @returns - undefined (error) or a result that indicates if the extension is executed on a local + * or remote environment. The result includes a `path` (if local) or a `command` (if remote). + */ +async function parseKaniCoverageOutput(stdout: string): Promise { + const kaniOutput: string = stdout; + const kaniOutputArray: string[] = kaniOutput.split('Coverage Results:\n'); + + const coverageResults = kaniOutputArray.at(1); + + if(coverageResults === undefined) { + return ''; + } + + const coverageResultsArray = coverageResults.split('\n')!; + + // If the global setting for showing output is on, show the output + const config = vscode.workspace.getConfiguration('Kani'); + const showOutputWindow = config.get('showOutputWindow'); + + const terminal = vscode.window.createOutputChannel('Coverage Report'); + terminal.appendLine(coverageResults); + + // Use the value to show or hide the output window + if (showOutputWindow) { + // Open channel but don't change focus + terminal.show(); + } + + const coverage = parseCoverageData(coverageResultsArray); + + // No command found from Kani + return coverage; +} + +// Parse `CoverageEntry` objects and convert it into CoverageMap or a map>. +// We store this map as the global cache since it allows easy sorting and retrieval by file name, needed by VS Code. +function parseCoverageFormatted(entries: CoverageEntry[]): Map> { + const nestedMap: Map> = new Map(); + + for (const entry of entries) { + const { filePath, lineNumber, coverageStatus } = entry; + + // Check if the outer map already has an entry for the filePath + let innerMap = nestedMap.get(filePath); + + // If not, create a new inner map and set it in the outer map + if (!innerMap) { + innerMap = new Map(); + nestedMap.set(filePath, innerMap); + } + + // Set the coverageStatus in the inner map for the lineNumber + innerMap.set(lineNumber, coverageStatus); + } + + return nestedMap; +} + +// Convert coverage Kani's output into CoverageEntry objects +function parseCoverageData(data: string[]): CoverageEntry[] { + const coverageEntries: CoverageEntry[] = []; + + for (const entry of data) { + const parts = entry.split(', '); + + if (parts.length === 3) { + const [filePath, lineNumberStr, coverageStatus] = parts; + if(filePath.includes('Complete - ')) { + return coverageEntries; + } + const lineNumber = parseInt(lineNumberStr.trim(), 10); + + coverageEntries.push({ + filePath, + lineNumber, + coverageStatus, + }); + } + } + + return coverageEntries; +} + +// Class representing the Renderer that handles rendering coverage highlights in the editor. +export class CoverageRenderer { + private configStore: Config; + constructor( + configStore: Config, + ) { + this.configStore = configStore; + } + + /** + * Renders coverage highlights for multiple files. + * @param editors - An array of text editor files to render coverage highlights for. + * @param coverageMap - A map containing coverage data for each file. + */ + public renderInterface(editors: readonly vscode.TextEditor[], coverageMap: Map>): void { + editors.forEach((editor) => { + // If coverageMap is empty, de-highlight the files + if(coverageMap.size == 0) { + const coverageLines: CoverageLines = { + full: [], + none: [], + partial: [], + }; + + this.renderHighlight(editor, coverageLines); + return; + } + + // Fetch the coverage data for a file from the coverageMap. + const fileMap = coverageMap.get(editor.document.fileName)!; + const coverageLines = this.createCoverage(editor.document, fileMap); + this.renderHighlight(editor, coverageLines); + return; + }); + } + + /** + * Renders coverage highlights for a single text editor file. + * @param editor - The text editor to render coverage highlights for. + * @param coverageMap - A map containing coverage data for each file. + */ + public renderInterfaceForFile(editor: vscode.TextEditor, coverageMap: Map>): void { + if(coverageMap.size == 0) { + const coverageLines: CoverageLines = { + full: [], + none: [], + partial: [], + }; + + this.renderHighlight(editor, coverageLines); + } + const fileMap = coverageMap.get(editor.document.fileName); + if(fileMap === undefined){ + return; + } + const coverageLines = this.createCoverage(editor.document, fileMap); + this.renderHighlight(editor, coverageLines); + } + + + /** + * Creates coverage highlights for a given text document based on the coverageFileMap. + * @param doc - The text document for which coverage highlights are to be created. + * @param coverageFileMap - A map containing coverage status for each line number. + * @returns An object containing coverage highlights categorized as 'full', 'partial', and 'none'. + */ + public createCoverage(doc: vscode.TextDocument, coverageFileMap: Map): CoverageLines { + const coverageLines: CoverageLines = { + full: [], + none: [], + partial: [], + }; + + for (let lineNum = 1; lineNum <= doc.lineCount; lineNum++) { + const line = doc.lineAt(lineNum - 1); + const status = coverageFileMap.get(lineNum); + + if(status === undefined) { + continue; + } + + const range = new vscode.Range(line.range.start, line.range.end); + switch (status) { + case "FULL": + coverageLines.full.push(range); + break; + case "PARTIAL": + coverageLines.partial.push(range); + break; + case "NONE": + coverageLines.none.push(range); + break; + default: + break; + } + } + + return coverageLines; + } + + /** + * Applies the coverage highlights to the given text editor. + * @param editor - The text editor to apply the coverage highlights to. + * @param coverageLinesInfo - An object containing coverage highlights categorized as 'full', 'partial', and 'none'. + */ + public renderHighlight(editor: vscode.TextEditor, coverageLinesInfo: CoverageLines): void { + editor.setDecorations(this.configStore.covered, coverageLinesInfo.full); + editor.setDecorations(this.configStore.partialcovered, coverageLinesInfo.partial); + editor.setDecorations(this.configStore.uncovered, coverageLinesInfo.none); + } +}