From 137e581f7080de1d6f5a771821e95acacd3bd096 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 4 Jul 2025 11:16:35 +0000
Subject: [PATCH] Implement support for Cargo.toml's default-members

Cargo has resolved https://github.com/rust-lang/cargo/issues/8033.
Invoking `cargo kani` now correctly mimics cargo's behavior when there
is a `default-members` entry in `Cargo.toml`.
---
 kani-driver/src/call_cargo.rs                   | 17 ++++++++---------
 tests/cargo-kani/default-members/Cargo.toml     | 17 +++++++++++++++++
 .../default-members/builds-ok/Cargo.toml        |  8 ++++++++
 .../default-members/builds-ok/src/main.rs       |  6 ++++++
 .../default-members/dont-build-me/Cargo.toml    |  8 ++++++++
 .../default-members/dont-build-me/src/main.rs   |  5 +++++
 tests/cargo-kani/default-members/main.expected  |  3 +++
 tests/cargo-kani/default-members/src/main.rs    |  5 +++++
 8 files changed, 60 insertions(+), 9 deletions(-)
 create mode 100644 tests/cargo-kani/default-members/Cargo.toml
 create mode 100644 tests/cargo-kani/default-members/builds-ok/Cargo.toml
 create mode 100644 tests/cargo-kani/default-members/builds-ok/src/main.rs
 create mode 100644 tests/cargo-kani/default-members/dont-build-me/Cargo.toml
 create mode 100644 tests/cargo-kani/default-members/dont-build-me/src/main.rs
 create mode 100644 tests/cargo-kani/default-members/main.expected
 create mode 100644 tests/cargo-kani/default-members/src/main.rs

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index f669612c5960..db1dd8c9a87c 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -408,14 +408,14 @@ crate-type = ["lib"]
 
     /// Extract the packages that should be verified.
     ///
-    /// The result is built following these rules:
+    /// The result is built following these rules (mimicking cargo, see
+    /// https://github.com/rust-lang/cargo/blob/master/src/cargo/core/workspace.rs):
     /// - If `--package <pkg>` is given, return the list of packages selected.
     /// - If `--exclude <pkg>` is given, return the list of packages not excluded.
     /// - If `--workspace` is given, return the list of workspace members.
-    /// - If no argument provided, return the root package if there's one or all members.
-    ///   - I.e.: Do whatever cargo does when there's no `default_members`.
-    ///   - This is because `default_members` is not available in cargo metadata.
-    ///     See <https://github.com/rust-lang/cargo/issues/8033>.
+    /// - Else obtain the set of packages from cargo's default_workspace_members (i.e., if
+    ///   `default-members` is specified in Cargo.toml, use that list; else if a root package is
+    ///   specified use that; else use all members).
     ///
     /// In addition, if either `--package <pkg>` or `--exclude <pkg>` is given,
     /// validate that `<pkg>` is a package name in the workspace, or return an error
@@ -455,11 +455,10 @@ crate-type = ["lib"]
                 .into_iter()
                 .filter(|pkg| !pkg_ids.contains_key(&pkg.id))
                 .collect()
+        } else if args.cargo.workspace {
+            metadata.workspace_packages()
         } else {
-            match (args.cargo.workspace, metadata.root_package()) {
-                (true, _) | (_, None) => metadata.workspace_packages(),
-                (_, Some(root_pkg)) => vec![root_pkg],
-            }
+            metadata.workspace_default_packages()
         };
         trace!(?packages, "packages_to_verify result");
         Ok(packages)
diff --git a/tests/cargo-kani/default-members/Cargo.toml b/tests/cargo-kani/default-members/Cargo.toml
new file mode 100644
index 000000000000..40f439dddc0d
--- /dev/null
+++ b/tests/cargo-kani/default-members/Cargo.toml
@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "empty-main"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]
+members = [ "builds-ok","dont-build-me"]
+
+# This indicates what package to e.g. build with 'cargo build' without --workspace
+default-members = [
+  ".",
+  "builds-ok",
+]
diff --git a/tests/cargo-kani/default-members/builds-ok/Cargo.toml b/tests/cargo-kani/default-members/builds-ok/Cargo.toml
new file mode 100644
index 000000000000..08d2a18b1b2a
--- /dev/null
+++ b/tests/cargo-kani/default-members/builds-ok/Cargo.toml
@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "builds-ok"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
diff --git a/tests/cargo-kani/default-members/builds-ok/src/main.rs b/tests/cargo-kani/default-members/builds-ok/src/main.rs
new file mode 100644
index 000000000000..390a15b9c89d
--- /dev/null
+++ b/tests/cargo-kani/default-members/builds-ok/src/main.rs
@@ -0,0 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn main() {
+    assert!(1 == 2);
+}
diff --git a/tests/cargo-kani/default-members/dont-build-me/Cargo.toml b/tests/cargo-kani/default-members/dont-build-me/Cargo.toml
new file mode 100644
index 000000000000..da966981930e
--- /dev/null
+++ b/tests/cargo-kani/default-members/dont-build-me/Cargo.toml
@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "dont-build-me"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
diff --git a/tests/cargo-kani/default-members/dont-build-me/src/main.rs b/tests/cargo-kani/default-members/dont-build-me/src/main.rs
new file mode 100644
index 000000000000..cb17e1fa7c9d
--- /dev/null
+++ b/tests/cargo-kani/default-members/dont-build-me/src/main.rs
@@ -0,0 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+fn main() {
+    this - is - not - valid - rust;
+}
diff --git a/tests/cargo-kani/default-members/main.expected b/tests/cargo-kani/default-members/main.expected
new file mode 100644
index 000000000000..be58472a087b
--- /dev/null
+++ b/tests/cargo-kani/default-members/main.expected
@@ -0,0 +1,3 @@
+FAILURE\
+assertion failed: 1 == 2
+VERIFICATION:- FAILED
diff --git a/tests/cargo-kani/default-members/src/main.rs b/tests/cargo-kani/default-members/src/main.rs
new file mode 100644
index 000000000000..45d8c4ae1cfe
--- /dev/null
+++ b/tests/cargo-kani/default-members/src/main.rs
@@ -0,0 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+fn main() {
+    println!("Hello, world!");
+}
