Use concrete types instead of any

Author: Carolyn Zech

src/ui/coverage/config.ts

@@ -29,18 +29,12 @@ class CoverageConfig {
 			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);
 	}
 }

src/ui/coverage/coverageInfo.ts

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+import { ExecFileException, execFile } from 'child_process';
 import * as fs from 'fs';
 import * as path from 'path';
 
@@ -9,13 +10,22 @@ import Config from './config';
 import GlobalConfig from '../../globalConfig';
 import { fullToRelativePath, getRootDir } from '../../utils';
 
-const { execFile } = require('child_process');
+enum CoverageStatus {
+	COVERED = 'COVERED',
+	UNCOVERED = 'UNCOVERED',
+}
+
+// Coverage information for a given file.
+type FileCoverageMap = Map<vscode.Range, CoverageStatus>;
+
+// Map files to their coverage information.
+type CoverageMap = Map<string, FileCoverageMap>;
 
-// Interface for storing the coverage status for each line of a document.
-export interface CoverageLines {
-	full: vscode.Range[];
-	partial: vscode.Range[];
-	none: vscode.Range[];
+// Result of running the coverage command.
+interface CoverageCommandResult {
+	statusCode: number;
+	coverage?: CoverageMap;
+	error?: string;
 }
 
 const warningMessage = `Source-based coverage is an unstable feature.`;
@@ -32,15 +42,17 @@ export async function runCodeCoverageAction(
 
 	// Run this command: cargo kani --coverage -Z source-coverage --harness verify_success
 	// to generate the source coverage output
-	const playbackCommand: string = `${kaniBinaryPath} --coverage -Z source-coverage --harness ${functionName}`;
-	const processOutput = await runCoverageCommand(playbackCommand, functionName);
-	if (processOutput.statusCode == 0) {
-		const coverageGlobalMap = processOutput.result;
+	const coverageCommand: string = `${kaniBinaryPath} --coverage -Z source-coverage --harness ${functionName}`;
+	const processOutput = await runCoverageCommand(coverageCommand, functionName);
 
+	if (processOutput.statusCode === 0 && processOutput.coverage) {
 		// Convert the array of (file, line, status) objects into Map<file <line, status>>
 		// since we need to cache this globally
-		globalConfig.setCoverage(coverageGlobalMap);
-		renderer.renderInterface(vscode.window.visibleTextEditors, coverageGlobalMap);
+		globalConfig.setCoverage(processOutput.coverage);
+		renderer.renderInterface(vscode.window.visibleTextEditors, processOutput.coverage);
+	} else if (processOutput.error) {
+		renderer.clearAllHighlights(); // Clear highlights if there's an error
+		vscode.window.showErrorMessage(`Coverage generation failed: ${processOutput.error}`);
 	}
 }
 
@@ -51,7 +63,10 @@ export async function runCodeCoverageAction(
  * @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<any> {
+async function runCoverageCommand(
+	command: string,
+	harnessName: string,
+): Promise<CoverageCommandResult> {
 	// Get the full resolved path for the root directory of the crate
 	const directory = path.resolve(getRootDir());
 	const commmandSplit = command.split(' ');
@@ -68,13 +83,27 @@ async function runCoverageCommand(command: string, harnessName: string): Promise
 	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 });
-			}
-		});
+	return new Promise<CoverageCommandResult>((resolve) => {
+		execFile(
+			kaniBinaryPath,
+			args,
+			options,
+			(error: ExecFileException | null, stdout: string | Buffer, stderr: string | Buffer) => {
+				if (error) {
+					resolve({
+						statusCode: typeof error.code === 'number' ? error.code : 1,
+						error: error.message,
+					});
+				} else if (stdout) {
+					parseKaniCoverageOutput(stdout.toString()).then(resolve);
+				} else {
+					resolve({
+						statusCode: 1,
+						error: stderr.toString() || 'No output from coverage command',
+					});
+				}
+			},
+		);
 	});
 }
 
@@ -107,10 +136,9 @@ function readJsonFromPath(filePath: string): any {
  * @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<any | undefined> {
-	const kaniOutput: string = stdout;
-	const jsonFilePath = getCoverageJsonPath(kaniOutput);
-	const coverageMap: Map<string, Map<any, string>> = new Map();
+async function parseKaniCoverageOutput(stdout: string): Promise<CoverageCommandResult> {
+	const jsonFilePath = getCoverageJsonPath(stdout);
+	const coverageMap: CoverageMap = new Map();
 
 	if (jsonFilePath) {
 		const files = fs.readdirSync(jsonFilePath);
@@ -123,20 +151,19 @@ async function parseKaniCoverageOutput(stdout: string): Promise<any | undefined>
 				const filePath = path.join(jsonFilePath, kanirawJson);
 				const jsonContent = readJsonFromPath(filePath);
 
-				// Take this jsonContent and create an Map<file <region, status>>
-				if (jsonContent) {
-					for (const file in jsonContent['data']) {
-						const regions = jsonContent['data'][file];
-						const regionMap: Map<any, string> = new Map();
+				if (jsonContent && 'data' in jsonContent) {
+					for (const file in jsonContent.data) {
+						const regions = jsonContent.data[file];
+						const regionMap: FileCoverageMap = new Map();
 
 						for (const region of regions) {
 							const startLine = region.region.start[0];
 							const startCol = region.region.start[1];
 							const endLine = region.region.end[0];
 							const endCol = region.region.end[1];
 
-							const status = region.status;
-							// Create a VSCode range with start line and column
+							const status =
+								region.status === 'COVERED' ? CoverageStatus.COVERED : CoverageStatus.UNCOVERED;
 							const start = new vscode.Position(startLine - 1, startCol - 1);
 							const end = new vscode.Position(endLine - 1, endCol - 1);
 							const range = new vscode.Range(start, end);
@@ -151,8 +178,11 @@ async function parseKaniCoverageOutput(stdout: string): Promise<any | undefined>
 		}
 	}
 
-	if (coverageMap === undefined || coverageMap.size == 0) {
-		return '';
+	if (coverageMap.size === 0) {
+		return {
+			statusCode: 1,
+			error: 'No coverage data found',
+		};
 	}
 
 	// If the global setting for showing output is on, show the output
@@ -168,8 +198,10 @@ async function parseKaniCoverageOutput(stdout: string): Promise<any | undefined>
 		terminal.show();
 	}
 
-	// No command found from Kani
-	return coverageMap;
+	return {
+		statusCode: 0,
+		coverage: coverageMap,
+	};
 }
 
 // Class representing the Renderer that handles rendering coverage highlights in the editor.
@@ -180,136 +212,49 @@ export class CoverageRenderer {
 	}
 
 	/**
-	 * 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.
+	 * Clears all existing coverage highlights.
 	 */
-	public renderInterface(
-		editors: readonly vscode.TextEditor[],
-		coverageMap: Map<string, Map<any, any>>,
-	): 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 relativePath = fullToRelativePath(editor.document.fileName);
-			const fileMap = coverageMap.get(relativePath)!;
-
-			const coverageLines = this.convertMapToLines(fileMap);
-			this.renderHighlight(editor, coverageLines);
-			return;
+	public clearAllHighlights(): void {
+		vscode.window.visibleTextEditors.forEach((editor) => {
+			this.renderHighlight(editor, new Map());
 		});
 	}
 
-	public convertMapToLines(coverageMap: Map<any, any>): CoverageLines {
-		// Parse this into coverageLines i.e if the status of the range in coverageMap is COVERED, add it to full or else if it is UNCOVERED, add it to None
-		const coverageLines: CoverageLines = {
-			full: [],
-			none: [],
-			partial: [],
-		};
-
-		for (const [range, status] of coverageMap) {
-			if (status === 'COVERED') {
-				coverageLines.full.push(range);
-			} else if (status === 'UNCOVERED') {
-				coverageLines.none.push(range);
-			}
-		}
-
-		return coverageLines;
+	/**
+	 * 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: CoverageMap): void {
+		this.clearAllHighlights();
+		editors.forEach((editor) => this.renderInterfaceForFile(editor, coverageMap));
 	}
 
 	/**
 	 * 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<string, Map<any, string>>,
-	): void {
-		if (coverageMap.size == 0) {
-			const coverageLines: CoverageLines = {
-				full: [],
-				none: [],
-				partial: [],
-			};
-
-			this.renderHighlight(editor, coverageLines);
-		}
-
+	public renderInterfaceForFile(editor: vscode.TextEditor, coverageMap: CoverageMap): void {
 		const relativePath = fullToRelativePath(editor.document.fileName);
-		const fileMap = coverageMap.get(relativePath)!;
-		if (fileMap === undefined) {
-			return;
-		}
-
-		const coverageLines = this.convertMapToLines(fileMap);
-		this.renderHighlight(editor, coverageLines);
+		const fileMap = coverageMap.get(relativePath);
+		this.renderHighlight(editor, fileMap || new Map());
 	}
 
 	/**
-	 * 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'.
+	 * Applies the coverage highlights to the given text editor.
+	 * @param editor - The text editor to apply the coverage highlights to.
+	 * @param fileCoverageMap - A map containing coverage highlights for the file.
 	 */
-	public createCoverage(
-		doc: vscode.TextDocument,
-		coverageFileMap: Map<number, string>,
-	): CoverageLines {
-		const coverageLines: CoverageLines = {
-			full: [],
-			none: [],
-			partial: [],
-		};
+	public renderHighlight(editor: vscode.TextEditor, fileCoverageMap: FileCoverageMap): void {
+		const coveredRanges: vscode.Range[] = [];
+		const uncoveredRanges: vscode.Range[] = [];
 
-		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;
-			}
+		for (const [range, status] of fileCoverageMap) {
+			(status === CoverageStatus.COVERED ? coveredRanges : uncoveredRanges).push(range);
 		}
 
-		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);
+		editor.setDecorations(this.configStore.covered, coveredRanges);
+		editor.setDecorations(this.configStore.uncovered, uncoveredRanges);
 	}
 }