allow for including/excluding fns explicitly & improve summary printing

kani-compiler/src/args.rs

@@ -90,6 +90,12 @@ pub struct Arguments {
     /// Print the final LLBC file to stdout.
     #[clap(long)]
     pub print_llbc: bool,
+    /// If we are running the autoverify subcommand, the functions to autoverify
+    #[arg(long = "autoverify-include-function", num_args(1))]
+    pub autoverify_included_functions: Vec<String>,
+    /// If we are running the autoverify subcommand, the functions to exclude from autoverification
+    #[arg(long = "autoverify-exclude-function", num_args(1))]
+    pub autoverify_excluded_functions: Vec<String>,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/kani_middle/codegen_units.rs

@@ -62,7 +62,8 @@ impl CodegenUnits {
         let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() };
         let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
         let base_filename = base_filepath.as_path();
-        match queries.args().reachability_analysis {
+        let args = queries.args();
+        match args.reachability_analysis {
             ReachabilityType::Harnesses => {
                 let all_harnesses = get_all_manual_harnesses(tcx, base_filename);
                 // Even if no_stubs is empty we still need to store rustc metadata.
@@ -80,8 +81,18 @@ impl CodegenUnits {
                 let kani_harness_intrinsic =
                     kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap();
                 let kani_any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap();
+
                 let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool {
-                    is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst)
+                    // If the user specified functions to include or exclude, only allow instances matching those filters.
+                    let user_included = if !args.autoverify_included_functions.is_empty() {
+                        fn_list_contains_instance(&instance, &args.autoverify_included_functions)
+                    } else if !args.autoverify_excluded_functions.is_empty() {
+                        !fn_list_contains_instance(&instance, &args.autoverify_excluded_functions)
+                    } else {
+                        true
+                    };
+                    user_included
+                        && is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst)
                 });
                 let automatic_harnesses = get_all_automatic_harnesses(
                     tcx,
@@ -378,3 +389,11 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst:
         false
     })
 }
+
+/// Return whether the name of `instance` is included in `fn_list`.
+/// If `exact = true`, then `instance`'s exact, fully-qualified name must be in `fn_list`; otherwise, `fn_list`
+/// can have a substring of `instance`'s name.
+fn fn_list_contains_instance(instance: &Instance, fn_list: &[String]) -> bool {
+    let pretty_name = instance.name();
+    fn_list.contains(&pretty_name) || fn_list.iter().any(|fn_name| pretty_name.contains(fn_name))
+}

kani-driver/src/args/autoverify_args.rs

@@ -1,19 +1,42 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-//! Implements the subcommand handling of the list subcommand
+//! Implements the subcommand handling of the autoverify subcommand
 
 use std::path::PathBuf;
 
 use crate::args::{ValidateArgs, VerificationArgs};
 use clap::{Error, Parser, error::ErrorKind};
 use kani_metadata::UnstableFeature;
 
-// TODO add --function option to only verify functions matching the substring
-// (akin to --harness).
+#[derive(Debug, Parser)]
+pub struct CommonAutoverifyArgs {
+    /// If specified, only autoverify 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 autoverify 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.
+}
 
 /// Automatically verify functions in a crate.
 #[derive(Debug, Parser)]
 pub struct CargoAutoverifyArgs {
+    #[command(flatten)]
+    pub common_autoverify_args: CommonAutoverifyArgs,
+
     #[command(flatten)]
     pub verify_opts: VerificationArgs,
 }
@@ -28,13 +51,15 @@ pub struct StandaloneAutoverifyArgs {
     #[arg(long, hide = true)]
     pub crate_name: Option<String>,
 
+    #[command(flatten)]
+    pub common_autoverify_args: CommonAutoverifyArgs,
+
     #[command(flatten)]
     pub verify_opts: VerificationArgs,
 }
 
 impl ValidateArgs for CargoAutoverifyArgs {
     fn validate(&self) -> Result<(), Error> {
-        self.verify_opts.validate()?;
         if !self
             .verify_opts
             .common_args
@@ -62,13 +87,14 @@ impl ValidateArgs for CargoAutoverifyArgs {
             ));
         }
 
+        self.verify_opts.validate()?;
+
         Ok(())
     }
 }
 
 impl ValidateArgs for StandaloneAutoverifyArgs {
     fn validate(&self) -> Result<(), Error> {
-        self.verify_opts.validate()?;
         if !self
             .verify_opts
             .common_args
@@ -105,6 +131,8 @@ impl ValidateArgs for StandaloneAutoverifyArgs {
             ));
         }
 
+        self.verify_opts.validate()?;
+
         Ok(())
     }
 }

kani-driver/src/assess/mod.rs

@@ -53,7 +53,7 @@ fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
         session.args.jobs = Some(None); // -j, num_cpu
     }
 
-    let project = project::cargo_project(&session, true)?;
+    let project = project::cargo_project(&mut session, true)?;
     let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo");
 
     let packages_metadata =

kani-driver/src/autoverify/mod.rs

@@ -0,0 +1,72 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::call_cbmc::VerificationStatus;
+use crate::call_single_file::to_rustc_arg;
+use crate::harness_runner::HarnessResult;
+use crate::session::KaniSession;
+use anyhow::Result;
+
+impl KaniSession {
+    /// Enable autoverify mode.
+    pub fn enable_autoverify(&mut self) {
+        self.autoverify = true;
+    }
+
+    /// Add the compiler arguments specific to the `autoverify` subcommand.
+    pub fn add_auto_verify_args(&mut self, included: Vec<String>, excluded: Vec<String>) {
+        for func in included {
+            self.pkg_args
+                .push(to_rustc_arg(vec![format!("--autoverify-include-function {}", func)]));
+        }
+        for func in excluded {
+            self.pkg_args
+                .push(to_rustc_arg(vec![format!("--autoverify-exclude-function {}", func)]));
+        }
+    }
+
+    /// Prints the results from running the `autoverify` subcommand.
+    pub fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> {
+        let (successes, failures): (Vec<_>, Vec<_>) =
+            automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
+
+        let succeeding = successes.len();
+        let failing = failures.len();
+        let total = succeeding + failing;
+
+        // TODO: it would be nice if we had access to which functions the user included/excluded here
+        // so that we could print a comparison for them of any of the included functions that we skipped.
+        println!("Autoverify Summary:");
+        println!(
+            "Note that Kani will only autoverify a function if it determines that each of its arguments implement the Arbitrary trait."
+        );
+        println!(
+            "Examine the summary closely to determine which functions were automatically verified."
+        );
+
+        // Since autoverification skips over some functions, print the successes to make it easier to see what we verified in one place.
+        for success in successes {
+            println!("Verification succeeded for - {}", success.harness.pretty_name);
+        }
+
+        for failure in failures {
+            println!("Verification failed for - {}", failure.harness.pretty_name);
+        }
+
+        if total > 0 {
+            println!(
+                "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total."
+            );
+        } else {
+            println!("
+                No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary.");
+            println!(
+                "If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive."
+            );
+        }
+
+        // Manual harness summary may come afterward, so separate them with a new line.
+        println!();
+        Ok(())
+    }
+}

kani-driver/src/call_cargo.rs

@@ -126,7 +126,7 @@ crate-type = ["lib"]
     }
 
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
-    pub fn cargo_build(&self, keep_going: bool) -> Result<CargoOutputs> {
+    pub fn cargo_build(&mut self, keep_going: bool) -> Result<CargoOutputs> {
         let build_target = env!("TARGET"); // see build.rs
         let metadata = self.cargo_metadata(build_target)?;
         let target_dir = self
@@ -183,13 +183,12 @@ crate-type = ["lib"]
         }
 
         // Arguments that will only be passed to the target package.
-        let mut pkg_args: Vec<String> = vec![];
-        pkg_args.extend(["--".to_string(), self.reachability_arg()]);
+        self.pkg_args.push(self.reachability_arg());
         if let Some(backend_arg) = self.backend_arg() {
-            pkg_args.push(backend_arg);
+            self.pkg_args.push(backend_arg);
         }
         if self.args.no_assert_contracts {
-            pkg_args.push("--no-assert-contracts".into());
+            self.pkg_args.push("--no-assert-contracts".into());
         }
 
         let mut found_target = false;
@@ -202,7 +201,7 @@ crate-type = ["lib"]
                 cmd.args(&cargo_args)
                     .args(vec!["-p", &package.id.to_string()])
                     .args(verification_target.to_args())
-                    .args(&pkg_args)
+                    .args(&self.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/harness_runner.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::{Result, bail};
-use kani_metadata::{ArtifactType, HarnessMetadata};
+use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata};
 use rayon::prelude::*;
 use std::fs::File;
 use std::io::Write;
@@ -169,10 +169,17 @@ impl KaniSession {
         let thread_index = rayon::current_thread_index().unwrap_or_default();
         // If the harness is automatically generated, pretty_name refers to the function under verification.
         let mut msg = if harness.is_automatically_generated {
-            format!(
-                "Autoverify: Checking function {} against all possible inputs...",
-                harness.pretty_name
-            )
+            if matches!(harness.attributes.kind, HarnessKind::Proof) {
+                format!(
+                    "Autoverify: Checking function {} against all possible inputs...",
+                    harness.pretty_name
+                )
+            } else {
+                format!(
+                    "Autoverify: Checking function {}'s contract against all possible inputs...",
+                    harness.pretty_name
+                )
+            }
         } else {
             format!("Checking harness {}...", harness.pretty_name)
         };
@@ -190,34 +197,6 @@ impl KaniSession {
         Ok(result)
     }
 
-    /// Prints the results from running the `autoverify` subcommand.
-    fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> {
-        let (successes, failures): (Vec<_>, Vec<_>) =
-            automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
-
-        let succeeding = successes.len();
-        let failing = failures.len();
-        let total = succeeding + failing;
-
-        if failing > 0 {
-            println!("Summary:");
-        }
-        for failure in failures.iter() {
-            println!("Verification failed for - {}", failure.harness.pretty_name);
-        }
-
-        if total > 0 {
-            println!(
-                "Autoverify: Complete - {succeeding} successfully verified functions, {failing} failures, {total} total."
-            );
-        } else {
-            println!("
-                Autoverify: No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary.");
-        }
-
-        Ok(())
-    }
-
     /// Concludes a session by printing a summary report and exiting the process with an
     /// error code (if applicable).
     ///
@@ -231,7 +210,7 @@ impl KaniSession {
         let (automatic, manual): (Vec<_>, Vec<_>) =
             results.iter().partition(|r| r.harness.is_automatically_generated);
 
-        if self.auto_verify {
+        if self.autoverify {
             self.print_autoverify_summary(automatic)?;
         }
 
@@ -256,7 +235,7 @@ impl KaniSession {
 
         // We currently omit a summary if there was just 1 harness
         if failing > 0 {
-            println!("Summary:");
+            println!("Manual Harness Summary:");
         }
         for failure in failures.iter() {
             println!("Verification failed for - {}", failure.harness.pretty_name);

kani-driver/src/list/collect_metadata.rs

@@ -78,12 +78,12 @@ fn process_metadata(metadata: Vec<KaniMetadata>) -> ListMetadata {
 pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
     let quiet = args.common_args.quiet;
     verify_opts.common_args = args.common_args;
-    let session = KaniSession::new(verify_opts)?;
+    let mut session = KaniSession::new(verify_opts)?;
     if !quiet {
         print_kani_version(InvocationType::CargoKani(vec![]));
     }
 
-    let project = cargo_project(&session, false)?;
+    let project = cargo_project(&mut session, false)?;
     let list_metadata = process_metadata(project.metadata);
 
     output_list_results(list_metadata, args.format, quiet)