Autoharness: change pattern options to accept regexes

Cargo.lock

@@ -985,6 +985,7 @@ dependencies = [
  "lazy_static",
  "num",
  "quote",
+ "regex",
  "serde",
  "serde_json",
  "strum",

docs/src/reference/experimental/autoharness.md

@@ -43,45 +43,37 @@ autoharness feature means that you are also opting into the function contracts a
 Kani generates and runs these harnesses internally—the user only sees the verification results.
 
 ### Options
-The `autoharness` subcommand has options `--include-pattern` and `--exclude-pattern` to include and exclude particular functions.
-These flags look for partial matches against the fully qualified name of a function.
-
-For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run:
-```
-cargo run autoharness -Z autoharness --include-pattern my_module::foo --include-pattern my_module::bar
-```
-To exclude `my_module` entirely, run:
-```
-cargo run autoharness -Z autoharness --exclude-pattern my_module
-```
+The `autoharness` subcommand has options `--include-pattern [REGEX]` and `--exclude-pattern [REGEX]` to include and exclude particular functions using regular expressions.
+When matching, Kani prefixes the function's path with the crate name. For example, a function `foo` in the `my_crate` crate will be matched as `my_crate::foo`.
 
 The selection algorithm is as follows:
 - If only `--include-pattern`s are provided, include a function if it matches any of the provided patterns.
 - If only `--exclude-pattern`s are provided, include a function if it does not match any of the provided patterns.
 - If both are provided, include a function if it matches an include pattern *and* does not match any of the exclude patterns. Note that this implies that the exclude pattern takes precedence, i.e., if a function matches both an include pattern and an exclude pattern, it will be excluded.
 
-Here are some more examples:
+Here are some examples:
 
-```
-# Include functions whose paths contain the substring foo or baz, but not foo::bar
-kani autoharness -Z autoharness --include-pattern foo --include-pattern baz --exclude-pattern foo::bar
+```bash
+# Include functions containing foo but not bar
+kani autoharness -Z autoharness --include-pattern 'foo' --exclude-pattern 'bar'
+
+# Include my_crate::foo exactly
+kani autoharness -Z autoharness --include-pattern '^my_crate::foo$'
 
-# Include functions whose paths contain the substring foo, but not bar.
-kani autoharness -Z autoharness --include-pattern foo --exclude-pattern bar
+# Include functions in the foo module, but not in foo::bar
+kani autoharness -Z autoharness --include-pattern 'foo::.*' --exclude-pattern 'foo::bar::.*'
 
-# Include functions whose paths contain the substring foo::bar, but not bar.
-# This ends up including nothing, since all foo::bar matches will also contain bar.
-# Kani will emit a warning that these flags conflict.
-kani autoharness -Z autoharness --include-pattern foo::bar --exclude-pattern bar
+# Include functions starting with test_, but not if they're in a private module
+kani autoharness -Z autoharness --include-pattern 'test_.*' --exclude-pattern '.*::private::.*'
 
-# Include functions whose paths contain the substring foo, but not foo.
-# This ends up including nothing, and Kani will emit a warning that these flags conflict.
-kani autoharness -Z autoharness --include-pattern foo --exclude--pattern foo
+# This ends up including nothing since all foo::bar matches will also contain bar.
+# Kani will emit a warning that these options conflict.
+kani autoharness -Z autoharness --include-pattern 'foo::bar' --exclude-pattern 'bar'
 ```
 
-Currently, the only supported "patterns" are substrings of the fully qualified path of the function.
-However, if more sophisticated patterns (e.g., regular expressions) would be useful for you,
-please let us know in a comment on [this GitHub issue](https://github.com/model-checking/kani/issues/3832). 
+Note that because Kani prefixes function paths with the crate name, some patterns might match more than you expect.
+For example, given a function `foo_top_level` inside crate `my_crate`, the regex `.*::foo_.*` will match `foo_top_level`, since Kani interprets it as `my_crate::foo_top_level`.
+To match only `foo_` functions inside modules, use a more specific pattern, e.g. `.*::[^:]+::foo_.*`.
 
 ## Example
 Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:

kani-compiler/Cargo.toml

@@ -17,6 +17,7 @@ kani_metadata = { path = "../kani_metadata" }
 lazy_static = "1.5.0"
 num = { version = "0.4.0", optional = true }
 quote = "1.0.36"
+regex = "1.11.1"
 serde = { version = "1", optional = true }
 serde_json = "1"
 strum = "0.27.1"

kani-compiler/src/kani_middle/codegen_units.rs

@@ -21,6 +21,7 @@ use kani_metadata::{
     ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind,
     HarnessMetadata, KaniMetadata,
 };
+use regex::RegexSet;
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
@@ -356,6 +357,29 @@ fn get_all_automatic_harnesses(
         .collect::<HashMap<_, _>>()
 }
 
+fn make_regex_set(patterns: Vec<String>) -> Option<RegexSet> {
+    if patterns.is_empty() {
+        None
+    } else {
+        Some(RegexSet::new(patterns).unwrap_or_else(|e| {
+            panic!("Invalid regexes should have been caught during argument validation: {e}")
+        }))
+    }
+}
+
+/// A function is filtered out if 1) none of the include patterns match it or 2) one of the exclude patterns matches it.
+fn autoharness_filtered_out(
+    name: &str,
+    included_set: &Option<RegexSet>,
+    excluded_set: &Option<RegexSet>,
+) -> bool {
+    // A function is included if `--include-pattern` is not provided or if at least one of its regexes matches `name`
+    let included = included_set.as_ref().is_none_or(|set| set.is_match(name));
+    // A function is excluded if `--exclude-pattern` is provided and at least one of its regexes matches `name`
+    let excluded = excluded_set.as_ref().is_some_and(|set| set.is_match(name));
+    !included || excluded
+}
+
 /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses,
 /// and `skipped` is a map of function names to the reason why we skipped them.
 fn automatic_harness_partition(
@@ -364,12 +388,15 @@ fn automatic_harness_partition(
     crate_name: &str,
     kani_any_def: FnDef,
 ) -> (Vec<Instance>, BTreeMap<String, AutoHarnessSkipReason>) {
-    // If `filter_list` contains `name`, either as an exact match or a substring.
-    let filter_contains = |name: &str, filter_list: &[String]| -> bool {
-        filter_list.iter().any(|filter_name| name.contains(filter_name))
-    };
+    let crate_fns =
+        stable_mir::all_local_items().into_iter().filter(|item| item.ty().kind().is_fn());
+
+    let included_set = make_regex_set(args.autoharness_included_patterns.clone());
+    let excluded_set = make_regex_set(args.autoharness_excluded_patterns.clone());
 
     // If `func` is not eligible for an automatic harness, return the reason why; if it is eligible, return None.
+    // Note that we only return one reason for ineligiblity, when there could be multiple;
+    // we can revisit this implementation choice in the future if users request more verbose output.
     let skip_reason = |fn_item: CrateItem| -> Option<AutoHarnessSkipReason> {
         if KaniAttributes::for_def_id(tcx, fn_item.def_id()).is_kani_instrumentation() {
             return Some(AutoHarnessSkipReason::KaniImpl);
@@ -397,34 +424,8 @@ fn automatic_harness_partition(
             return Some(AutoHarnessSkipReason::KaniImpl);
         }
 
-        match (
-            args.autoharness_included_patterns.is_empty(),
-            args.autoharness_excluded_patterns.is_empty(),
-        ) {
-            // If no filters were specified, then continue.
-            (true, true) => {}
-            // If only --exclude-pattern was provided, filter out the function if excluded_patterns contains its name.
-            (true, false) => {
-                if filter_contains(&name, &args.autoharness_excluded_patterns) {
-                    return Some(AutoHarnessSkipReason::UserFilter);
-                }
-            }
-            // If only --include-pattern was provided, filter out the function if included_patterns does not contain its name.
-            (false, true) => {
-                if !filter_contains(&name, &args.autoharness_included_patterns) {
-                    return Some(AutoHarnessSkipReason::UserFilter);
-                }
-            }
-            // If both are specified, filter out the function if included_patterns does not contain its name.
-            // Then, filter out any functions that excluded_patterns does match.
-            // This order is important, since it preserves the semantics described in kani_driver::autoharness_args where exclude takes precedence over include.
-            (false, false) => {
-                if !filter_contains(&name, &args.autoharness_included_patterns)
-                    || filter_contains(&name, &args.autoharness_excluded_patterns)
-                {
-                    return Some(AutoHarnessSkipReason::UserFilter);
-                }
-            }
+        if autoharness_filtered_out(&name, &included_set, &excluded_set) {
+            return Some(AutoHarnessSkipReason::UserFilter);
         }
 
         // Each argument of `instance` must implement Arbitrary.
@@ -472,14 +473,6 @@ fn automatic_harness_partition(
     let mut chosen = vec![];
     let mut skipped = BTreeMap::new();
 
-    // FIXME: ideally, this filter would be matches!(item.kind(), ItemKind::Fn), since that would allow us to generate harnesses for top-level closures,
-    // c.f. https://github.com/model-checking/kani/issues/3832#issuecomment-2701671798.
-    // Note that filtering closures out here is a UX choice: we could instead call skip_reason() on closures,
-    // but the limitations in the linked issue would cause the user to be flooded with reports of "skipping" Kani instrumentation functions.
-    // Instead, we just pretend closures don't exist in our reporting of what we did and did not verify, which has the downside of also ignoring the user's top-level closures, but those are rare.
-    let crate_fns =
-        stable_mir::all_local_items().into_iter().filter(|item| item.ty().kind().is_fn());
-
     for func in crate_fns {
         if let Some(reason) = skip_reason(func) {
             skipped.insert(func.name(), reason);
@@ -490,3 +483,179 @@ fn automatic_harness_partition(
 
     (chosen, skipped)
 }
+
+#[cfg(test)]
+mod autoharness_filter_tests {
+    use super::*;
+
+    #[test]
+    fn both_none() {
+        let included = None;
+        let excluded = None;
+        assert!(!autoharness_filtered_out("test_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn only_included() {
+        let included = make_regex_set(vec!["test.*".to_string()]);
+        let excluded = None;
+
+        assert!(!autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("other_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn only_excluded() {
+        let included = None;
+        let excluded = make_regex_set(vec!["test.*".to_string()]);
+
+        assert!(autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("other_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn both_matching() {
+        let included = make_regex_set(vec![".*_fn".to_string()]);
+        let excluded = make_regex_set(vec!["test.*".to_string()]);
+
+        assert!(autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("other_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn multiple_include_patterns() {
+        let included = make_regex_set(vec!["test.*".to_string(), "other.*".to_string()]);
+        let excluded = None;
+
+        assert!(!autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("other_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("different_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn multiple_exclude_patterns() {
+        let included = None;
+        let excluded = make_regex_set(vec!["test.*".to_string(), "other.*".to_string()]);
+
+        assert!(autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("other_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("different_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn exclude_precedence_identical_patterns() {
+        let pattern = "test.*".to_string();
+        let included = make_regex_set(vec![pattern.clone()]);
+        let excluded = make_regex_set(vec![pattern]);
+
+        assert!(autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("other_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn exclude_precedence_overlapping_patterns() {
+        let included = make_regex_set(vec![".*_fn".to_string()]);
+        let excluded = make_regex_set(vec!["test_.*".to_string(), "other_.*".to_string()]);
+
+        assert!(autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("other_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("different_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn exact_match() {
+        let included = make_regex_set(vec!["^test_fn$".to_string()]);
+        let excluded = None;
+
+        assert!(!autoharness_filtered_out("test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("test_fn_extra", &included, &excluded));
+    }
+
+    #[test]
+    fn include_specific_module() {
+        let included = make_regex_set(vec!["module1::.*".to_string()]);
+        let excluded = None;
+
+        assert!(!autoharness_filtered_out("module1::test_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("crate::module1::test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("module2::test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("crate::module2::test_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn exclude_specific_module() {
+        let included = None;
+        let excluded = make_regex_set(vec![".*::internal::.*".to_string()]);
+
+        assert!(autoharness_filtered_out("crate::internal::helper_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("my_crate::internal::test_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("crate::public::test_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn test_exact_match_with_crate() {
+        let included = make_regex_set(vec!["^lib::foo_function$".to_string()]);
+        let excluded = None;
+
+        assert!(!autoharness_filtered_out("lib::foo_function", &included, &excluded));
+        assert!(autoharness_filtered_out("lib::foo_function_extra", &included, &excluded));
+        assert!(autoharness_filtered_out("lib::other::foo_function", &included, &excluded));
+        assert!(autoharness_filtered_out("other::foo_function", &included, &excluded));
+        assert!(autoharness_filtered_out("foo_function", &included, &excluded));
+    }
+
+    #[test]
+    fn complex_path_patterns() {
+        let included = make_regex_set(vec![
+            "crate::module1::.*".to_string(),
+            "other_crate::tests::.*".to_string(),
+        ]);
+        let excluded =
+            make_regex_set(vec![".*::internal::.*".to_string(), ".*::private::.*".to_string()]);
+
+        assert!(!autoharness_filtered_out("crate::module1::test_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("other_crate::tests::test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out(
+            "crate::module1::internal::test_fn",
+            &included,
+            &excluded
+        ));
+        assert!(autoharness_filtered_out(
+            "other_crate::tests::private::test_fn",
+            &included,
+            &excluded
+        ));
+        assert!(autoharness_filtered_out("crate::module2::test_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn crate_specific_filtering() {
+        let included = make_regex_set(vec!["my_crate::.*".to_string()]);
+        let excluded = make_regex_set(vec!["other_crate::.*".to_string()]);
+
+        assert!(!autoharness_filtered_out("my_crate::test_fn", &included, &excluded));
+        assert!(!autoharness_filtered_out("my_crate::module::test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("other_crate::test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("third_crate::test_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn root_crate_paths() {
+        let included = make_regex_set(vec!["^crate::.*".to_string()]);
+        let excluded = None;
+
+        assert!(!autoharness_filtered_out("crate::test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("other_crate::test_fn", &included, &excluded));
+        assert!(autoharness_filtered_out("test_fn", &included, &excluded));
+    }
+
+    #[test]
+    fn impl_paths_with_spaces() {
+        let included = make_regex_set(vec!["num::<impl.i8>::wrapping_.*".to_string()]);
+        let excluded = None;
+
+        assert!(!autoharness_filtered_out("num::<impl i8>::wrapping_sh", &included, &excluded));
+        assert!(!autoharness_filtered_out("num::<impl i8>::wrapping_add", &included, &excluded));
+        assert!(autoharness_filtered_out("num::<impl i16>::wrapping_sh", &included, &excluded));
+    }
+}

kani-driver/Cargo.toml

@@ -22,7 +22,7 @@ serde = { version = "1", features = ["derive"] }
 serde_json = { version = "1", features = ["preserve_order"] }
 clap = { version = "4.4.11", features = ["derive"] }
 toml = "0.8"
-regex = "1.6"
+regex = "1.11.1"
 rustc-demangle = "0.1.21"
 pathdiff = "0.2.1"
 rayon = "1.5.3"