Fix error reporting in workspaces

src/crateMetadata.ts

@@ -0,0 +1,74 @@
+import * as util from "./util";
+import * as config from "./config";
+import * as dependencies from "./dependencies";
+
+interface CargoMetadata {
+    target_directory: string;
+    workspace_root?: string;
+}
+
+/**
+ * Parses the output of `cargo metadata` into a `CargoMetadata` object.
+ *
+ * @param output The output to parse.
+ */
+function parseCargoMetadata(output: string): CargoMetadata {
+    return JSON.parse(output) as CargoMetadata;
+}
+
+export enum MetadataStatus {
+    Crash,
+    Errors,
+    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<util.KillFunction>): Promise<[CargoMetadata, MetadataStatus, 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 = MetadataStatus.Crash;
+    if (output.code === 0) {
+        status = MetadataStatus.Ok;
+    }
+    if (output.code === 1) {
+        status = MetadataStatus.Errors;
+    }
+    if (output.code === 101) {
+        status = MetadataStatus.Errors;
+    }
+    if (/error: internal compiler error/.exec(output.stderr) !== null) {
+        status = MetadataStatus.Crash;
+    }
+    if (/^thread '.*' panicked at/.exec(output.stderr) !== null) {
+        status = MetadataStatus.Crash;
+    }
+    const metadata: CargoMetadata = parseCargoMetadata(output.stdout);
+    return [metadata, status, output.duration];
+}

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, MetadataStatus } 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);
 
@@ -176,7 +178,7 @@ function parseCargoMessage(msgDiag: CargoMessage, rootPath: string, defaultRange
         primaryRange = parseMultiSpanRange(primaryCallSiteSpans);
         primaryFilePath = primaryCallSiteSpans[0].file_name;
         if (!path.isAbsolute(primaryFilePath)) {
-            primaryFilePath = path.join(rootPath, primaryFilePath);
+            primaryFilePath = path.join(basePath, primaryFilePath);
         }
     }
     const diagnostic = new vscode.Diagnostic(
@@ -195,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(
@@ -214,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(
@@ -238,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
@@ -265,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);
@@ -300,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(
@@ -323,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()
@@ -344,14 +345,22 @@ 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 metadata, the exist status, and the duration of the query.
  */
-async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, rootPath: string, serverAddress: string, destructors: Set<util.KillFunction>): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
+async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, cratePath: string, serverAddress: string, destructors: Set<util.KillFunction>): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
+    let [metadata, metadataStatus, metadataDuration] = await queryCrateMetadata(prusti, cratePath, destructors);
+    if (metadataStatus !== MetadataStatus.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()
     );
@@ -369,7 +378,7 @@ async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, rootPa
         cargoPrustiArgs,
         {
             options: {
-                cwd: rootPath,
+                cwd: cratePath,
                 env: cargoPrustiEnv,
             }
         },
@@ -391,26 +400,27 @@ 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.
+ *
+ * @param filePath The path of the file on which to run prusti-rustc.
  * @returns An array of diagnostics for the given rust project.
  */
-async function queryProgramDiagnostics(prusti: dependencies.PrustiLocation, programPath: string, serverAddress: string, destructors: Set<util.KillFunction>): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
+async function queryProgramDiagnostics(prusti: dependencies.PrustiLocation, filePath: string, serverAddress: string, destructors: Set<util.KillFunction>): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
     const prustiRustcArgs = [
         "--crate-type=lib",
         "--error-format=json",
-        programPath
+        filePath
     ].concat(
         config.extraPrustiRustcArgs()
     );
@@ -428,7 +438,7 @@ async function queryProgramDiagnostics(prusti: dependencies.PrustiLocation, prog
         prustiRustcArgs,
         {
             options: {
-                cwd: path.dirname(programPath),
+                cwd: path.dirname(filePath),
                 env: prustiRustcEnv,
             }
         },
@@ -453,7 +463,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];

src/test/extension.test.ts

@@ -56,7 +56,7 @@ 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 represent diagnostics
 type Position = {
     line: number,
     character: number
@@ -73,6 +73,8 @@ type RelatedInformation = {
     message: string
 }
 type Diagnostic = {
+    // This path is relative to VSCode's workspace
+    uri: string,
     range: Range,
     severity: number,
     message: string,
@@ -91,8 +93,9 @@ function rangeToPlainObject(range: vscode.Range): Range {
         }
     };
 }
-function diagnosticToPlainObject(diagnostic: vscode.Diagnostic): Diagnostic {
+function diagnosticToPlainObject(uri: vscode.Uri, diagnostic: vscode.Diagnostic): Diagnostic {
     const plainDiagnostic: Diagnostic = {
+        uri: vscode.workspace.asRelativePath(uri),
         range: rangeToPlainObject(diagnostic.range),
         severity: diagnostic.severity,
         message: diagnostic.message,
@@ -170,8 +173,10 @@ describe("Extension", () => {
             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);
+            let plainDiagnostics: Diagnostic[] = vscode.languages.getDiagnostics().flatMap(pair => {
+                const [uri, diagnostics] = pair;
+                return diagnostics.map(diagnostic => diagnosticToPlainObject(uri, diagnostic));
+            });
             const expectedData = await fs.readFile(programPath + ".json", "utf-8");
             type MultiDiagnostics = [
                 { filter?: [string: string], diagnostics: Diagnostic[] }

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"
     }
 ]

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"
     }
 ]

src/test/scenarios/shared/crates/workspace/Cargo.toml

@@ -0,0 +1,5 @@
+[workspace]
+members = [
+    "first",
+    "second",
+]

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 = "*"

src/test/scenarios/shared/crates/workspace/first/src/lib.rs

@@ -0,0 +1,11 @@
+use prusti_contracts::*;
+
+#[requires(dividend != 0)]
+#[ensures(divisor == result * dividend + (divisor % dividend))]
+pub fn divide_by(divisor: usize, dividend: usize) -> usize {
+    divisor / dividend
+}
+
+pub fn generate_error() {
+    assert!(false)
+}

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

src/test/scenarios/shared/crates/workspace/second/src/main.rs

@@ -0,0 +1,4 @@
+fn main() {
+    let result = first::divide_by(10, 2);
+    assert!(result == 5);
+}