Running verify-std no longer changes Cargo files

kani-driver/src/call_cargo.rs

@@ -46,10 +46,39 @@ pub struct CargoOutputs {
 
 impl KaniSession {
     /// Create a new cargo library in the given path.
+    ///
+    /// Since we cannot create a new workspace with `cargo init --lib`, we create the dummy
+    /// crate manually. =( See <https://github.com/rust-lang/cargo/issues/8365>.
+    ///
+    /// Without setting up a new workspace, cargo init will modify the workspace where this is
+    /// running. See <https://github.com/model-checking/kani/issues/3574> for details.
     pub fn cargo_init_lib(&self, path: &Path) -> Result<()> {
-        let mut cmd = setup_cargo_command()?;
-        cmd.args(["init", "--lib", path.to_string_lossy().as_ref()]);
-        self.run_terminal(cmd)
+        let toml_path = path.join("Cargo.toml");
+        if toml_path.exists() {
+            bail!("Cargo.toml already exists in {}", path.display());
+        }
+
+        // Create folder for library
+        fs::create_dir_all(path.join("src"))?;
+
+        // Create dummy crate and write dummy body
+        let lib_path = path.join("src/lib.rs");
+        fs::write(&lib_path, "pub fn dummy() {}")?;
+
+        // Create Cargo.toml
+        fs::write(
+            &toml_path,
+            r#"[package]
+name = "dummy"
+version = "0.1.0"
+
+[lib]
+crate-type = ["lib"]
+
+[workspace]
+"#,
+        )?;
+        Ok(())
     }
 
     pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result<Vec<Artifact>> {

tests/script-based-pre/verify_std_cmd/verify_std.expected

@@ -1,3 +1,7 @@
+[TEST] Only codegen inside library folder
+No kani crate inside Cargo.toml as expected
+
+
 [TEST] Run kani verify-std
 
 Checking harness verify::dummy_proof...

tests/script-based-pre/verify_std_cmd/verify_std.sh

@@ -50,17 +50,44 @@ cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs
 echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs
 cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs
 
+# Test that the command works inside the library folder and does not change
+# the existing workspace
+# See https://github.com/model-checking/kani/issues/3574
+echo "[TEST] Only codegen inside library folder"
+pushd "${TMP_DIR}/library" >& /dev/null
+RUSTFLAGS="--cfg=uninit_checks" kani verify-std \
+    -Z unstable-options \
+    . \
+    -Z function-contracts \
+    -Z stubbing \
+    -Z mem-predicates \
+    --only-codegen
+popd
+# Grep should not find anything and exit status is 1.
+grep -c kani ${TMP_DIR}/library/Cargo.toml \
+    && echo "Unexpected kani crate inside Cargo.toml" \
+    || echo "No kani crate inside Cargo.toml as expected"
+
 echo "[TEST] Run kani verify-std"
 export RUST_BACKTRACE=1
-kani verify-std -Z unstable-options "${TMP_DIR}/library" \
-    --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \
+kani verify-std \
+    -Z unstable-options \
+    "${TMP_DIR}/library" \
+    --target-dir "${TMP_DIR}/target" \
+    -Z function-contracts \
+    -Z stubbing \
     -Z mem-predicates
 
+# Test that uninit-checks basic setup works on a no-core library
 echo "[TEST] Run kani verify-std -Z uninit-checks"
-export RUSTFLAGS="--cfg=uninit_checks"
-kani verify-std -Z unstable-options "${TMP_DIR}/library" \
-    --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \
-    -Z mem-predicates -Z uninit-checks
+RUSTFLAGS="--cfg=uninit_checks" kani verify-std \
+    -Z unstable-options \
+    "${TMP_DIR}/library" \
+    --target-dir "${TMP_DIR}/target" \
+    -Z function-contracts \
+    -Z stubbing \
+    -Z mem-predicates \
+    -Z uninit-checks
 
 # Cleanup
 rm -r ${TMP_DIR}