diff --git a/docs/src/kani-single-file.md b/docs/src/kani-single-file.md index 90b92b94467f..96081bcff3af 100644 --- a/docs/src/kani-single-file.md +++ b/docs/src/kani-single-file.md @@ -22,9 +22,9 @@ kani filenames.rs --visualize --cbmc-args --object-bits 11 --unwind 15 **`--visualize`** will generate a report in the local directory accessible through `report/html/index.html`. This report will shows coverage information, as well as give traces for each failure Kani finds. -**`--function `** Kani defaults to assuming the starting function is called `main`. -You can change it to a different function with this argument. -Note that to "find" the function given, it needs to be given the `#[kani::proof]` annotation. +**`--harness `** Kani defaults to checking all proof harnesses. +You can switch to checking just one harness using this flag. +Proof harnesses are functions that have been given the `#[kani::proof]` annotation. **`--gen-c`** will generate a C file that roughly corresponds to the input Rust file. This can sometimes be helpful when trying to debug a problem with Kani. diff --git a/docs/src/tutorial-first-steps.md b/docs/src/tutorial-first-steps.md index d9078697bf18..85675e9bed5d 100644 --- a/docs/src/tutorial-first-steps.md +++ b/docs/src/tutorial-first-steps.md @@ -185,7 +185,7 @@ Fortunately, Kani is able to report a coverage metric for each proof harness. Try running: ``` -kani --visualize src/final_form.rs --function verify_success +kani --visualize src/final_form.rs --harness verify_success open report/html/index.html ``` diff --git a/docs/src/tutorial-kinds-of-failure.md b/docs/src/tutorial-kinds-of-failure.md index 035edb7108c3..2908664d770e 100644 --- a/docs/src/tutorial-kinds-of-failure.md +++ b/docs/src/tutorial-kinds-of-failure.md @@ -43,7 +43,7 @@ But we're able to check this unsafe code with Kani: ``` ``` -# kani src/bounds_check.rs --function bound_check +# kani src/bounds_check.rs --harness bound_check [...] ** 15 of 448 failed [...] @@ -56,7 +56,7 @@ Kani is inserting a lot more checks than appear as asserts in our code, so the o Let's narrow that output down a bit: ``` -# kani src/bounds_check.rs --function bound_check | grep Failed +# kani src/bounds_check.rs --harness bound_check | grep Failed Failed Checks: attempt to compute offset which would overflow Failed Checks: attempt to calculate the remainder with a divisor of zero Failed Checks: attempt to add with overflow @@ -92,7 +92,7 @@ Consider trying a few more small exercises with this example: Having switched back to the safe indexing operation, Kani reports two failures: ``` -# kani src/bounds_check.rs --function bound_check | grep Failed +# kani src/bounds_check.rs --harness bound_check | grep Failed Failed Checks: index out of bounds: the length is less than or equal to the given index Failed Checks: dereference failure: pointer outside object bounds ``` @@ -176,7 +176,7 @@ Kani will find these failures as well. Here's the output from Kani: ``` -# kani src/overflow.rs --function add_overflow +# kani src/overflow.rs --harness add_overflow [...] RESULTS: Check 1: simple_addition.assertion.1 diff --git a/docs/src/tutorial-nondeterministic-variables.md b/docs/src/tutorial-nondeterministic-variables.md index aca8a59dc62a..cbc4e663d975 100644 --- a/docs/src/tutorial-nondeterministic-variables.md +++ b/docs/src/tutorial-nondeterministic-variables.md @@ -32,7 +32,7 @@ You can try it out by running the example under [arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): ``` -cargo kani --function safe_update +cargo kani --harness safe_update ``` ## Unsafe nondeterministic variables @@ -57,7 +57,7 @@ The compiler is able to represent `Option` using `32` bits by using You can try it out by running the example under [arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): ``` -cargo kani --function unsafe_update +cargo kani --harness unsafe_update ``` ## Safe nondeterministic variables for custom types @@ -88,5 +88,5 @@ You can try it out by running the example under [`docs/src/tutorial/arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/): ``` -cargo kani --function check_rating +cargo kani --harness check_rating ``` diff --git a/src/cargo-kani/src/args.rs b/src/cargo-kani/src/args.rs index 61d3eacfb250..f026f1d21f8a 100644 --- a/src/cargo-kani/src/args.rs +++ b/src/cargo-kani/src/args.rs @@ -72,9 +72,14 @@ pub struct KaniArgs { #[structopt(flatten)] pub checks: CheckArgs, - /// Entry point for verification - #[structopt(long, default_value = "main")] - pub function: String, + /// Entry point for verification (symbol name) + #[structopt(long, hidden = true)] + pub function: Option, + /// Entry point for verification (proof harness) + // In a dry-run, we don't have kani-metadata.json to read, so we can't use this flag + #[structopt(long, conflicts_with = "function", conflicts_with = "dry-run")] + pub harness: Option, + /// Link external C files referenced by Rust code. /// This is an experimental feature. #[structopt(long, parse(from_os_str), hidden = true)] @@ -286,6 +291,14 @@ impl KaniArgs { ) .exit(); } + + if self.cbmc_args.contains(&OsString::from("--function")) { + Error::with_description( + "Invalid flag: --function should be provided to Kani directly, not via --cbmc-args.", + ErrorKind::ArgumentConflict, + ) + .exit(); + } } } @@ -317,4 +330,13 @@ mod tests { assert_eq!(t, format!("{}", AbstractionType::from_str(t).unwrap())); } } + + #[test] + fn check_dry_run_harness_conflicts() { + // harness needs metadata which we don't have with dry-run + let args = vec!["kani", "file.rs", "--dry-run", "--harness", "foo"]; + let app = StandaloneArgs::clap(); + let err = app.get_matches_from_safe(args).unwrap_err(); + assert!(err.kind == ErrorKind::ArgumentConflict); + } } diff --git a/src/cargo-kani/src/call_cargo.rs b/src/cargo-kani/src/call_cargo.rs index b24e32667628..7ea334f4987c 100644 --- a/src/cargo-kani/src/call_cargo.rs +++ b/src/cargo-kani/src/call_cargo.rs @@ -3,7 +3,7 @@ use anyhow::{Context, Result}; use std::ffi::OsString; -use std::path::PathBuf; +use std::path::{Path, PathBuf}; use std::process::Command; use crate::session::KaniSession; @@ -17,6 +17,8 @@ pub struct CargoOutputs { pub symtabs: Vec, /// The location of vtable restrictions files (a directory of *.restrictions.json) pub restrictions: Option, + /// The kani-metadata.json files written by kani-compiler. + pub metadata: Vec, } impl KaniSession { @@ -44,7 +46,7 @@ impl KaniSession { args.push(build_target.into()); args.push("--target-dir".into()); - args.push(target_dir.clone().into()); + args.push(target_dir.into()); if self.args.verbose { args.push("-v".into()); @@ -59,26 +61,26 @@ impl KaniSession { self.run_terminal(cmd)?; if self.args.dry_run { - // mock an answer + // mock an answer: mostly the same except we don't/can't expand the globs return Ok(CargoOutputs { outdir: outdir.clone(), - symtabs: vec![outdir.join("dry-run.symtab.json")], + symtabs: vec![outdir.join("*.symtab.json")], + metadata: vec![outdir.join("*.kani-metadata.json")], restrictions: self.args.restrict_vtable().then(|| outdir), }); } - let symtabs = glob(&outdir.join("*.symtab.json")); - Ok(CargoOutputs { outdir: outdir.clone(), - symtabs: symtabs?, + symtabs: glob(&outdir.join("*.symtab.json"))?, + metadata: glob(&outdir.join("*.kani-metadata.json"))?, restrictions: self.args.restrict_vtable().then(|| outdir), }) } } /// Given a `path` with glob characters in it (e.g. `*.json`), return a vector of matching files -fn glob(path: &PathBuf) -> Result> { +fn glob(path: &Path) -> Result> { let results = glob::glob(path.to_str().context("Non-UTF-8 path enountered")?)?; // the logic to turn "Iter>" into "Result, E>" doesn't play well // with anyhow, so a type annotation is required diff --git a/src/cargo-kani/src/call_cbmc_viewer.rs b/src/cargo-kani/src/call_cbmc_viewer.rs index 681f0c26a89c..461fc34734c9 100644 --- a/src/cargo-kani/src/call_cbmc_viewer.rs +++ b/src/cargo-kani/src/call_cbmc_viewer.rs @@ -12,7 +12,7 @@ use crate::util::alter_extension; impl KaniSession { /// Run CBMC appropriately to produce 3 output XML files, then run cbmc-viewer on them to produce a report. /// Viewer doesn't give different error codes depending on verification failure, so as long as it works, we report success. - pub fn run_visualize(&self, file: &Path, default_reportdir: &str) -> Result<()> { + pub fn run_visualize(&self, file: &Path, report_dir: &Path) -> Result<()> { let results_filename = alter_extension(file, "results.xml"); let coverage_filename = alter_extension(file, "coverage.xml"); let property_filename = alter_extension(file, "property.xml"); @@ -28,12 +28,6 @@ impl KaniSession { self.cbmc_variant(file, &["--xml-ui", "--cover", "location"], &coverage_filename)?; self.cbmc_variant(file, &["--xml-ui", "--show-properties"], &property_filename)?; - let reportdir = if let Some(pb) = &self.args.target_dir { - pb.join("report").into_os_string() - } else { - default_reportdir.into() - }; - let args: Vec = vec![ "--result".into(), results_filename.into(), @@ -48,7 +42,7 @@ impl KaniSession { "--goto".into(), file.into(), "--reportdir".into(), - reportdir.clone(), + report_dir.into(), ]; // TODO get cbmc-viewer path from self @@ -59,7 +53,7 @@ impl KaniSession { // Let the user know if !self.args.quiet { - println!("Report written to: {}/html/index.html", reportdir.to_string_lossy()); + println!("Report written to: {}/html/index.html", report_dir.to_string_lossy()); } Ok(()) diff --git a/src/cargo-kani/src/call_goto_instrument.rs b/src/cargo-kani/src/call_goto_instrument.rs index 8e0d5fc46219..adf751977c80 100644 --- a/src/cargo-kani/src/call_goto_instrument.rs +++ b/src/cargo-kani/src/call_goto_instrument.rs @@ -6,14 +6,10 @@ use std::ffi::OsString; use std::path::Path; use std::process::Command; +use crate::metadata::collect_and_link_function_pointer_restrictions; use crate::session::KaniSession; use crate::util::alter_extension; -use kani_metadata::{InternedString, TraitDefinedMethod, VtableCtxResults}; -use std::collections::HashMap; -use std::fs::File; -use std::io::{BufReader, BufWriter}; - impl KaniSession { /// Postprocess a goto binary (before cbmc, after linking) in-place by calling goto-instrument pub fn run_goto_instrument(&self, input: &Path, output: &Path, function: &str) -> Result<()> { @@ -28,6 +24,9 @@ impl KaniSession { } if self.args.gen_c { + if !self.args.quiet { + println!("Generated C code written to {}", output.to_string_lossy()); + } self.gen_c(output)?; } @@ -124,77 +123,3 @@ impl KaniSession { self.run_suppress(cmd) } } - -/// Collect all vtable restriction metadata together, and write one combined output in CBMC's format -fn link_function_pointer_restrictions( - data_per_crate: Vec, - output_filename: &Path, -) -> Result<()> { - // Combine all method possibilities into one global mapping - let mut combined_possible_methods: HashMap> = - HashMap::new(); - for crate_data in &data_per_crate { - for entry in &crate_data.possible_methods { - combined_possible_methods - .insert(entry.trait_method.clone(), entry.possibilities.clone()); - } - } - - // Emit a restriction for every call site - let mut output = HashMap::new(); - for crate_data in data_per_crate { - for call_site in crate_data.call_sites { - // CBMC Now supports referencing callsites by label: - // https://github.com/diffblue/cbmc/pull/6508 - let cbmc_call_site_name = format!("{}.{}", call_site.function_name, call_site.label); - let trait_def = call_site.trait_method; - - // Look up all possibilities, defaulting to the empty set - let possibilities = - combined_possible_methods.get(&trait_def).unwrap_or(&vec![]).clone(); - output.insert(cbmc_call_site_name, possibilities); - } - } - - let f = File::create(output_filename)?; - let f = BufWriter::new(f); - serde_json::to_writer(f, &output)?; - Ok(()) -} - -/// From either a file or a path with multiple files, output the CBMC restrictions file we should use. -fn collect_and_link_function_pointer_restrictions( - path: &Path, - output_filename: &Path, -) -> Result<()> { - let md = std::fs::metadata(path)?; - - // Fill with data from all files in that path with the expected suffix - let mut per_crate_restrictions = Vec::new(); - - if md.is_dir() { - for element in path.read_dir()? { - let path = element?.path(); - if path.as_os_str().to_str().unwrap().ends_with(".restrictions.json") { - let restrictions = read_restrictions(&path)?; - per_crate_restrictions.push(restrictions); - } - } - } else if md.is_file() { - assert!(path.as_os_str().to_str().unwrap().ends_with(".restrictions.json")); - let restrictions = read_restrictions(path)?; - per_crate_restrictions.push(restrictions); - } else { - unreachable!("Path must be restrcitions file or directory containing restrictions files") - } - - link_function_pointer_restrictions(per_crate_restrictions, output_filename) -} - -/// Deserialize a *.restrictions.json file -fn read_restrictions(path: &Path) -> Result { - let file = File::open(path)?; - let reader = BufReader::new(file); - let restrictions = serde_json::from_reader(reader)?; - Ok(restrictions) -} diff --git a/src/cargo-kani/src/call_single_file.rs b/src/cargo-kani/src/call_single_file.rs index 9cfa83375de0..4c19ed94c342 100644 --- a/src/cargo-kani/src/call_single_file.rs +++ b/src/cargo-kani/src/call_single_file.rs @@ -18,6 +18,8 @@ pub struct SingleOutputs { pub symtab: PathBuf, /// The vtable restrictions files, if any. pub restrictions: Option, + /// The kani-metadata.json file written by kani-compiler. + pub metadata: PathBuf, } impl KaniSession { @@ -34,7 +36,7 @@ impl KaniSession { let mut temps = self.temporaries.borrow_mut(); temps.push(output_filename.clone()); temps.push(typemap_filename); - temps.push(metadata_filename); + temps.push(metadata_filename.clone()); if self.args.restrict_vtable() { temps.push(restrictions_filename.clone()); } @@ -55,11 +57,11 @@ impl KaniSession { args.push(t); } } else { - if self.args.function != "main" { - // Unless entry function for proof harness is main, compile code as lib. - // This ensures that rustc won't prune functions that are not reachable - // from main as well as enable compilation of crates that don't have a main - // function. + // If we specifically request "--function main" then don't override crate type + if Some("main".to_string()) != self.args.function { + // We only run against proof harnesses normally, and this change + // 1. Means we do not require a `fn main` to exist + // 2. Don't forget it also changes visibility rules. args.push("--crate-type".into()); args.push("lib".into()); } @@ -80,6 +82,7 @@ impl KaniSession { Ok(SingleOutputs { outdir, symtab: output_filename, + metadata: metadata_filename, restrictions: if self.args.restrict_vtable() { Some(restrictions_filename) } else { diff --git a/src/cargo-kani/src/main.rs b/src/cargo-kani/src/main.rs index a294ae4878cf..24b478078c70 100644 --- a/src/cargo-kani/src/main.rs +++ b/src/cargo-kani/src/main.rs @@ -4,9 +4,12 @@ use anyhow::Result; use args_toml::join_args; use call_cbmc::VerificationStatus; +use kani_metadata::HarnessMetadata; +use session::KaniSession; use std::ffi::OsString; -use std::path::PathBuf; +use std::path::{Path, PathBuf}; use structopt::StructOpt; +use util::append_path; mod args; mod args_toml; @@ -18,6 +21,7 @@ mod call_goto_cc; mod call_goto_instrument; mod call_single_file; mod call_symtab; +mod metadata; mod session; mod util; @@ -49,21 +53,25 @@ fn cargokani_main(input_args: Vec) -> Result<()> { ctx.apply_vtable_restrictions(&linked_obj, &restrictions)?; } - let specialized_obj = outputs.outdir.join(format!("cbmc-for-{}.out", &ctx.args.function)); - ctx.run_goto_instrument(&linked_obj, &specialized_obj, &ctx.args.function)?; + let metadata = ctx.collect_kani_metadata(&outputs.metadata)?; + let harnesses = ctx.determine_targets(&metadata)?; + let report_base = ctx.args.target_dir.clone().unwrap_or(PathBuf::from("target")); - if ctx.args.visualize { - ctx.run_visualize(&specialized_obj, "target/report")?; - } else { - let result = ctx.run_cbmc(&specialized_obj)?; + let mut failed_harnesses: Vec<&HarnessMetadata> = Vec::new(); + + for harness in &harnesses { + let harness_filename = harness.pretty_name.replace("::", "-"); + let report_dir = report_base.join(format!("report-{}", harness_filename)); + let specialized_obj = outputs.outdir.join(format!("cbmc-for-{}.out", harness_filename)); + ctx.run_goto_instrument(&linked_obj, &specialized_obj, &harness.mangled_name)?; + + let result = ctx.check_harness(&specialized_obj, &report_dir, &harness)?; if result == VerificationStatus::Failure { - // Failure exit code without additional error message - drop(ctx); - std::process::exit(1); + failed_harnesses.push(&harness); } } - Ok(()) + ctx.print_final_summary(&harnesses, &failed_harnesses) } fn standalone_main() -> Result<()> { @@ -72,6 +80,9 @@ fn standalone_main() -> Result<()> { let ctx = session::KaniSession::new(args.common_opts)?; let outputs = ctx.compile_single_rust_file(&args.input)?; + if ctx.args.only_codegen { + return Ok(()); + } let goto_obj = ctx.symbol_table_to_gotoc(&outputs.symtab)?; let linked_obj = util::alter_extension(&args.input, "out"); @@ -83,20 +94,81 @@ fn standalone_main() -> Result<()> { if let Some(restriction) = outputs.restrictions { ctx.apply_vtable_restrictions(&linked_obj, &restriction)?; } - ctx.run_goto_instrument(&linked_obj, &linked_obj, &ctx.args.function)?; - if ctx.args.visualize { - ctx.run_visualize(&linked_obj, "report")?; - } else { - let result = ctx.run_cbmc(&linked_obj)?; + let metadata = ctx.collect_kani_metadata(&[outputs.metadata])?; + let harnesses = ctx.determine_targets(&metadata)?; + let report_base = ctx.args.target_dir.clone().unwrap_or(PathBuf::from(".")); + + let mut failed_harnesses: Vec<&HarnessMetadata> = Vec::new(); + + for harness in &harnesses { + let harness_filename = harness.pretty_name.replace("::", "-"); + let report_dir = report_base.join(format!("report-{}", harness_filename)); + let specialized_obj = append_path(&linked_obj, &format!("-for-{}", harness_filename)); + { + let mut temps = ctx.temporaries.borrow_mut(); + temps.push(specialized_obj.to_owned()); + } + ctx.run_goto_instrument(&linked_obj, &specialized_obj, &harness.mangled_name)?; + + let result = ctx.check_harness(&specialized_obj, &report_dir, &harness)?; if result == VerificationStatus::Failure { + failed_harnesses.push(&harness); + } + } + + ctx.print_final_summary(&harnesses, &failed_harnesses) +} + +impl KaniSession { + fn check_harness( + &self, + binary: &Path, + report_dir: &Path, + harness: &HarnessMetadata, + ) -> Result { + if !self.args.quiet { + println!("Checking harness {}...", harness.pretty_name); + } + + if self.args.visualize { + self.run_visualize(&binary, &report_dir)?; + // Strictly speaking, we're faking success here. This is more "no error" + Ok(VerificationStatus::Success) + } else { + self.run_cbmc(&binary) + } + } + + fn print_final_summary( + self, + harnesses: &[HarnessMetadata], + failed_harnesses: &[&HarnessMetadata], + ) -> Result<()> { + if !self.args.quiet && !self.args.visualize && harnesses.len() > 1 { + if !failed_harnesses.is_empty() { + println!("Summary:"); + } + for harness in failed_harnesses.iter() { + println!("Verification failed for - {}", harness.pretty_name); + } + + println!( + "Complete - {} successfully verified harnesses, {} failures, {} total.", + harnesses.len() - failed_harnesses.len(), + failed_harnesses.len(), + harnesses.len() + ); + } + + if !failed_harnesses.is_empty() { // Failure exit code without additional error message - drop(ctx); + drop(self); std::process::exit(1); } - } - Ok(()) + Ok(()) + } } #[derive(Debug, PartialEq)] diff --git a/src/cargo-kani/src/metadata.rs b/src/cargo-kani/src/metadata.rs new file mode 100644 index 000000000000..8321d3e30b1c --- /dev/null +++ b/src/cargo-kani/src/metadata.rs @@ -0,0 +1,210 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use anyhow::{bail, Result}; +use std::path::{Path, PathBuf}; + +use kani_metadata::{ + HarnessMetadata, InternedString, KaniMetadata, TraitDefinedMethod, VtableCtxResults, +}; +use std::collections::HashMap; +use std::fs::File; +use std::io::{BufReader, BufWriter}; + +use crate::session::KaniSession; + +/// From either a file or a path with multiple files, output the CBMC restrictions file we should use. +pub fn collect_and_link_function_pointer_restrictions( + path: &Path, + output_filename: &Path, +) -> Result<()> { + let md = std::fs::metadata(path)?; + + // Fill with data from all files in that path with the expected suffix + let mut per_crate_restrictions = Vec::new(); + + if md.is_dir() { + for element in path.read_dir()? { + let path = element?.path(); + if path.as_os_str().to_str().unwrap().ends_with(".restrictions.json") { + let restrictions = read_restrictions(&path)?; + per_crate_restrictions.push(restrictions); + } + } + } else if md.is_file() { + assert!(path.as_os_str().to_str().unwrap().ends_with(".restrictions.json")); + let restrictions = read_restrictions(path)?; + per_crate_restrictions.push(restrictions); + } else { + unreachable!("Path must be restrcitions file or directory containing restrictions files") + } + + link_function_pointer_restrictions(per_crate_restrictions, output_filename) +} + +/// Collect all vtable restriction metadata together, and write one combined output in CBMC's format +fn link_function_pointer_restrictions( + data_per_crate: Vec, + output_filename: &Path, +) -> Result<()> { + // Combine all method possibilities into one global mapping + let mut combined_possible_methods: HashMap> = + HashMap::new(); + for crate_data in &data_per_crate { + for entry in &crate_data.possible_methods { + combined_possible_methods + .insert(entry.trait_method.clone(), entry.possibilities.clone()); + } + } + + // Emit a restriction for every call site + let mut output = HashMap::new(); + for crate_data in data_per_crate { + for call_site in crate_data.call_sites { + // CBMC Now supports referencing callsites by label: + // https://github.com/diffblue/cbmc/pull/6508 + let cbmc_call_site_name = format!("{}.{}", call_site.function_name, call_site.label); + let trait_def = call_site.trait_method; + + // Look up all possibilities, defaulting to the empty set + let possibilities = + combined_possible_methods.get(&trait_def).unwrap_or(&vec![]).clone(); + output.insert(cbmc_call_site_name, possibilities); + } + } + + let f = File::create(output_filename)?; + let f = BufWriter::new(f); + serde_json::to_writer(f, &output)?; + Ok(()) +} + +/// Deserialize a *.restrictions.json file +fn read_restrictions(path: &Path) -> Result { + let file = File::open(path)?; + let reader = BufReader::new(file); + let restrictions = serde_json::from_reader(reader)?; + Ok(restrictions) +} + +/// Deserialize a *.restrictions.json file +fn read_kani_metadata(path: &Path) -> Result { + let file = File::open(path)?; + let reader = BufReader::new(file); + let restrictions = serde_json::from_reader(reader)?; + Ok(restrictions) +} + +/// Consumes a vector of parsed metadata, and produces a combined structure +fn merge_kani_metadata(files: Vec) -> KaniMetadata { + let mut result = KaniMetadata { proof_harnesses: Vec::new() }; + for md in files { + // Note that we're taking ownership of the original vec, and so we can move the data into the new data structure. + result.proof_harnesses.extend(md.proof_harnesses); + } + result +} + +impl KaniSession { + /// Reads a collection of kani-metadata.json files and merges the results. + pub fn collect_kani_metadata(&self, files: &[PathBuf]) -> Result { + if self.args.dry_run { + // Mock an answer + Ok(KaniMetadata { proof_harnesses: vec![] }) + } else { + // TODO: one possible future improvement here would be to return some kind of Lazy + // value, that only computes this metadata if it turns out we need it. + let results: Result, _> = files.iter().map(|x| read_kani_metadata(x)).collect(); + Ok(merge_kani_metadata(results?)) + } + } + + /// Determine which function to use as entry point, based on command-line arguments and kani-metadata. + pub fn determine_targets(&self, metadata: &KaniMetadata) -> Result> { + if let Some(name) = &self.args.function { + // --function is untranslated, create a mock harness + return Ok(vec![mock_proof_harness(name)]); + } + if let Some(name) = &self.args.harness { + // Linear search, since this is only ever called once + let harness = find_proof_harness(name, &metadata.proof_harnesses)?; + return Ok(vec![harness.clone()]); + } + if metadata.proof_harnesses.is_empty() { + // 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. + bail!("No proof harnesses (functions with #[kani::proof]) were found to verify."); + } else { + Ok(metadata.proof_harnesses.clone()) + } + } +} + +fn mock_proof_harness(name: &str) -> HarnessMetadata { + HarnessMetadata { + pretty_name: name.into(), + mangled_name: name.into(), + original_file: "".into(), + original_line: "".into(), + unwind_value: None, + } +} + +/// 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); + } + } + } + if let Some(x) = result { + Ok(x) + } else { + bail!("A proof harness named {} was not found", name); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn check_find_proof_harness() { + let harnesses = vec![ + mock_proof_harness("check_one"), + mock_proof_harness("module::check_two"), + mock_proof_harness("module::not_check_three"), + ]; + assert!(find_proof_harness("check_three", &harnesses).is_err()); + assert!( + find_proof_harness("check_two", &harnesses).unwrap().mangled_name + == "module::check_two" + ); + assert!(find_proof_harness("check_one", &harnesses).unwrap().mangled_name == "check_one"); + } +} diff --git a/src/kani_metadata/src/harness.rs b/src/kani_metadata/src/harness.rs index 870f4649627f..a445b26cc857 100644 --- a/src/kani_metadata/src/harness.rs +++ b/src/kani_metadata/src/harness.rs @@ -4,7 +4,7 @@ use serde::{Deserialize, Serialize}; /// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find -#[derive(Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize)] pub struct HarnessMetadata { /// The name the user gave to the function pub pretty_name: String, diff --git a/tests/cargo-kani/output-format/src/main.rs b/tests/cargo-kani/output-format/src/main.rs index 05bcce27d05e..f2c8040e4ec7 100644 --- a/tests/cargo-kani/output-format/src/main.rs +++ b/tests/cargo-kani/output-format/src/main.rs @@ -1,6 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +#[kani::proof] fn main() { assert!(1 + 1 == 2); } diff --git a/tests/cargo-kani/rectangle-example/README.md b/tests/cargo-kani/rectangle-example/README.md index 7311bebe6e90..b07c61a96c9c 100644 --- a/tests/cargo-kani/rectangle-example/README.md +++ b/tests/cargo-kani/rectangle-example/README.md @@ -26,7 +26,7 @@ test rectangle::proptests::stretched_rectangle_can_hold_original ... ok Use `cargo kani` to verify the first proof harness `stretched_rectangle_can_hold_original`. As we explain in the post, verification failure is expected. ```bash -$ cargo kani --function stretched_rectangle_can_hold_original --output-format terse +$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse # --snip-- VERIFICATION:- FAILED ``` @@ -34,7 +34,7 @@ VERIFICATION:- FAILED In order to view a trace (a step-by-step execution of the program) use the `--visualize` flag: ```bash -$ cargo kani --function stretched_rectangle_can_hold_original --output-format terse --visualize +$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse --visualize # --snip-- VERIFICATION:- FAILED # and generates a html report in target/report/html/index.html diff --git a/tests/cargo-kani/simple-main/src/main.rs b/tests/cargo-kani/simple-main/src/main.rs index 37592b921f22..3bc601d23bd6 100644 --- a/tests/cargo-kani/simple-main/src/main.rs +++ b/tests/cargo-kani/simple-main/src/main.rs @@ -1,5 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +#[kani::proof] fn main() { assert!(1 == 2); } diff --git a/tests/cargo-kani/simple-proof-annotation/expected b/tests/cargo-kani/simple-proof-annotation/expected new file mode 100644 index 000000000000..e8525a017fbd --- /dev/null +++ b/tests/cargo-kani/simple-proof-annotation/expected @@ -0,0 +1,2 @@ +FAILURE\ +assertion failed: 3 == 4 diff --git a/tests/cargo-kani/simple-proof-annotation/main.expected b/tests/cargo-kani/simple-proof-annotation/main.expected index 0d19b5b087e5..6cf62a785b3e 100644 --- a/tests/cargo-kani/simple-proof-annotation/main.expected +++ b/tests/cargo-kani/simple-proof-annotation/main.expected @@ -1,2 +1 @@ -FAILURE\ -assertion failed: 1 == 2 +Error: A proof harness named main was not found diff --git a/tests/cargo-kani/simple-proof-annotation/src/main.rs b/tests/cargo-kani/simple-proof-annotation/src/main.rs index 49f38fc3e4b3..ec6472221385 100644 --- a/tests/cargo-kani/simple-proof-annotation/src/main.rs +++ b/tests/cargo-kani/simple-proof-annotation/src/main.rs @@ -5,13 +5,6 @@ fn main() { assert!(1 == 2); } -// NOTE: Currently the below is not detected or run by this test! - -// The expected file presently looks for "1 == 2" above. -// But eventually this test may start to fail as we might stop regarding 'main' -// as a valid proof harness, since it isn't annotated as such. -// This test should be updated if we go that route. - #[kani::proof] fn harness() { assert!(3 == 4); diff --git a/tests/cargo-kani/simple-unwind-annotation/Cargo.toml b/tests/cargo-kani/simple-unwind-annotation/Cargo.toml index 193f77880916..401ebf5cad48 100644 --- a/tests/cargo-kani/simple-unwind-annotation/Cargo.toml +++ b/tests/cargo-kani/simple-unwind-annotation/Cargo.toml @@ -7,7 +7,3 @@ version = "0.1.0" edition = "2021" [dependencies] - -# Remove this once unwind has been hooked up -[package.metadata.kani] -flags = {function = "harness"} diff --git a/tests/cargo-kani/simple-unwind-annotation/expected b/tests/cargo-kani/simple-unwind-annotation/expected new file mode 100644 index 000000000000..9dc068369282 --- /dev/null +++ b/tests/cargo-kani/simple-unwind-annotation/expected @@ -0,0 +1,2 @@ +FAILURE\ +assertion failed: counter < 10 diff --git a/tests/cargo-kani/simple-unwind-annotation/main.expected b/tests/cargo-kani/simple-unwind-annotation/main.expected deleted file mode 100644 index 41aa49b571d8..000000000000 --- a/tests/cargo-kani/simple-unwind-annotation/main.expected +++ /dev/null @@ -1 +0,0 @@ -Failed Checks: assertion failed: 1 == 2 diff --git a/tests/cargo-kani/simple-unwind-annotation/src/main.rs b/tests/cargo-kani/simple-unwind-annotation/src/lib.rs similarity index 79% rename from tests/cargo-kani/simple-unwind-annotation/src/main.rs rename to tests/cargo-kani/simple-unwind-annotation/src/lib.rs index 39b10f10724f..2705b506b358 100644 --- a/tests/cargo-kani/simple-unwind-annotation/src/main.rs +++ b/tests/cargo-kani/simple-unwind-annotation/src/lib.rs @@ -1,12 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// -// This harness should fail because unwind limit is too high. - -fn main() { - assert!(1 == 2); -} +// TODO: When unwind is hooked up, `harness.expected` should now see success #[kani::proof] #[kani::unwind(9)] fn harness() { diff --git a/tests/cargo-kani/simple-visualize/main.expected b/tests/cargo-kani/simple-visualize/main.expected index a77a82910a33..a863a195a4ff 100644 --- a/tests/cargo-kani/simple-visualize/main.expected +++ b/tests/cargo-kani/simple-visualize/main.expected @@ -1 +1 @@ -report/html/index.html +report-main/html/index.html diff --git a/tests/cargo-kani/simple-visualize/src/main.rs b/tests/cargo-kani/simple-visualize/src/main.rs index 37592b921f22..3bc601d23bd6 100644 --- a/tests/cargo-kani/simple-visualize/src/main.rs +++ b/tests/cargo-kani/simple-visualize/src/main.rs @@ -1,5 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT +#[kani::proof] fn main() { assert!(1 == 2); } diff --git a/tests/expected/dry-run/main.rs b/tests/expected/dry-run/main.rs index 6b07392d6bba..4d10b02857cd 100644 --- a/tests/expected/dry-run/main.rs +++ b/tests/expected/dry-run/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --dry-run +// kani-flags: --dry-run --function main // `--dry-run` causes Kani to print out commands instead of running them // In `expected` you will find substrings of these commands because the diff --git a/tests/expected/expect-fail/main.rs b/tests/expected/expect-fail/main.rs index 6158701b9ada..3c49a74a4570 100644 --- a/tests/expected/expect-fail/main.rs +++ b/tests/expected/expect-fail/main.rs @@ -1,3 +1,4 @@ +#[kani::proof] fn main() { let x: i32 = kani::any(); kani::expect_fail(x == 5, "x is not 5!"); diff --git a/tests/expected/one-assert/test.rs b/tests/expected/one-assert/test.rs index 7a66eb4e3375..8706d4002d89 100644 --- a/tests/expected/one-assert/test.rs +++ b/tests/expected/one-assert/test.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --function check_assert -// compile-flags: --crate-type lib #[kani::proof] pub fn check_assert() { let x: u8 = kani::any(); diff --git a/tests/expected/reach/assert/unreachable/test.rs b/tests/expected/reach/assert/unreachable/test.rs index 4368c418f3fe..0016ad958d33 100644 --- a/tests/expected/reach/assert/unreachable/test.rs +++ b/tests/expected/reach/assert/unreachable/test.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --function foo #[kani::proof] fn foo(x: i32) { diff --git a/tests/kani/ArithOperators/unsafe_add_fail.rs b/tests/kani/ArithOperators/unsafe_add_fail.rs index f38abb057ed2..00b7093527c4 100644 --- a/tests/kani/ArithOperators/unsafe_add_fail.rs +++ b/tests/kani/ArithOperators/unsafe_add_fail.rs @@ -1,10 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// + // Check that regular arithmetic operations in unsafe blocks still trigger overflow checks. // kani-verify-fail -// kani-flags: --function check_add -// compile-flags: --crate-type lib #[kani::proof] pub fn check_add(a: u8, b: u8) { unsafe { diff --git a/tests/kani/ArithOperators/unsafe_mul_fail.rs b/tests/kani/ArithOperators/unsafe_mul_fail.rs index fcffbf405555..e73d2d9855b3 100644 --- a/tests/kani/ArithOperators/unsafe_mul_fail.rs +++ b/tests/kani/ArithOperators/unsafe_mul_fail.rs @@ -1,10 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// + // Check that regular arithmetic operations in unsafe blocks still trigger overflow checks. // kani-verify-fail -// kani-flags: --function check_mul -// compile-flags: --crate-type lib #[kani::proof] pub fn check_mul(a: u8, b: u8) { diff --git a/tests/kani/ArithOperators/unsafe_sub_fail.rs b/tests/kani/ArithOperators/unsafe_sub_fail.rs index 296b85c5ca4c..c7428382e980 100644 --- a/tests/kani/ArithOperators/unsafe_sub_fail.rs +++ b/tests/kani/ArithOperators/unsafe_sub_fail.rs @@ -1,10 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// + // Check that regular arithmetic operations in unsafe blocks still trigger overflow checks. // kani-verify-fail -// kani-flags: --function check_sub -// compile-flags: --crate-type lib #[kani::proof] pub fn check_sub(a: u8, b: u8) { diff --git a/tests/kani/Cleanup/unwind_fixme.rs b/tests/kani/Cleanup/unwind_fixme.rs index 5d52340971b0..696d69d7844a 100644 --- a/tests/kani/Cleanup/unwind_fixme.rs +++ b/tests/kani/Cleanup/unwind_fixme.rs @@ -1,17 +1,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// + // We currently do not support stack unwinding panic strategy. Once we do, this testcase should // fail during the verification with both the panic and the assertion failing. // https://github.com/model-checking/kani/issues/692 -// -// To run manually, execute: -// ``` -// RUSTFLAGS="--C panic=unwind --crate-type lib" kani unwind_fixme.rs --function create -// ``` -// + // compile-flags: --C panic=unwind --crate-type lib -// kani-flags: --function create // kani-verify-fail pub struct DummyResource { diff --git a/tests/kani/Closure/fn_mut_closure.rs b/tests/kani/Closure/fn_mut_closure.rs index 1006e97da758..e0eabd823d64 100644 --- a/tests/kani/Closure/fn_mut_closure.rs +++ b/tests/kani/Closure/fn_mut_closure.rs @@ -15,6 +15,7 @@ where } } +#[kani::proof] fn main() { let mut sum = 0_usize; let elems = [1_usize, 2, 3, 4, 5]; diff --git a/tests/kani/Match/match_bool.rs b/tests/kani/Match/match_bool.rs index 012306f050d0..d52c0993e2b6 100644 --- a/tests/kani/Match/match_bool.rs +++ b/tests/kani/Match/match_bool.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// compile-flags: --crate-type lib -// kani-flags: --function match_bool #[kani::proof] pub fn match_bool() { diff --git a/tests/kani/Options/check_tests.rs b/tests/kani/Options/check_tests.rs index 4ff7ed73abe2..5510bb6be9c9 100644 --- a/tests/kani/Options/check_tests.rs +++ b/tests/kani/Options/check_tests.rs @@ -5,7 +5,7 @@ // Note: We need to provide the compile-flags because compile test runs rustc directly and via kani. // compile-flags: --test -// kani-flags: --tests --function test_harness +// kani-flags: --tests pub mod my_mod { pub fn fn_under_verification(a: i32) { diff --git a/tests/kani/Repr/check_repr.rs b/tests/kani/Repr/check_repr.rs index 399edfbf318c..df388ffaed90 100644 --- a/tests/kani/Repr/check_repr.rs +++ b/tests/kani/Repr/check_repr.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// compile-flags: --crate-type lib -// kani-flags: --function find_error #![feature(decl_macro)] pub type Key = i8; diff --git a/tests/kani/Repr/issue_837.rs b/tests/kani/Repr/issue_837.rs index 51dd1278f92c..81b5d6cd3f3d 100644 --- a/tests/kani/Repr/issue_837.rs +++ b/tests/kani/Repr/issue_837.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// compile-flags: --crate-type lib -// kani-flags: --function find_error #![feature(decl_macro)] // This test checks for the case where transparent structs have zero sized fields diff --git a/tests/smack/basic/arith.rs b/tests/smack/basic/arith.rs index 79d7f28d36d3..b497952f0f37 100644 --- a/tests/smack/basic/arith.rs +++ b/tests/smack/basic/arith.rs @@ -1,8 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @expect verified -pub fn main() { +#[kani::proof] +fn main() { // unsigned { let a: u32 = 2; diff --git a/tests/smack/basic/arith_assume.rs b/tests/smack/basic/arith_assume.rs index abc3ab3b430d..d4420420de5a 100644 --- a/tests/smack/basic/arith_assume.rs +++ b/tests/smack/basic/arith_assume.rs @@ -1,8 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @expect verified -pub fn main() { +#[kani::proof] +fn main() { let a = kani::any(); let b = kani::any(); if 4 < a && a < 8 { diff --git a/tests/smack/basic/arith_assume2.rs b/tests/smack/basic/arith_assume2.rs index abc3ab3b430d..d4420420de5a 100644 --- a/tests/smack/basic/arith_assume2.rs +++ b/tests/smack/basic/arith_assume2.rs @@ -1,8 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @expect verified -pub fn main() { +#[kani::proof] +fn main() { let a = kani::any(); let b = kani::any(); if 4 < a && a < 8 { diff --git a/tests/smack/functions/closure.rs b/tests/smack/functions/closure.rs index 2e31fa3ba6e7..a4cf52513f87 100644 --- a/tests/smack/functions/closure.rs +++ b/tests/smack/functions/closure.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @flag --no-memory-splitting -// @expect verified fn call_with_one(mut some_closure: F) -> () where @@ -10,7 +8,8 @@ where some_closure(1); } -pub fn main() { +#[kani::proof] +fn main() { let mut num: i32 = kani::any(); if num <= std::i32::MAX - 10 { let original_num = num; diff --git a/tests/smack/functions/double.rs b/tests/smack/functions/double.rs index c399b7fb4c98..7326fc606fb0 100644 --- a/tests/smack/functions/double.rs +++ b/tests/smack/functions/double.rs @@ -1,12 +1,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @expect verified fn double(a: u32) -> u32 { a * 2 } -pub fn main() { +#[kani::proof] +fn main() { let a = kani::any(); if a <= std::u32::MAX / 2 { let b = double(a); diff --git a/tests/smack/generics/generic_function.rs b/tests/smack/generics/generic_function.rs index 103faa56ba60..4fe7ba38d2d1 100644 --- a/tests/smack/generics/generic_function.rs +++ b/tests/smack/generics/generic_function.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @expect verified struct Point { pub x: T, @@ -33,7 +32,8 @@ fn swapem>(s: U) -> U { s.swap_items() } -pub fn main() { +#[kani::proof] +fn main() { let x2 = kani::any(); let y2 = kani::any(); let x3 = kani::any(); diff --git a/tests/smack/loops/gauss_sum_nondet.rs b/tests/smack/loops/gauss_sum_nondet.rs index 0038fb0d92c9..cb9fea745e1f 100644 --- a/tests/smack/loops/gauss_sum_nondet.rs +++ b/tests/smack/loops/gauss_sum_nondet.rs @@ -1,10 +1,9 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @flag --no-memory-splitting --unroll=4 -// @expect verified // cbmc-flags: --unwind 5 -pub fn main() { +#[kani::proof] +fn main() { let mut sum = 0; let b: u64 = kani::any(); if b < 5 && b > 1 { diff --git a/tests/smack/loops/iterator.rs b/tests/smack/loops/iterator.rs index 52a60b83b284..d9ec0d13d1f4 100644 --- a/tests/smack/loops/iterator.rs +++ b/tests/smack/loops/iterator.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @flag --no-memory-splitting --unroll=4 -// @expect verified // cbmc-flags: --unwind 5 @@ -13,7 +11,8 @@ fn fac(n: u64) -> u64 { } } -pub fn main() { +#[kani::proof] +fn main() { let mut a = 1; let n = kani::any(); if n < 5 { diff --git a/tests/smack/recursion/fac.rs b/tests/smack/recursion/fac.rs index 8c8aa954cd91..074c4bf7d006 100644 --- a/tests/smack/recursion/fac.rs +++ b/tests/smack/recursion/fac.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @flag --unroll=10 -// @expect verified fn fac(n: u64, acc: u64) -> u64 { match n { @@ -10,7 +8,8 @@ fn fac(n: u64, acc: u64) -> u64 { } } -pub fn main() { +#[kani::proof] +fn main() { let x = fac(5, 1); assert!(x == 120); } diff --git a/tests/smack/recursion/fib.rs b/tests/smack/recursion/fib.rs index e101406716aa..ae8da77fcbfc 100644 --- a/tests/smack/recursion/fib.rs +++ b/tests/smack/recursion/fib.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @flag --unroll=10 -// @expect verified fn fib(x: u64) -> u64 { match x { @@ -11,7 +9,8 @@ fn fib(x: u64) -> u64 { } } -pub fn main() { +#[kani::proof] +fn main() { let x = fib(6); assert!(x == 8); } diff --git a/tests/smack/structures/option.rs b/tests/smack/structures/option.rs index 4d75dd0ece14..fd8c701c3c4e 100644 --- a/tests/smack/structures/option.rs +++ b/tests/smack/structures/option.rs @@ -1,12 +1,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @expect verified fn safe_div(x: u32, y: u32) -> Option { if y != 0 { Some(x / y) } else { None } } -pub fn main() { +#[kani::proof] +fn main() { let x = kani::any(); if x > 0 && x <= 200 { // avoid overflow diff --git a/tests/smack/structures/point.rs b/tests/smack/structures/point.rs index a566edf12dde..963dc1278c9c 100644 --- a/tests/smack/structures/point.rs +++ b/tests/smack/structures/point.rs @@ -1,6 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @expect verified use std::ops::{Add, AddAssign}; @@ -36,7 +35,8 @@ impl AddAssign for Point { } } -pub fn main() { +#[kani::proof] +fn main() { let w = kani::any(); let x = kani::any(); let y = kani::any(); diff --git a/tests/smack/vector/vec1.rs b/tests/smack/vector/vec1.rs index 06f01e307a71..b90ba8d1f265 100644 --- a/tests/smack/vector/vec1.rs +++ b/tests/smack/vector/vec1.rs @@ -1,9 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @flag --no-memory-splitting -// @expect verified -pub fn main() { +#[kani::proof] +fn main() { let mut v: Vec = Vec::new(); v.push(0); v.push(1); diff --git a/tests/smack/vector/vec_resize.rs b/tests/smack/vector/vec_resize.rs index 49acd9c0c0ab..6fc942fdb832 100644 --- a/tests/smack/vector/vec_resize.rs +++ b/tests/smack/vector/vec_resize.rs @@ -1,9 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// @flag --no-memory-splitting --unroll=3 -// @expect verified -pub fn main() { +#[kani::proof] +fn main() { let mut v1: Vec = vec![0]; let mut v2: Vec = vec![3]; v1.append(&mut v2); diff --git a/tests/ui/logging/debug/trivial.rs b/tests/ui/logging/debug/trivial.rs index 6c1e8fcf7705..6280b8206705 100644 --- a/tests/ui/logging/debug/trivial.rs +++ b/tests/ui/logging/debug/trivial.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// -// kani-flags: --function harness --debug + +// kani-flags: --debug // This test is to make sure we are correctly printing debug messages in the compiler. // // We don't rely in a specific debug message since they can change at any point. We do however diff --git a/tests/ui/logging/warning/trivial.rs b/tests/ui/logging/warning/trivial.rs index 1f4600687cad..2c8e3b412b72 100644 --- a/tests/ui/logging/warning/trivial.rs +++ b/tests/ui/logging/warning/trivial.rs @@ -1,7 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --function harness // This test is to make sure we are correctly printing warnings from the kani-compiler. // FIXME: This should also print a warning: @@ -16,7 +15,7 @@ fn is_true(b: bool) { assert!(b); } -// This should print a warning since this is a no-op. +// Duplicate proof harness attributes should produce a warning #[kani::proof] #[kani::proof] fn harness() { diff --git a/tests/ui/multiple-harnesses/expected b/tests/ui/multiple-harnesses/expected new file mode 100644 index 000000000000..e4069333d590 --- /dev/null +++ b/tests/ui/multiple-harnesses/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/test.rs b/tests/ui/multiple-harnesses/test.rs new file mode 100644 index 000000000000..fdacf08c2611 --- /dev/null +++ b/tests/ui/multiple-harnesses/test.rs @@ -0,0 +1,14 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn check_first_harness() { + assert!(1 == 1); +} + +#[kani::proof] +fn check_second_harness() { + assert!(2 == 2); +} + +fn main() {} diff --git a/tests/ui/unwind-without-proof/main.rs b/tests/ui/unwind-without-proof/main.rs index c2fb5fcf81c2..90284eba5fc9 100644 --- a/tests/ui/unwind-without-proof/main.rs +++ b/tests/ui/unwind-without-proof/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --no-unwinding-checks --function harness +// kani-flags: --no-unwinding-checks // This test is to check Kani's error handling for harnesses that have unwind attributes // without '#[kani::proof]' attribute declared diff --git a/tools/bookrunner/src/util.rs b/tools/bookrunner/src/util.rs index cfaee4d628b1..dde493d7ec41 100644 --- a/tools/bookrunner/src/util.rs +++ b/tools/bookrunner/src/util.rs @@ -203,7 +203,9 @@ pub fn add_codegen_job(litani: &mut Litani, test_props: &TestProps) { pub fn add_verification_job(litani: &mut Litani, test_props: &TestProps) { let exit_status = if test_props.fail_step == Some(FailStep::Verification) { 10 } else { 0 }; let mut kani = Command::new("kani"); - kani.arg(&test_props.path).args(&test_props.kani_args); + // Add `--function main` so we can run these without having to amend them to add `#[kani::proof]`. + // Some of test_props.kani_args will contains `--cbmc-args` so we should always put that last. + kani.arg(&test_props.path).args(&["--function", "main"]).args(&test_props.kani_args); if !test_props.rustc_args.is_empty() { kani.env("RUSTFLAGS", test_props.rustc_args.join(" ")); } diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 538ba762a301..a982d5f8eb4e 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -374,7 +374,9 @@ fn collect_tests_from_dir( if config.mode == Mode::CargoKani && dir.join("Cargo.toml").exists() { for file in fs::read_dir(dir)? { let file_path = file?.path(); - if file_path.to_str().unwrap().ends_with(".expected") { + if file_path.to_str().unwrap().ends_with(".expected") + || "expected" == file_path.file_name().unwrap() + { fs::create_dir_all(&build_dir.join(file_path.file_stem().unwrap())).unwrap(); let paths = TestPaths { file: file_path, relative_dir: relative_dir_path.to_path_buf() }; diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index b10a601a1a12..eebbe14cb7c8 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -280,15 +280,17 @@ impl<'test> TestCx<'test> { /// `self.testpaths.file`. An error message is printed to stdout if a result /// is not expected. fn run_kani_test(&self) { - self.check(); - if self.props.kani_panic_step == Some(KaniFailStep::Check) { - return; - } - self.codegen(); - if self.props.kani_panic_step == Some(KaniFailStep::Codegen) { - return; + match self.props.kani_panic_step { + Some(KaniFailStep::Check) => { + self.check(); + } + Some(KaniFailStep::Codegen) => { + self.codegen(); + } + Some(KaniFailStep::Verify) | None => { + self.verify(); + } } - self.verify(); } /// If the test file contains expected failures in some locations, ensure @@ -317,10 +319,12 @@ impl<'test> TestCx<'test> { let function_name = self.testpaths.file.file_stem().unwrap().to_str().unwrap(); cargo .arg("kani") - .args(["--function", function_name]) .arg("--target-dir") .arg(self.output_base_dir().join("target")) .current_dir(&parent_dir); + if "expected" != self.testpaths.file.file_name().unwrap() { + cargo.args(["--harness", function_name]); + } self.add_kani_dir_to_path(&mut cargo); let proc_res = self.compose_and_run(cargo); let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap();