Support fully-qualified --package arguments

kani-driver/src/args/cargo.rs

@@ -33,7 +33,7 @@ pub struct CargoCommonArgs {
     #[arg(long)]
     pub workspace: bool,
 
-    /// Run Kani on the specified packages.
+    /// Run Kani on the specified packages (see `cargo help pkgid` for the accepted format)
     #[arg(long, short, conflicts_with("workspace"), num_args(1..))]
     pub package: Vec<String>,
 

kani-driver/src/call_cargo.rs

@@ -9,14 +9,15 @@ use crate::util;
 use anyhow::{Context, Result, bail};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{
-    Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, Target,
+    Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, PackageId, Target,
 };
 use kani_metadata::{ArtifactType, CompilerArtifactStub};
+use std::collections::HashMap;
 use std::ffi::{OsStr, OsString};
 use std::fmt::{self, Display};
 use std::fs::{self, File};
-use std::io::BufReader;
 use std::io::IsTerminal;
+use std::io::{BufRead, BufReader};
 use std::path::{Path, PathBuf};
 use std::process::Command;
 use tracing::{debug, trace};
@@ -166,14 +167,14 @@ 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 = self.packages_to_verify(&self.args, &metadata)?;
         let mut artifacts = vec![];
         let mut failed_targets = vec![];
         for package in packages {
             for verification_target in package_targets(&self.args, package) {
                 let mut cmd = setup_cargo_command()?;
                 cmd.args(&cargo_args)
-                    .args(vec!["-p", &package.name])
+                    .args(vec!["-p", &package.id.to_string()])
                     .args(verification_target.to_args())
                     .args(&pkg_args)
                     .env("RUSTC", &self.kani_compiler)
@@ -336,6 +337,93 @@ impl KaniSession {
             if same_target(&artifact.target, target) { map_kani_artifact(artifact) } else { None }
         }))
     }
+
+    /// Check that all package names are present in the workspace, otherwise return which aren't.
+    fn to_package_ids<'a>(
+        &self,
+        package_names: &'a [String],
+    ) -> Result<HashMap<PackageId, &'a str>> {
+        package_names
+            .iter()
+            .map(|pkg| {
+                let mut cmd = setup_cargo_command()?;
+                cmd.arg("pkgid");
+                cmd.arg(pkg);
+                // For some reason clippy cannot see that we are invoking wait() in the next line.
+                #[allow(clippy::zombie_processes)]
+                let mut process = self.run_piped(cmd)?.unwrap();
+                let result = process.wait()?;
+                if !result.success() {
+                    bail!("Failed to retrieve information for `{pkg}`");
+                }
+
+                let mut reader = BufReader::new(process.stdout.take().unwrap());
+                let mut line = String::new();
+                reader.read_line(&mut line)?;
+                trace!(package_id=?line, "package_ids");
+                Ok((PackageId { repr: line.trim().to_string() }, pkg.as_str()))
+            })
+            .collect()
+    }
+
+    /// Extract the packages that should be verified.
+    ///
+    /// The result is built following these rules:
+    /// - 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>.
+    ///
+    /// 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>(
+        &self,
+        args: &VerificationArgs,
+        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() {
+            let pkg_ids = self.to_package_ids(&args.cargo.package)?;
+            let filtered: Vec<_> = metadata
+                .workspace_packages()
+                .into_iter()
+                .filter(|pkg| pkg_ids.contains_key(&pkg.id))
+                .collect();
+            if filtered.len() < args.cargo.package.len() {
+                // Some packages specified in `--package` were not found in the workspace.
+                let outer: Vec<_> = metadata
+                    .packages
+                    .iter()
+                    .filter_map(|pkg| pkg_ids.get(&pkg.id).copied())
+                    .collect();
+                bail!(
+                    "The following specified packages were not found in this workspace: `{}`",
+                    outer.join("`,")
+                );
+            }
+            filtered
+        } else if !args.cargo.exclude.is_empty() {
+            // should be ensured by argument validation
+            assert!(args.cargo.workspace);
+            let pkg_ids = self.to_package_ids(&args.cargo.exclude)?;
+            metadata
+                .workspace_packages()
+                .into_iter()
+                .filter(|pkg| !pkg_ids.contains_key(&pkg.id))
+                .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");
+        Ok(packages)
+    }
 }
 
 pub fn cargo_config_args() -> Vec<OsString> {
@@ -361,71 +449,6 @@ 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.
-///
-/// The result is build following these rules:
-/// - 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>.
-///
-/// 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: &VerificationArgs,
-    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).unwrap())
-            .collect()
-    } else if !args.cargo.exclude.is_empty() {
-        // should be ensured by argument validation
-        assert!(args.cargo.workspace);
-        validate_package_names(&args.cargo.exclude, &metadata.packages)?;
-        metadata
-            .workspace_packages()
-            .into_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");
-    Ok(packages)
-}
-
 /// Extract Kani artifact that might've been generated from a given rustc artifact.
 /// Not every rustc artifact will map to a kani artifact, hence the `Option<>`.
 ///

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

@@ -1 +1,2 @@
-error: couldn't find package `unknown_package`
+error: package ID specification `unknown_package` did not match any packages
+error: Failed to retrieve information for `unknown_package`

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

@@ -1 +1,2 @@
-error: couldn't find package `unknown_package`
+error: package ID specification `unknown_package` did not match any packages
+error: Failed to retrieve information for `unknown_package`

tests/script-based-pre/ambiguous_crate/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "zerocopy"
+version = "0.0.1"
+edition = "2021"
+
+[dependencies]
+zerocopy = "=0.8.4"
+
+[workspace]

tests/script-based-pre/ambiguous_crate/ambiguous.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+# Test how Kani handle ambiguous crate names.
+
+rm -rf target
+set -e
+cargo kani --output-format terse && echo "No package is needed"
+cargo kani -p zerocopy@0.0.1 --output-format terse && echo "But passing the correct package works"
+
+# These next commands should fail so disable failures
+set +e
+cargo kani -p zerocopy || echo "Found expected ambiguous crate error"
+cargo kani -p zerocopy@0.8.4 || echo "Found expected out of workspace error"
+
+rm -rf target

tests/script-based-pre/ambiguous_crate/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: ambiguous.sh
+expected: expected

tests/script-based-pre/ambiguous_crate/expected

@@ -0,0 +1,15 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total\
+No package is needed
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total\
+But passing the correct package works
+
+error: There are multiple `zerocopy` packages in your project, and the specification `zerocopy` is ambiguous.
+Please re-run this command with one of the following specifications:
+  zerocopy@0.0.1
+  zerocopy@0.8.4
+error: Failed to retrieve information for `zerocopy`
+Found expected ambiguous crate error
+
+error: The following packages specified do not belong to this workspace: `zerocopy@0.8.4`
+Found expected out of workspace error

tests/script-based-pre/ambiguous_crate/src/lib.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Test that cargo kani works when there are ambiguous packages.
+//! See <https://github.com/model-checking/kani/issues/3563>
+
+use zerocopy::FromZeros;
+
+#[kani::proof]
+fn check_zero_copy() {
+    let opt = Option::<&char>::new_zeroed();
+    assert_eq!(opt, None);
+}