diff --git a/package.json b/package.json index d55fe832..90f5b84b 100644 --- a/package.json +++ b/package.json @@ -2,7 +2,7 @@ "name": "prusti-assistant", "displayName": "Prusti Assistant", "description": "Verify Rust programs with the Prusti verifier.", - "version": "0.12.6", + "version": "0.12.7", "publisher": "viper-admin", "repository": { "type": "git", diff --git a/src/crateMetadata.ts b/src/crateMetadata.ts new file mode 100644 index 00000000..804778e3 --- /dev/null +++ b/src/crateMetadata.ts @@ -0,0 +1,62 @@ +import * as util from "./util"; +import * as config from "./config"; +import * as dependencies from "./dependencies"; + +export interface CrateMetadata { + target_directory: string; + workspace_root?: string; +} + +export enum CrateMetadataStatus { + Error, + Ok +} + +/** + * Queries for the metadata of a Rust crate using cargo-prusti. + * + * @param prusti The location of Prusti files. + * @param cratePath The path of a Rust crate. + * @param destructors Where to store the destructors of the spawned processes. + * @returns A tuple containing the metadata, the exist status, and the duration of the query. + */ +export async function queryCrateMetadata( + prusti: dependencies.PrustiLocation, + cratePath: string, + destructors: Set, +): Promise<[CrateMetadata, CrateMetadataStatus, util.Duration]> { + const cargoPrustiArgs = ["--no-deps", "--offline", "--format-version=1"].concat( + config.extraCargoPrustiArgs() + ); + const cargoPrustiEnv = { + ...process.env, // Needed to run Rustup + ...{ + PRUSTI_CARGO_COMMAND: "metadata", + PRUSTI_QUIET: "true", + }, + ...config.extraPrustiEnv(), + }; + const output = await util.spawn( + prusti.cargoPrusti, + cargoPrustiArgs, + { + options: { + cwd: cratePath, + env: cargoPrustiEnv, + } + }, + destructors, + ); + let status = CrateMetadataStatus.Error; + if (output.code === 0) { + status = CrateMetadataStatus.Ok; + } + if (/error: internal compiler error/.exec(output.stderr) !== null) { + status = CrateMetadataStatus.Error; + } + if (/^thread '.*' panicked at/.exec(output.stderr) !== null) { + status = CrateMetadataStatus.Error; + } + const metadata = JSON.parse(output.stdout) as CrateMetadata; + return [metadata, status, output.duration]; +} diff --git a/src/diagnostics.ts b/src/diagnostics.ts index ee453a41..3b9df8ed 100644 --- a/src/diagnostics.ts +++ b/src/diagnostics.ts @@ -4,6 +4,7 @@ import * as vscode from "vscode"; import * as path from "path"; import * as vvt from "vs-verification-toolbox"; import * as dependencies from "./dependencies"; +import { queryCrateMetadata, CrateMetadataStatus } from "./crateMetadata"; // ======================================================== // JSON Schemas @@ -142,12 +143,13 @@ function getCallSiteSpan(span: Span): Span { /** * Parses a message into a diagnostic. - * - * @param msg The message to parse. - * @param rootPath The root path of the rust project the message was generated - * for. + * + * @param msgDiag The message to parse. + * @param basePath The base path to resolve the relative paths in the diagnostics. + * @param defaultRange The default range to use if no span is found in the message. + * @returns The parsed diagnostic. */ -function parseCargoMessage(msgDiag: CargoMessage, rootPath: string, defaultRange?: vscode.Range): Diagnostic { +function parseCargoMessage(msgDiag: CargoMessage, basePath: string, defaultRange?: vscode.Range): Diagnostic { const msg = msgDiag.message; const level = parseMessageLevel(msg.level); @@ -174,7 +176,10 @@ function parseCargoMessage(msgDiag: CargoMessage, rootPath: string, defaultRange let primaryRange = defaultRange ?? dummyRange(); if (primaryCallSiteSpans.length > 0) { primaryRange = parseMultiSpanRange(primaryCallSiteSpans); - primaryFilePath = path.join(rootPath, primaryCallSiteSpans[0].file_name); + primaryFilePath = primaryCallSiteSpans[0].file_name; + if (!path.isAbsolute(primaryFilePath)) { + primaryFilePath = path.join(basePath, primaryFilePath); + } } const diagnostic = new vscode.Diagnostic( primaryRange, @@ -192,7 +197,7 @@ function parseCargoMessage(msgDiag: CargoMessage, rootPath: string, defaultRange const message = `[Note] ${span.label ?? ""}`; const callSiteSpan = getCallSiteSpan(span); const range = parseSpanRange(callSiteSpan); - const filePath = path.join(rootPath, callSiteSpan.file_name); + const filePath = path.join(basePath, callSiteSpan.file_name); const fileUri = vscode.Uri.file(filePath); relatedInformation.push( @@ -211,7 +216,7 @@ function parseCargoMessage(msgDiag: CargoMessage, rootPath: string, defaultRange }, message: child }; - const childDiagnostic = parseCargoMessage(childMsgDiag, rootPath, primaryRange); + const childDiagnostic = parseCargoMessage(childMsgDiag, basePath, primaryRange); const fileUri = vscode.Uri.file(childDiagnostic.file_path); relatedInformation.push( new vscode.DiagnosticRelatedInformation( @@ -235,12 +240,11 @@ function parseCargoMessage(msgDiag: CargoMessage, rootPath: string, defaultRange /** * Parses a message into diagnostics. - * + * * @param msg The message to parse. - * @param rootPath The root path of the rust project the message was generated - * for. + * @param filePath The path of the file that was being compiled. */ -function parseRustcMessage(msg: Message, mainFilePath: string, defaultRange?: vscode.Range): Diagnostic { +function parseRustcMessage(msg: Message, filePath: string, defaultRange?: vscode.Range): Diagnostic { const level = parseMessageLevel(msg.level); // Read primary message @@ -262,7 +266,7 @@ function parseRustcMessage(msg: Message, mainFilePath: string, defaultRange?: vs } // Convert MultiSpans to Range and Diagnostic - let primaryFilePath = mainFilePath; + let primaryFilePath = filePath; let primaryRange = defaultRange ?? dummyRange(); if (primaryCallSiteSpans.length > 0) { primaryRange = parseMultiSpanRange(primaryCallSiteSpans); @@ -297,7 +301,7 @@ function parseRustcMessage(msg: Message, mainFilePath: string, defaultRange?: vs // Recursively parse child messages. for (const child of msg.children) { - const childDiagnostic = parseRustcMessage(child, mainFilePath, primaryRange); + const childDiagnostic = parseRustcMessage(child, filePath, primaryRange); const fileUri = vscode.Uri.file(childDiagnostic.file_path); relatedInformation.push( new vscode.DiagnosticRelatedInformation( @@ -320,13 +324,13 @@ function parseRustcMessage(msg: Message, mainFilePath: string, defaultRange?: vs } /** - * Removes rust's metadata in the specified project folder. This is a work + * Removes Rust's metadata in the specified project folder. This is a work * around for `cargo check` not reissuing warning information for libs. - * - * @param rootPath The root path of a rust project. + * + * @param targetPath The target path of a rust project. */ -async function removeDiagnosticMetadata(rootPath: string) { - const pattern = new vscode.RelativePattern(path.join(rootPath, "target", "debug"), "*.rmeta"); +async function removeDiagnosticMetadata(targetPath: string) { + const pattern = new vscode.RelativePattern(path.join(targetPath, "debug"), "*.rmeta"); const files = await vscode.workspace.findFiles(pattern); const promises = files.map(file => { return (new vvt.Location(file.fsPath)).remove() @@ -341,14 +345,27 @@ enum VerificationStatus { } /** - * Queries for the diagnostics of a rust project using cargo-prusti. - * - * @param rootPath The root path of a rust project. - * @returns An array of diagnostics for the given rust project. + * Queries for the diagnostics of a rust crate using cargo-prusti. + * + * @param prusti The location of Prusti files. + * @param cratePath The path of a Rust crate. + * @param destructors Where to store the destructors of the spawned processes. + * @returns A tuple containing the diagnostics, status and duration of the verification. */ -async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, rootPath: string, serverAddress: string, destructors: Set): Promise<[Diagnostic[], VerificationStatus, util.Duration]> { +async function queryCrateDiagnostics( + prusti: dependencies.PrustiLocation, + cratePath: string, + serverAddress: string, + destructors: Set, +): Promise<[Diagnostic[], VerificationStatus, util.Duration]> { + const [metadata, metadataStatus, metadataDuration] = await queryCrateMetadata(prusti, cratePath, destructors); + if (metadataStatus !== CrateMetadataStatus.Ok) { + return [[], VerificationStatus.Crash, metadataDuration]; + } + // FIXME: Workaround for warning generation for libs. - await removeDiagnosticMetadata(rootPath); + await removeDiagnosticMetadata(metadata.target_directory); + const cargoPrustiArgs = ["--message-format=json"].concat( config.extraCargoPrustiArgs() ); @@ -366,7 +383,7 @@ async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, rootPa cargoPrustiArgs, { options: { - cwd: rootPath, + cwd: cratePath, env: cargoPrustiEnv, } }, @@ -388,26 +405,34 @@ async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, rootPa if (/^thread '.*' panicked at/.exec(output.stderr) !== null) { status = VerificationStatus.Crash; } + const basePath = metadata.workspace_root ?? cratePath; const diagnostics: Diagnostic[] = []; for (const messages of parseCargoOutput(output.stdout)) { diagnostics.push( - parseCargoMessage(messages, rootPath) + parseCargoMessage(messages, basePath) ); } return [diagnostics, status, output.duration]; } /** - * Queries for the diagnostics of a rust program using prusti-rustc. - * - * @param programPath The root path of a rust program. - * @returns An array of diagnostics for the given rust project. + * Queries for the diagnostics of a rust crate using prusti-rustc. + * + * @param prusti The location of Prusti files. + * @param filePath The path of a Rust program. + * @param destructors Where to store the destructors of the spawned processes. + * @returns A tuple containing the diagnostics, status and duration of the verification. */ -async function queryProgramDiagnostics(prusti: dependencies.PrustiLocation, programPath: string, serverAddress: string, destructors: Set): Promise<[Diagnostic[], VerificationStatus, util.Duration]> { +async function queryProgramDiagnostics( + prusti: dependencies.PrustiLocation, + filePath: string, + serverAddress: string, + destructors: Set, +): Promise<[Diagnostic[], VerificationStatus, util.Duration]> { const prustiRustcArgs = [ "--crate-type=lib", "--error-format=json", - programPath + filePath ].concat( config.extraPrustiRustcArgs() ); @@ -425,7 +450,7 @@ async function queryProgramDiagnostics(prusti: dependencies.PrustiLocation, prog prustiRustcArgs, { options: { - cwd: path.dirname(programPath), + cwd: path.dirname(filePath), env: prustiRustcEnv, } }, @@ -450,7 +475,7 @@ async function queryProgramDiagnostics(prusti: dependencies.PrustiLocation, prog const diagnostics: Diagnostic[] = []; for (const messages of parseRustcOutput(output.stderr)) { diagnostics.push( - parseRustcMessage(messages, programPath) + parseRustcMessage(messages, filePath) ); } return [diagnostics, status, output.duration]; diff --git a/src/test/extension.test.ts b/src/test/extension.test.ts index 82421b81..615f40ff 100644 --- a/src/test/extension.test.ts +++ b/src/test/extension.test.ts @@ -9,11 +9,30 @@ import * as config from "../config"; import * as state from "../state"; import * as extension from "../extension" +/** + * Get the path of the workspace. + * + * @returns The path of the workspace. + */ function workspacePath(): string { assert.ok(vscode.workspace.workspaceFolders?.length); return vscode.workspace.workspaceFolders[0].uri.fsPath; } +/** + * Convert a URI to a relative workspace path with forward slashes. + * + * @param uri The URI to convert. + * @returns The computed relative path. + */ +function asRelativeWorkspacePath(target: vscode.Uri): string { + // Resolve symlinks (e.g., in MacOS, `/var` is a symlink to `/private/var`). + // We do this manually becase `vscode.workspace.asRelativePath` does not resolve symlinks. + const normalizedTarget = fs.realpathSync(target.fsPath); + const normalizedWorkspace = fs.realpathSync(workspacePath()); + return path.relative(normalizedWorkspace, normalizedTarget).replace(/\\/g, "/"); +} + /** * Open a file in the IDE * @param filePath The file to open. @@ -31,7 +50,7 @@ function openFile(filePath: string): Promise { } /** - * Evaluate tje filter used in the `.rs.json` expected diagnostics. + * Evaluate one of the filters contained in the `.rs.json` expected diagnostics. * @param filter The filter dictionary. * @param name The name of the filter. * @returns True if the filter is fully satisfied, otherwise false. @@ -56,15 +75,17 @@ function evaluateFilter(filter: [string: string], name: string): boolean { return true; } -// Types that make sure our tests don't rely on the stringification of vscode +// JSON-like types used to normalize the diagnostics type Position = { line: number, character: number } + type Range = { start: Position, end: Position } + type RelatedInformation = { location: { uri: string, @@ -72,7 +93,10 @@ type RelatedInformation = { }, message: string } + type Diagnostic = { + // This path is relative to VSCode's workspace + uri: string, range: Range, severity: number, message: string, @@ -91,18 +115,26 @@ function rangeToPlainObject(range: vscode.Range): Range { } }; } -function diagnosticToPlainObject(diagnostic: vscode.Diagnostic): Diagnostic { + +/** + * Normalize a diagnostic, converting it to a plain object. + * + * @param uri The URI of the file containing the diagnostic. + * @param diagnostic The diagnostic to convert. + * @returns The normalized diagnostic. + */ +function diagnosticToPlainObject(uri: vscode.Uri, diagnostic: vscode.Diagnostic): Diagnostic { const plainDiagnostic: Diagnostic = { + uri: asRelativeWorkspacePath(uri), range: rangeToPlainObject(diagnostic.range), severity: diagnostic.severity, message: diagnostic.message, }; if (diagnostic.relatedInformation) { plainDiagnostic.relatedInformation = diagnostic.relatedInformation.map((relatedInfo) => { - const uri = vscode.workspace.asRelativePath(relatedInfo.location.uri); return { location: { - uri: uri, + uri: asRelativeWorkspacePath(relatedInfo.location.uri), range: rangeToPlainObject(relatedInfo.location.range) }, message: relatedInfo.message, @@ -112,7 +144,7 @@ function diagnosticToPlainObject(diagnostic: vscode.Diagnostic): Diagnostic { return plainDiagnostic; } -// Prepare the workspace +// Constants used in the tests const PROJECT_ROOT = path.join(__dirname, "..", ".."); const SCENARIOS_ROOT = path.join(PROJECT_ROOT, "src", "test", "scenarios"); const SCENARIO = process.env.SCENARIO; @@ -153,12 +185,12 @@ describe("Extension", () => { }) it(`scenario ${SCENARIO} can update Prusti`, async () => { - // tests are run serially, so nothing will run & break while we're updating + // Tests are run serially, so nothing will run & break while we're updating await openFile(path.join(workspacePath(), "programs", "assert_true.rs")); await vscode.commands.executeCommand("prusti-assistant.update"); }); - // Test every Rust program in the workspace + // Generate a test for every Rust program with expected diagnostics in the test suite. const programs: Array = [SCENARIO_PATH, SHARED_SCENARIO_PATH].flatMap(cwd => glob.sync("**/*.rs.json", { cwd: cwd }).map(filePath => filePath.replace(/\.json$/, "")) ); @@ -166,12 +198,19 @@ describe("Extension", () => { assert.ok(programs.length >= 3, `There are not enough programs to test (${programs.length})`); programs.forEach(program => { it(`scenario ${SCENARIO} reports expected diagnostics on ${program}`, async () => { + // Verify the program const programPath = path.join(workspacePath(), program); await openFile(programPath); await vscode.commands.executeCommand("prusti-assistant.clear-diagnostics"); await vscode.commands.executeCommand("prusti-assistant.verify"); - const diagnostics = vscode.languages.getDiagnostics().flatMap((pair) => pair[1]); - const plainDiagnostics = diagnostics.map(diagnosticToPlainObject); + + // Collect and normalize the diagnostics + const plainDiagnostics = vscode.languages.getDiagnostics().flatMap(pair => { + const [uri, diagnostics] = pair; + return diagnostics.map(diagnostic => diagnosticToPlainObject(uri, diagnostic)); + }); + + // Load the expected diagnostics. A single JSON file can contain multiple alternatives. const expectedData = await fs.readFile(programPath + ".json", "utf-8"); type MultiDiagnostics = [ { filter?: [string: string], diagnostics: Diagnostic[] } @@ -185,7 +224,8 @@ describe("Extension", () => { } else { expectedMultiDiagnostics = expected as MultiDiagnostics; } - // Different Prusti versions or OSs migh report slightly different diagnostics. + + // Select the expected diagnostics to be used for the current environment let expectedDiagnostics = expectedMultiDiagnostics.find((alternative, index) => { if (!alternative.filter) { console.log( @@ -205,6 +245,7 @@ describe("Extension", () => { }; } + // Compare the actual with the expected diagnostics expect(plainDiagnostics).to.deep.equal(expectedDiagnostics.diagnostics); }); }); diff --git a/src/test/scenarios/shared/crates/git_contracts/src/main.rs.json b/src/test/scenarios/shared/crates/git_contracts/src/main.rs.json index 5491a2fa..01da7242 100644 --- a/src/test/scenarios/shared/crates/git_contracts/src/main.rs.json +++ b/src/test/scenarios/shared/crates/git_contracts/src/main.rs.json @@ -45,7 +45,8 @@ "message": "if this is intentional, prefix it with an underscore" } ], - "severity": 1 + "severity": 1, + "uri": "crates/git_contracts/src/main.rs" }, { "message": "[Prusti: verification error] precondition might not hold.", @@ -77,6 +78,7 @@ "message": "the failing assertion is here" } ], - "severity": 0 + "severity": 0, + "uri": "crates/git_contracts/src/main.rs" } ] diff --git a/src/test/scenarios/shared/crates/latest_contracts/src/main.rs.json b/src/test/scenarios/shared/crates/latest_contracts/src/main.rs.json index 1c2f7027..0d82aec7 100644 --- a/src/test/scenarios/shared/crates/latest_contracts/src/main.rs.json +++ b/src/test/scenarios/shared/crates/latest_contracts/src/main.rs.json @@ -45,7 +45,8 @@ "message": "if this is intentional, prefix it with an underscore" } ], - "severity": 1 + "severity": 1, + "uri": "crates/latest_contracts/src/main.rs" }, { "message": "[Prusti: verification error] precondition might not hold.", @@ -77,6 +78,7 @@ "message": "the failing assertion is here" } ], - "severity": 0 + "severity": 0, + "uri": "crates/latest_contracts/src/main.rs" } ] diff --git a/src/test/scenarios/shared/crates/workspace/Cargo.toml b/src/test/scenarios/shared/crates/workspace/Cargo.toml new file mode 100644 index 00000000..5c3d587a --- /dev/null +++ b/src/test/scenarios/shared/crates/workspace/Cargo.toml @@ -0,0 +1,5 @@ +[workspace] +members = [ + "first", + "second", +] diff --git a/src/test/scenarios/shared/crates/workspace/first/Cargo.toml b/src/test/scenarios/shared/crates/workspace/first/Cargo.toml new file mode 100644 index 00000000..d35aa325 --- /dev/null +++ b/src/test/scenarios/shared/crates/workspace/first/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "first" +version = "0.1.0" +edition = "2021" + +[dependencies] +prusti-contracts = "*" diff --git a/src/test/scenarios/shared/crates/workspace/first/src/lib.rs b/src/test/scenarios/shared/crates/workspace/first/src/lib.rs new file mode 100644 index 00000000..b5b125a7 --- /dev/null +++ b/src/test/scenarios/shared/crates/workspace/first/src/lib.rs @@ -0,0 +1,10 @@ +use prusti_contracts::*; + +#[requires(dividend != 0)] +pub fn divide_by(divisor: usize, dividend: usize) -> usize { + divisor / dividend +} + +pub fn generate_error() { + assert!(false) +} diff --git a/src/test/scenarios/shared/crates/workspace/second/Cargo.toml b/src/test/scenarios/shared/crates/workspace/second/Cargo.toml new file mode 100644 index 00000000..32b4295e --- /dev/null +++ b/src/test/scenarios/shared/crates/workspace/second/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "second" +version = "0.1.0" +edition = "2021" + +[dependencies] +prusti-contracts = "*" +first = { path = "../first" } diff --git a/src/test/scenarios/shared/crates/workspace/second/src/main.rs b/src/test/scenarios/shared/crates/workspace/second/src/main.rs new file mode 100644 index 00000000..d078152a --- /dev/null +++ b/src/test/scenarios/shared/crates/workspace/second/src/main.rs @@ -0,0 +1,3 @@ +fn main() { + let _ = first::divide_by(10, 2); +} diff --git a/src/test/scenarios/shared/crates/workspace/second/src/main.rs.json b/src/test/scenarios/shared/crates/workspace/second/src/main.rs.json new file mode 100644 index 00000000..d6061516 --- /dev/null +++ b/src/test/scenarios/shared/crates/workspace/second/src/main.rs.json @@ -0,0 +1,18 @@ +[ + { + "message": "[Prusti: verification error] the asserted expression might not hold", + "range": { + "end": { + "character": 18, + "line": 8 + }, + "start": { + "character": 4, + "line": 8 + } + }, + "relatedInformation": [], + "severity": 0, + "uri": "crates/workspace/first/src/lib.rs" + } +] diff --git a/src/test/scenarios/shared/programs/assert_false.rs.json b/src/test/scenarios/shared/programs/assert_false.rs.json index c5afdc9d..66253495 100644 --- a/src/test/scenarios/shared/programs/assert_false.rs.json +++ b/src/test/scenarios/shared/programs/assert_false.rs.json @@ -12,6 +12,7 @@ } }, "relatedInformation": [], - "severity": 0 + "severity": 0, + "uri": "programs/assert_false.rs" } ] diff --git a/src/test/scenarios/shared/programs/failing_post.rs.json b/src/test/scenarios/shared/programs/failing_post.rs.json index 2db143b9..5dec31da 100644 --- a/src/test/scenarios/shared/programs/failing_post.rs.json +++ b/src/test/scenarios/shared/programs/failing_post.rs.json @@ -35,7 +35,8 @@ "message": "the error originates here" } ], - "severity": 0 + "severity": 0, + "uri": "programs/failing_post.rs" } ] }, @@ -71,7 +72,8 @@ "message": "the error originates here" } ], - "severity": 0 + "severity": 0, + "uri": "programs/failing_post.rs" } ] } diff --git a/src/test/scenarios/shared/programs/notes.rs.json b/src/test/scenarios/shared/programs/notes.rs.json index 08244b77..63808884 100644 --- a/src/test/scenarios/shared/programs/notes.rs.json +++ b/src/test/scenarios/shared/programs/notes.rs.json @@ -45,6 +45,7 @@ "message": "if this is intentional, prefix it with an underscore" } ], - "severity": 1 + "severity": 1, + "uri": "programs/notes.rs" } ] diff --git a/src/test/scenarios/taggedVersion/crates/contracts_0.1/src/main.rs.json b/src/test/scenarios/taggedVersion/crates/contracts_0.1/src/main.rs.json index a74cf769..8e87c1d2 100644 --- a/src/test/scenarios/taggedVersion/crates/contracts_0.1/src/main.rs.json +++ b/src/test/scenarios/taggedVersion/crates/contracts_0.1/src/main.rs.json @@ -45,7 +45,8 @@ "message": "if this is intentional, prefix it with an underscore" } ], - "severity": 1 + "severity": 1, + "uri": "crates/contracts_0.1/src/main.rs" }, { "message": "[Prusti: verification error] precondition might not hold.", @@ -77,6 +78,7 @@ "message": "the failing assertion is here" } ], - "severity": 0 + "severity": 0, + "uri": "crates/contracts_0.1/src/main.rs" } ]