Ensure cargo-kani setup is idempotent (model-checking#1193)

* Ensure cargo-kani setup is idempotent

* add test, flip print order for better errors

Author: tedinski

.github/workflows/kani.yml

@@ -107,6 +107,7 @@ jobs:
           docker run -w /tmp/kani/tests/cargo-kani/simple-lib  kani-latest  cargo kani
           docker run -w /tmp/kani/tests/cargo-kani/simple-visualize  kani-latest  cargo kani
           docker run -w /tmp/kani/tests/cargo-kani/build-rs-works  kani-latest  cargo kani
+          docker run kani-latest  cargo-kani setup --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz
 
       # We can't run macos in a container, so we can only test locally.
       # Hopefully any dependency issues won't be unique to macos.

src/lib.rs

@@ -111,16 +111,20 @@ fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
     std::fs::create_dir_all(&base_dir)?;
 
     if let Some(pathstr) = use_local_bundle {
+        println!("[2/6] Installing local Kani bundle: {}", pathstr.to_string_lossy());
         let path = Path::new(&pathstr).canonicalize()?;
-        println!("[2/6] Installing local Kani bundle: {}", path.display());
-        Command::new("tar").arg("zxf").arg(&path).current_dir(base_dir).run()?;
-
-        // when given a local bundle, it's often "-latest" but we expect "-1.0" or something. Hack it up.
-        let file = path.file_name().expect("has filename").to_string_lossy();
-        let components: Vec<_> = file.split('-').collect();
-        let expected_dir = format!("{}-{}", components[0], components[1]);
-
-        std::fs::rename(base_dir.join(expected_dir), &kani_dir)?;
+        // When given a local bundle, it's often "-latest" but we expect "-1.0" or something.
+        // tar supports "stripping" the first directory from the bundle, so do that and
+        // extract it directly into the expected (kani_dir) directory (instead of base_dir).
+        if !kani_dir.exists() {
+            std::fs::create_dir(&kani_dir)?;
+        }
+        Command::new("tar")
+            .arg("--strip-components=1")
+            .arg("-zxf")
+            .arg(&path)
+            .current_dir(&kani_dir)
+            .run()?;
     } else {
         let filename = download_filename();
         println!("[2/6] Downloading Kani release bundle: {}", &filename);
@@ -145,7 +149,7 @@ fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
 
     let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version);
 
-    Command::new("ln").arg("-s").arg(toolchain).arg(kani_dir.join("toolchain")).run()?;
+    symlink_rust_toolchain(&toolchain, &kani_dir)?;
 
     println!("[4/6] Installing Kani python dependencies...");
     let pyroot = kani_dir.join("pyroot");
@@ -201,6 +205,17 @@ fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
     Ok(())
 }
 
+/// Creates a `kani_dir/toolchain` symlink pointing to `toolchain`.
+fn symlink_rust_toolchain(toolchain: &Path, kani_dir: &Path) -> Result<()> {
+    let path = kani_dir.join("toolchain");
+    // We want to be idempotent, so if the symlink already exists, delete it first
+    if path.exists() && path.is_symlink() {
+        std::fs::remove_file(&path)?;
+    }
+    std::os::unix::fs::symlink(toolchain, path)?;
+    Ok(())
+}
+
 /// Executes `kani-driver` in `bin` mode (kani or cargo-kani)
 /// augmenting environment variables to accomodate our release environment
 fn exec(bin: &str) -> Result<()> {