Allow users to select a subset of harness to run (rust-lang#2202)

Users can now select a subset of harnesses to run using `--harness` multiple times. Previously users could either run a single harness or they had to run them all.

For the example provided in rust-lang#1778:
```rust
// example.rs
#[kani::proof]
fn a() {}
#[kani::proof] 
fn b() {}
#[kani::proof] 
fn c() {std::unimplemented!();}
```

Users can select harnesses `a` and `b` by running:
```bash
$ kani example.rs --harness a --harness b
```

In case of multiple matches, Kani will run all harnesses that matches at least one of the `--harness` argument.

Author: celinval

Cargo.lock

@@ -469,6 +469,15 @@ dependencies = [
  "windows-sys 0.45.0",
 ]
 
+[[package]]
+name = "itertools"
+version = "0.10.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473"
+dependencies = [
+ "either",
+]
+
 [[package]]
 name = "itoa"
 version = "1.0.5"
@@ -492,6 +501,7 @@ dependencies = [
  "clap",
  "cprover_bindings",
  "home",
+ "itertools",
  "kani_metadata",
  "kani_queries",
  "lazy_static",

kani-compiler/Cargo.toml

@@ -15,6 +15,7 @@ bitflags = { version = "1.0", optional = true }
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = { version = "4.1.3", features = ["cargo"] }
 home = "0.5"
+itertools = "0.10"
 kani_queries = {path = "kani_queries"}
 kani_metadata = { path = "../kani_metadata", optional = true }
 lazy_static = "1.4.0"

kani-compiler/src/kani_compiler.rs

@@ -20,9 +20,10 @@ use crate::kani_middle::stubbing;
 use crate::parser::{self, KaniCompilerParser};
 use crate::session::init_session;
 use clap::ArgMatches;
+use itertools::Itertools;
 use kani_queries::{QueryDb, ReachabilityType, UserInput};
 use rustc_codegen_ssa::traits::CodegenBackend;
-use rustc_data_structures::fx::FxHashMap;
+use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_driver::{Callbacks, Compilation, RunCompiler};
 use rustc_hir::definitions::DefPathHash;
 use rustc_interface::Config;
@@ -101,9 +102,18 @@ impl KaniCompiler {
         let all_stubs = stubbing::collect_stub_mappings(tcx);
         if all_stubs.is_empty() {
             FxHashMap::default()
-        } else if let Some(harness) = self.args.as_ref().unwrap().get_one::<String>(parser::HARNESS)
+        } else if let Some(harnesses) =
+            self.args.as_ref().unwrap().get_many::<String>(parser::HARNESS)
         {
-            find_harness_stub_mapping(harness, all_stubs).unwrap_or_default()
+            let mappings = filter_stub_mapping(harnesses.collect(), all_stubs);
+            if mappings.len() > 1 {
+                tcx.sess.err(format!(
+                    "Failed to apply stubs. Harnesses with stubs must be verified separately. Found: `{}`",
+                     mappings.into_keys().join("`, `")));
+                FxHashMap::default()
+            } else {
+                mappings.into_values().next().unwrap_or_default()
+            }
         } else {
             // No harness was provided. Nothing to do.
             FxHashMap::default()
@@ -167,20 +177,16 @@ impl Callbacks for KaniCompiler {
     }
 }
 
-/// Find the stub mapping for the given harness.
+/// Find the stub mapping for the given harnesses.
 ///
 /// This function is necessary because Kani currently allows a harness to be
-/// specified by a partially qualified name, whereas stub mappings use fully
-/// qualified names.
-fn find_harness_stub_mapping(
-    harness: &str,
-    stub_mappings: FxHashMap<String, FxHashMap<DefPathHash, DefPathHash>>,
-) -> Option<FxHashMap<DefPathHash, DefPathHash>> {
-    let suffix = String::from("::") + harness;
-    for (name, mapping) in stub_mappings {
-        if name == harness || name.ends_with(&suffix) {
-            return Some(mapping);
-        }
-    }
-    None
+/// specified as a filter, whereas stub mappings use fully qualified names.
+fn filter_stub_mapping(
+    harnesses: FxHashSet<&String>,
+    mut stub_mappings: FxHashMap<String, FxHashMap<DefPathHash, DefPathHash>>,
+) -> FxHashMap<String, FxHashMap<DefPathHash, DefPathHash>> {
+    stub_mappings.retain(|name, _| {
+        harnesses.contains(name) || harnesses.iter().any(|harness| name.contains(*harness))
+    });
+    stub_mappings
 }

kani-compiler/src/parser.rs

@@ -129,7 +129,7 @@ pub fn parser() -> Command {
                 .long(HARNESS)
                 .help("Selects the harness to target.")
                 .value_name("HARNESS")
-                .action(ArgAction::Set),
+                .action(ArgAction::Append),
         )
         .arg(
             Arg::new(ENABLE_STUBBING)

kani-driver/src/args.rs

@@ -128,9 +128,15 @@ pub struct KaniArgs {
     /// This is an unstable feature. Consider using --harness instead
     #[arg(long, hide = true, requires("enable_unstable"))]
     pub function: Option<String>,
-    /// Entry point for verification (proof harness)
-    #[arg(long, conflicts_with = "function")]
-    pub harness: 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.
+    #[arg(
+        long = "harness",
+        conflicts_with = "function",
+        num_args(1),
+        value_name = "HARNESS_FILTER"
+    )]
+    pub harnesses: Vec<String>,
 
     /// Link external C files referenced by Rust code.
     /// This is an experimental feature and requires `--enable-unstable` to be used
@@ -155,7 +161,7 @@ pub struct KaniArgs {
     #[arg(long)]
     pub default_unwind: Option<u32>,
     /// Specify the value used for loop unwinding for the specified harness in CBMC
-    #[arg(long, requires("harness"))]
+    #[arg(long, requires("harnesses"))]
     pub unwind: Option<u32>,
     /// Specify the CBMC solver to use. Overrides the harness `solver` attribute.
     #[arg(long, value_parser = CbmcSolverValueParser::new(CbmcSolver::VARIANTS))]
@@ -232,7 +238,7 @@ pub struct KaniArgs {
         long,
         hide_short_help = true,
         requires("enable_unstable"),
-        requires("harness"),
+        requires("harnesses"),
         conflicts_with("concrete_playback")
     )]
     pub enable_stubbing: bool,
@@ -650,6 +656,25 @@ mod tests {
         .unwrap();
         // no assertion: the above might fail if it fails to allow 0 args to cbmc-args
     }
+
+    /// Ensure users can pass multiple harnesses options and that the value is accumulated.
+    #[test]
+    fn check_multiple_harnesses() {
+        let args =
+            StandaloneArgs::try_parse_from("kani input.rs --harness a --harness b".split(" "))
+                .unwrap();
+        assert_eq!(args.common_opts.harnesses, vec!["a".to_owned(), "b".to_owned()]);
+    }
+
+    #[test]
+    fn check_multiple_harnesses_without_flag_fail() {
+        let result = StandaloneArgs::try_parse_from(
+            "kani input.rs --harness harness_1 harness_2".split(" "),
+        );
+        assert!(result.is_err());
+        assert_eq!(result.unwrap_err().kind(), ErrorKind::UnknownArgument);
+    }
+
     #[test]
     fn check_multiple_packages() {
         // accepts repeated:

kani-driver/src/args_toml.rs

@@ -106,7 +106,8 @@ fn toml_to_args(tomldata: &str) -> Result<(Vec<OsString>, Vec<OsString>)> {
     for (flag, value) in map {
         if flag == "cbmc-args" {
             // --cbmc-args has to come last because it eats all remaining arguments
-            insert_arg_from_toml(&flag, &value, &mut cbmc_args)?;
+            cbmc_args.push("--cbmc-args".into());
+            cbmc_args.append(&mut cbmc_arg_from_toml(&value)?);
         } else {
             insert_arg_from_toml(&flag, &value, &mut args)?;
         }
@@ -129,9 +130,9 @@ fn insert_arg_from_toml(flag: &str, value: &Value, args: &mut Vec<OsString>) ->
             }
         }
         Value::Array(a) => {
-            args.push(format!("--{flag}").into());
             for arg in a {
                 if let Some(arg) = arg.as_str() {
+                    args.push(format!("--{flag}").into());
                     args.push(arg.into());
                 } else {
                     bail!("flag {} contains non-string values", flag);
@@ -149,6 +150,33 @@ fn insert_arg_from_toml(flag: &str, value: &Value, args: &mut Vec<OsString>) ->
     Ok(())
 }
 
+/// Translates one toml entry (flag, value) into arguments and inserts it into `args`
+fn cbmc_arg_from_toml(value: &Value) -> Result<Vec<OsString>> {
+    let mut args = vec![];
+    const CBMC_FLAG: &str = "--cbmc-args";
+    match value {
+        Value::Boolean(_) => {
+            bail!("cannot pass boolean value to `{CBMC_FLAG}`")
+        }
+        Value::Array(a) => {
+            for arg in a {
+                if let Some(arg) = arg.as_str() {
+                    args.push(arg.into());
+                } else {
+                    bail!("flag {CBMC_FLAG} contains non-string values");
+                }
+            }
+        }
+        Value::String(s) => {
+            args.push(s.into());
+        }
+        _ => {
+            bail!("Unknown key type {CBMC_FLAG}");
+        }
+    }
+    Ok(args)
+}
+
 /// Take 'a.b.c' and turn it into 'start['a']['b']['c']' reliably, and interpret the result as a table
 fn get_table<'a>(start: &'a Value, table: &str) -> Option<&'a Table> {
     let mut current = start;

kani-driver/src/assess/mod.rs

@@ -91,8 +91,8 @@ fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
     }
 
     // Done with the 'cargo-kani' part, now we're going to run *test* harnesses instead of proof:
-    let harnesses = metadata.test_harnesses;
-    let runner = crate::harness_runner::HarnessRunner { sess: &session, project };
+    let harnesses = Vec::from_iter(metadata.test_harnesses.iter());
+    let runner = crate::harness_runner::HarnessRunner { sess: &session, project: &project };
 
     let results = runner.check_all_harnesses(&harnesses)?;
 

kani-driver/src/call_single_file.rs

@@ -90,7 +90,7 @@ impl KaniSession {
         if self.args.enable_stubbing {
             flags.push("--enable-stubbing".into());
         }
-        if let Some(harness) = &self.args.harness {
+        for harness in &self.args.harnesses {
             flags.push(format!("--harness={harness}"));
         }
 

kani-driver/src/harness_runner.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use anyhow::Result;
+use anyhow::{bail, Result};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
 use std::path::Path;
@@ -10,33 +10,33 @@ use crate::args::OutputFormat;
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
 use crate::session::KaniSession;
-use crate::util::specialized_harness_name;
+use crate::util::{error, specialized_harness_name};
 
 /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents
 /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed.
 ///
 /// This struct is basically just a nicer way of passing many arguments to [`Self::check_all_harnesses`]
-pub(crate) struct HarnessRunner<'sess> {
+pub(crate) struct HarnessRunner<'sess, 'pr> {
     /// The underlying kani session
     pub sess: &'sess KaniSession,
     /// The project under verification.
-    pub project: Project,
+    pub project: &'pr Project,
 }
 
 /// The result of checking a single harness. This both hangs on to the harness metadata
 /// (as a means to identify which harness), and provides that harness's verification result.
-pub(crate) struct HarnessResult<'sess> {
-    pub harness: &'sess HarnessMetadata,
+pub(crate) struct HarnessResult<'pr> {
+    pub harness: &'pr HarnessMetadata,
     pub result: VerificationResult,
 }
 
-impl<'sess> HarnessRunner<'sess> {
+impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
     /// Given a [`HarnessRunner`] (to abstract over how these harnesses were generated), this runs
     /// the proof-checking process for each harness in `harnesses`.
-    pub(crate) fn check_all_harnesses<'a>(
+    pub(crate) fn check_all_harnesses(
         &self,
-        harnesses: &'a [HarnessMetadata],
-    ) -> Result<Vec<HarnessResult<'a>>> {
+        harnesses: &'pr [&HarnessMetadata],
+    ) -> Result<Vec<HarnessResult<'pr>>> {
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
 
         let pool = {
@@ -47,10 +47,10 @@ impl<'sess> HarnessRunner<'sess> {
             builder.build()?
         };
 
-        let results = pool.install(|| -> Result<Vec<HarnessResult<'a>>> {
+        let results = pool.install(|| -> Result<Vec<HarnessResult<'pr>>> {
             sorted_harnesses
                 .par_iter()
-                .map(|harness| -> Result<HarnessResult<'a>> {
+                .map(|harness| -> Result<HarnessResult<'pr>> {
                     let harness_filename = harness.pretty_name.replace("::", "-");
                     let report_dir = self.project.outdir.join(format!("report-{harness_filename}"));
                     let goto_file =
@@ -139,11 +139,27 @@ impl KaniSession {
                     "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total."
                 );
             } else {
-                // TODO: This could use a better error message, possibly with links to Kani documentation.
-                // New users may encounter this and could use a pointer to how to write proof harnesses.
-                println!(
-                    "No proof harnesses (functions with #[kani::proof]) were found to verify."
-                );
+                match (self.args.harnesses.as_slice(), &self.args.function) {
+                    ([], None) =>
+                    // TODO: This could use a better message, possibly with links to Kani documentation.
+                    // New users may encounter this and could use a pointer to how to write proof harnesses.
+                    {
+                        println!(
+                            "No proof harnesses (functions with #[kani::proof]) were found to verify."
+                        )
+                    }
+                    ([harness], None) => {
+                        bail!("no harnesses matched the harness filter: `{harness}`")
+                    }
+                    (harnesses, None) => bail!(
+                        "no harnesses matched the harness filters: `{}`",
+                        harnesses.join("`, `")
+                    ),
+                    ([], Some(func)) => error(&format!("No function named {func} was found")),
+                    _ => unreachable!(
+                        "invalid configuration. Cannot specify harness and function at the same time"
+                    ),
+                };
             }
         }
 

kani-driver/src/main.rs

@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 #![feature(let_chains)]
 #![feature(array_methods)]
-
 use std::ffi::OsString;
 use std::process::ExitCode;
 
@@ -91,7 +90,7 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
     debug!(n = harnesses.len(), ?harnesses, "verify_project");
 
     // Verification
-    let runner = harness_runner::HarnessRunner { sess: &session, project };
+    let runner = harness_runner::HarnessRunner { sess: &session, project: &project };
     let results = runner.check_all_harnesses(&harnesses)?;
 
     session.print_final_summary(&results)