Add target selection for cargo kani (#2507)

Add the following options to restrict `cargo kani` verification target: - `--bin <BIN_TARGET>` - `--bins` - `--lib`. I found this very helpful for example to skip integration tests when running `cargo kani` with `--tests`.
model-checking · Jun 7, 2023 · 7378419 · 7378419
1 parent f990744
commit 7378419
Show file tree

Hide file tree

Showing 17 changed files with 324 additions and 23 deletions.
diff --git a/kani-driver/src/args/cargo.rs b/kani-driver/src/args/cargo.rs
@@ -94,30 +94,32 @@ impl ValidateArgs for CargoCommonArgs {
     }
 }
 
-/// Arguments that Kani pass down into Cargo test essentially uninterpreted.
+/// Arguments that cargo Kani supports to select build / verification / test target.
+/// See <https://doc.rust-lang.org/cargo/commands/cargo-test.html#target-selection> for more
+/// details.
 #[derive(Debug, Default, clap::Args)]
-pub struct CargoTestArgs {
-    /// Test only the specified binary target.
+pub struct CargoTargetArgs {
+    /// Check only the specified binary target.
     #[arg(long)]
     pub bin: Vec<String>,
 
-    /// 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,
-
-    /// 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<OsString> {
-        let mut cargo_args = self.common.to_cargo_args();
+        let mut cargo_args = self
+            .bin
+            .iter()
+            .map(|binary| format!("--bin={binary}").into())
+            .collect::<Vec<OsString>>();
 
         if self.bins {
             cargo_args.push("--bins".into());
@@ -127,14 +129,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<OsString> {
+        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
@@ -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};
@@ -298,6 +299,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,
 }
@@ -429,9 +434,37 @@ 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")?;
         if let Some(input) = &self.input {
             if !input.is_file() {
                 return Err(Error::raw(
@@ -882,4 +915,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<Item = &'a str>,
+        {
+            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
@@ -418,23 +418,31 @@ fn package_targets(args: &VerificationArgs, package: &Package) -> Vec<Verificati
         for kind in &target.kind {
             match kind.as_str() {
                 CRATE_TYPE_BIN => {
-                    // 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
+}