diff --git a/kani-driver/src/args/cargo.rs b/kani-driver/src/args/cargo.rs index 6a9e478667b5..ee12b082381d 100644 --- a/kani-driver/src/args/cargo.rs +++ b/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, diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index b566f0ff79c7..fbd3f4c84826 100644 --- a/kani-driver/src/call_cargo.rs +++ b/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}; @@ -198,14 +199,14 @@ crate-type = ["lib"] } 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) @@ -368,6 +369,93 @@ crate-type = ["lib"] 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> { + 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 ` is given, return the list of packages selected. + /// - If `--exclude ` 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 . + /// + /// In addition, if either `--package ` or `--exclude ` is given, + /// validate that `` is a package name in the workspace, or return an error + /// otherwise. + fn packages_to_verify<'b>( + &self, + args: &VerificationArgs, + metadata: &'b Metadata, + ) -> Result> { + 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 { @@ -393,71 +481,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 = 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 = - 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 ` is given, return the list of packages selected. -/// - If `--exclude ` 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 . -/// -/// In addition, if either `--package ` or `--exclude ` is given, -/// validate that `` is a package name in the workspace, or return an error -/// otherwise. -fn packages_to_verify<'b>( - args: &VerificationArgs, - metadata: &'b Metadata, -) -> Result> { - 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<>`. /// diff --git a/tests/cargo-ui/ws-package-exclude-unknown/expected b/tests/cargo-ui/ws-package-exclude-unknown/expected index 1473676bc28e..a98487641d6f 100644 --- a/tests/cargo-ui/ws-package-exclude-unknown/expected +++ b/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` diff --git a/tests/cargo-ui/ws-package-select-unknown/expected b/tests/cargo-ui/ws-package-select-unknown/expected index 1473676bc28e..a98487641d6f 100644 --- a/tests/cargo-ui/ws-package-select-unknown/expected +++ b/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` diff --git a/tests/script-based-pre/ambiguous_crate/Cargo.toml b/tests/script-based-pre/ambiguous_crate/Cargo.toml new file mode 100644 index 000000000000..ebc052ce5be8 --- /dev/null +++ b/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] diff --git a/tests/script-based-pre/ambiguous_crate/ambiguous.sh b/tests/script-based-pre/ambiguous_crate/ambiguous.sh new file mode 100755 index 000000000000..a39cfbce1d03 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/ambiguous_crate/config.yml b/tests/script-based-pre/ambiguous_crate/config.yml new file mode 100644 index 000000000000..dca00947ee79 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/ambiguous_crate/expected b/tests/script-based-pre/ambiguous_crate/expected new file mode 100644 index 000000000000..7b9578cdda05 --- /dev/null +++ b/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 specified packages were not found in this workspace: `zerocopy@0.8.4` +Found expected out of workspace error diff --git a/tests/script-based-pre/ambiguous_crate/src/lib.rs b/tests/script-based-pre/ambiguous_crate/src/lib.rs new file mode 100644 index 000000000000..1ce6bbca8fd6 --- /dev/null +++ b/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 + +use zerocopy::FromZeros; + +#[kani::proof] +fn check_zero_copy() { + let opt = Option::<&char>::new_zeroed(); + assert_eq!(opt, None); +}