diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index dbc80fedbb99..31cae95e2a61 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -169,6 +169,7 @@ pub struct VerificationArgs { pub function: Option, /// If specified, only run harnesses that match this filter. This option can be provided /// multiple times, which will run all tests matching any of the filters. + /// If used with --exact, the harness filter will only match the exact fully qualified name of a harness. #[arg( long = "harness", conflicts_with = "function", @@ -177,6 +178,10 @@ pub struct VerificationArgs { )] pub harnesses: Vec, + /// When specified, the harness filter will only match the exact fully qualified name of a harness + #[arg(long, requires("harnesses"))] + pub exact: bool, + /// Link external C files referenced by Rust code. /// This is an experimental feature and requires `-Z c-ffi` to be used #[arg(long, hide = true, num_args(1..))] diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index f1f0befc4ddd..fdafa8a5c18b 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -154,7 +154,7 @@ impl KaniSession { } // We currently omit a summary if there was just 1 harness - if !self.args.common_args.quiet && !self.args.visualize && total != 1 { + if !self.args.common_args.quiet && !self.args.visualize { if failing > 0 { println!("Summary:"); } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 613129d8188c..871be621c6b0 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::Result; +use anyhow::{bail, Result}; use std::path::{Path, PathBuf}; use tracing::{debug, trace}; @@ -121,11 +121,35 @@ impl KaniSession { BTreeSet::from_iter(self.args.harnesses.iter()) }; + let total_harnesses = harnesses.len(); + let all_targets = &harnesses; + if harnesses.is_empty() { Ok(Vec::from(all_harnesses)) } else { - let harnesses = find_proof_harnesses(harnesses, all_harnesses); - Ok(harnesses) + let harnesses_found: Vec<&HarnessMetadata> = + find_proof_harnesses(&harnesses, all_harnesses, self.args.exact); + + // If even one harness was not found with --exact, return an error to user + if self.args.exact && harnesses_found.len() < total_harnesses { + let harness_found_names: BTreeSet<&String> = + harnesses_found.iter().map(|&h| &h.pretty_name).collect(); + + // Check which harnesses are missing from the difference of targets and harnesses_found + let harnesses_missing: Vec<&String> = + all_targets.difference(&harness_found_names).cloned().collect(); + let joined_string = harnesses_missing + .iter() + .map(|&s| (*s).clone()) + .collect::>() + .join("`, `"); + + bail!( + "Failed to match the following harness(es):\n{joined_string}\nPlease specify the fully-qualified name of a harness.", + ); + } + + Ok(harnesses_found) } } } @@ -167,20 +191,31 @@ pub fn mock_proof_harness( /// At the present time, we use `no_mangle` so collisions shouldn't happen, /// but this function is written to be robust against that changing in the future. fn find_proof_harnesses<'a>( - targets: BTreeSet<&String>, + targets: &BTreeSet<&String>, all_harnesses: &[&'a HarnessMetadata], + exact_filter: bool, ) -> Vec<&'a HarnessMetadata> { debug!(?targets, "find_proof_harness"); let mut result = vec![]; for md in all_harnesses.iter() { - // Either an exact match, or a substring match. We check the exact first since it's cheaper. - if targets.contains(&md.pretty_name) - || targets.contains(&md.get_harness_name_unqualified().to_string()) - || targets.iter().any(|target| md.pretty_name.contains(*target)) - { - result.push(*md); + if exact_filter { + // Check for exact match only + if targets.contains(&md.pretty_name) { + // if exact match found, stop searching + result.push(*md); + } else { + trace!(skip = md.pretty_name, "find_proof_harnesses"); + } } else { - trace!(skip = md.pretty_name, "find_proof_harnesses"); + // Either an exact match, or a substring match. We check the exact first since it's cheaper. + if targets.contains(&md.pretty_name) + || targets.contains(&md.get_harness_name_unqualified().to_string()) + || targets.iter().any(|target| md.pretty_name.contains(*target)) + { + result.push(*md); + } else { + trace!(skip = md.pretty_name, "find_proof_harnesses"); + } } } result @@ -191,31 +226,88 @@ mod tests { use super::*; #[test] - fn check_find_proof_harness() { + fn check_find_proof_harness_without_exact() { let harnesses = vec![ mock_proof_harness("check_one", None, None, None), mock_proof_harness("module::check_two", None, None, None), mock_proof_harness("module::not_check_three", None, None, None), ]; let ref_harnesses = harnesses.iter().collect::>(); + + // Check with harness filtering assert_eq!( - find_proof_harnesses(BTreeSet::from([&"check_three".to_string()]), &ref_harnesses) - .len(), + find_proof_harnesses( + &BTreeSet::from([&"check_three".to_string()]), + &ref_harnesses, + false + ) + .len(), 1 ); assert!( - find_proof_harnesses(BTreeSet::from([&"check_two".to_string()]), &ref_harnesses) - .first() - .unwrap() - .mangled_name + find_proof_harnesses( + &BTreeSet::from([&"check_two".to_string()]), + &ref_harnesses, + false + ) + .first() + .unwrap() + .mangled_name == "module::check_two" ); assert!( - find_proof_harnesses(BTreeSet::from([&"check_one".to_string()]), &ref_harnesses) + find_proof_harnesses( + &BTreeSet::from([&"check_one".to_string()]), + &ref_harnesses, + false + ) + .first() + .unwrap() + .mangled_name + == "check_one" + ); + } + + #[test] + fn check_find_proof_harness_with_exact() { + // Check with exact match + + let harnesses = vec![ + mock_proof_harness("check_one", None, None, None), + mock_proof_harness("module::check_two", None, None, None), + mock_proof_harness("module::not_check_three", None, None, None), + ]; + let ref_harnesses = harnesses.iter().collect::>(); + + assert!( + find_proof_harnesses( + &BTreeSet::from([&"check_three".to_string()]), + &ref_harnesses, + true + ) + .is_empty() + ); + assert!( + find_proof_harnesses(&BTreeSet::from([&"check_two".to_string()]), &ref_harnesses, true) + .is_empty() + ); + assert_eq!( + find_proof_harnesses(&BTreeSet::from([&"check_one".to_string()]), &ref_harnesses, true) .first() .unwrap() - .mangled_name - == "check_one" + .mangled_name, + "check_one" + ); + assert_eq!( + find_proof_harnesses( + &BTreeSet::from([&"module::not_check_three".to_string()]), + &ref_harnesses, + true + ) + .first() + .unwrap() + .mangled_name, + "module::not_check_three" ); } } diff --git a/tests/ui/check_summary_for_single_harness/expected b/tests/ui/check_summary_for_single_harness/expected new file mode 100644 index 000000000000..17aaa37eee0c --- /dev/null +++ b/tests/ui/check_summary_for_single_harness/expected @@ -0,0 +1,2 @@ +Checking harness check_foo... +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/ui/check_summary_for_single_harness/single_harness.rs b/tests/ui/check_summary_for_single_harness/single_harness.rs new file mode 100644 index 000000000000..3d032881d446 --- /dev/null +++ b/tests/ui/check_summary_for_single_harness/single_harness.rs @@ -0,0 +1,9 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness check_foo --exact +//! Check for the summary line at the end of the verification output + +#[kani::proof] +fn check_foo() { + assert!(1 == 1); +} diff --git a/tests/ui/exact-harness/check-qualified-name/expected b/tests/ui/exact-harness/check-qualified-name/expected new file mode 100644 index 000000000000..59ff06ae136d --- /dev/null +++ b/tests/ui/exact-harness/check-qualified-name/expected @@ -0,0 +1,3 @@ +Checking harness first::check_foo... +VERIFICATION:- SUCCESSFUL +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/ui/exact-harness/check-qualified-name/select_harness_with_module.rs b/tests/ui/exact-harness/check-qualified-name/select_harness_with_module.rs new file mode 100644 index 000000000000..9269b93afa37 --- /dev/null +++ b/tests/ui/exact-harness/check-qualified-name/select_harness_with_module.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness first::check_foo --exact +//! Ensure that only the specified harness is run + +mod first { + #[kani::proof] + fn check_foo() { + assert!(1 == 1); + } + + /// A harness that will fail verification if it is run. + #[kani::proof] + fn check_blah() { + assert!(1 == 2); + } + + /// A harness that will fail verification if it is run. + #[kani::proof] + fn ignore_third_harness() { + assert!(3 == 2); + } +} diff --git a/tests/ui/exact-harness/check_some/expected b/tests/ui/exact-harness/check_some/expected new file mode 100644 index 000000000000..875c01a46612 --- /dev/null +++ b/tests/ui/exact-harness/check_some/expected @@ -0,0 +1,3 @@ +Checking harness check_second_harness... +Checking harness check_first_harness... +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/ui/exact-harness/check_some/select_harnesses.rs b/tests/ui/exact-harness/check_some/select_harnesses.rs new file mode 100644 index 000000000000..0ac125fde552 --- /dev/null +++ b/tests/ui/exact-harness/check_some/select_harnesses.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness check_first_harness --harness check_second_harness --exact +//! Ensure that we can select multiple harnesses at a time. +#[kani::proof] +fn check_first_harness() { + assert!(1 == 1); +} + +#[kani::proof] +fn check_second_harness() { + assert!(2 == 2); +} + +/// A harness that will fail verification if it is run. +#[kani::proof] +fn ignore_third_harness() { + assert!(3 == 2); +} diff --git a/tests/ui/exact-harness/check_substring_not_matching/expected b/tests/ui/exact-harness/check_substring_not_matching/expected new file mode 100644 index 000000000000..6db88e2b537f --- /dev/null +++ b/tests/ui/exact-harness/check_substring_not_matching/expected @@ -0,0 +1,4 @@ +Checking harness first::harness... +VERIFICATION:- SUCCESSFUL +Complete - 1 successfully verified harnesses, 0 failures, 1 total. + diff --git a/tests/ui/exact-harness/check_substring_not_matching/select_harness_with_module.rs b/tests/ui/exact-harness/check_substring_not_matching/select_harness_with_module.rs new file mode 100644 index 000000000000..f46deb719f74 --- /dev/null +++ b/tests/ui/exact-harness/check_substring_not_matching/select_harness_with_module.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness first::harness --exact +//! Ensure that only the harness specified with --exact is picked up + +mod first { + #[kani::proof] + fn harness() { + assert!(1 == 1); + } + + /// A harness that will fail verification if it is picked up. + #[kani::proof] + fn harness_1() { + assert!(1 == 2); + } + + /// A harness that will fail verification if it is picked up. + #[kani::proof] + fn harness_2() { + assert!(3 == 2); + } +} diff --git a/tests/ui/exact-harness/fail_on_missing/expected b/tests/ui/exact-harness/fail_on_missing/expected new file mode 100644 index 000000000000..45cc61032413 --- /dev/null +++ b/tests/ui/exact-harness/fail_on_missing/expected @@ -0,0 +1,3 @@ +error: Failed to match the following harness(es): +check_blah`, `check_foo +Please specify the fully-qualified name of a harness. diff --git a/tests/ui/exact-harness/fail_on_missing/subset.rs b/tests/ui/exact-harness/fail_on_missing/subset.rs new file mode 100644 index 000000000000..6fe025dd44a3 --- /dev/null +++ b/tests/ui/exact-harness/fail_on_missing/subset.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness existing --harness check_blah --harness check_foo --exact +//! Check that we error out with non-matching filters when --exact is used + +mod first { + #[kani::proof] + fn check_foo() { + assert!(1 == 2); + } + + #[kani::proof] + fn check_blah() { + assert!(2 == 2); + } + + /// A harness that will fail verification if it is run. + #[kani::proof] + fn ignore_third_harness() { + assert!(3 == 2); + } +} + +// This harness will be picked up +#[kani::proof] +fn existing() { + assert!(1 == 1); +} + +#[kani::proof] +fn existing_harness() { + assert!(1 == 2); +} + +/// A harness that will fail verification if it is run. +#[kani::proof] +fn ignored_harness() { + assert!(3 == 2); +} diff --git a/tests/ui/exact-harness/incomplete-harness-name/expected b/tests/ui/exact-harness/incomplete-harness-name/expected new file mode 100644 index 000000000000..93ef322aeebb --- /dev/null +++ b/tests/ui/exact-harness/incomplete-harness-name/expected @@ -0,0 +1,3 @@ +error: Failed to match the following harness(es): +ignore_third_harness +Please specify the fully-qualified name of a harness. diff --git a/tests/ui/exact-harness/incomplete-harness-name/incomplete_harness.rs b/tests/ui/exact-harness/incomplete-harness-name/incomplete_harness.rs new file mode 100644 index 000000000000..0a1d6b44ed7f --- /dev/null +++ b/tests/ui/exact-harness/incomplete-harness-name/incomplete_harness.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness ignore_third_harness --exact +//! Check that we error out with non-matching filters when --exact is used + +mod first { + #[kani::proof] + fn check_foo() { + assert!(1 == 1); + } + + #[kani::proof] + fn check_blah() { + assert!(2 == 2); + } + + /// A harness that will fail verification if it is run. + #[kani::proof] + fn ignore_third_harness() { + assert!(3 == 2); + } +} diff --git a/tests/ui/exact-harness/multiple_matches/expected b/tests/ui/exact-harness/multiple_matches/expected new file mode 100644 index 000000000000..8c2420d08c77 --- /dev/null +++ b/tests/ui/exact-harness/multiple_matches/expected @@ -0,0 +1,3 @@ +Checking harness second::verify_foo... +Checking harness first::check_blah... +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/ui/exact-harness/multiple_matches/select_multiple_harnesses.rs b/tests/ui/exact-harness/multiple_matches/select_multiple_harnesses.rs new file mode 100644 index 000000000000..68aa59fbfa69 --- /dev/null +++ b/tests/ui/exact-harness/multiple_matches/select_multiple_harnesses.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness first::check_blah --exact --harness second::verify_foo +//! Ensure that only the specified harnesses are run + +mod first { + #[kani::proof] + fn check_foo() { + assert!(1 == 1); + } + + #[kani::proof] + fn check_blah() { + assert!(2 == 2); + } + + /// A harness that will fail verification if it is run. + #[kani::proof] + fn ignore_third_harness() { + assert!(3 == 2); + } +} + +mod second { + #[kani::proof] + fn verify_foo() { + assert!(1 == 1); + } + + #[kani::proof] + fn verify_blah() { + assert!(2 == 2); + } + + #[kani::proof] + fn verify_harness() { + assert!(3 == 3); + } +}