From bb7662dda4a3127b4297f1c1cd1e59228f58b541 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 15 Feb 2023 18:05:18 -0800 Subject: [PATCH] Allow users to select a subset of harness to run (#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 #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. --- Cargo.lock | 10 ++ kani-compiler/Cargo.toml | 1 + kani-compiler/src/kani_compiler.rs | 40 ++++---- kani-compiler/src/parser.rs | 2 +- kani-driver/src/args.rs | 35 ++++++- kani-driver/src/args_toml.rs | 32 ++++++- kani-driver/src/assess/mod.rs | 4 +- kani-driver/src/call_single_file.rs | 2 +- kani-driver/src/harness_runner.rs | 50 ++++++---- kani-driver/src/main.rs | 3 +- kani-driver/src/metadata.rs | 94 +++++++++---------- kani_metadata/src/harness.rs | 2 +- .../simple-proof-annotation/main.expected | 2 +- tests/cargo-ui/multiple-harnesses/Cargo.toml | 11 +++ tests/cargo-ui/multiple-harnesses/expected | 3 + tests/cargo-ui/multiple-harnesses/src/lib.rs | 14 +++ .../function-stubbing-no-harness/expected | 2 +- .../{ => check_all}/expected | 0 .../{ => check_all}/test.rs | 0 .../ui/multiple-harnesses/check_some/expected | 3 + .../check_some/select_harnesses.rs | 19 ++++ .../multiple_matches/expected | 5 + .../multiple_matches/select_harnesses.rs | 39 ++++++++ .../no_matching_harness/expected | 1 + .../no_matching_harness/non_matching.rs | 10 ++ .../some_matching_harnesses/expected | 3 + .../some_matching_harnesses/subset.rs | 19 ++++ .../expected | 1 + .../stub_harnesses.rs | 34 +++++++ 29 files changed, 344 insertions(+), 97 deletions(-) create mode 100644 tests/cargo-ui/multiple-harnesses/Cargo.toml create mode 100644 tests/cargo-ui/multiple-harnesses/expected create mode 100644 tests/cargo-ui/multiple-harnesses/src/lib.rs rename tests/ui/multiple-harnesses/{ => check_all}/expected (100%) rename tests/ui/multiple-harnesses/{ => check_all}/test.rs (100%) create mode 100644 tests/ui/multiple-harnesses/check_some/expected create mode 100644 tests/ui/multiple-harnesses/check_some/select_harnesses.rs create mode 100644 tests/ui/multiple-harnesses/multiple_matches/expected create mode 100644 tests/ui/multiple-harnesses/multiple_matches/select_harnesses.rs create mode 100644 tests/ui/multiple-harnesses/no_matching_harness/expected create mode 100644 tests/ui/multiple-harnesses/no_matching_harness/non_matching.rs create mode 100644 tests/ui/multiple-harnesses/some_matching_harnesses/expected create mode 100644 tests/ui/multiple-harnesses/some_matching_harnesses/subset.rs create mode 100644 tests/ui/stubbing-unsupported-multiple-harness/expected create mode 100644 tests/ui/stubbing-unsupported-multiple-harness/stub_harnesses.rs diff --git a/Cargo.lock b/Cargo.lock index 99c954cb1c6d8..ff7261bc013b7 100644 --- a/Cargo.lock +++ b/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", diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 89e5aa7efcd7a..6af985d15f3fd 100644 --- a/kani-compiler/Cargo.toml +++ b/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" diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index be8e5c8855948..f958cbe294924 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/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::(parser::HARNESS) + } else if let Some(harnesses) = + self.args.as_ref().unwrap().get_many::(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>, -) -> Option> { - 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>, +) -> FxHashMap> { + stub_mappings.retain(|name, _| { + harnesses.contains(name) || harnesses.iter().any(|harness| name.contains(*harness)) + }); + stub_mappings } diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs index c7922dba5a834..c34f27baf0f46 100644 --- a/kani-compiler/src/parser.rs +++ b/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) diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 7687d644b8b4d..6def7979317c9 100644 --- a/kani-driver/src/args.rs +++ b/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, - /// Entry point for verification (proof harness) - #[arg(long, conflicts_with = "function")] - pub harness: Option, + /// 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, /// 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, /// Specify the value used for loop unwinding for the specified harness in CBMC - #[arg(long, requires("harness"))] + #[arg(long, requires("harnesses"))] pub unwind: Option, /// 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: diff --git a/kani-driver/src/args_toml.rs b/kani-driver/src/args_toml.rs index 14b5d34d3d18f..c6ab7dc65c282 100644 --- a/kani-driver/src/args_toml.rs +++ b/kani-driver/src/args_toml.rs @@ -106,7 +106,8 @@ fn toml_to_args(tomldata: &str) -> Result<(Vec, Vec)> { 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) -> } } 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) -> Ok(()) } +/// Translates one toml entry (flag, value) into arguments and inserts it into `args` +fn cbmc_arg_from_toml(value: &Value) -> Result> { + 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; diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs index 993f346df582a..6b076616e23b1 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -91,8 +91,8 @@ fn assess_project(mut session: KaniSession) -> Result { } // 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)?; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index efcb1912185b9..d1691ee5a6e74 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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}")); } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index a862d23226139..cb183f7038243 100644 --- a/kani-driver/src/harness_runner.rs +++ b/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>> { + harnesses: &'pr [&HarnessMetadata], + ) -> Result>> { 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>> { + let results = pool.install(|| -> Result>> { sorted_harnesses .par_iter() - .map(|harness| -> Result> { + .map(|harness| -> Result> { 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" + ), + }; } } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index fcc283e8cc3f6..8e5c31925fe8c 100644 --- a/kani-driver/src/main.rs +++ b/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) diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 4030b48983000..b6f84c0e7d74d 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -1,13 +1,14 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{bail, Result}; +use anyhow::Result; use std::path::Path; +use tracing::debug; use kani_metadata::{ HarnessMetadata, InternedString, KaniMetadata, TraitDefinedMethod, VtableCtxResults, }; -use std::collections::HashMap; +use std::collections::{BTreeSet, HashMap}; use std::fs::File; use std::io::{BufReader, BufWriter}; @@ -109,16 +110,22 @@ pub fn merge_kani_metadata(files: Vec) -> KaniMetadata { impl KaniSession { /// Determine which function to use as entry point, based on command-line arguments and kani-metadata. - pub fn determine_targets( + pub fn determine_targets<'a>( &self, - all_harnesses: &[&HarnessMetadata], - ) -> Result> { - if let Some(name) = self.args.harness.clone().or(self.args.function.clone()) { - // Linear search, since this is only ever called once - let harness = find_proof_harness(&name, all_harnesses)?; - return Ok(vec![harness.clone()]); + all_harnesses: &[&'a HarnessMetadata], + ) -> Result> { + let harnesses = if self.args.harnesses.is_empty() { + BTreeSet::from_iter(self.args.function.iter()) + } else { + BTreeSet::from_iter(self.args.harnesses.iter()) + }; + + if harnesses.is_empty() { + Ok(Vec::from(all_harnesses)) + } else { + let harnesses = find_proof_harnesses(harnesses, all_harnesses); + Ok(harnesses) } - Ok(all_harnesses.iter().map(|md| (*md).clone()).collect()) } } @@ -126,8 +133,8 @@ impl KaniSession { /// appearing harnesses get processed earlier. /// This is necessary for the concrete playback feature (with in-place unit test modification) /// because it guarantees that injected unit tests will not change the location of to-be-processed harnesses. -pub fn sort_harnesses_by_loc(harnesses: &[HarnessMetadata]) -> Vec<&HarnessMetadata> { - let mut harnesses_clone: Vec<_> = harnesses.iter().by_ref().collect(); +pub fn sort_harnesses_by_loc<'a>(harnesses: &[&'a HarnessMetadata]) -> Vec<&'a HarnessMetadata> { + let mut harnesses_clone = harnesses.to_vec(); harnesses_clone.sort_unstable_by(|harness1, harness2| { harness1 .original_file @@ -158,40 +165,22 @@ pub fn mock_proof_harness( /// Search for a proof harness with a particular name. /// At the present time, we use `no_mangle` so collisions shouldn't happen, /// but this function is written to be robust against that changing in the future. -fn find_proof_harness<'a>( - name: &str, - harnesses: &'a [&HarnessMetadata], -) -> Result<&'a HarnessMetadata> { - let mut result: Option<&'a HarnessMetadata> = None; - for h in harnesses.iter() { - // Either an exact match, or... - let matches = h.pretty_name == *name || { - // pretty_name will be things like `module::submodule::name_of_function` - // and we want people to be able to specify `--harness name_of_function` - if let Some(prefix) = h.pretty_name.strip_suffix(name) { - prefix.ends_with("::") - } else { - false - } - }; - if matches { - if let Some(other) = result { - bail!( - "Conflicting proof harnesses named {}:\n {}\n {}", - name, - other.pretty_name, - h.pretty_name - ); - } else { - result = Some(h); - } +fn find_proof_harnesses<'a>( + targets: BTreeSet<&String>, + all_harnesses: &[&'a HarnessMetadata], +) -> Vec<&'a HarnessMetadata> { + debug!(?targets, "find_proof_harness"); + let mut result = vec![]; + for md in all_harnesses.iter() { + // Either an exact match, or a substring match. We check the exact first since it's cheaper. + if targets.contains(&md.pretty_name) + || targets.contains(&md.get_harness_name_unqualified().to_string()) + || targets.iter().any(|target| md.pretty_name.contains(*target)) + { + result.push(*md); } } - if let Some(x) = result { - Ok(x) - } else { - bail!("A proof harness named {} was not found", name); - } + result } #[cfg(test)] @@ -206,13 +195,24 @@ mod tests { mock_proof_harness("module::not_check_three", None, None), ]; let ref_harnesses = harnesses.iter().collect::>(); - assert!(find_proof_harness("check_three", &ref_harnesses).is_err()); + assert_eq!( + find_proof_harnesses(BTreeSet::from([&"check_three".to_string()]), &ref_harnesses) + .len(), + 1 + ); assert!( - find_proof_harness("check_two", &ref_harnesses).unwrap().mangled_name + find_proof_harnesses(BTreeSet::from([&"check_two".to_string()]), &ref_harnesses) + .first() + .unwrap() + .mangled_name == "module::check_two" ); assert!( - find_proof_harness("check_one", &ref_harnesses).unwrap().mangled_name == "check_one" + find_proof_harnesses(BTreeSet::from([&"check_one".to_string()]), &ref_harnesses) + .first() + .unwrap() + .mangled_name + == "check_one" ); } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 90d3015c3bca7..0ec31d3a31cda 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -8,7 +8,7 @@ use std::path::PathBuf; /// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find. #[derive(Debug, Clone, Serialize, Deserialize)] pub struct HarnessMetadata { - /// The name the user gave to the function. + /// The fully qualified name the user gave to the function (i.e. includes the module path). pub pretty_name: String, /// The name of the function in the CBMC symbol table. pub mangled_name: String, diff --git a/tests/cargo-kani/simple-proof-annotation/main.expected b/tests/cargo-kani/simple-proof-annotation/main.expected index 7fca8f525e17d..1a0db0160d5cc 100644 --- a/tests/cargo-kani/simple-proof-annotation/main.expected +++ b/tests/cargo-kani/simple-proof-annotation/main.expected @@ -1 +1 @@ -error: A proof harness named main was not found +error: no harnesses matched the harness filter: `main` diff --git a/tests/cargo-ui/multiple-harnesses/Cargo.toml b/tests/cargo-ui/multiple-harnesses/Cargo.toml new file mode 100644 index 0000000000000..1e3c9d87f8dc8 --- /dev/null +++ b/tests/cargo-ui/multiple-harnesses/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "harnesses" +version = "0.1.0" +edition = "2021" + +[dependencies] + +[package.metadata.kani.flags] +harness = ["foo", "bar"] diff --git a/tests/cargo-ui/multiple-harnesses/expected b/tests/cargo-ui/multiple-harnesses/expected new file mode 100644 index 0000000000000..d31fc64ada834 --- /dev/null +++ b/tests/cargo-ui/multiple-harnesses/expected @@ -0,0 +1,3 @@ +Checking harness bar... +Checking harness foo... +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/cargo-ui/multiple-harnesses/src/lib.rs b/tests/cargo-ui/multiple-harnesses/src/lib.rs new file mode 100644 index 0000000000000..cab063cd1b259 --- /dev/null +++ b/tests/cargo-ui/multiple-harnesses/src/lib.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test checks if we can specify multiple harnesses in the Cargo.toml file. + +#[kani::proof] +pub fn foo() { + assert_eq!(1 + 2, 3); +} + +#[kani::proof] +pub fn bar() { + assert_ne!(2, 3); +} diff --git a/tests/expected/function-stubbing-no-harness/expected b/tests/expected/function-stubbing-no-harness/expected index a9a9341e27267..47dea3fe757d2 100644 --- a/tests/expected/function-stubbing-no-harness/expected +++ b/tests/expected/function-stubbing-no-harness/expected @@ -1 +1 @@ -error: A proof harness named foo was not found +error: no harnesses matched the harness filter: `foo` diff --git a/tests/ui/multiple-harnesses/expected b/tests/ui/multiple-harnesses/check_all/expected similarity index 100% rename from tests/ui/multiple-harnesses/expected rename to tests/ui/multiple-harnesses/check_all/expected diff --git a/tests/ui/multiple-harnesses/test.rs b/tests/ui/multiple-harnesses/check_all/test.rs similarity index 100% rename from tests/ui/multiple-harnesses/test.rs rename to tests/ui/multiple-harnesses/check_all/test.rs diff --git a/tests/ui/multiple-harnesses/check_some/expected b/tests/ui/multiple-harnesses/check_some/expected new file mode 100644 index 0000000000000..e4069333d590d --- /dev/null +++ b/tests/ui/multiple-harnesses/check_some/expected @@ -0,0 +1,3 @@ +Checking harness check_first_harness... +Checking harness check_second_harness... +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/ui/multiple-harnesses/check_some/select_harnesses.rs b/tests/ui/multiple-harnesses/check_some/select_harnesses.rs new file mode 100644 index 0000000000000..d2e24c4ccb34a --- /dev/null +++ b/tests/ui/multiple-harnesses/check_some/select_harnesses.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness check_first_harness --harness check_second_harness +//! Ensure that we can select multiple harnesses at a time. +#[kani::proof] +fn check_first_harness() { + assert!(1 == 1); +} + +#[kani::proof] +fn check_second_harness() { + assert!(2 == 2); +} + +/// A harness that will fail verification if it is run. +#[kani::proof] +fn ignore_third_harness() { + assert!(3 == 2); +} diff --git a/tests/ui/multiple-harnesses/multiple_matches/expected b/tests/ui/multiple-harnesses/multiple_matches/expected new file mode 100644 index 0000000000000..7aadd93cdb530 --- /dev/null +++ b/tests/ui/multiple-harnesses/multiple_matches/expected @@ -0,0 +1,5 @@ +Checking harness second::verify_harness... +Checking harness second::verify_blah... +Checking harness second::verify_foo... +Checking harness first::check_foo... +Complete - 4 successfully verified harnesses, 0 failures, 4 total. diff --git a/tests/ui/multiple-harnesses/multiple_matches/select_harnesses.rs b/tests/ui/multiple-harnesses/multiple_matches/select_harnesses.rs new file mode 100644 index 0000000000000..250bfdef7597f --- /dev/null +++ b/tests/ui/multiple-harnesses/multiple_matches/select_harnesses.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness second --harness foo +//! Ensure that the set of harnesses run is the union of all arguments. + +mod first { + #[kani::proof] + fn check_foo() { + assert!(1 == 1); + } + + #[kani::proof] + fn check_blah() { + assert!(2 == 2); + } + + /// A harness that will fail verification if it is run. + #[kani::proof] + fn ignore_third_harness() { + assert!(3 == 2); + } +} + +mod second { + #[kani::proof] + fn verify_foo() { + assert!(1 == 1); + } + + #[kani::proof] + fn verify_blah() { + assert!(2 == 2); + } + + #[kani::proof] + fn verify_harness() { + assert!(3 == 3); + } +} diff --git a/tests/ui/multiple-harnesses/no_matching_harness/expected b/tests/ui/multiple-harnesses/no_matching_harness/expected new file mode 100644 index 0000000000000..d0eb27af10f8c --- /dev/null +++ b/tests/ui/multiple-harnesses/no_matching_harness/expected @@ -0,0 +1 @@ +error: no harnesses matched the harness filters: `non_existing`, `invalid` diff --git a/tests/ui/multiple-harnesses/no_matching_harness/non_matching.rs b/tests/ui/multiple-harnesses/no_matching_harness/non_matching.rs new file mode 100644 index 0000000000000..2c3e5d5ffa886 --- /dev/null +++ b/tests/ui/multiple-harnesses/no_matching_harness/non_matching.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness non_existing --harness invalid +//! Check that we just ignore non-matching filters + +/// A harness that will fail verification if it is run. +#[kani::proof] +fn ignored_harness() { + assert!(3 == 2); +} diff --git a/tests/ui/multiple-harnesses/some_matching_harnesses/expected b/tests/ui/multiple-harnesses/some_matching_harnesses/expected new file mode 100644 index 0000000000000..08b81d02e429c --- /dev/null +++ b/tests/ui/multiple-harnesses/some_matching_harnesses/expected @@ -0,0 +1,3 @@ +Checking harness existing_harness... +Checking harness existing... +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/ui/multiple-harnesses/some_matching_harnesses/subset.rs b/tests/ui/multiple-harnesses/some_matching_harnesses/subset.rs new file mode 100644 index 0000000000000..662ca3a192a8e --- /dev/null +++ b/tests/ui/multiple-harnesses/some_matching_harnesses/subset.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness existing --harness non_existing --harness invalid +//! Check that we just ignore non-matching filters +#[kani::proof] +fn existing() { + assert!(1 == 1); +} + +#[kani::proof] +fn existing_harness() { + assert!(2 == 2); +} + +/// A harness that will fail verification if it is run. +#[kani::proof] +fn ignored_harness() { + assert!(3 == 2); +} diff --git a/tests/ui/stubbing-unsupported-multiple-harness/expected b/tests/ui/stubbing-unsupported-multiple-harness/expected new file mode 100644 index 0000000000000..dd50480542547 --- /dev/null +++ b/tests/ui/stubbing-unsupported-multiple-harness/expected @@ -0,0 +1 @@ +error: Failed to apply stubs. Harnesses with stubs must be verified separately. Found: `check_no_stub`, `check_stub_bar`, `check_stub_foo` diff --git a/tests/ui/stubbing-unsupported-multiple-harness/stub_harnesses.rs b/tests/ui/stubbing-unsupported-multiple-harness/stub_harnesses.rs new file mode 100644 index 0000000000000..f83dc309277e6 --- /dev/null +++ b/tests/ui/stubbing-unsupported-multiple-harness/stub_harnesses.rs @@ -0,0 +1,34 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: --harness check --enable-unstable --enable-stubbing +// +//! This tests whether we provide a user friendly error if more than one harness has stubs + +fn foo(b: bool) { + assert!(b); +} + +fn bar(b: bool) { + assert!(!b); +} + +/// Harness should succeed if stub has been applied and fail otherwise. +#[kani::proof] +#[kani::stub(foo, bar)] +fn check_stub_foo() { + foo(false) +} + +/// Harness should succeed if stub has been applied and fail otherwise. +#[kani::proof] +#[kani::stub(bar, foo)] +fn check_stub_bar() { + bar(true) +} + +#[kani::proof] +fn check_no_stub() { + foo(true); + bar(false); +}