From f48e0ddba5ae2ac98c4a91de1b8322858625016c Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 3 Feb 2025 17:28:06 -0500 Subject: [PATCH] allow for including/excluding fns explicitly & improve summary printing --- kani-compiler/src/args.rs | 6 ++ .../src/kani_middle/codegen_units.rs | 23 +++++- kani-driver/src/args/autoverify_args.rs | 38 ++++++++-- kani-driver/src/assess/mod.rs | 2 +- kani-driver/src/autoverify/mod.rs | 72 +++++++++++++++++++ kani-driver/src/call_cargo.rs | 11 ++- kani-driver/src/harness_runner.rs | 49 ++++--------- kani-driver/src/list/collect_metadata.rs | 4 +- kani-driver/src/main.rs | 14 +++- kani-driver/src/project.rs | 2 +- kani-driver/src/session.rs | 14 ++-- .../contracts.expected | 19 +++-- .../cargo_autoverify_contracts/src/lib.rs | 6 ++ .../cargo_autoverify_exclude/Cargo.toml | 7 ++ .../cargo_autoverify_exclude/config.yml | 4 ++ .../cargo_autoverify_exclude/exclude.expected | 4 ++ .../cargo_autoverify_exclude/exclude.sh | 5 ++ .../cargo_autoverify_exclude/src/lib.rs | 23 ++++++ .../cargo_autoverify_filter/filter.expected | 2 +- .../harnesses_fail.expected | 25 +++++-- .../src/lib.rs | 12 ++++ .../cargo_autoverify_include/Cargo.toml | 7 ++ .../cargo_autoverify_include/config.yml | 4 ++ .../cargo_autoverify_include/include.expected | 4 ++ .../cargo_autoverify_include/include.sh | 5 ++ .../cargo_autoverify_include/src/lib.rs | 24 +++++++ 26 files changed, 314 insertions(+), 72 deletions(-) create mode 100644 kani-driver/src/autoverify/mod.rs create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/exclude.expected create mode 100755 tests/script-based-pre/cargo_autoverify_exclude/exclude.sh create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs create mode 100644 tests/script-based-pre/cargo_autoverify_include/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_include/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_include/include.expected create mode 100755 tests/script-based-pre/cargo_autoverify_include/include.sh create mode 100644 tests/script-based-pre/cargo_autoverify_include/src/lib.rs diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 9fe129dade03..d93162da005d 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -90,6 +90,12 @@ pub struct Arguments { /// Print the final LLBC file to stdout. #[clap(long)] pub print_llbc: bool, + /// If we are running the autoverify subcommand, the functions to autoverify + #[arg(long = "autoverify-include-function", num_args(1))] + pub autoverify_included_functions: Vec, + /// If we are running the autoverify subcommand, the functions to exclude from autoverification + #[arg(long = "autoverify-exclude-function", num_args(1))] + pub autoverify_excluded_functions: Vec, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 2948fc1186af..62d089be6b21 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -62,7 +62,8 @@ impl CodegenUnits { let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() }; let base_filepath = tcx.output_filenames(()).path(OutputType::Object); let base_filename = base_filepath.as_path(); - match queries.args().reachability_analysis { + let args = queries.args(); + match args.reachability_analysis { ReachabilityType::Harnesses => { let all_harnesses = get_all_manual_harnesses(tcx, base_filename); // Even if no_stubs is empty we still need to store rustc metadata. @@ -80,8 +81,18 @@ impl CodegenUnits { let kani_harness_intrinsic = kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); let kani_any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap(); + let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool { - is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst) + // If the user specified functions to include or exclude, only allow instances matching those filters. + let user_included = if !args.autoverify_included_functions.is_empty() { + fn_list_contains_instance(&instance, &args.autoverify_included_functions) + } else if !args.autoverify_excluded_functions.is_empty() { + !fn_list_contains_instance(&instance, &args.autoverify_excluded_functions) + } else { + true + }; + user_included + && is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst) }); let automatic_harnesses = get_all_automatic_harnesses( tcx, @@ -378,3 +389,11 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: false }) } + +/// Return whether the name of `instance` is included in `fn_list`. +/// If `exact = true`, then `instance`'s exact, fully-qualified name must be in `fn_list`; otherwise, `fn_list` +/// can have a substring of `instance`'s name. +fn fn_list_contains_instance(instance: &Instance, fn_list: &[String]) -> bool { + let pretty_name = instance.name(); + fn_list.contains(&pretty_name) || fn_list.iter().any(|fn_name| pretty_name.contains(fn_name)) +} diff --git a/kani-driver/src/args/autoverify_args.rs b/kani-driver/src/args/autoverify_args.rs index c8f961643e40..b7c1ffc1dfdc 100644 --- a/kani-driver/src/args/autoverify_args.rs +++ b/kani-driver/src/args/autoverify_args.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Implements the subcommand handling of the list subcommand +//! Implements the subcommand handling of the autoverify subcommand use std::path::PathBuf; @@ -8,12 +8,35 @@ use crate::args::{ValidateArgs, VerificationArgs}; use clap::{Error, Parser, error::ErrorKind}; use kani_metadata::UnstableFeature; -// TODO add --function option to only verify functions matching the substring -// (akin to --harness). +#[derive(Debug, Parser)] +pub struct CommonAutoverifyArgs { + /// If specified, only autoverify functions that match this filter. This option can be provided + /// multiple times, which will verify all functions matching any of the filters. + /// Note that this filter will match against partial names, i.e., providing the name of a module will include all functions from that module. + /// Also note that if the function specified is unable to be automatically verified, this flag will have no effect. + #[arg( + long = "include-function", + num_args(1), + value_name = "FUNCTION", + conflicts_with = "exclude_function" + )] + pub include_function: Vec, + + /// If specified, only autoverify functions that do not match this filter. This option can be provided + /// multiple times, which will verify all functions that do not match any of the filters. + /// Note that this filter will match against partial names, i.e., providing the name of a module will exclude all functions from that module. + #[arg(long = "exclude-function", num_args(1), value_name = "FUNCTION")] + pub exclude_function: Vec, + // TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches, + // like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though. +} /// Automatically verify functions in a crate. #[derive(Debug, Parser)] pub struct CargoAutoverifyArgs { + #[command(flatten)] + pub common_autoverify_args: CommonAutoverifyArgs, + #[command(flatten)] pub verify_opts: VerificationArgs, } @@ -28,13 +51,15 @@ pub struct StandaloneAutoverifyArgs { #[arg(long, hide = true)] pub crate_name: Option, + #[command(flatten)] + pub common_autoverify_args: CommonAutoverifyArgs, + #[command(flatten)] pub verify_opts: VerificationArgs, } impl ValidateArgs for CargoAutoverifyArgs { fn validate(&self) -> Result<(), Error> { - self.verify_opts.validate()?; if !self .verify_opts .common_args @@ -62,13 +87,14 @@ impl ValidateArgs for CargoAutoverifyArgs { )); } + self.verify_opts.validate()?; + Ok(()) } } impl ValidateArgs for StandaloneAutoverifyArgs { fn validate(&self) -> Result<(), Error> { - self.verify_opts.validate()?; if !self .verify_opts .common_args @@ -105,6 +131,8 @@ impl ValidateArgs for StandaloneAutoverifyArgs { )); } + self.verify_opts.validate()?; + Ok(()) } } diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs index ec91918ac8b5..02b3da0974f8 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -53,7 +53,7 @@ fn assess_project(mut session: KaniSession) -> Result { session.args.jobs = Some(None); // -j, num_cpu } - let project = project::cargo_project(&session, true)?; + let project = project::cargo_project(&mut session, true)?; let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo"); let packages_metadata = diff --git a/kani-driver/src/autoverify/mod.rs b/kani-driver/src/autoverify/mod.rs new file mode 100644 index 000000000000..5fae52ad30f4 --- /dev/null +++ b/kani-driver/src/autoverify/mod.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::call_cbmc::VerificationStatus; +use crate::call_single_file::to_rustc_arg; +use crate::harness_runner::HarnessResult; +use crate::session::KaniSession; +use anyhow::Result; + +impl KaniSession { + /// Enable autoverify mode. + pub fn enable_autoverify(&mut self) { + self.autoverify = true; + } + + /// Add the compiler arguments specific to the `autoverify` subcommand. + pub fn add_auto_verify_args(&mut self, included: Vec, excluded: Vec) { + for func in included { + self.pkg_args + .push(to_rustc_arg(vec![format!("--autoverify-include-function {}", func)])); + } + for func in excluded { + self.pkg_args + .push(to_rustc_arg(vec![format!("--autoverify-exclude-function {}", func)])); + } + } + + /// Prints the results from running the `autoverify` subcommand. + pub fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { + let (successes, failures): (Vec<_>, Vec<_>) = + automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success); + + let succeeding = successes.len(); + let failing = failures.len(); + let total = succeeding + failing; + + // TODO: it would be nice if we had access to which functions the user included/excluded here + // so that we could print a comparison for them of any of the included functions that we skipped. + println!("Autoverify Summary:"); + println!( + "Note that Kani will only autoverify a function if it determines that each of its arguments implement the Arbitrary trait." + ); + println!( + "Examine the summary closely to determine which functions were automatically verified." + ); + + // Since autoverification skips over some functions, print the successes to make it easier to see what we verified in one place. + for success in successes { + println!("Verification succeeded for - {}", success.harness.pretty_name); + } + + for failure in failures { + println!("Verification failed for - {}", failure.harness.pretty_name); + } + + if total > 0 { + println!( + "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total." + ); + } else { + println!(" + No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."); + println!( + "If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive." + ); + } + + // Manual harness summary may come afterward, so separate them with a new line. + println!(); + Ok(()) + } +} diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 0bc716115989..4c39b03183b6 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -126,7 +126,7 @@ crate-type = ["lib"] } /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir` - pub fn cargo_build(&self, keep_going: bool) -> Result { + pub fn cargo_build(&mut self, keep_going: bool) -> Result { let build_target = env!("TARGET"); // see build.rs let metadata = self.cargo_metadata(build_target)?; let target_dir = self @@ -183,13 +183,12 @@ crate-type = ["lib"] } // Arguments that will only be passed to the target package. - let mut pkg_args: Vec = vec![]; - pkg_args.extend(["--".to_string(), self.reachability_arg()]); + self.pkg_args.push(self.reachability_arg()); if let Some(backend_arg) = self.backend_arg() { - pkg_args.push(backend_arg); + self.pkg_args.push(backend_arg); } if self.args.no_assert_contracts { - pkg_args.push("--no-assert-contracts".into()); + self.pkg_args.push("--no-assert-contracts".into()); } let mut found_target = false; @@ -202,7 +201,7 @@ crate-type = ["lib"] cmd.args(&cargo_args) .args(vec!["-p", &package.id.to_string()]) .args(verification_target.to_args()) - .args(&pkg_args) + .args(&self.pkg_args) .env("RUSTC", &self.kani_compiler) // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See // https://doc.rust-lang.org/cargo/reference/environment-variables.html diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 905910b54f06..c9c42eddb172 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::{Result, bail}; -use kani_metadata::{ArtifactType, HarnessMetadata}; +use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata}; use rayon::prelude::*; use std::fs::File; use std::io::Write; @@ -169,10 +169,17 @@ impl KaniSession { let thread_index = rayon::current_thread_index().unwrap_or_default(); // If the harness is automatically generated, pretty_name refers to the function under verification. let mut msg = if harness.is_automatically_generated { - format!( - "Autoverify: Checking function {} against all possible inputs...", - harness.pretty_name - ) + if matches!(harness.attributes.kind, HarnessKind::Proof) { + format!( + "Autoverify: Checking function {} against all possible inputs...", + harness.pretty_name + ) + } else { + format!( + "Autoverify: Checking function {}'s contract against all possible inputs...", + harness.pretty_name + ) + } } else { format!("Checking harness {}...", harness.pretty_name) }; @@ -190,34 +197,6 @@ impl KaniSession { Ok(result) } - /// Prints the results from running the `autoverify` subcommand. - fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { - let (successes, failures): (Vec<_>, Vec<_>) = - automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success); - - let succeeding = successes.len(); - let failing = failures.len(); - let total = succeeding + failing; - - if failing > 0 { - println!("Summary:"); - } - for failure in failures.iter() { - println!("Verification failed for - {}", failure.harness.pretty_name); - } - - if total > 0 { - println!( - "Autoverify: Complete - {succeeding} successfully verified functions, {failing} failures, {total} total." - ); - } else { - println!(" - Autoverify: No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."); - } - - Ok(()) - } - /// Concludes a session by printing a summary report and exiting the process with an /// error code (if applicable). /// @@ -231,7 +210,7 @@ impl KaniSession { let (automatic, manual): (Vec<_>, Vec<_>) = results.iter().partition(|r| r.harness.is_automatically_generated); - if self.auto_verify { + if self.autoverify { self.print_autoverify_summary(automatic)?; } @@ -256,7 +235,7 @@ impl KaniSession { // We currently omit a summary if there was just 1 harness if failing > 0 { - println!("Summary:"); + println!("Manual Harness Summary:"); } for failure in failures.iter() { println!("Verification failed for - {}", failure.harness.pretty_name); diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index a7901e997ab1..588cab0b63af 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -78,12 +78,12 @@ fn process_metadata(metadata: Vec) -> ListMetadata { pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { let quiet = args.common_args.quiet; verify_opts.common_args = args.common_args; - let session = KaniSession::new(verify_opts)?; + let mut session = KaniSession::new(verify_opts)?; if !quiet { print_kani_version(InvocationType::CargoKani(vec![])); } - let project = cargo_project(&session, false)?; + let project = cargo_project(&mut session, false)?; let list_metadata = process_metadata(project.metadata); output_list_results(list_metadata, args.format, quiet) diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 2282a2bdb342..59eaebe16aa6 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -22,6 +22,7 @@ use tracing::debug; mod args; mod args_toml; mod assess; +mod autoverify; mod call_cargo; mod call_cbmc; mod call_goto_cc; @@ -72,7 +73,7 @@ fn cargokani_main(input_args: Vec) -> Result<()> { return list_cargo(*list_args, args.verify_opts); } - let session = match args.command { + let mut session = match args.command { Some(CargoKaniSubcommand::Assess(assess_args)) => { let sess = session::KaniSession::new(args.verify_opts)?; return assess::run_assess(sess, *assess_args); @@ -80,6 +81,11 @@ fn cargokani_main(input_args: Vec) -> Result<()> { Some(CargoKaniSubcommand::Autoverify(args)) => { let mut sess = session::KaniSession::new(args.verify_opts)?; sess.enable_autoverify(); + sess.add_auto_verify_args( + args.common_autoverify_args.include_function, + args.common_autoverify_args.exclude_function, + ); + sess } Some(CargoKaniSubcommand::Playback(args)) => { @@ -97,7 +103,7 @@ fn cargokani_main(input_args: Vec) -> Result<()> { return assess::run_assess(session, assess::AssessArgs::default()); } - let project = project::cargo_project(&session, false)?; + let project = project::cargo_project(&mut session, false)?; if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } @@ -110,6 +116,10 @@ fn standalone_main() -> Result<()> { Some(StandaloneSubcommand::Autoverify(args)) => { let mut session = KaniSession::new(args.verify_opts)?; session.enable_autoverify(); + session.add_auto_verify_args( + args.common_autoverify_args.include_function, + args.common_autoverify_args.exclude_function, + ); if !session.args.common_args.quiet { print_kani_version(InvocationType::Standalone); diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index da04cc0517ba..2a1aad2c1eff 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -175,7 +175,7 @@ impl Artifact { /// Generate a project using `cargo`. /// Accept a boolean to build as many targets as possible. The number of failures in that case can /// be collected from the project. -pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result { +pub fn cargo_project(session: &mut KaniSession, keep_going: bool) -> Result { let outputs = session.cargo_build(keep_going)?; let outdir = outputs.outdir.canonicalize()?; // For the MIR Linker we know there is only one metadata per crate. Use that in our favor. diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 9c2e8e5ced0c..8a78ef62841b 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -32,7 +32,10 @@ pub struct KaniSession { pub args: VerificationArgs, /// Automatically verify functions in the crate, in addition to running manual harnesses. - pub auto_verify: bool, + pub autoverify: bool, + + /// The arguments that will be passed to the target package, i.e. kani_compiler. + pub pkg_args: Vec, /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from /// a proof harness. Useful when attempting to verify things that were not annotated with kani @@ -68,7 +71,8 @@ impl KaniSession { Ok(KaniSession { args, - auto_verify: false, + autoverify: false, + pkg_args: vec!["--".to_string()], codegen_tests: false, kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, @@ -77,10 +81,6 @@ impl KaniSession { }) } - pub fn enable_autoverify(&mut self) { - self.auto_verify = true; - } - /// Record a temporary file so we can cleanup after ourselves at the end. /// Note that there will be no failure if the file does not exist. pub fn record_temporary_file>(&self, temp: &T) { @@ -101,7 +101,7 @@ impl KaniSession { pub fn reachability_mode(&self) -> ReachabilityMode { if self.codegen_tests { ReachabilityMode::Tests - } else if self.auto_verify { + } else if self.autoverify { ReachabilityMode::Automatic } else { ReachabilityMode::ProofHarnesses diff --git a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected index 314b4b6fad9e..4901a7019cd8 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected @@ -1,19 +1,28 @@ -Autoverify: Checking function should_fail::max against all possible inputs... +Autoverify: Checking function should_fail::max's contract against all possible inputs... assertion\ - Status: FAILURE\ - Description: "|result : &u32| *result == x" -Autoverify: Checking function should_pass::has_loop_contract against all possible inputs... +Autoverify: Checking function should_pass::has_loop_contract's contract against all possible inputs... should_pass::has_loop_contract.assertion\ - Status: SUCCESS\ - Description: "assertion failed: x == 2" -Autoverify: Checking function should_pass::has_recursion_gcd against all possible inputs... +Autoverify: Checking function should_pass::has_recursion_gcd's contract against all possible inputs... assertion\ - Status: SUCCESS\ - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" -Autoverify: Checking function should_pass::div against all possible inputs... +Autoverify: Checking function should_pass::div's contract against all possible inputs... +Autoverify: Checking function should_pass::unchecked_mul's contract against all possible inputs... +arithmetic_overflow\ + - Status: SUCCESS\ + - Description: "attempt to compute `unchecked_mul` which would overflow" + +Verification succeeded for - should_pass::unchecked_mul +Verification succeeded for - should_pass::has_loop_contract +Verification succeeded for - should_pass::has_recursion_gcd +Verification succeeded for - should_pass::div Verification failed for - should_fail::max -Autoverify: Complete - 3 successfully verified functions, 1 failures, 4 total. +Complete - 4 successfully verified functions, 1 failures, 5 total. diff --git a/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs index ead636fd51ec..e2ac9654bd36 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs +++ b/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs @@ -40,6 +40,12 @@ mod should_pass { assert!(x == 2); } + + // Test that we can autoverify functions for unsafe functions with contracts + #[kani::requires(!left.overflowing_mul(rhs).1)] + unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { + left.unchecked_mul(rhs) + } } mod should_fail { diff --git a/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml b/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml new file mode 100644 index 000000000000..b27dd09bd126 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_include" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_exclude/config.yml b/tests/script-based-pre/cargo_autoverify_exclude/config.yml new file mode 100644 index 000000000000..d3c26a0301f4 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: exclude.sh +expected: exclude.expected diff --git a/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected b/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected new file mode 100644 index 000000000000..b093236133a1 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected @@ -0,0 +1,4 @@ +Autoverify: Checking function include::simple against all possible inputs... +VERIFICATION:- SUCCESSFUL +Verification succeeded for - include::simple +Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh b/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh new file mode 100755 index 000000000000..31d3b54e2725 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options --exclude-function exclude diff --git a/tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs b/tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs new file mode 100644 index 000000000000..7757239126c0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature selects functions correctly +// when --exclude-function is provided. + +mod include { + fn simple(x: u8, _y: u16) -> u8 { + x + } + + // Doesn't implement Arbitrary, so still should not be included. + fn generic(x: u32, _y: T) -> u32 { + x + } +} + +// These functions are eligible for autoverification, but are excluded. +mod excluded { + fn simple(x: u8, _y: u16) -> u8 { + x + } +} diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.expected b/tests/script-based-pre/cargo_autoverify_filter/filter.expected index ee74fa8d5ad6..879c40eed631 100644 --- a/tests/script-based-pre/cargo_autoverify_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoverify_filter/filter.expected @@ -37,4 +37,4 @@ Autoverify: Checking function yes_harness::f_unsupported_return_type against all Autoverify: Checking function yes_harness::f_multiple_args against all possible inputs... Autoverify: Checking function yes_harness::f_derives_arbitrary against all possible inputs... Autoverify: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... -Autoverify: Complete - 39 successfully verified functions, 0 failures, 39 total. \ No newline at end of file +Complete - 39 successfully verified functions, 0 failures, 39 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected index 8e5400a5edae..6d7fd2bec692 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected @@ -14,11 +14,21 @@ oob_unsafe_array_access.pointer_dereference\ - Description: "dereference failure: pointer outside object bounds" Autoverify: Checking function oob_safe_array_access against all possible inputs... ->::index.assertion\ +assertion\ + - Status: FAILURE\ + - Description: "index out of bounds: the length is less than or equal to the given index" + +Autoverify: Checking function unchecked_mul against all possible inputs... +arithmetic_overflow\ - Status: FAILURE\ - - Description: "index out of bounds: the length is less than or equal to the given index" + - Description: "attempt to compute `unchecked_mul` which would overflow" -Autoverify: Complete - 0 successfully verified functions, 4 failures, 4 total. +Verification failed for - panic +Verification failed for - integer_overflow +Verification failed for - oob_unsafe_array_access +Verification failed for - oob_safe_array_access +Verification failed for - unchecked_mul +Complete - 0 successfully verified functions, 5 failures, 5 total. Checking harness panic_harness... panic.assertion\ @@ -35,8 +45,13 @@ oob_unsafe_array_access.pointer_dereference\ - Status: FAILURE\ Checking harness oob_safe_array_access_harness... ->::index.assertion\ +assertion\ - Status: FAILURE\ - Description: "index out of bounds: the length is less than or equal to the given index" -Complete - 0 successfully verified harnesses, 4 failures, 4 total. +Checking harness unchecked_mul_harness... +arithmetic_overflow\ + - Status: FAILURE\ + - Description: "attempt to compute `unchecked_mul` which would overflow" + +Complete - 0 successfully verified harnesses, 5 failures, 5 total. diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs index 92e711eb5d0b..072dae12c133 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs @@ -35,6 +35,11 @@ fn panic() { } } +// Test that we can autoverify functions for unsafe functions +unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { + left.unchecked_mul(rhs) +} + #[kani::proof] fn oob_safe_array_access_harness() { oob_safe_array_access(kani::any()); @@ -54,3 +59,10 @@ fn integer_overflow_harness() { fn panic_harness() { panic(); } + +#[kani::proof] +fn unchecked_mul_harness() { + unsafe { + unchecked_mul(kani::any(), kani::any()); + } +} diff --git a/tests/script-based-pre/cargo_autoverify_include/Cargo.toml b/tests/script-based-pre/cargo_autoverify_include/Cargo.toml new file mode 100644 index 000000000000..b27dd09bd126 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_include" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_include/config.yml b/tests/script-based-pre/cargo_autoverify_include/config.yml new file mode 100644 index 000000000000..8df48ec69865 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: include.sh +expected: include.expected diff --git a/tests/script-based-pre/cargo_autoverify_include/include.expected b/tests/script-based-pre/cargo_autoverify_include/include.expected new file mode 100644 index 000000000000..b093236133a1 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/include.expected @@ -0,0 +1,4 @@ +Autoverify: Checking function include::simple against all possible inputs... +VERIFICATION:- SUCCESSFUL +Verification succeeded for - include::simple +Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_include/include.sh b/tests/script-based-pre/cargo_autoverify_include/include.sh new file mode 100755 index 000000000000..040a246290dd --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/include.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options --include-function include diff --git a/tests/script-based-pre/cargo_autoverify_include/src/lib.rs b/tests/script-based-pre/cargo_autoverify_include/src/lib.rs new file mode 100644 index 000000000000..68b30bf7afe8 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/src/lib.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature selects functions correctly +// when --include-function is provided. + +// Each function inside this module matches the filter. +mod include { + fn simple(x: u8, _y: u16) -> u8 { + x + } + + // Doesn't implement Arbitrary, so still should not be included. + fn generic(x: u32, _y: T) -> u32 { + x + } +} + +// These functions are eligible for autoverification, but do not match the filter. +mod excluded { + fn simple(x: u8, _y: u16) -> u8 { + x + } +}