diff --git a/src/checks.ts b/src/checks.ts index b4c02346..c089176a 100644 --- a/src/checks.ts +++ b/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(); diff --git a/src/dependencies/PrustiLocation.ts b/src/dependencies/PrustiLocation.ts index 3664f869..7c37d6a5 100644 --- a/src/dependencies/PrustiLocation.ts +++ b/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"); } } diff --git a/src/dependencies/index.ts b/src/dependencies/index.ts index 5e0b292d..4397a7ca 100644 --- a/src/dependencies/index.ts +++ b/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 { @@ -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 { } 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 { + 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 { + 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 { + 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; + } +}