Merge branch 'main' into llbc4

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -403,13 +403,7 @@ impl CodegenBackend for GotocCodegenBackend {
     /// We need to emit `rlib` files normally if requested. Cargo expects these in some
     /// circumstances and sends them to subsequent builds with `-L`.
     ///
-    /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects.
-    /// What determines whether the native linker is invoked or not is the set of `crate_types`.
-    /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker.
-    ///
-    /// Thus, we manually build the rlib file including only the `rmeta` file.
-    ///
-    /// For cases where no metadata file was requested, we stub the file requested by writing the
+    /// For other crate types, we stub the file requested by writing the
     /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata.
     /// See <https://github.com/model-checking/kani/issues/2234> for more details.
     fn link(
@@ -419,6 +413,14 @@ impl CodegenBackend for GotocCodegenBackend {
         outputs: &OutputFilenames,
     ) -> Result<(), ErrorGuaranteed> {
         let requested_crate_types = &codegen_results.crate_info.crate_types;
+        // Create the rlib if one was requested.
+        if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) {
+            link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?;
+        }
+
+        // But override all the other outputs.
+        // Note: Do this after `link_binary` call, since it may write to the object files
+        // and override the json we are creating.
         for crate_type in requested_crate_types {
             let out_fname = out_filename(
                 sess,
@@ -428,10 +430,7 @@ impl CodegenBackend for GotocCodegenBackend {
             );
             let out_path = out_fname.as_path();
             debug!(?crate_type, ?out_path, "link");
-            if *crate_type == CrateType::Rlib {
-                // Emit the `rlib` that contains just one file: `<crate>.rmeta`
-                link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?
-            } else {
+            if *crate_type != CrateType::Rlib {
                 // Write the location of the kani metadata file in the requested compiler output file.
                 let base_filepath = outputs.path(OutputType::Object);
                 let base_filename = base_filepath.as_path();

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/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml

@@ -0,0 +1,13 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "supported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle supported crate types"
+
+[lib]
+name = "lib"
+crate-type = ["cdylib", "rlib"]
+path = "../src/lib.rs"
+

tests/cargo-ui/supported-lib-types/cdylib-rlib/expected

@@ -0,0 +1,2 @@
+Checking harness check_ok...
+VERIFICATION:- SUCCESSFUL

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}