Autoharness: Update Filtering Options

docs/src/reference/experimental/autoharness.md

@@ -43,18 +43,46 @@ 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-function` and `--exclude-function` to include and exclude particular functions.
+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-function foo --include-function bar
+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-function my_module
+cargo run autoharness -Z autoharness --exclude-pattern my_module
 ```
 
+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:
+
+```
+# 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
+
+# Include functions whose paths contain the substring foo, but not bar.
+kani autoharness -Z autoharness --include-pattern foo --exclude-pattern 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 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
+```
+
+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). 
+
 ## Example
 Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:
 ```rust

kani-compiler/src/args.rs

@@ -91,16 +91,14 @@ pub struct Arguments {
     /// Print the final LLBC file to stdout.
     #[clap(long)]
     pub print_llbc: bool,
-    /// If we are running the autoharness subcommand, the functions to include
-    #[arg(
-        long = "autoharness-include-function",
-        num_args(1),
-        conflicts_with = "autoharness_excluded_functions"
-    )]
-    pub autoharness_included_functions: Vec<String>,
-    /// If we are running the autoharness subcommand, the functions to exclude
-    #[arg(long = "autoharness-exclude-function", num_args(1))]
-    pub autoharness_excluded_functions: Vec<String>,
+    /// If we are running the autoharness subcommand, the paths to include.
+    /// See kani_driver::autoharness_args for documentation.
+    #[arg(long = "autoharness-include-pattern", num_args(1))]
+    pub autoharness_included_patterns: Vec<String>,
+    /// If we are running the autoharness subcommand, the paths to exclude.
+    /// See kani_driver::autoharness_args for documentation.
+    #[arg(long = "autoharness-exclude-pattern", num_args(1))]
+    pub autoharness_excluded_patterns: Vec<String>,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/kani_middle/codegen_units.rs

@@ -90,6 +90,7 @@ impl CodegenUnits {
                 let (chosen, skipped) = automatic_harness_partition(
                     tcx,
                     args,
+                    &crate_info.name,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
                 );
                 AUTOHARNESS_MD
@@ -360,6 +361,7 @@ fn get_all_automatic_harnesses(
 fn automatic_harness_partition(
     tcx: TyCtxt,
     args: &Arguments,
+    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.
@@ -384,7 +386,8 @@ fn automatic_harness_partition(
             return Some(AutoHarnessSkipReason::NoBody);
         }
 
-        let name = instance.name();
+        // Preprend the crate name so that users can filter out entire crates using the existing function filter flags.
+        let name = format!("{crate_name}::{}", instance.name());
         let body = instance.body().unwrap();
 
         if is_proof_harness(tcx, instance)
@@ -394,12 +397,34 @@ fn automatic_harness_partition(
             return Some(AutoHarnessSkipReason::KaniImpl);
         }
 
-        if (!args.autoharness_included_functions.is_empty()
-            && !filter_contains(&name, &args.autoharness_included_functions))
-            || (!args.autoharness_excluded_functions.is_empty()
-                && filter_contains(&name, &args.autoharness_excluded_functions))
-        {
-            return Some(AutoHarnessSkipReason::UserFilter);
+        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);
+                }
+            }
         }
 
         // Each argument of `instance` must implement Arbitrary.

kani-driver/src/args/autoharness_args.rs

@@ -9,27 +9,28 @@ use crate::args::{ValidateArgs, VerificationArgs, validate_std_path};
 use clap::{Error, Parser, error::ErrorKind};
 use kani_metadata::UnstableFeature;
 
+// TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches,
+// like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though.
 #[derive(Debug, Parser)]
 pub struct CommonAutoharnessArgs {
-    /// If specified, only autoharness functions that match this filter. This option can be provided
-    /// multiple times, which will verify all functions matching any of the filters.
-    /// Note that this filter will match against partial names, i.e., providing the name of a module will include all functions from that module.
-    /// Also note that if the function specified is unable to be automatically verified, this flag will have no effect.
-    #[arg(
-        long = "include-function",
-        num_args(1),
-        value_name = "FUNCTION",
-        conflicts_with = "exclude_function"
-    )]
-    pub include_function: Vec<String>,
-
-    /// If specified, only autoharness functions that do not match this filter. This option can be provided
-    /// multiple times, which will verify all functions that do not match any of the filters.
-    /// Note that this filter will match against partial names, i.e., providing the name of a module will exclude all functions from that module.
-    #[arg(long = "exclude-function", num_args(1), value_name = "FUNCTION")]
-    pub exclude_function: Vec<String>,
-    // TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches,
-    // like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though.
+    /// Only create automatic harnesses for functions that match the given pattern.
+    /// This option can be provided multiple times, which will verify functions matching any of the patterns.
+    /// Kani considers a function to match the pattern if its fully qualified path contains PATTERN as a substring.
+    /// Example: `--include-pattern foo` matches all functions whose fully qualified paths contain the substring "foo".
+    #[arg(long = "include-pattern", num_args(1), value_name = "PATTERN")]
+    pub include_pattern: Vec<String>,
+
+    /// Only create automatic harnesses for functions that do not match the given pattern.
+    /// This option can be provided multiple times, which will verify functions that do not match any of the patterns.
+    /// Kani considers a function to match the pattern if its fully qualified path contains PATTERN as a substring.
+
+    /// This option takes precedence over `--include-pattern`, i.e., Kani will first select all functions that match `--include-pattern`,
+    /// then exclude those that match `--exclude-pattern.`
+    /// Example: `--include-pattern foo --exclude-pattern foo::bar` creates automatic harnesses for all functions whose paths contain "foo" without "foo::bar".
+    /// Example: `--include-pattern foo::bar --exclude-pattern foo` makes the `--include-pattern` a no-op, since the exclude pattern is a superset of the include pattern.
+    #[arg(long = "exclude-pattern", num_args(1), value_name = "PATTERN")]
+    pub exclude_pattern: Vec<String>,
+
     /// Run the `list` subcommand after generating the automatic harnesses. Requires -Z list. Note that this option implies --only-codegen.
     #[arg(long)]
     pub list: bool,

kani-driver/src/args/mod.rs

@@ -178,6 +178,7 @@ pub enum CargoKaniSubcommand {
     List(Box<list_args::CargoListArgs>),
 
     /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts.
+    /// See https://model-checking.github.io/kani/reference/experimental/autoharness.html for documentation.
     Autoharness(Box<autoharness_args::CargoAutoharnessArgs>),
 }
 

kani-driver/src/autoharness/mod.rs

@@ -9,12 +9,12 @@ use crate::args::autoharness_args::{
 };
 use crate::args::common::UnstableFeature;
 use crate::call_cbmc::VerificationStatus;
-use crate::call_single_file::to_rustc_arg;
 use crate::harness_runner::HarnessResult;
 use crate::list::collect_metadata::process_metadata;
 use crate::list::output::output_list_results;
 use crate::project::{Project, standalone_project, std_project};
 use crate::session::KaniSession;
+use crate::util::warning;
 use crate::{InvocationType, print_kani_version, project, verify_project};
 use anyhow::Result;
 use comfy_table::Table as PrettyTable;
@@ -56,8 +56,8 @@ fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAuto
     session.enable_autoharness();
     session.add_default_bounds();
     session.add_auto_harness_args(
-        &common_autoharness_args.include_function,
-        &common_autoharness_args.exclude_function,
+        &common_autoharness_args.include_pattern,
+        &common_autoharness_args.exclude_pattern,
     );
 }
 
@@ -84,17 +84,20 @@ fn postprocess_project(
 /// Print automatic harness metadata to the terminal.
 fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
     let mut chosen_table = PrettyTable::new();
-    chosen_table.set_header(vec!["Selected Function"]);
+    chosen_table.set_header(vec!["Crate", "Selected Function"]);
 
     let mut skipped_table = PrettyTable::new();
-    skipped_table.set_header(vec!["Skipped Function", "Reason for Skipping"]);
+    skipped_table.set_header(vec!["Crate", "Skipped Function", "Reason for Skipping"]);
 
     for md in metadata {
         let autoharness_md = md.autoharness_md.unwrap();
-        chosen_table.add_rows(autoharness_md.chosen.into_iter().map(|func| vec![func]));
+        chosen_table.add_rows(
+            autoharness_md.chosen.into_iter().map(|func| vec![md.crate_name.clone(), func]),
+        );
         skipped_table.add_rows(autoharness_md.skipped.into_iter().filter_map(|(func, reason)| {
             match reason {
                 AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => Some(vec![
+                    md.crate_name.clone(),
                     func,
                     format!(
                         "{reason} {}",
@@ -106,7 +109,9 @@ fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
                 ]),
                 AutoHarnessSkipReason::GenericFn
                 | AutoHarnessSkipReason::NoBody
-                | AutoHarnessSkipReason::UserFilter => Some(vec![func, reason.to_string()]),
+                | AutoHarnessSkipReason::UserFilter => {
+                    Some(vec![md.crate_name.clone(), func, reason.to_string()])
+                }
                 // We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation.
                 // For those we don't insert during instrumentation that are in this category (manual harnesses or Kani trait implementations),
                 // it should be obvious that we wouldn't generate harnesses, so reporting those functions as "skipped" is unlikely to be useful.
@@ -151,23 +156,36 @@ fn print_skipped_table(table: &mut PrettyTable) {
 impl KaniSession {
     /// Enable autoharness mode.
     pub fn enable_autoharness(&mut self) {
-        self.auto_harness = true;
+        self.autoharness_compiler_flags = Some(vec![]);
         self.args.common_args.unstable_features.enable_feature(UnstableFeature::FunctionContracts);
         self.args.common_args.unstable_features.enable_feature(UnstableFeature::LoopContracts);
     }
 
     /// Add the compiler arguments specific to the `autoharness` subcommand.
-    /// TODO: this should really be appending onto the `kani_compiler_flags()` output instead of `pkg_args`.
-    /// It doesn't affect functionality since autoharness doesn't examine dependencies, but would still be better practice.
     pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) {
-        for func in included {
-            self.pkg_args
-                .push(to_rustc_arg(vec![format!("--autoharness-include-function {}", func)]));
+        for include_pattern in included {
+            for exclude_pattern in excluded {
+                // Check if include pattern contains exclude pattern
+                // This catches cases like include="foo::bar" exclude="bar" or include="foo" exclude="foo"
+                if include_pattern.contains(exclude_pattern) {
+                    warning(&format!(
+                        "Include pattern '{}' contains exclude pattern '{}'. \
+                            This combination will never match any functions since all functions matching \
+                            the include pattern will also match the exclude pattern, and the exclude pattern takes precedence.",
+                        include_pattern, exclude_pattern
+                    ));
+                }
+            }
+        }
+
+        let mut args = vec![];
+        for pattern in included {
+            args.push(format!("--autoharness-include-pattern {}", pattern));
         }
-        for func in excluded {
-            self.pkg_args
-                .push(to_rustc_arg(vec![format!("--autoharness-exclude-function {}", func)]));
+        for pattern in excluded {
+            args.push(format!("--autoharness-exclude-pattern {}", pattern));
         }
+        self.autoharness_compiler_flags = Some(args);
     }
 
     /// Add global harness timeout and loop unwinding bounds if not provided.
@@ -196,13 +214,15 @@ impl KaniSession {
 
         let mut verified_fns = PrettyTable::new();
         verified_fns.set_header(vec![
+            "Crate",
             "Selected Function",
             "Kind of Automatic Harness",
             "Verification Result",
         ]);
 
         for success in successes {
             verified_fns.add_row(vec![
+                success.harness.crate_name.clone(),
                 success.harness.pretty_name.clone(),
                 success.harness.attributes.kind.to_string(),
                 success.result.status.to_string(),
@@ -211,13 +231,16 @@ impl KaniSession {
 
         for failure in failures {
             verified_fns.add_row(vec![
+                failure.harness.crate_name.clone(),
                 failure.harness.pretty_name.clone(),
                 failure.harness.attributes.kind.to_string(),
                 failure.result.status.to_string(),
             ]);
         }
 
-        println!("{verified_fns}");
+        if total > 0 {
+            println!("{verified_fns}");
+        }
 
         if failing > 0 {
             println!(

kani-driver/src/call_cargo.rs

@@ -194,7 +194,7 @@ crate-type = ["lib"]
         // If you are adding a new `kani-compiler` argument, you likely want to put it `kani_compiler_flags()` instead,
         // unless there a reason it shouldn't be passed to dependencies.
         // (Note that at the time of writing, passing the other compiler args to dependencies is a no-op, since `--reachability=None` skips codegen anyway.)
-        self.pkg_args.push(self.reachability_arg());
+        let pkg_args = vec!["--".into(), self.reachability_arg()];
 
         let mut found_target = false;
         let packages = self.packages_to_verify(&self.args, &metadata)?;
@@ -206,7 +206,7 @@ crate-type = ["lib"]
                 cmd.args(&cargo_args)
                     .args(vec!["-p", &package.id.to_string()])
                     .args(verification_target.to_args())
-                    .args(&self.pkg_args)
+                    .args(&pkg_args)
                     .env("RUSTC", &self.kani_compiler)
                     // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
                     // https://doc.rust-lang.org/cargo/reference/environment-variables.html

kani-driver/src/call_single_file.rs

@@ -151,6 +151,10 @@ impl KaniSession {
             flags.push("--no-assert-contracts".into());
         }
 
+        if let Some(args) = self.autoharness_compiler_flags.clone() {
+            flags.extend(args);
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
 
         flags

kani-driver/src/harness_runner.rs

@@ -298,11 +298,11 @@ impl KaniSession {
             self.show_coverage_summary()?;
         }
 
-        if self.auto_harness {
+        if self.autoharness_compiler_flags.is_some() {
             self.print_autoharness_summary(automatic)?;
         }
 
-        if failing > 0 && !self.auto_harness {
+        if failing > 0 && self.autoharness_compiler_flags.is_none() {
             // Failure exit code without additional error message
             drop(self);
             std::process::exit(1);