From 937e1142f5a798aaca574e096fec06a4a69e2462 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 5 Jun 2023 15:17:58 -0700 Subject: [PATCH 1/2] Add target selection for cargo kani Given the driver architecture, I explicitly added a check to ensure standalone Kani does not accept the new arguments. --- kani-driver/src/args/cargo.rs | 60 +++++++++++++++---- kani-driver/src/args/mod.rs | 57 ++++++++++++++++++ kani-driver/src/call_cargo.rs | 26 +++++--- .../target-selection/all-targets/Cargo.toml | 24 ++++++++ .../target-selection/all-targets/expected | 5 ++ .../target-selection/bin-target/Cargo.toml | 20 +++++++ .../target-selection/bin-target/expected | 7 +++ .../target-selection/bins-target/Cargo.toml | 20 +++++++ .../target-selection/bins-target/expected | 9 +++ .../target-selection/lib-target/Cargo.toml | 25 ++++++++ .../target-selection/lib-target/expected | 4 ++ .../non-test-targets/Cargo.toml | 22 +++++++ .../non-test-targets/expected | 5 ++ .../cargo-ui/target-selection/src/bin/bar.rs | 16 +++++ .../cargo-ui/target-selection/src/bin/foo.rs | 16 +++++ tests/cargo-ui/target-selection/src/lib.rs | 12 ++++ .../cargo-ui/target-selection/tests/integ.rs | 12 ++++ 17 files changed, 320 insertions(+), 20 deletions(-) create mode 100644 tests/cargo-ui/target-selection/all-targets/Cargo.toml create mode 100644 tests/cargo-ui/target-selection/all-targets/expected create mode 100644 tests/cargo-ui/target-selection/bin-target/Cargo.toml create mode 100644 tests/cargo-ui/target-selection/bin-target/expected create mode 100644 tests/cargo-ui/target-selection/bins-target/Cargo.toml create mode 100644 tests/cargo-ui/target-selection/bins-target/expected create mode 100644 tests/cargo-ui/target-selection/lib-target/Cargo.toml create mode 100644 tests/cargo-ui/target-selection/lib-target/expected create mode 100644 tests/cargo-ui/target-selection/non-test-targets/Cargo.toml create mode 100644 tests/cargo-ui/target-selection/non-test-targets/expected create mode 100644 tests/cargo-ui/target-selection/src/bin/bar.rs create mode 100644 tests/cargo-ui/target-selection/src/bin/foo.rs create mode 100644 tests/cargo-ui/target-selection/src/lib.rs create mode 100644 tests/cargo-ui/target-selection/tests/integ.rs diff --git a/kani-driver/src/args/cargo.rs b/kani-driver/src/args/cargo.rs index 11b64cb6f716..ed4734346469 100644 --- a/kani-driver/src/args/cargo.rs +++ b/kani-driver/src/args/cargo.rs @@ -94,9 +94,9 @@ impl ValidateArgs for CargoCommonArgs { } } -/// Arguments that Kani pass down into Cargo test essentially uninterpreted. +/// Arguments that cargo Kani supports to select build / test target. #[derive(Debug, Default, clap::Args)] -pub struct CargoTestArgs { +pub struct CargoTargetArgs { /// Test only the specified binary target. #[arg(long)] pub bin: Vec, @@ -108,16 +108,16 @@ pub struct CargoTestArgs { /// Test only the package's library unit tests. #[arg(long)] pub lib: bool, - - /// Arguments to pass down to Cargo - #[command(flatten)] - pub common: CargoCommonArgs, } -impl CargoTestArgs { +impl CargoTargetArgs { /// Convert the arguments back to a format that cargo can understand. pub fn to_cargo_args(&self) -> Vec { - let mut cargo_args = self.common.to_cargo_args(); + let mut cargo_args = self + .bin + .iter() + .map(|binary| format!("--bin={binary}").into()) + .collect::>(); if self.bins { cargo_args.push("--bins".into()); @@ -127,14 +127,52 @@ impl CargoTestArgs { cargo_args.push("--lib".into()); } - cargo_args.extend(self.bin.iter().map(|binary| format!("--bin={binary}").into())); + cargo_args + } + + pub fn include_bin(&self, name: &String) -> bool { + self.bins || (self.bin.is_empty() && !self.lib) || self.bin.contains(name) + } + + pub fn include_lib(&self) -> bool { + self.lib || (!self.bins && self.bin.is_empty()) + } + + pub fn include_tests(&self) -> bool { + !self.lib && !self.bins && self.bin.is_empty() + } +} + +impl ValidateArgs for CargoTargetArgs { + fn validate(&self) -> Result<(), Error> { + Ok(()) + } +} + +/// Arguments that Kani pass down into Cargo test essentially uninterpreted. +#[derive(Debug, Default, clap::Args)] +pub struct CargoTestArgs { + /// Arguments to pass down to Cargo + #[command(flatten)] + pub common: CargoCommonArgs, + + /// Arguments used to select Cargo target. + #[command(flatten)] + pub target: CargoTargetArgs, +} + +impl CargoTestArgs { + /// Convert the arguments back to a format that cargo can understand. + pub fn to_cargo_args(&self) -> Vec { + let mut cargo_args = self.common.to_cargo_args(); + cargo_args.append(&mut self.target.to_cargo_args()); cargo_args } } -/// Leave it for Cargo to validate these for now. impl ValidateArgs for CargoTestArgs { fn validate(&self) -> Result<(), Error> { - self.common.validate() + self.common.validate()?; + self.target.validate() } } diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 370989d21574..92a3775a7ca0 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -10,6 +10,7 @@ pub mod playback_args; pub use assess_args::*; use self::common::*; +use crate::args::cargo::CargoTargetArgs; use crate::util::warning; use cargo::CargoCommonArgs; use clap::builder::{PossibleValue, TypedValueParser}; @@ -299,6 +300,10 @@ pub struct VerificationArgs { #[command(flatten)] pub cargo: CargoCommonArgs, + /// Arguments used to select Cargo target. + #[command(flatten)] + pub target: CargoTargetArgs, + #[command(flatten)] pub common_args: CommonArgs, } @@ -430,9 +435,38 @@ impl CheckArgs { } } +/// Utility function to error out on arguments that are invalid Cargo specific. +/// +/// We currently define a bunch of cargo specific arguments as part of the overall arguments, +/// however, they are invalid in the Kani standalone usage. Explicitly check them for now. +/// TODO: Remove this as part of https://github.com/model-checking/kani/issues/1831 +fn check_no_cargo_opt(is_set: bool, name: &str) -> Result<(), Error> { + if is_set { + Err(Error::raw( + ErrorKind::UnknownArgument, + &format!("argument `{}` cannot be used with standalone Kani.", name), + )) + } else { + Ok(()) + } +} + impl ValidateArgs for StandaloneArgs { fn validate(&self) -> Result<(), Error> { self.verify_opts.validate()?; + // Cargo target arguments. + check_no_cargo_opt(self.verify_opts.target.bins, "--bins")?; + check_no_cargo_opt(self.verify_opts.target.lib, "--lib")?; + check_no_cargo_opt(!self.verify_opts.target.bin.is_empty(), "--bin")?; + // Cargo common arguments. + check_no_cargo_opt(self.verify_opts.cargo.all_features, "--all-features")?; + check_no_cargo_opt(self.verify_opts.cargo.no_default_features, "--no-default-features")?; + check_no_cargo_opt(!self.verify_opts.cargo.features().is_empty(), "--features / -F")?; + check_no_cargo_opt(!self.verify_opts.cargo.package.is_empty(), "--package / -p")?; + check_no_cargo_opt(!self.verify_opts.cargo.exclude.is_empty(), "--exclude")?; + check_no_cargo_opt(self.verify_opts.cargo.workspace, "--workspace")?; + check_no_cargo_opt(self.verify_opts.cargo.manifest_path.is_some(), "--manifest-path")?; + check_no_cargo_opt(self.verify_opts.cargo.workspace, "--workspace")?; if let Some(input) = &self.input { if !input.is_file() { return Err(Error::raw( @@ -885,4 +919,27 @@ mod tests { assert_eq!(args.input, None); assert!(matches!(args.command, Some(StandaloneSubcommand::Playback(..)))); } + + #[test] + fn check_standalone_does_not_accept_cargo_opts() { + fn check_invalid_args<'a, I>(args: I) + where + I: IntoIterator, + { + let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err(); + assert_eq!(err.kind(), ErrorKind::UnknownArgument) + } + + check_invalid_args("kani input.rs --bins".split_whitespace()); + check_invalid_args("kani input.rs --bin Binary".split_whitespace()); + check_invalid_args("kani input.rs --lib".split_whitespace()); + + check_invalid_args("kani input.rs --all-features".split_whitespace()); + check_invalid_args("kani input.rs --no-default-features".split_whitespace()); + check_invalid_args("kani input.rs --features feat".split_whitespace()); + check_invalid_args("kani input.rs --manifest-path pkg/Cargo.toml".split_whitespace()); + check_invalid_args("kani input.rs --workspace".split_whitespace()); + check_invalid_args("kani input.rs --package foo".split_whitespace()); + check_invalid_args("kani input.rs --exclude bar --workspace".split_whitespace()); + } } diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 382db291ed2d..30dac09eddaa 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -418,23 +418,31 @@ fn package_targets(args: &VerificationArgs, package: &Package) -> Vec { - // Binary targets. - verification_targets.push(VerificationTarget::Bin(target.clone())); + if args.target.include_bin(&target.name) { + // Binary targets. + verification_targets.push(VerificationTarget::Bin(target.clone())); + } } CRATE_TYPE_LIB | CRATE_TYPE_RLIB | CRATE_TYPE_CDYLIB | CRATE_TYPE_DYLIB | CRATE_TYPE_STATICLIB => { - supported_lib = true; + if args.target.include_lib() { + supported_lib = true; + } } CRATE_TYPE_PROC_MACRO => { - unsupported_lib = true; - ignored_unsupported.push(target.name.as_str()); + if args.target.include_lib() { + unsupported_lib = true; + ignored_unsupported.push(target.name.as_str()); + } } CRATE_TYPE_TEST => { // Test target. - if args.tests { - verification_targets.push(VerificationTarget::Test(target.clone())); - } else { - ignored_tests.push(target.name.as_str()); + if args.target.include_tests() { + if args.tests { + verification_targets.push(VerificationTarget::Test(target.clone())); + } else { + ignored_tests.push(target.name.as_str()); + } } } _ => { diff --git a/tests/cargo-ui/target-selection/all-targets/Cargo.toml b/tests/cargo-ui/target-selection/all-targets/Cargo.toml new file mode 100644 index 000000000000..f96f7f7efb8f --- /dev/null +++ b/tests/cargo-ui/target-selection/all-targets/Cargo.toml @@ -0,0 +1,24 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "lib_pkg" +version = "0.1.0" +edition = "2021" + +[lib] +path = "../src/lib.rs" + +[[bin]] +name = "foo" +path = "../src/bin/foo.rs" + +[[bin]] +name = "bar" +path = "../src/bin/bar.rs" + +[[test]] +name = "integ" +path = "../tests/integ.rs" + +[package.metadata.kani.flags] +tests=true diff --git a/tests/cargo-ui/target-selection/all-targets/expected b/tests/cargo-ui/target-selection/all-targets/expected new file mode 100644 index 000000000000..514cfcc8f3e5 --- /dev/null +++ b/tests/cargo-ui/target-selection/all-targets/expected @@ -0,0 +1,5 @@ +Checking harness verify::bar_harness... +Checking harness verify::foo_harness... +Checking harness verify::lib_harness... +Checking harness verify::integ_harness... +Complete - 4 successfully verified harnesses, 0 failures, 4 total. diff --git a/tests/cargo-ui/target-selection/bin-target/Cargo.toml b/tests/cargo-ui/target-selection/bin-target/Cargo.toml new file mode 100644 index 000000000000..2f46a58a8adc --- /dev/null +++ b/tests/cargo-ui/target-selection/bin-target/Cargo.toml @@ -0,0 +1,20 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "bin_pkg" +version = "0.1.0" +edition = "2021" + +[lib] +path = "../src/lib.rs" + +[[bin]] +name = "foo" +path = "../src/bin/foo.rs" + +[[bin]] +name = "bar" +path = "../src/bin/bar.rs" + +[package.metadata.kani.flags] +bin="foo" diff --git a/tests/cargo-ui/target-selection/bin-target/expected b/tests/cargo-ui/target-selection/bin-target/expected new file mode 100644 index 000000000000..3922c5503ef2 --- /dev/null +++ b/tests/cargo-ui/target-selection/bin-target/expected @@ -0,0 +1,7 @@ +Checking harness verify::foo_harness... + +Status: SATISFIED\ +Description: "Cover `foo`" + +** 1 of 1 cover properties satisfied + diff --git a/tests/cargo-ui/target-selection/bins-target/Cargo.toml b/tests/cargo-ui/target-selection/bins-target/Cargo.toml new file mode 100644 index 000000000000..781cdfe8e60a --- /dev/null +++ b/tests/cargo-ui/target-selection/bins-target/Cargo.toml @@ -0,0 +1,20 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "bin_pkg" +version = "0.1.0" +edition = "2021" + +[lib] +path = "../src/lib.rs" + +[[bin]] +name = "foo" +path = "../src/bin/foo.rs" + +[[bin]] +name = "bar" +path = "../src/bin/bar.rs" + +[package.metadata.kani.flags] +bins=true diff --git a/tests/cargo-ui/target-selection/bins-target/expected b/tests/cargo-ui/target-selection/bins-target/expected new file mode 100644 index 000000000000..60300805d98b --- /dev/null +++ b/tests/cargo-ui/target-selection/bins-target/expected @@ -0,0 +1,9 @@ +Checking harness verify::bar_harness... +Status: SATISFIED\ +Description: "Cover `bar`" + +Checking harness verify::foo_harness... +Status: SATISFIED\ +Description: "Cover `foo`" + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/cargo-ui/target-selection/lib-target/Cargo.toml b/tests/cargo-ui/target-selection/lib-target/Cargo.toml new file mode 100644 index 000000000000..6e94e9aaac1d --- /dev/null +++ b/tests/cargo-ui/target-selection/lib-target/Cargo.toml @@ -0,0 +1,25 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "lib_pkg" +version = "0.1.0" +edition = "2021" + +[lib] +path = "../src/lib.rs" + +[[bin]] +name = "foo" +path = "../src/bin/foo.rs" + +[[bin]] +name = "bar" +path = "../src/bin/bar.rs" + +[[test]] +name = "integ" +path = "../tests/integ.rs" + +[package.metadata.kani.flags] +lib=true +tests=true diff --git a/tests/cargo-ui/target-selection/lib-target/expected b/tests/cargo-ui/target-selection/lib-target/expected new file mode 100644 index 000000000000..aa78bbef28bf --- /dev/null +++ b/tests/cargo-ui/target-selection/lib-target/expected @@ -0,0 +1,4 @@ +Checking harness verify::lib_harness... +Status: SATISFIED\ +Description: "Cover lib" + diff --git a/tests/cargo-ui/target-selection/non-test-targets/Cargo.toml b/tests/cargo-ui/target-selection/non-test-targets/Cargo.toml new file mode 100644 index 000000000000..8819e950edf5 --- /dev/null +++ b/tests/cargo-ui/target-selection/non-test-targets/Cargo.toml @@ -0,0 +1,22 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "lib_pkg" +version = "0.1.0" +edition = "2021" + +[lib] +path = "../src/lib.rs" + +[[bin]] +name = "foo" +path = "../src/bin/foo.rs" + +[[bin]] +name = "bar" +path = "../src/bin/bar.rs" + + +[package.metadata.kani.flags] +lib=true +bins=true diff --git a/tests/cargo-ui/target-selection/non-test-targets/expected b/tests/cargo-ui/target-selection/non-test-targets/expected new file mode 100644 index 000000000000..94b96db37dda --- /dev/null +++ b/tests/cargo-ui/target-selection/non-test-targets/expected @@ -0,0 +1,5 @@ +Checking harness verify::bar_harness... +Checking harness verify::foo_harness... +Checking harness verify::lib_harness... + +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/cargo-ui/target-selection/src/bin/bar.rs b/tests/cargo-ui/target-selection/src/bin/bar.rs new file mode 100644 index 000000000000..24ea05124fcf --- /dev/null +++ b/tests/cargo-ui/target-selection/src/bin/bar.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Define a binary with a "bar" cover used to ensure pkg targets are correctly picked by Kani. + +#[cfg(kani)] +mod verify { + #[kani::proof] + fn bar_harness() { + kani::cover!(true, "Cover `bar`"); + } +} + +fn main() { + // Do nothing +} diff --git a/tests/cargo-ui/target-selection/src/bin/foo.rs b/tests/cargo-ui/target-selection/src/bin/foo.rs new file mode 100644 index 000000000000..5bbd5a47a906 --- /dev/null +++ b/tests/cargo-ui/target-selection/src/bin/foo.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Define a binary with a "foo" cover used to ensure pkg targets are correctly picked by Kani. + +#[cfg(kani)] +mod verify { + #[kani::proof] + fn foo_harness() { + kani::cover!(true, "Cover `foo`"); + } +} + +fn main() { + // Do nothing +} diff --git a/tests/cargo-ui/target-selection/src/lib.rs b/tests/cargo-ui/target-selection/src/lib.rs new file mode 100644 index 000000000000..684b07edd3d7 --- /dev/null +++ b/tests/cargo-ui/target-selection/src/lib.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Define a library with a lib cover used to ensure pkg targets are correctly picked by Kani. + +#[cfg(kani)] +mod verify { + #[kani::proof] + fn lib_harness() { + kani::cover!(true, "Cover lib"); + } +} diff --git a/tests/cargo-ui/target-selection/tests/integ.rs b/tests/cargo-ui/target-selection/tests/integ.rs new file mode 100644 index 000000000000..8956fbaeece1 --- /dev/null +++ b/tests/cargo-ui/target-selection/tests/integ.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Define an integration test crate used to ensure pkg targets are correctly picked by Kani. + +#[cfg(kani)] +mod verify { + #[kani::proof] + fn integ_harness() { + kani::cover!(true, "Cover integration test"); + } +} From a273682922db3f9d5f4d6b3fb276574fc9c88768 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 7 Jun 2023 11:15:55 -0700 Subject: [PATCH 2/2] Address comments: - remove redundant check - Enhance comments --- kani-driver/src/args/cargo.rs | 10 ++++++---- kani-driver/src/args/mod.rs | 1 - 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/kani-driver/src/args/cargo.rs b/kani-driver/src/args/cargo.rs index ed4734346469..6a9e478667b5 100644 --- a/kani-driver/src/args/cargo.rs +++ b/kani-driver/src/args/cargo.rs @@ -94,18 +94,20 @@ impl ValidateArgs for CargoCommonArgs { } } -/// Arguments that cargo Kani supports to select build / test target. +/// Arguments that cargo Kani supports to select build / verification / test target. +/// See for more +/// details. #[derive(Debug, Default, clap::Args)] pub struct CargoTargetArgs { - /// Test only the specified binary target. + /// Check only the specified binary target. #[arg(long)] pub bin: Vec, - /// Test all binaries. + /// Check all binaries. #[arg(long)] pub bins: bool, - /// Test only the package's library unit tests. + /// Check only the package's library unit tests. #[arg(long)] pub lib: bool, } diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 657fad353c08..dbc80fedbb99 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -465,7 +465,6 @@ impl ValidateArgs for StandaloneArgs { check_no_cargo_opt(!self.verify_opts.cargo.exclude.is_empty(), "--exclude")?; check_no_cargo_opt(self.verify_opts.cargo.workspace, "--workspace")?; check_no_cargo_opt(self.verify_opts.cargo.manifest_path.is_some(), "--manifest-path")?; - check_no_cargo_opt(self.verify_opts.cargo.workspace, "--workspace")?; if let Some(input) = &self.input { if !input.is_file() { return Err(Error::raw(