Add --exact flag

kani-driver/src/args/mod.rs

@@ -177,6 +177,10 @@ pub struct VerificationArgs {
     )]
     pub harnesses: Vec<String>,
 
+    /// If specified, with the fully qualified name of the harness provided, runs that specific harness and nothing more
+    #[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..))]

kani-driver/src/metadata.rs

@@ -124,7 +124,8 @@ impl KaniSession {
         if harnesses.is_empty() {
             Ok(Vec::from(all_harnesses))
         } else {
-            let harnesses = find_proof_harnesses(harnesses, all_harnesses);
+            let harnesses: Vec<&HarnessMetadata> =
+                find_proof_harnesses(harnesses, all_harnesses, self.args.exact);
             Ok(harnesses)
         }
     }
@@ -169,18 +170,29 @@ pub fn mock_proof_harness(
 fn find_proof_harnesses<'a>(
     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);
+        // Check for exact match only
+        if exact_filter {
+            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 +203,83 @@ 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::<Vec<_>>();
+
+        // 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)
+            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"
         );
+
+        // Check with exact match
+        assert_eq!(
+            find_proof_harnesses(
+                BTreeSet::from([&"check_three".to_string()]),
+                &ref_harnesses,
+                true
+            )
+            .len(),
+            0
+        );
+        assert_eq!(
+            find_proof_harnesses(BTreeSet::from([&"check_two".to_string()]), &ref_harnesses, true)
+                .first()
+                .is_none(),
+            true
+        );
+        assert_eq!(
+            find_proof_harnesses(BTreeSet::from([&"check_one".to_string()]), &ref_harnesses, true)
+                .first()
+                .unwrap()
+                .mangled_name,
+            "check_one"
+        );
+        assert_ne!(
+            find_proof_harnesses(
+                BTreeSet::from([&"module::not_check_three".to_string()]),
+                &ref_harnesses,
+                true
+            )
+            .first()
+            .unwrap()
+            .mangled_name,
+            "not_check_three"
+        );
+        assert_eq!(
+            find_proof_harnesses(
+                BTreeSet::from([&"module::not_check_three".to_string()]),
+                &ref_harnesses,
+                true
+            )
+            .first()
+            .unwrap()
+            .mangled_name,
+            "module::not_check_three"
+        );
     }
 }

tests/ui/exact-harness/check-qualified-name/expected

@@ -0,0 +1,2 @@
+Checking harness first::check_foo...
+VERIFICATION:- SUCCESSFUL

tests/ui/exact-harness/check-qualified-name/select_harness_with_module.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --harness first::check_foo --exact
+//! Ensure that the set of harnesses run is the union of all arguments.
+
+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);
+    }
+}

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.

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);
+}

tests/ui/exact-harness/incomplete-harness-name/expected

@@ -0,0 +1 @@
+error: no harnesses matched the harness filter: `check_blah`

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 check_blah --exact
+//! Check that we just ignore non-matching filters
+
+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);
+    }
+}

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.

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 the set of harnesses run is the union of all arguments.
+
+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);
+    }
+}

tests/ui/exact-harness/some_matching_harnesses/expected

@@ -0,0 +1,2 @@
+Checking harness existing...
+VERIFICATION:- SUCCESSFUL

tests/ui/exact-harness/some_matching_harnesses/subset.rs

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --harness existing --harness check_blah --exact
+//! Check that we just ignore non-matching filters
+
+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);
+    }
+}
+
+// This harness will be picked up
+#[kani::proof]
+fn existing() {
+    assert!(1 == 1);
+}
+
+#[kani::proof]
+fn existing_harness() {
+    assert!(2 == 2);
+}
+
+/// A harness that will fail verification if it is run.
+#[kani::proof]
+fn ignored_harness() {
+    assert!(3 == 2);
+}