Add persistent caching

package.json

@@ -2,7 +2,7 @@
     "name": "prusti-assistant",
     "displayName": "Prusti Assistant",
     "description": "Verify Rust programs with the Prusti verifier.",
-    "version": "0.10.2",
+    "version": "0.10.3",
     "publisher": "viper-admin",
     "repository": {
         "type": "git",
@@ -57,6 +57,11 @@
                 "command": "prusti-assistant.restart-server",
                 "title": "restart Prusti server",
                 "category": "Prusti"
+            },
+            {
+                "command": "prusti-assistant.clear-cache",
+                "title": "clear verification cache",
+                "category": "Prusti"
             }
         ],
         "configuration": {

src/config.ts

@@ -1,5 +1,6 @@
 import * as vscode from "vscode";
 import { Location } from "vs-verification-toolbox";
+import * as path from "path";
 import * as util from "./util";
 import { findJavaHome, JavaHome } from "./javaHome";
 
@@ -85,6 +86,10 @@ export function serverAddress(): string {
     return config().get(serverAddressKey, "");
 }
 
+export function cachePath(context: vscode.ExtensionContext): string {
+    return path.join(context.globalStoragePath, `cache-${buildChannel()}.bin`)
+}
+
 export function extraPrustiEnv(): Record<string, string> {
     return config().get("extraPrustiEnv", {});
 }

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 * as fs from 'fs';
 
 // ========================================================
 // JSON Schemas
@@ -585,6 +586,11 @@ export class DiagnosticsManager {
         this.procDestructors.forEach((kill) => kill());
     }
 
+    public async clearCache(context: vscode.ExtensionContext): Promise<void> {
+        const cacheFile = config.cachePath(context);
+        await fs.promises.unlink(cacheFile).catch(err => util.log(`Failed to clear cache at "${cacheFile}". ${err}`))
+    }
+
     public async verify(prusti: dependencies.PrustiLocation, serverAddress: string, targetPath: string, target: VerificationTarget): Promise<void> {
         // Prepare verification
         this.runCount += 1;

src/extension.ts

@@ -13,6 +13,7 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
     const verifyProgramCommand = "prusti-assistant.verify";
     const killAllCommand = "prusti-assistant.killAll";
     const updateCommand = "prusti-assistant.update";
+    const clearCacheCommand = "prusti-assistant.clear-cache";
 
     // Verification status
     const verificationStatus = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 10);
@@ -86,6 +87,14 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
         })
     );
 
+    // Verify on click
+    const clearCacheButton = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 13);
+    clearCacheButton.command = clearCacheCommand;
+    clearCacheButton.text = "$(trash)";
+    clearCacheButton.tooltip = "Restart Prusti server and clear verification cache.";
+    clearCacheButton.show();
+    context.subscriptions.push(clearCacheButton);
+
     // Verify on click
     const verifyProgramButton = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 12);
     verifyProgramButton.command = verifyProgramCommand;
@@ -150,8 +159,7 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
     // Define verification function
     async function verify(document: vscode.TextDocument) {
         util.log(`Run verification on ${document.uri.fsPath}...`);
-        const projects = await util.findProjects();
-        const cratePath = projects.getParent(document.uri.fsPath);
+        const cratePath = await util.getCratePath(document.uri.fsPath);
 
         if (server.address === undefined) {
             // Just warn, as Prusti can run even without a server.
@@ -184,6 +192,15 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
         }
     }
 
+    // Clear cache file on command
+    context.subscriptions.push(
+        vscode.commands.registerCommand(clearCacheCommand, async () => {
+            await server.stop();
+            await verificationManager.clearCache(context);
+            await server.restart(context, verificationStatus);
+        })
+    );
+
     // Verify on command
     context.subscriptions.push(
         vscode.commands.registerCommand(verifyProgramCommand, async () => {

src/server.ts

@@ -1,4 +1,5 @@
 import * as vscode from "vscode";
+import * as http from "http";
 import * as util from "./util";
 import { prusti } from "./dependencies";
 import * as config from "./config";
@@ -57,8 +58,25 @@ export let address: string | undefined;
  * Stop the server.
  */
 export async function stop(): Promise<void> {
+    if (address !== undefined) {
+        const options = {
+          hostname: address.split(':')[0],
+          port: parseInt(address.split(':')[1], 10),
+          path: '/save',
+          method: 'POST',
+        }
+        const req = http.request(options, res => {
+          res.on('data', () => {
+            server.initiateStop();
+          })
+        })
+        req.on('error', () => {
+            server.initiateStop();
+        })
+        req.end()
+    }
+
     address = undefined;
-    server.initiateStop();
     await server.waitForStopped();
 }
 
@@ -121,6 +139,7 @@ export async function restart(context: vscode.ExtensionContext, verificationStat
         ...{
             JAVA_HOME: (await config.javaHome())!.path,
         },
+        DEFAULT_PRUSTI_CACHE_PATH: config.cachePath(context),
         ...config.extraPrustiEnv(),
     };
 

src/toolbox/serverManager.ts

@@ -171,7 +171,7 @@ export class ServerManager {
             this.log(`Kill server process ${this.proc?.pid}.`);
             const proc = this.proc as childProcess.ChildProcessWithoutNullStreams;
             proc.removeListener("exit", this.procExitCallback);
-            treeKill(proc.pid, "SIGKILL", (err) => {
+            treeKill(proc.pid, "SIGTERM", (err) => {
                 if (err) {
                     this.log(`Failed to kill process tree of ${proc.pid}: ${err}`);
                     const succeeded = proc.kill("SIGKILL");

src/util.ts

@@ -117,8 +117,7 @@ export function spawn(
     function killProc() {
         if (!status.killed) {
             status.killed = true;
-            // TODO: Try with SIGTERM before.
-            treeKill(proc.pid, "SIGKILL", (err) => {
+            treeKill(proc.pid, "SIGTERM", (err) => {
                 if (err) {
                     log(`Failed to kill process tree of ${proc.pid}: ${err}`);
                     const succeeded = proc.kill("SIGKILL");
@@ -238,3 +237,13 @@ export async function findProjects(): Promise<ProjectList> {
     });
     return new ProjectList(projects);
 }
+
+/**
+ * Given a file in a crate, get the crate reference
+ *
+ * @returns The Project crate or undefined.
+ */
+ export async function getCratePath(file: string): Promise<Project | undefined> {
+    const projects = await findProjects();
+    return projects.getParent(file);
+}