Rejoin kani-verifer into the overall workspace (rust-lang#1058)

* Rejoin kani-verifer into the overall workspace

* Instead of copying binaries, let's cargo install the package into the container.

Author: tedinski

Diff for: .dockerignore

@@ -1,4 +1,5 @@
 .git
 firecracker
-target
+target/debug
+target/release
 build

Diff for: .github/workflows/kani.yml

@@ -84,7 +84,7 @@ jobs:
       - name: Build release bundle
         run: |
           cargo run -p make-kani-release -- latest
-          rm -rf target
+          cargo package -p kani-verifier
       
       - name: Build container test
         run: |

Diff for: .gitignore

@@ -86,4 +86,3 @@ tests/kani-multicrate/type-mismatch/mismatch/target
 /docs/book
 /docs/mdbook*
 /kani-*.tar.gz
-/src/kani-verifier/target

Diff for: Cargo.lock

@@ -449,6 +449,14 @@ dependencies = [
  "toml",
 ]
 
+[[package]]
+name = "kani-verifier"
+version = "0.1.0"
+dependencies = [
+ "anyhow",
+ "home",
+]
+
 [[package]]
 name = "kani_macros"
 version = "0.1.0"

Diff for: Cargo.toml

@@ -8,6 +8,7 @@ members = [
   "tools/bookrunner",
   "tools/compiletest",
   "tools/make-kani-release",
+  "src/kani-verifier",
   "src/kani-driver",
   "src/kani-compiler",
   "src/kani_metadata",
@@ -16,8 +17,6 @@ members = [
 ]
 
 exclude = [
-  # temporarily exclude `kani-verifier` until we don't have colliding binary names (cargo-kani)
-  "src/kani-verifier",
   "build",
   "target",
   # dependency tests have their own workspace

Diff for: scripts/ci/Dockerfile.release-bundle-test

@@ -14,6 +14,7 @@ ENV PATH="/root/.cargo/bin:${PATH}"
 WORKDIR /tmp/kani
 COPY ./tests ./tests
 COPY ./kani-latest-x86_64-unknown-linux-gnu.tar.gz ./
-COPY ./src/kani-verifier/target/release/kani /root/.cargo/bin/
-COPY ./src/kani-verifier/target/release/cargo-kani /root/.cargo/bin/
+# Very awkward glob (not regex!) to get `kani-verifier-*` and not `kani-verifier-*.crate`
+COPY ./target/package/kani-verifier-*[^e] ./kani-verifier
+RUN cargo install --path ./kani-verifier
 RUN cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz

Diff for: src/kani-verifier/src/lib.rs

@@ -58,6 +58,7 @@ pub fn proxy(bin: &str) -> Result<()> {
             setup(None)
         }
     } else {
+        fail_if_in_dev_environment()?;
         if !appears_setup() {
             setup(None)?;
         }
@@ -70,6 +71,25 @@ fn appears_setup() -> bool {
     kani_dir().exists()
 }
 
+/// In dev environments, this proxy shouldn't be used.
+/// But accidentally using it (with the test suite) can fire off
+/// hundreds of HTTP requests trying to download a non-existent release bundle.
+/// So if we positively detect a dev environment, raise an error early.
+fn fail_if_in_dev_environment() -> Result<()> {
+    if let Ok(exe) = std::env::current_exe() {
+        if let Some(path) = exe.parent() {
+            if path.ends_with("target/debug") || path.ends_with("target/release") {
+                bail!(
+                    "Running a release-only executable, {}, from a development environment. This is usually caused by PATH including 'target/release' erroneously.",
+                    exe.file_name().unwrap().to_string_lossy()
+                )
+            }
+        }
+    }
+
+    Ok(())
+}
+
 /// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION`
 fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
     let kani_dir = kani_dir();

Diff for: tools/compiletest/src/main.rs

@@ -40,9 +40,21 @@ fn main() {
     let config = parse_config(env::args().collect());
 
     log_config(&config);
+    add_kani_to_path();
     run_tests(config);
 }
 
+/// Adds Kani to the current `PATH` environment variable.
+fn add_kani_to_path() {
+    let cwd = env::current_dir().unwrap();
+    let kani_bin = cwd.join("target").join("debug");
+    let kani_scripts = cwd.join("scripts");
+    env::set_var(
+        "PATH",
+        format!("{}:{}:{}", kani_scripts.display(), kani_bin.display(), env::var("PATH").unwrap()),
+    );
+}
+
 pub fn parse_config(args: Vec<String>) -> Config {
     let mut opts = Options::new();
     opts.optopt("", "compile-lib-path", "path to host shared libraries", "PATH")

Diff for: tools/compiletest/src/runtest.rs

@@ -163,21 +163,6 @@ impl<'test> TestCx<'test> {
         proc_res.fatal(None, || ());
     }
 
-    /// Adds kani scripts directory to the `PATH` environment variable.
-    fn add_kani_dir_to_path(&self, command: &mut Command) {
-        // If the PATH environment variable is already defined,
-        if let Some((key, val)) = env::vars().find(|(key, _)| key == "PATH") {
-            // Add the Kani scripts directory to the PATH.
-            command.env(key, format!("{}:{}", self.config.kani_dir_path.to_str().unwrap(), val));
-        } else {
-            // Otherwise, insert PATH as a new environment variable and set its value to the Kani scripts directory.
-            command.env(
-                String::from("PATH"),
-                String::from(self.config.kani_dir_path.to_str().unwrap()),
-            );
-        }
-    }
-
     /// Runs `kani-compiler` on the test file specified by `self.testpaths.file`. An
     /// error message is printed to stdout if the check result is not expected.
     fn check(&self) {
@@ -187,7 +172,6 @@ impl<'test> TestCx<'test> {
             .args(self.props.compile_flags.clone())
             .args(["-Z", "no-codegen"])
             .arg(&self.testpaths.file);
-        self.add_kani_dir_to_path(&mut rustc);
         let proc_res = self.compose_and_run(rustc);
         if self.props.kani_panic_step == Some(KaniFailStep::Check) {
             if proc_res.status.success() {
@@ -211,7 +195,6 @@ impl<'test> TestCx<'test> {
             .args(["--out-dir"])
             .arg(self.output_base_dir())
             .arg(&self.testpaths.file);
-        self.add_kani_dir_to_path(&mut rustc);
         let proc_res = self.compose_and_run(rustc);
         if self.props.kani_panic_step == Some(KaniFailStep::Codegen) {
             if proc_res.status.success() {
@@ -325,7 +308,6 @@ impl<'test> TestCx<'test> {
         if "expected" != self.testpaths.file.file_name().unwrap() {
             cargo.args(["--harness", function_name]);
         }
-        self.add_kani_dir_to_path(&mut cargo);
         let proc_res = self.compose_and_run(cargo);
         let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap();
         self.verify_output(&proc_res, &expected);
@@ -352,7 +334,6 @@ impl<'test> TestCx<'test> {
             kani.arg("--enable-unstable").arg("--cbmc-args").args(&self.props.cbmc_flags);
         }
 
-        self.add_kani_dir_to_path(&mut kani);
         self.compose_and_run(kani)
     }
 

Diff for: tools/make-kani-release/src/main.rs

@@ -64,13 +64,6 @@ fn prebundle(dir: &Path) -> Result<()> {
     // Before we begin, ensure Kani is built successfully in release mode.
     Command::new("cargo").args(&["build", "--release"]).run()?;
 
-    // TODO: temporarily, until cargo-kani is renamed kani-driver, we need to build this thing not in our workspace.
-    // This isn't actually used by this script, but by the Dockerfile that tests this script
-    Command::new("cargo")
-        .args(&["build", "--release"])
-        .current_dir(Path::new("src/kani-verifier"))
-        .run()?;
-
     Ok(())
 }