Allow excluding packages from verification with --exclude (model-checking#2399)

Author: adpaco-aws

kani-driver/src/args.rs

@@ -302,6 +302,7 @@ pub struct CargoArgs {
     /// Do not activate the `default` feature
     #[arg(long)]
     pub no_default_features: bool,
+
     // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach...
     /// Comma separated list of features to activate
     #[arg(short = 'F', long)]
@@ -314,9 +315,14 @@ pub struct CargoArgs {
     /// Build all packages in the workspace
     #[arg(long)]
     pub workspace: bool,
+
     /// Run Kani on the specified packages.
     #[arg(long, short, conflicts_with("workspace"), num_args(1..))]
     pub package: Vec<String>,
+
+    /// Exclude the specified packages
+    #[arg(long, short, requires("workspace"), conflicts_with("package"), num_args(1..))]
+    pub exclude: Vec<String>,
 }
 
 impl CargoArgs {

kani-driver/src/call_cargo.rs

@@ -104,7 +104,7 @@ impl KaniSession {
         pkg_args.extend(["--".to_string(), self.reachability_arg()]);
 
         let mut found_target = false;
-        let packages = packages_to_verify(&self.args, &metadata);
+        let packages = packages_to_verify(&self.args, &metadata)?;
         let mut artifacts = vec![];
         let mut failed_targets = vec![];
         for package in packages {
@@ -261,35 +261,57 @@ fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> {
     Ok(())
 }
 
+/// Check that all package names are present in the workspace, otherwise return which aren't.
+fn validate_package_names(package_names: &[String], packages: &[Package]) -> Result<()> {
+    let package_list: Vec<String> = packages.iter().map(|pkg| pkg.name.clone()).collect();
+    let unknown_packages: Vec<&String> =
+        package_names.iter().filter(|pkg_name| !package_list.contains(pkg_name)).collect();
+
+    // Some packages aren't in the workspace. Return an error which includes their names.
+    if !unknown_packages.is_empty() {
+        let fmt_packages: Vec<String> =
+            unknown_packages.iter().map(|pkg| format!("`{pkg}`")).collect();
+        let error_msg = if unknown_packages.len() == 1 {
+            format!("couldn't find package {}", fmt_packages[0])
+        } else {
+            format!("couldn't find packages {}", fmt_packages.join(", "))
+        };
+        bail!(error_msg);
+    };
+    Ok(())
+}
+
 /// Extract the packages that should be verified.
 /// 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>.
-fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Vec<&'b Package> {
-    debug!(package_selection=?args.cargo.package, workspace=args.cargo.workspace, "packages_to_verify args");
+/// 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
+/// otherwise.
+fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Result<Vec<&'b Package>> {
+    debug!(package_selection=?args.cargo.package, package_exclusion=?args.cargo.exclude, workspace=args.cargo.workspace, "packages_to_verify args");
     let packages = if !args.cargo.package.is_empty() {
+        validate_package_names(&args.cargo.package, &metadata.packages)?;
         args.cargo
             .package
             .iter()
-            .map(|pkg_name| {
-                metadata
-                    .packages
-                    .iter()
-                    .find(|pkg| pkg.name == *pkg_name)
-                    .expect(&format!("Cannot find package '{pkg_name}'"))
-            })
+            .map(|pkg_name| metadata.packages.iter().find(|pkg| pkg.name == *pkg_name).unwrap())
             .collect()
+    } else if !args.cargo.exclude.is_empty() {
+        validate_package_names(&args.cargo.exclude, &metadata.packages)?;
+        metadata.packages.iter().filter(|pkg| !args.cargo.exclude.contains(&pkg.name)).collect()
     } else {
         match (args.cargo.workspace, metadata.root_package()) {
             (true, _) | (_, None) => metadata.workspace_packages(),
             (_, Some(root_pkg)) => vec![root_pkg],
         }
     };
     trace!(?packages, "packages_to_verify result");
-    packages
+    Ok(packages)
 }
 
 /// Extract Kani artifact that might've been generated from a given rustc artifact.

tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This workspace test checks that the `--exclude` option prints a user-friendly
+# error when the package isn't found in the workspace.
+
+[package]
+name = "ws-package-exclude"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+members = ["lib_package", "bin_package"]
+
+[workspace.metadata.kani.flags]
+workspace = true
+exclude = ["unknown_package"]

tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "bin_package"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {}
+
+#[kani::proof]
+fn harness_in_bin_package() {
+    assert!(1 + 1 == 2);
+}

tests/cargo-ui/ws-package-exclude-unknown/expected

@@ -0,0 +1 @@
+error: couldn't find package `unknown_package`

tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "lib_package"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "lib_package"
+path = "src/lib.rs"

tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn api() {}
+
+#[kani::proof]
+fn harness_in_lib_package() {
+    assert!(1 + 1 == 2);
+}

tests/cargo-ui/ws-package-exclude-unknown/src/main.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {}
+
+#[kani::proof]
+fn harness_in_ws_package() {
+    assert!(1 + 1 == 3);
+}

tests/cargo-ui/ws-package-exclude/Cargo.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This workspace test checks that the `--exclude` option removes the
+# `ws-package-exclude` package from the packages to verify.
+
+[package]
+name = "ws-package-exclude"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+members = ["lib_package", "bin_package"]
+
+[workspace.metadata.kani.flags]
+workspace = true
+exclude = ["ws-package-exclude"]