diff --git a/.eslintrc b/.eslintrc index 17704154..fac17325 100644 --- 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 index 9d7f0341..c9a42e6f 100644 --- 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 index c5e5eb53..4089aa5b 100644 --- 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 { + 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 index 3de7e2c9..f5995cec 100644 --- 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): 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): 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 index 262df0bf..0adec2b2 100644 --- 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 index f73a7a3c..2a9a9107 100644 --- 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 index a2216c14..985683f0 100644 --- 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); }