model-checking · jaisnan · Jun 19, 2023 · Jun 14, 2023 · Jun 14, 2023 · Jun 15, 2023
@@ -169,6 +169,7 @@ pub struct VerificationArgs {
     pub function: Option<String>,
     /// 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<String>,
 
+    /// 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..))]

@@ -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:");
             }

@@ -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::<Vec<String>>()
+                    .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::<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)
-                .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::<Vec<_>>();
+
+        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"
         );
     }
 }
@@ -0,0 +1,2 @@
+Checking harness check_foo...
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
@@ -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);
+}
@@ -0,0 +1,3 @@
+Checking harness first::check_foo...
+VERIFICATION:- SUCCESSFUL
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
@@ -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);
+    }
+}
@@ -0,0 +1,3 @@
+Checking harness check_second_harness...
+Checking harness check_first_harness...
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
@@ -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);
+}
@@ -0,0 +1,4 @@
+Checking harness first::harness...
+VERIFICATION:- SUCCESSFUL
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
+
@@ -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);
+    }
+}
@@ -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.
@@ -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);
+}
@@ -0,0 +1,3 @@
+error: Failed to match the following harness(es):
+ignore_third_harness
+Please specify the fully-qualified name of a harness.
@@ -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);
+    }
+}
@@ -0,0 +1,3 @@
+Checking harness second::verify_foo...
+Checking harness first::check_blah...
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		Checking harness check_foo...
		Complete - 1 successfully verified harnesses, 0 failures, 1 total.