Merge pull request #139 from viperproject/extra-env-and-args

Configure Prusti arguments and environment variables
viperproject · Feb 2, 2022 · 15e4353 · 15e4353
2 parents 8c12156 + 9862bc5
commit 15e4353
Show file tree

Hide file tree

Showing 7 changed files with 113 additions and 38 deletions.
diff --git a/.eslintrc b/.eslintrc
@@ -25,5 +25,6 @@
         "import/no-cycle": "error",
         "@typescript-eslint/restrict-template-expressions": "off",
         "@typescript-eslint/explicit-module-boundary-types": "error",
+        "@typescript-eslint/no-non-null-assertion": "off"
     }
 }
diff --git a/package.json b/package.json
@@ -55,7 +55,6 @@
             }
         ],
         "configuration": {
-            "type": "object",
             "title": "Prusti Assistant",
             "properties": {
                 "prusti-assistant.buildChannel": {
@@ -107,6 +106,42 @@
                     "type": "string",
                     "default": "",
                     "description": "Specifies the address of a Prusti server to use for verification. If not set, the extension will start up and manage its own server."
+                },
+                "prusti-assistant.extraPrustiEnv": {
+                    "type": "object",
+                    "properties": {
+                        "RUST_BACKTRACE": "true",
+                        "PRUSTI_LOG": "info"
+                    },
+                    "additionalProperties": { "type": "string" },
+                    "default": {},
+                    "description": "Specifies additional environment variables to be passed to all Prusti runs. Remember to restart the Prusti Server after modifying this setting."
+                },
+                "prusti-assistant.extraPrustiRustcArgs": {
+                    "type": "array",
+                    "items": {
+                        "type": "string"
+                    },
+                    "default": [
+                        "--edition=2018"
+                    ],
+                    "description": "Specifies additional arguments to be passed to Prusti-Rustc. Used when verifying a Rust file that is not part of a crate."
+                },
+                "prusti-assistant.extraCargoPrustiArgs": {
+                    "type": "array",
+                    "items": {
+                        "type": "string"
+                    },
+                    "default": [],
+                    "description": "Specifies additional arguments to be passed to Cargo-Prusti. Used when verifying a crate."
+                },
+                "prusti-assistant.extraPrustiServerArgs": {
+                    "type": "array",
+                    "items": {
+                        "type": "string"
+                    },
+                    "default": [],
+                    "description": "Specifies additional arguments to be passed to the Prusti Server. Remember to restart the Prusti Server after modifying this setting."
                 }
             }
         }

diff --git a/src/config.ts b/src/config.ts
@@ -84,3 +84,19 @@ export const serverAddressPath = `${namespace}.${serverAddressKey}`;
 export function serverAddress(): string {
     return config().get(serverAddressKey, "");
 }
+
+export function extraPrustiEnv(): Record<string, string> {
+    return config().get("extraPrustiEnv", {});
+}
+
+export function extraPrustiRustcArgs(): string[] {
+    return config().get("extraPrustiRustcArgs", []);
+}
+
+export function extraCargoPrustiArgs(): string[] {
+    return config().get("extraCargoPrustiArgs", []);
+}
+
+export function extraPrustiServerArgs(): string[] {
+    return config().get("extraPrustiServerArgs", []);
+}
diff --git a/src/diagnostics.ts b/src/diagnostics.ts
@@ -359,20 +359,25 @@ enum VerificationStatus {
 async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, rootPath: string, serverAddress: string, destructors: Set<util.KillFunction>): Promise<[Diagnostic[], VerificationStatus, util.Duration]> {
     // FIXME: Workaround for warning generation for libs.
     await removeDiagnosticMetadata(rootPath);
+    const cargoPrustiArgs = ["--message-format=json"].concat(
+        config.extraCargoPrustiArgs()
+    );
+    const cargoPrustiEnv = {
+        ...process.env,  // Needed to run Rustup
+        ...{
+            PRUSTI_SERVER_ADDRESS: serverAddress,
+            PRUSTI_QUIET: "true",
+            JAVA_HOME: (await config.javaHome())!.path,
+        },
+        ...config.extraPrustiEnv(),
+    };
     const output = await util.spawn(
         prusti.cargoPrusti,
-        ["--message-format=json"],
+        cargoPrustiArgs,
         {
             options: {
                 cwd: rootPath,
-                env: {
-                    ...process.env,  // Needed e.g. to run Rustup
-                    PRUSTI_SERVER_ADDRESS: serverAddress,
-                    RUST_BACKTRACE: "1",
-                    PRUSTI_LOG: "info",
-                    PRUSTI_QUIET: "true",
-                    JAVA_HOME: (await config.javaHome())!.path,
-                }
+                env: cargoPrustiEnv,
             }
         },
         destructors,
@@ -409,26 +414,29 @@ async function queryCrateDiagnostics(prusti: dependencies.PrustiLocation, rootPa
  * @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]> {
-    // For backward compatibility
+    const prustiRustcArgs = [
+        "--crate-type=lib",
+        "--error-format=json",
+        programPath
+    ].concat(
+        config.extraPrustiRustcArgs()
+    );
+    const prustiRustcEnv = {
+        ...process.env,  // Needed to run Rustup
+        ...{
+            PRUSTI_SERVER_ADDRESS: serverAddress,
+            PRUSTI_QUIET: "true",
+            JAVA_HOME: (await config.javaHome())!.path,
+        },
+        ...config.extraPrustiEnv(),
+    };
     const output = await util.spawn(
         prusti.prustiRustc,
-        [
-            "--crate-type=lib",
-            "--error-format=json",
-            "--edition=2018",
-            programPath
-        ],
+        prustiRustcArgs,
         {
             options: {
                 cwd: path.dirname(programPath),
-                env: {
-                    ...process.env,  // Needed e.g. to run Rustup
-                    PRUSTI_SERVER_ADDRESS: serverAddress,
-                    RUST_BACKTRACE: "1",
-                    PRUSTI_LOG: "info",
-                    PRUSTI_QUIET: "true",
-                    JAVA_HOME: (await config.javaHome())!.path,
-                }
+                env: prustiRustcEnv,
             }
         },
         destructors

diff --git a/src/server.ts b/src/server.ts
@@ -105,20 +105,32 @@ export async function restart(context: vscode.ExtensionContext, verificationStat
         return;
     }
 
+    let prustiServerCwd: string | undefined;
+    if (vscode.workspace.workspaceFolders !== undefined) {
+        prustiServerCwd = vscode.workspace.workspaceFolders[0].uri.fsPath;
+        util.log(`Prusti server will be executed in '${prustiServerCwd}'`);
+    }
+
+    const prustiServerArgs = ["--port=0"].concat(
+        config.extraPrustiServerArgs()
+    );
+    const prustiServerEnv = {
+        ...process.env,  // Needed to run Rustup
+        ...{
+            JAVA_HOME: (await config.javaHome())!.path,
+        },
+        ...config.extraPrustiEnv(),
+    };
+
     server.initiateStart(
         prusti!.prustiServer,
-        ["--port", "0"],
+        prustiServerArgs,
         {
-            env: {
-                ...process.env,  // Needed e.g. to run Rustup
-                // Might not exist yet, but that's handled on the rust side
-                PRUSTI_LOG_DIR: context.logPath,
-                RUST_BACKTRACE: "1",
-                RUST_LOG: "info",
-                JAVA_HOME: (await config.javaHome())!.path,
-            },
+            cwd: prustiServerCwd,
+            env: prustiServerEnv,
             onStdout: data => {
                 serverChannel.append(`[stdout] ${data}`);
+                console.log(`[Prusti Server][stdout] ${data}`);
                 // Extract the server port from the output
                 if (address === undefined) {
                     const port = parseInt(data.toString().split("port: ")[1], 10);
@@ -130,6 +142,7 @@ export async function restart(context: vscode.ExtensionContext, verificationStat
             },
             onStderr: data => {
                 serverChannel.append(`[stderr] ${data}`);
+                console.log(`[Prusti Server][stderr] ${data}`);
             }
         }
     );

diff --git a/src/test/runTest.ts b/src/test/runTest.ts
@@ -33,7 +33,7 @@ async function main() {
             // closing an old one.
             await new Promise(resolve => setTimeout(resolve, 5000));
         }
-        console.info(`Testing with settings '${settingsFile}'...`);
+        console.info(`Begin testing with settings '${settingsFile}'...`);
         const tmpWorkspace = tmp.dirSync({ unsafeCleanup: true });
         try {
             // Prepare the workspace with the settings
@@ -54,14 +54,15 @@ async function main() {
                 launchArgs: ["--disable-extensions", tmpWorkspace.name],
             });
         } finally {
+            // Delete folder even in case of errors
             tmpWorkspace.removeCallback();
         }
+        console.info(`End of testing with settings '${settingsFile}'.`);
         firstIteration = false;
     }
 }
 
 main().catch(err => {
-    console.error(err);
-    console.error("Failed to run tests");
+    console.error(`Failed to run tests. Error: ${err}`);
     process.exit(1);
 });
diff --git a/src/util.ts b/src/util.ts
@@ -79,11 +79,12 @@ const logChannel = vscode.window.createOutputChannel("Prusti Assistant");
 export function log(message: string): void {
     console.log(message);
     logChannel.appendLine(message);
-    trace(message);
+    traceChannel.appendLine(message);
 }
 
 const traceChannel = vscode.window.createOutputChannel("Prusti Assistant Trace");
 export function trace(message: string): void {
+    console.log(message);
     traceChannel.appendLine(message);
 }