Lift requirement of having the prusti feature enabled (#1146)

* Lift requirement to enable `prusti` feature

* Do `prusti-contracts` dependency check prior to `cargo verify`

* Minimise changes

* Reorganise crates

* Revert `22d8c005624510779f3b6566246e0c1566bd672a`

* fmt fix

* Implement discussed changes

* Update expected stderr

* Don't run polonius on impure no_verify fns

* Merge

* Remove test-crates invalid dependency (cannot dep on bin crate)

* Correct doc

* Re-add dependencies to test-crates

* Clarify how providing flags in multi-crate projects works

* Update "Quantifier_Instantiations" -> "QI"

* Change how bodies (with facts) are loaded

* Add requirement that `prusti-contracts` isn't a subdir

* Enable Polonius again for `verify` crates

* Review changes

* Add note on re-verification

.cargo/config

@@ -0,0 +1,2 @@
+[unstable]
+bindeps = true

.gitignore

@@ -11,6 +11,9 @@ core
 report.csv
 *.profraw
 
+*.lock
+!/Cargo.lock
+
 .workspaces/
 viper_tools/
 prusti_tools/

Cargo.toml

@@ -5,6 +5,7 @@ members = [
     "prusti-contracts-build",
     "prusti-tests",
     "prusti-common",
+    "prusti-utils",
     "prusti-interface",
     "prusti-viper",
     "prusti-server",

docs/dev-guide/src/config/providing.md

@@ -3,10 +3,39 @@
 Flags can be set in one of four ways, in increasing order of priority:
 
 1. Provided individually as environment variables with the prefix `DEFAULT_PRUSTI_` (for example, `DEFAULT_PRUSTI_CACHE_PATH` for the [`CACHE_PATH`](flags.md#cache_path) flag).
-> NOTE: One should only use this to change the default value of flags, such that this can be overridden by a config file
+> **Note:** One should only use this to change the default value of flags, such that this can be overridden by a config file
 
-2. Provided lowercase in a file ([allowed formats](https://docs.rs/config/latest/config/enum.FileFormat.html)) with the path in the environment variable `PRUSTI_CONFIG` (for example, `check_overflows` for the [`CHECK_OVERFLOWS`](flags.md#check_overflows) flag). This path defaults to `./Prusti.toml` if the environment variable is not set.<a name="flags-2"></a>
+2. Provided lowercase in a `Prusti.toml` file ([allowed formats](https://docs.rs/config/latest/config/enum.FileFormat.html), e.g. `check_overflows = true` for the [`CHECK_OVERFLOWS`](flags.md#check_overflows) flag). Prusti searches for a `Prusti.toml` depending on how it is run:<a name="flags-2"></a>
+
+    - As `cargo prusti` (on an entire crate): in the [`CARGO_MANIFEST_DIR`](https://doc.rust-lang.org/cargo/reference/environment-variables.html#environment-variables-cargo-sets-for-crates), i.e. next to the crate's `Cargo.toml`
+    - As `prusti-rustc` (on a single Rust file): in the current working directory
 
 3. Provided individually as environment variables with the prefix `PRUSTI_` (for example, `PRUSTI_ASSERT_TIMEOUT` for the [`ASSERT_TIMEOUT`](flags.md#assert_timeout) flag).
 
 4. Provided individually as command-line arguments to Prusti with the prefix `-P` (for example, `-Pprint_desugared_specs` for the [`PRINT_DESUGARED_SPECS`](flags.md#print_desugared_specs) flag).
+
+## Multi-crate Cargo Prusti Projects
+
+Setting flags becomes slightly more complicated when Prusti is run on multiple crates as `cargo prusti`; e.g. which `Prusti.toml` file will be used. Though overriding priority as above remains the same, the three possible approaches to providing flags all behave differently, in particular depending on flag [Category](flags.md#list-of-configuration-flags).
+
+### Environment Variables
+
+The environment persists throughout compilation, therefore all flags set through the `DEFAULT_PRUSTI_` or `PRUSTI_` will apply to all crates, and flags of both Category A and B. For example setting `PRUSTI_CHECK_OVERFLOWS=false` will disable overflow checks in all dependencies, even if they try to override this with a `Prusti.toml` file.
+
+### Prusti Config File
+
+A `Prusti.toml` is optionally loaded from the current working directory prior to compilation. This file is used to configure flags in Category B _only_ and these flags apply to the entire compilation.
+
+Then, as each individual crate is checked (from the roots of the dependency tree) a `Prusti.toml` is optionally loaded from the directory where the crate's corresponding `Cargo.toml` is located. This file is used to configure flags in Category A _only_ — it would not make sense to set e.g. [`NO_VERIFY_DEPS`](flags.md#no_verify_deps) in a dependency since all of its dependencies have already been verified.
+
+Therefore, when publishing a `lib` crate to git/crates.io one can configure Category A flags by including a `Prusti.toml` file next to their `Cargo.toml`.
+
+> **Note:** Currently cargo does not track `Prusti.toml` files as a [dependency](https://doc.rust-lang.org/cargo/guide/build-cache.html#dep-info-files), therefore if it's the only file that changed in a crate you may need to run `cargo clean -p <crate>` to force reverification
+
+The `Prusti.toml` used to load Category B flags at the start and the one used to load Category A flags at the end for the root crate will often be one and the same because `cargo prusti` is typically run from the root crate's directory. This can be changed by providing the [`--manifest-path` flag](https://doc.rust-lang.org/cargo/commands/cargo-check.html#manifest-options).
+
+### Commandline Arguments
+
+Prusti `-P` flags can be provided after a `--` (e.g. `cargo prusti -- -Pcargo_command=build`). Currently flags from Category B _only_ are supported; providing a flag in Category A this way will be ignored.
+
+Flags to cargo are provided in the [regular way](https://doc.rust-lang.org/cargo/commands/cargo-check.html#options) (e.g. `cargo prusti --features foo`).

prusti-common/Cargo.toml

@@ -8,14 +8,13 @@ edition = "2021"
 doctest = false # we have no doc tests
 
 [dependencies]
-log = { version = "0.4", features = ["release_max_level_info"] }
+prusti-utils = { path = "../prusti-utils" }
 viper = { path = "../viper" }
 vir = { path = "../vir" }
-prusti-launch = { path = "../prusti-launch" }
+log = { version = "0.4", features = ["release_max_level_info"] }
 config = "0.13"
 itertools = "0.10.3"
 serde = { version = "1.0", features = ["derive"] }
 lazy_static = "1.4.0"
 uuid = { version = "1.0", features = ["v4"] }
-regex = "1.5"
 fxhash = "0.2.1"

prusti-common/src/lib.rs

@@ -9,10 +9,5 @@
 
 #![deny(unused_must_use)]
 
-pub mod config;
-pub mod report;
-mod stopwatch;
-pub mod utils;
 pub mod vir;
-
-pub use stopwatch::Stopwatch;
+pub use prusti_utils::*;

prusti-contracts-build/Cargo.toml

@@ -5,7 +5,6 @@ authors = ["Vytautas Astrauskas <[email protected]>"]
 edition = "2021"
 
 [build-dependencies]
-prusti-launch = { path = "../prusti-launch" }
-
-[features]
-prusti-contracts-dep = []
+prusti-utils = { path = "../prusti-utils" }
+prusti = { path = "../prusti", artifact = "bin" }
+prusti-launch = { path = "../prusti-launch", artifact = "bin" }

prusti-contracts-build/build.rs

@@ -1,14 +1,12 @@
 use std::{path::PathBuf, process::Command};
 
 fn main() {
-    // In theory we should build to here (i.e. set `CARGO_TARGET_DIR` to this),
-    // but this is hard to find for linking. So instead build to the `prusti-contracts` dir.
-    let _out_dir = std::env::var("OUT_DIR").unwrap();
-    // println!("cargo:warning=out_dir: {}", _out_dir);
+    // Rerun if running with e.g. cargo clippy
+    println!("cargo:rerun-if-env-changed=RUSTC_WORKSPACE_WRAPPER");
 
-    // Rebuild if any of the `prusti-contracts` crates change
-    let prusti_contrats = ["..", "prusti-contracts"].iter().collect::<PathBuf>();
-    let files = std::fs::read_dir(&prusti_contrats).unwrap();
+    // Rerun if any of the `prusti-contracts` crates change
+    let prusti_contracts = ["..", "prusti-contracts"].iter().collect::<PathBuf>();
+    let files = std::fs::read_dir(&prusti_contracts).unwrap();
     for file in files {
         let file = file.unwrap();
         let filename = file.file_name();
@@ -18,88 +16,59 @@ fn main() {
         }
     }
 
-    // Build `prusti-contracts`
+    let target = prusti_contracts.join("target").join("verify");
+    force_reexport_specs(target.as_path());
+
+    // Copy just-built binaries to `target/dir` dir
     let dir = if cfg!(debug_assertions) {
         "debug"
     } else {
         "release"
     };
-    // Cargo prusti
-    let exes = ["cargo-prusti", "prusti-rustc", "prusti-driver"].map(|exe| {
-        let exe = format!("{}{}", exe, if cfg!(windows) { ".exe" } else { "" });
-        let exe = ["..", "target", dir, &exe].iter().collect::<PathBuf>();
-        println!("cargo:rerun-if-changed={}", exe.to_string_lossy());
-        exe
-    });
-    // Rerun if running with e.g. cargo clippy
-    println!("cargo:rerun-if-env-changed=RUSTC_WORKSPACE_WRAPPER");
-    // Run only if possible
-    if exes.iter().all(|exe| exe.exists()) {
-        let target = prusti_contrats.join("target").join("verify");
-        let modified = modified_times(&exes);
-        let should_write_build_info =
-            check_exes_modified(target.as_path(), &modified).unwrap_or(true);
-        let args = ["--release", "--features", "prusti"];
-        match Command::new(&exes[0])
-            .current_dir(&prusti_contrats)
-            .args(args)
-            .env("CARGO_PRUSTI_COMMAND", "build")
-            .output()
-        {
-            Ok(output) => {
-                if output.status.success() {
-                    if should_write_build_info {
-                        use std::io::Write;
-                        std::fs::File::create(target.join("build_info.txt"))
-                            .and_then(|mut file| file.write_all(modified.as_bytes()))
-                            .ok();
-                    }
-                } else {
-                    let stdout = String::from_utf8(output.stdout).unwrap();
-                    let stderr = String::from_utf8(output.stderr).unwrap();
-                    println!("cargo:warning=Failed to build `prusti-contracts`!");
-                    let args = args.iter().fold(String::new(), |acc, a| acc + " " + a);
-                    println!(
-                        "cargo:warning=`prusti-contracts-build` ran '{}{}'",
-                        exes[0].to_string_lossy(),
-                        args
-                    );
-                    println!("cargo:warning=-------- stdout: --------");
-                    for line in stdout.lines() {
-                        println!("cargo:warning={}", line);
-                    }
-                    println!("cargo:warning=-------- stderr: --------");
-                    for line in stderr.lines() {
-                        println!("cargo:warning={}", line);
-                    }
-                    // Only panic when running with `x.py` to avoid errors on the first run
-                    if std::env::var("CARGO_FEATURE_PRUSTI_CONTRACTS_DEP").is_ok() {
-                        // Delete files to prevent Catch-22 where these files cannot be rebuilt
-                        for exe in exes {
-                            std::fs::remove_file(exe).ok();
-                        }
-                        panic!("Fix the above Prusti crash and run build again to rebuild Prusti.")
-                    } else {
-                        std::fs::remove_dir_all(target).ok();
-                    }
-                }
-            }
-            Err(e) => {
-                println!("cargo:warning=Failed to build `prusti-contracts`: {}", e);
-            }
-        }
-    } else {
+    for (krate, file) in [
+        ("PRUSTI_LAUNCH", "cargo-prusti"),
+        ("PRUSTI_LAUNCH", "prusti-rustc"),
+        ("PRUSTI", "prusti-driver"),
+    ] {
+        let file_from = std::env::var(format!("CARGO_BIN_FILE_{krate}_{file}")).unwrap();
+        let file_to = format!("{file}{}", if cfg!(windows) { ".exe" } else { "" });
+        let file_to = ["..", "target", dir, &file_to].iter().collect::<PathBuf>();
+        std::fs::copy(file_from, file_to).unwrap();
     }
+
+    // Run `cargo-prusti`
+    let cargo_prusti = format!("cargo-prusti{}", if cfg!(windows) { ".exe" } else { "" });
+    let cargo_prusti = ["..", "target", dir, &cargo_prusti]
+        .iter()
+        .collect::<PathBuf>();
+    let arg = "--release";
+    // Not a warning but no other way to print to console
+    println!(
+        "cargo:warning=Building `prusti-contracts` with '{} {arg}', please wait.",
+        cargo_prusti.to_string_lossy()
+    );
+
+    // In theory we should build to here (i.e. set `CARGO_TARGET_DIR` to this),
+    // but this is hard to find for linking. So instead build to the `prusti-contracts` dir.
+    // let out_dir = std::env::var("OUT_DIR").unwrap();
+    // println!("cargo:warning=out_dir: {}", out_dir);
+
+    let status = Command::new(&cargo_prusti)
+        .current_dir(&prusti_contracts)
+        .arg(arg)
+        .env_remove("CARGO_MANIFEST_DIR")
+        .status()
+        .expect("Failed to run cargo-prusti!");
+    assert!(status.success());
 }
 
-/// Cargo will rebuild prusti-contracts if any of those files changed, however we want to
-/// rebuild them also if any of the `cargo-prusti`/`prusti-{rustc,driver}` changed, and so
-/// we manually force that here if required.
-fn check_exes_modified(target: &std::path::Path, modified: &str) -> std::io::Result<bool> {
-    let contents = std::fs::read_to_string(target.join("build_info.txt"))?;
-    if contents != modified {
-        let files = std::fs::read_dir(target.join("release").join("deps"))?;
-        let libs = prusti_launch::PRUSTI_LIBS.map(|lib| format!("lib{}-", lib.replace('-', "_")));
+/// Cargo will rebuild prusti-contracts if any of those files changed, however we also want to
+/// reexport specs if any of the `cargo-prusti`/`prusti-{rustc,driver}` changed, and so
+/// we manually force that here by deleting the `PRUSTI_LIBS` files.
+fn force_reexport_specs(target: &std::path::Path) {
+    if let Ok(files) = std::fs::read_dir(target.join("release").join("deps")) {
+        let libs =
+            prusti_utils::launch::PRUSTI_LIBS.map(|lib| format!("lib{}-", lib.replace('-', "_")));
         for file in files {
             let file = file.unwrap();
             let filename = file.file_name();
@@ -108,25 +77,5 @@ fn check_exes_modified(target: &std::path::Path, modified: &str) -> std::io::Res
                 std::fs::remove_file(file.path()).ok();
             }
         }
-        Ok(true)
-    } else {
-        Ok(false)
     }
 }
-
-fn modified_times(files: &[PathBuf]) -> String {
-    files
-        .iter()
-        .map(|f| {
-            f.metadata()
-                .unwrap()
-                .modified()
-                .unwrap()
-                .duration_since(std::time::UNIX_EPOCH)
-                .unwrap()
-                .as_millis()
-                .to_string()
-        })
-        .collect::<Vec<_>>()
-        .join("\n")
-}