change arguments to no longer be exclusive; make --exclude take precedence

Also rename them to reference patterns to make it clearer how one might use them together.

Author: carolynzech

docs/src/reference/experimental/autoharness.md

@@ -43,16 +43,16 @@ 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 foo --include-pattern 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
 ```
 
 ## Example

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

@@ -394,12 +394,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

@@ -55,8 +55,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,
     );
 }
 
@@ -163,11 +163,11 @@ impl KaniSession {
     /// Add the compiler arguments specific to the `autoharness` subcommand.
     pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) {
         let mut args = vec![];
-        for func in included {
-            args.push(format!("--autoharness-include-function {}", func));
+        for pattern in included {
+            args.push(format!("--autoharness-include-pattern {}", pattern));
         }
-        for func in excluded {
-            args.push(format!("--autoharness-exclude-function {}", func));
+        for pattern in excluded {
+            args.push(format!("--autoharness-exclude-pattern {}", pattern));
         }
         self.autoharness_compiler_flags = Some(args);
     }

tests/script-based-pre/cargo_autoharness_exclude/exclude.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness --exclude-function exclude
+cargo kani autoharness -Z autoharness --exclude-pattern exclude

tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Test that the automatic harness generation feature selects functions correctly
-// when --exclude-function is provided.
+// when --exclude-pattern is provided.
 
 mod include {
     fn simple(x: u8, _y: u16) -> u8 {

tests/script-based-pre/cargo_autoharness_include/include.sh

@@ -2,4 +2,4 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-cargo kani autoharness -Z autoharness --include-function include
+cargo kani autoharness -Z autoharness --include-pattern include

tests/script-based-pre/cargo_autoharness_include/src/lib.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Test that the automatic harness generation feature selects functions correctly
-// when --include-function is provided.
+// when --include-pattern is provided.
 
 // Each function inside this module matches the filter.
 mod include {