Merge pull request #251 from zgrannan/zgrannan/more-permissive-tool-s…

…earch

Look in more places for rust-toolchain and viper_tools

src/checks.ts

@@ -78,7 +78,7 @@ export async function isOutdated(prusti: PrustiLocation, numDays = 30): Promise<
     }
 
     // TODO: Lookup on GitHub if there actually is a more recent version to download.
-    const prustiDownloadDate = (await fs.stat(prusti.rustToolchainFile().path())).ctime.getTime();
+    const prustiDownloadDate = (await fs.stat(prusti.rustToolchainFile.path())).ctime.getTime();
     const pastNumDays = new Date(new Date().setDate(new Date().getDate() - numDays)).getTime();
     const olderThanNumDays = prustiDownloadDate < pastNumDays;
     const extensionDownloadDate = (await fs.stat(__filename)).ctime.getTime();

src/dependencies/PrustiLocation.ts

@@ -3,7 +3,9 @@ import * as fs from "fs-extra";
 
 export class PrustiLocation {
     constructor(
-        private readonly location: Location
+        private readonly prustiLocation: Location,
+        private readonly viperToolsLocation: Location,
+        public readonly rustToolchainFile: Location
     ) {
         // Set execution flags (ignored on Windows)
         fs.chmodSync(this.prustiDriver, 0o775);
@@ -15,37 +17,33 @@ export class PrustiLocation {
         fs.chmodSync(this.prustiServer, 0o775);
     }
 
-    public rustToolchainFile(): Location {
-        return this.location.child("rust-toolchain");
-    }
-
     public get prustiDriver(): string {
-        return this.location.executable("prusti-driver");
+        return this.prustiLocation.executable("prusti-driver");
     }
 
     public get prustiRustc(): string {
-        return this.location.executable("prusti-rustc");
+        return this.prustiLocation.executable("prusti-rustc");
     }
 
     public get cargoPrusti(): string {
-        return this.location.executable("cargo-prusti");
+        return this.prustiLocation.executable("cargo-prusti");
     }
 
     public get prustiServerDriver(): string {
-        return this.location.executable("prusti-server-driver");
+        return this.prustiLocation.executable("prusti-server-driver");
     }
 
     public get prustiServer(): string {
-        return this.location.executable("prusti-server");
+        return this.prustiLocation.executable("prusti-server");
     }
 
     public get z3(): string {
-        return this.location.child("viper_tools").child("z3").child("bin")
+        return this.viperToolsLocation.child("z3").child("bin")
             .executable("z3");
     }
 
     public get boogie(): string {
-        return this.location.child("viper_tools").child("boogie")
+        return this.viperToolsLocation.child("boogie")
             .child("Binaries").executable("Boogie");
     }
 }

src/dependencies/index.ts

@@ -7,6 +7,7 @@ import * as server from "../server";
 import * as rustup from "./rustup";
 import { PrustiLocation } from "./PrustiLocation";
 import { prustiTools } from "./prustiTools";
+import { Location } from "vs-verification-toolbox";
 
 export let prusti: PrustiLocation | undefined;
 export async function installDependencies(context: vscode.ExtensionContext, shouldUpdate: boolean, verificationStatus: vscode.StatusBarItem): Promise<void> {
@@ -32,8 +33,10 @@ export async function installDependencies(context: vscode.ExtensionContext, shou
             return;
         }
         const location = result.value as tools.Location;
+        const viperToolsDirectory = await getViperToolsDirectory(location);
+        const rustToolchainLocation = await getRustToolchainLocation(location);
         util.log(`Using Prusti at ${location}`)
-        prusti = new PrustiLocation(location);
+        prusti = new PrustiLocation(location, viperToolsDirectory, rustToolchainLocation);
 
         // only notify user about success if we reported anything in between;
         // otherwise there was nothing to be done.
@@ -46,7 +49,7 @@ export async function installDependencies(context: vscode.ExtensionContext, shou
         // Install Rust toolchain
         await rustup.ensureRustToolchainInstalled(
             context,
-            prusti.rustToolchainFile(),
+            rustToolchainLocation
         );
     } catch (err) {
         util.userError(
@@ -72,3 +75,57 @@ export async function prustiVersion(): Promise<string> {
     }
     return version;
 }
+
+/**
+ * Returns the location of the `viper_tools` directory. This function starts the
+ * search by looking in the Prusti location for a child folder `viper_tools`; if
+ * not found, it looks upwards until a `viper_tools` directory can be found.
+ *
+ * In general, the `viper_tools` directory will be a child of the Prusti
+ * location; however, when using a development version of Prusti (e.g. where
+ * Prusti's location would be set as prusti-dev/target/debug), `viper_tools`
+ * would be in the `prusti-dev` directory.
+ */
+async function getViperToolsDirectory(prustiLocation: Location): Promise<Location> {
+    const location = await searchForChildInEnclosingFolders(prustiLocation, "viper_tools");
+    if(location) {
+        return location;
+    } else {
+        throw new Error(`Could not find viper_tools directory from ${prustiLocation}.`);
+    }
+}
+
+/**
+ * Returns the location of the `rust-toolchain` file. This function starts the
+ * search by looking in the Prusti location for a child file `rust-toolchain`;
+ * if not found, it looks upwards until a `rust-toolchain` file can be found.
+ *
+ * In general, the `rust-toolchain` file will be a child of the Prusti location;
+ * however, when using a development version of Prusti (e.g. where Prusti's
+ * location would be set as prusti-dev/target/debug), `rust-toolchain` would be
+ * in the `prusti-dev` directory.
+ */
+async function getRustToolchainLocation(prustiLocation: Location): Promise<Location> {
+    const location = await searchForChildInEnclosingFolders(prustiLocation, "rust-toolchain");
+    if(location) {
+        return location;
+    } else {
+        throw new Error(`Could not find rust-toolchain file from ${prustiLocation}.`);
+    }
+}
+
+async function searchForChildInEnclosingFolders(initialLocation: Location, childName: string): Promise<Location | undefined> {
+    let location = initialLocation;
+    // eslint-disable-next-line no-constant-condition
+    while (true) {
+        const childLocation = location.child(childName);
+        if(await childLocation.exists()) {
+            return childLocation;
+        }
+        if(location.path() === location.enclosingFolder.path()) {
+            // We've reached the root folder
+            return;
+        }
+        location = location.enclosingFolder;
+    }
+}