Skip to content

Commit

Permalink
Support fully-qualified --package arguments (#3593)
Browse files Browse the repository at this point in the history
We were previously matching the name of the package, which would limit
users if the name is ambiguous.

Instead, use `cargo pkgid` to validate the `--package` argument and to
retrieve the package id.

Resolves #3563 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>
  • Loading branch information
celinval and zhassan-aws authored Oct 12, 2024
1 parent 373af49 commit 5e67b63
Show file tree
Hide file tree
Showing 9 changed files with 156 additions and 72 deletions.
2 changes: 1 addition & 1 deletion kani-driver/src/args/cargo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,

Expand Down
161 changes: 92 additions & 69 deletions kani-driver/src/call_cargo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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<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> {
Expand All @@ -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<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<>`.
///
Expand Down
3 changes: 2 additions & 1 deletion tests/cargo-ui/ws-package-exclude-unknown/expected
Original file line number Diff line number Diff line change
@@ -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`
3 changes: 2 additions & 1 deletion tests/cargo-ui/ws-package-select-unknown/expected
Original file line number Diff line number Diff line change
@@ -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`
11 changes: 11 additions & 0 deletions tests/script-based-pre/ambiguous_crate/Cargo.toml
Original file line number Diff line number Diff line change
@@ -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]
16 changes: 16 additions & 0 deletions tests/script-based-pre/ambiguous_crate/ambiguous.sh
Original file line number Diff line number Diff line change
@@ -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 [email protected] --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 [email protected] || echo "Found expected out of workspace error"

rm -rf target
4 changes: 4 additions & 0 deletions tests/script-based-pre/ambiguous_crate/config.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
script: ambiguous.sh
expected: expected
15 changes: 15 additions & 0 deletions tests/script-based-pre/ambiguous_crate/expected
Original file line number Diff line number Diff line change
@@ -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:
[email protected]
[email protected]
error: Failed to retrieve information for `zerocopy`
Found expected ambiguous crate error

error: The following specified packages were not found in this workspace: `[email protected]`
Found expected out of workspace error
13 changes: 13 additions & 0 deletions tests/script-based-pre/ambiguous_crate/src/lib.rs
Original file line number Diff line number Diff line change
@@ -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);
}

0 comments on commit 5e67b63

Please sign in to comment.