diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 70c146489030..8ed90b2c975e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -613,7 +613,7 @@ impl GotoCodegenResults { // removes any contracts logic for ReachabilityType::Test or ReachabilityType::PubFns, // which are the two ReachabilityTypes under which the compiler calls this function. contracted_functions: vec![], - autoharness_skipped_fns: None, + autoharness_md: None, } } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index a0f63463053d..cf8b33232f40 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -18,7 +18,7 @@ use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; use crate::kani_queries::QueryDb; use kani_metadata::{ - ArtifactType, AssignsContract, AutoHarnessSkipReason, AutoHarnessSkippedFns, HarnessKind, + ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind, HarnessMetadata, KaniMetadata, }; use rustc_hir::def_id::DefId; @@ -32,6 +32,7 @@ use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; use std::path::{Path, PathBuf}; +use std::sync::OnceLock; use tracing::debug; /// An identifier for the harness function. @@ -40,6 +41,8 @@ type Harness = Instance; /// A set of stubs. pub type Stubs = HashMap; +static AUTOHARNESS_MD: OnceLock = OnceLock::new(); + /// Store some relevant information about the crate compilation. #[derive(Clone, Debug)] struct CrateInfo { @@ -49,7 +52,6 @@ struct CrateInfo { /// We group the harnesses that have the same stubs. pub struct CodegenUnits { - autoharness_skipped_fns: Option, crate_info: CrateInfo, harness_info: HashMap, units: Vec, @@ -74,12 +76,7 @@ impl CodegenUnits { let units = group_by_stubs(tcx, &all_harnesses); validate_units(tcx, &units); debug!(?units, "CodegenUnits::new"); - CodegenUnits { - units, - harness_info: all_harnesses, - crate_info, - autoharness_skipped_fns: None, - } + CodegenUnits { units, harness_info: all_harnesses, crate_info } } ReachabilityType::AllFns => { let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename); @@ -95,6 +92,11 @@ impl CodegenUnits { args, *kani_fns.get(&KaniModel::Any.into()).unwrap(), ); + let chosen_fn_names = + chosen.iter().map(|func| func.name().clone()).collect::>(); + AUTOHARNESS_MD + .set(AutoHarnessMetadata { chosen: chosen_fn_names, skipped }) + .expect("Initializing the autoharness metdata failed"); let automatic_harnesses = get_all_automatic_harnesses( tcx, @@ -117,21 +119,11 @@ impl CodegenUnits { // No need to validate the units again because validation only checks stubs, and we haven't added any stubs. debug!(?units, "CodegenUnits::new"); - CodegenUnits { - units, - harness_info: all_harnesses, - crate_info, - autoharness_skipped_fns: Some(skipped), - } + CodegenUnits { units, harness_info: all_harnesses, crate_info } } _ => { // Leave other reachability type handling as is for now. - CodegenUnits { - units: vec![], - harness_info: HashMap::default(), - crate_info, - autoharness_skipped_fns: None, - } + CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info } } } } @@ -176,7 +168,7 @@ impl CodegenUnits { unsupported_features: vec![], test_harnesses, contracted_functions: gen_contracts_metadata(tcx), - autoharness_skipped_fns: self.autoharness_skipped_fns.clone(), + autoharness_md: AUTOHARNESS_MD.get().cloned(), } } } @@ -432,7 +424,8 @@ fn automatic_harness_partition( var.argument_index.is_some_and(|arg_idx| idx + 1 == usize::from(arg_idx)) }) .map_or("_".to_string(), |debug_info| debug_info.name.to_string()); - problematic_args.push(arg_name) + let arg_type = format!("{}", arg.ty); + problematic_args.push((arg_name, arg_type)) } } if !problematic_args.is_empty() { diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs index 1e778e1f3646..bdba0e340d8d 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -4,7 +4,7 @@ use std::path::PathBuf; -use crate::args::{ValidateArgs, VerificationArgs}; +use crate::args::{ValidateArgs, VerificationArgs, validate_std_path}; use clap::{Error, Parser, error::ErrorKind}; use kani_metadata::UnstableFeature; @@ -54,6 +54,11 @@ pub struct StandaloneAutoharnessArgs { #[command(flatten)] pub common_autoharness_args: CommonAutoharnessArgs, + /// Pass this flag to run the `autoharness` subcommand on the standard library. + /// Ensure that the provided `input` is the `library` folder. + #[arg(long)] + pub std: bool, + #[command(flatten)] pub verify_opts: VerificationArgs, } @@ -99,7 +104,10 @@ impl ValidateArgs for StandaloneAutoharnessArgs { ), )); } - if !self.input.is_file() { + + if self.std { + validate_std_path(&self.input)?; + } else if !self.input.is_file() { return Err(Error::raw( ErrorKind::InvalidValue, format!( diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index ebd97d01f2fb..35d26f22eb36 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -4,7 +4,7 @@ use std::path::PathBuf; -use crate::args::{CommonArgs, ValidateArgs}; +use crate::args::{CommonArgs, ValidateArgs, validate_std_path}; use clap::{Error, Parser, ValueEnum, error::ErrorKind}; use kani_metadata::UnstableFeature; @@ -79,39 +79,7 @@ impl ValidateArgs for StandaloneListArgs { } if self.std { - if !self.input.exists() { - Err(Error::raw( - ErrorKind::InvalidValue, - format!( - "Invalid argument: `` argument `{}` does not exist", - self.input.display() - ), - )) - } else if !self.input.is_dir() { - Err(Error::raw( - ErrorKind::InvalidValue, - format!( - "Invalid argument: `` argument `{}` is not a directory", - self.input.display() - ), - )) - } else { - let full_path = self.input.canonicalize()?; - let dir = full_path.file_stem().unwrap(); - if dir != "library" { - Err(Error::raw( - ErrorKind::InvalidValue, - format!( - "Invalid argument: Expected `` to point to the `library` folder \ - containing the standard library crates.\n\ - Found `{}` folder instead", - dir.to_string_lossy() - ), - )) - } else { - Ok(()) - } - } + validate_std_path(&self.input) } else if self.input.is_file() { Ok(()) } else { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 26e9927cf67c..fb18504c6182 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -20,7 +20,7 @@ use clap::builder::{PossibleValue, TypedValueParser}; use clap::{ValueEnum, error::ContextKind, error::ContextValue, error::Error, error::ErrorKind}; use kani_metadata::CbmcSolver; use std::ffi::OsString; -use std::path::PathBuf; +use std::path::{Path, PathBuf}; use std::str::FromStr; use std::time::Duration; use strum::VariantNames; @@ -789,6 +789,42 @@ impl ValidateArgs for VerificationArgs { } } +pub(crate) fn validate_std_path(std_path: &Path) -> Result<(), Error> { + if !std_path.exists() { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: `` argument `{}` does not exist", + std_path.display() + ), + )) + } else if !std_path.is_dir() { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: `` argument `{}` is not a directory", + std_path.display() + ), + )) + } else { + let full_path = std_path.canonicalize()?; + let dir = full_path.file_stem().unwrap(); + if dir != "library" { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: Expected `` to point to the `library` folder \ + containing the standard library crates.\n\ + Found `{}` folder instead", + dir.to_string_lossy() + ), + )) + } else { + Ok(()) + } + } +} + /// clap parser for `CbmcSolver` #[derive(Clone, Debug)] pub struct CbmcSolverValueParser(Vec); diff --git a/kani-driver/src/args/std_args.rs b/kani-driver/src/args/std_args.rs index 3818b6261010..2968b1108cc0 100644 --- a/kani-driver/src/args/std_args.rs +++ b/kani-driver/src/args/std_args.rs @@ -3,7 +3,7 @@ //! Implements the `verify-std` subcommand handling. -use crate::args::{ValidateArgs, VerificationArgs}; +use crate::args::{ValidateArgs, VerificationArgs, validate_std_path}; use clap::error::ErrorKind; use clap::{Error, Parser}; use kani_metadata::UnstableFeature; @@ -40,38 +40,6 @@ impl ValidateArgs for VerifyStdArgs { )); } - if !self.std_path.exists() { - Err(Error::raw( - ErrorKind::InvalidValue, - format!( - "Invalid argument: `` argument `{}` does not exist", - self.std_path.display() - ), - )) - } else if !self.std_path.is_dir() { - Err(Error::raw( - ErrorKind::InvalidValue, - format!( - "Invalid argument: `` argument `{}` is not a directory", - self.std_path.display() - ), - )) - } else { - let full_path = self.std_path.canonicalize()?; - let dir = full_path.file_stem().unwrap(); - if dir != "library" { - Err(Error::raw( - ErrorKind::InvalidValue, - format!( - "Invalid argument: Expected `` to point to the `library` folder \ - containing the standard library crates.\n\ - Found `{}` folder instead", - dir.to_string_lossy() - ), - )) - } else { - Ok(()) - } - } + validate_std_path(&self.std_path) } } diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 69dd8b561103..251a35570720 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -8,6 +8,7 @@ use crate::args::autoharness_args::{CargoAutoharnessArgs, StandaloneAutoharnessA use crate::call_cbmc::VerificationStatus; use crate::call_single_file::to_rustc_arg; use crate::harness_runner::HarnessResult; +use crate::project::{standalone_project, std_project}; use crate::session::KaniSession; use crate::{InvocationType, print_kani_version, project, verify_project}; use anyhow::Result; @@ -25,11 +26,14 @@ pub fn autoharness_cargo(args: CargoAutoharnessArgs) -> Result<()> { args.common_autoharness_args.include_function, args.common_autoharness_args.exclude_function, ); + if !session.args.common_args.quiet { + print_kani_version(InvocationType::CargoKani(vec![])); + } let project = project::cargo_project(&mut session, false)?; - let metadata = project.metadata.clone(); - let res = verify_project(project, session); - print_skipped_fns(metadata); - res + if !session.args.common_args.quiet { + print_metadata(project.metadata.clone()); + } + if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { @@ -45,46 +49,83 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { print_kani_version(InvocationType::Standalone); } - let project = project::standalone_project(&args.input, args.crate_name, &session)?; - let metadata = project.metadata.clone(); - let res = verify_project(project, session); - print_skipped_fns(metadata); - res + let project = if args.std { + std_project(&args.input, &session)? + } else { + standalone_project(&args.input, args.crate_name, &session)? + }; + + if !session.args.common_args.quiet { + print_metadata(project.metadata.clone()); + } + if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } -/// Print a table of the functions that we skipped and why. -fn print_skipped_fns(metadata: Vec) { - let mut skipped_fns = PrettyTable::new(); - skipped_fns.set_header(vec!["Skipped Function", "Reason for Skipping"]); +/// Print automatic harness metadata to the terminal. +fn print_metadata(metadata: Vec) { + let mut chosen_table = PrettyTable::new(); + chosen_table.set_header(vec!["Chosen Function"]); + + let mut skipped_table = PrettyTable::new(); + skipped_table.set_header(vec!["Skipped Function", "Reason for Skipping"]); for md in metadata { - let skipped_md = md.autoharness_skipped_fns.unwrap(); - skipped_fns.add_rows(skipped_md.into_iter().filter_map(|(func, reason)| match reason { - AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => { - Some(vec![func, format!("{}: {}", reason, args.join(", "))]) + let autoharness_md = md.autoharness_md.unwrap(); + chosen_table.add_rows(autoharness_md.chosen.into_iter().map(|func| vec![func])); + skipped_table.add_rows(autoharness_md.skipped.into_iter().filter_map(|(func, reason)| { + match reason { + AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => Some(vec![ + func, + format!( + "{reason} {}", + args.iter() + .map(|(name, typ)| format!("{}: {}", name, typ)) + .collect::>() + .join(", ") + ), + ]), + AutoHarnessSkipReason::GenericFn + | AutoHarnessSkipReason::NoBody + | AutoHarnessSkipReason::UserFilter => Some(vec![func, reason.to_string()]), + // We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation. + // For those we don't insert during instrumentation that are in this category (manual harnesses or Kani trait implementations), + // it should be obvious that we wouldn't generate harnesses, so reporting those functions as "skipped" is unlikely to be useful. + AutoHarnessSkipReason::KaniImpl => None, } - AutoHarnessSkipReason::GenericFn - | AutoHarnessSkipReason::NoBody - | AutoHarnessSkipReason::UserFilter => Some(vec![func, reason.to_string()]), - // We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation. - // For those we don't insert during instrumentation that are in this category (manual harnesses or Kani trait implementations), - // it should be obvious that we wouldn't generate harnesses, so reporting those functions as "skipped" is unlikely to be useful. - AutoHarnessSkipReason::KaniImpl => None, })); } - if skipped_fns.is_empty() { + print_chosen_table(&mut chosen_table); + print_skipped_table(&mut skipped_table); +} + +/// Print the table of functions for which we generated automatic harnesses. +fn print_chosen_table(table: &mut PrettyTable) { + if table.is_empty() { + println!( + "\nChosen Functions: None. Kani did not generate automatic harnesses for any functions in the available crate(s)." + ); + return; + } + + println!("\nKani generated automatic harnesses for {} function(s):", table.row_count()); + println!("{table}"); +} + +/// Print the table of functions for which we did not generate automatic harnesses. +fn print_skipped_table(table: &mut PrettyTable) { + if table.is_empty() { println!( "\nSkipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s)." ); return; } - println!("\nKani did not generate automatic harnesses for the following functions."); + println!("\nKani did not generate automatic harnesses for {} function(s).", table.row_count()); println!( "If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832" ); - println!("{skipped_fns}"); + println!("{table}"); } impl KaniSession { diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 8a7ee8690fc8..5f83b298b9b8 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -97,7 +97,7 @@ pub fn merge_kani_metadata(files: Vec) -> KaniMetadata { unsupported_features: vec![], test_harnesses: vec![], contracted_functions: vec![], - autoharness_skipped_fns: None, + autoharness_md: None, }; 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. diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index 2fe1038647c1..775679329753 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -38,7 +38,18 @@ pub struct KaniMetadata { /// The functions with contracts in this crate pub contracted_functions: Vec, /// Metadata for the `autoharness` subcommand - pub autoharness_skipped_fns: Option, + pub autoharness_md: Option, +} + +/// For the autoharness subcommand, all of the user-defined functions we found, +/// which are "chosen" if we generated an automatic harness for them, and "skipped" otherwise. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct AutoHarnessMetadata { + /// Functions we generated automatic harnesses for. + pub chosen: Vec, + /// Map function names to the reason why we did not generate an automatic harness for that function. + /// We use an ordered map so that when we print the data, it is ordered alphabetically by function name. + pub skipped: BTreeMap, } /// Reasons that Kani does not generate an automatic harness for a function. @@ -51,9 +62,9 @@ pub enum AutoHarnessSkipReason { #[strum(serialize = "Kani implementation")] KaniImpl, /// At least one of the function's arguments does not implement kani::Arbitrary - /// (The Vec contains the list of argument names that do not implement it) + /// (The Vec<(String, String)> contains the list of (name, type) tuples for each argument that does not implement it #[strum(serialize = "Missing Arbitrary implementation for argument(s)")] - MissingArbitraryImpl(Vec), + MissingArbitraryImpl(Vec<(String, String)>), /// The function does not have a body. #[strum(serialize = "The function does not have a body")] NoBody, @@ -61,11 +72,6 @@ pub enum AutoHarnessSkipReason { #[strum(serialize = "Did not match provided filters")] UserFilter, } - -/// For the autoharness subcommand: map function names to the reason why we did not generate an automatic harness for that function. -/// We use an ordered map so that when we print the data, it is ordered alphabetically by function name. -pub type AutoHarnessSkippedFns = BTreeMap; - #[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord)] pub struct ContractedFunction { /// The fully qualified name the user gave to the function (i.e. includes the module path). diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected index 9babfe015117..200dd56bdaba 100644 --- a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected @@ -1,3 +1,20 @@ +Kani generated automatic harnesses for 5 function(s): ++--------------------------------+ +| Chosen Function | ++================================+ +| should_pass::div | +|--------------------------------| +| should_pass::has_recursion_gcd | +|--------------------------------| +| should_pass::has_loop_contract | +|--------------------------------| +| should_pass::unchecked_mul | +|--------------------------------| +| should_fail::max | ++--------------------------------+ + +Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). + Autoharness: Checking function should_fail::max's contract against all possible inputs... assertion\ - Status: FAILURE\ @@ -40,5 +57,3 @@ Autoharness Summary: Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). Complete - 4 successfully verified functions, 1 failures, 5 total. - -Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). diff --git a/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs index c9f9dd3fd1b0..c66b3dab4fbe 100644 --- a/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs @@ -44,7 +44,7 @@ mod should_pass { // Test that we can autoharness 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) + unsafe { left.unchecked_mul(rhs) } } } diff --git a/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected b/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected index 5a03fa9b8808..aee1a3675f06 100644 --- a/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected +++ b/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected @@ -1,4 +1,14 @@ +Kani generated automatic harnesses for 1 function(s): ++-----------------+ +| Chosen Function | ++=================+ +| yes_harness | ++-----------------+ + +Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). + Autoharness: Checking function yes_harness against all possible inputs... +VERIFICATION:- SUCCESSFUL Manual Harness Summary: No proof harnesses (functions with #[kani::proof]) were found to verify. @@ -10,5 +20,3 @@ Autoharness Summary: | yes_harness | #[kani::proof] | Success | +-------------------+---------------------------+---------------------+ Complete - 1 successfully verified functions, 0 failures, 1 total. - -Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected index 4c0192e92448..2f5e75ef5a3c 100644 --- a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected +++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected @@ -1,3 +1,20 @@ +Kani generated automatic harnesses for 1 function(s): ++-----------------+ +| Chosen Function | ++=================+ +| include::simple | ++-----------------+ + +Kani did not generate automatic harnesses for 2 function(s). +If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 ++------------------+--------------------------------+ +| Skipped Function | Reason for Skipping | ++===================================================+ +| excluded::simple | Did not match provided filters | +|------------------+--------------------------------| +| include::generic | Generic Function | ++------------------+--------------------------------+ + Autoharness: Checking function include::simple against all possible inputs... VERIFICATION:- SUCCESSFUL @@ -11,13 +28,3 @@ Autoharness Summary: | include::simple | #[kani::proof] | Success | +-------------------+---------------------------+---------------------+ Complete - 1 successfully verified functions, 0 failures, 1 total. - -Kani did not generate automatic harnesses for the following functions. -If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 -+------------------+--------------------------------+ -| Skipped Function | Reason for Skipping | -+===================================================+ -| excluded::simple | Did not match provided filters | -|------------------+--------------------------------| -| include::generic | Generic Function | -+------------------+--------------------------------+ diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected index f324effe3d9b..8be532a63419 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -1,3 +1,114 @@ +Kani generated automatic harnesses for 42 function(s): ++----------------------------------------------+ +| Chosen Function | ++==============================================+ +| yes_harness::f_u8 | +|----------------------------------------------| +| yes_harness::f_u16 | +|----------------------------------------------| +| yes_harness::f_u32 | +|----------------------------------------------| +| yes_harness::f_u64 | +|----------------------------------------------| +| yes_harness::f_u128 | +|----------------------------------------------| +| yes_harness::f_usize | +|----------------------------------------------| +| yes_harness::f_i8 | +|----------------------------------------------| +| yes_harness::f_i16 | +|----------------------------------------------| +| yes_harness::f_i32 | +|----------------------------------------------| +| yes_harness::f_i64 | +|----------------------------------------------| +| yes_harness::f_i128 | +|----------------------------------------------| +| yes_harness::f_isize | +|----------------------------------------------| +| yes_harness::f_bool | +|----------------------------------------------| +| yes_harness::f_char | +|----------------------------------------------| +| yes_harness::f_f32 | +|----------------------------------------------| +| yes_harness::f_f64 | +|----------------------------------------------| +| yes_harness::f_f16 | +|----------------------------------------------| +| yes_harness::f_f128 | +|----------------------------------------------| +| yes_harness::f_nonzero_u8 | +|----------------------------------------------| +| yes_harness::f_nonzero_u16 | +|----------------------------------------------| +| yes_harness::f_nonzero_u32 | +|----------------------------------------------| +| yes_harness::f_nonzero_u64 | +|----------------------------------------------| +| yes_harness::f_nonzero_u128 | +|----------------------------------------------| +| yes_harness::f_nonzero_usize | +|----------------------------------------------| +| yes_harness::f_nonzero_i8 | +|----------------------------------------------| +| yes_harness::f_nonzero_i16 | +|----------------------------------------------| +| yes_harness::f_nonzero_i32 | +|----------------------------------------------| +| yes_harness::f_nonzero_i64 | +|----------------------------------------------| +| yes_harness::f_nonzero_i128 | +|----------------------------------------------| +| yes_harness::f_nonzero_isize | +|----------------------------------------------| +| yes_harness::f_array | +|----------------------------------------------| +| yes_harness::f_option | +|----------------------------------------------| +| yes_harness::f_result | +|----------------------------------------------| +| yes_harness::f_maybe_uninit | +|----------------------------------------------| +| yes_harness::f_tuple | +|----------------------------------------------| +| yes_harness::f_unsupported_return_type | +|----------------------------------------------| +| yes_harness::f_multiple_args | +|----------------------------------------------| +| yes_harness::f_derives_arbitrary | +|----------------------------------------------| +| yes_harness::f_manually_implements_arbitrary | +|----------------------------------------------| +| yes_harness::f_phantom_data | +|----------------------------------------------| +| yes_harness::f_phantom_pinned | +|----------------------------------------------| +| yes_harness::empty_body | ++----------------------------------------------+ + +Kani did not generate automatic harnesses for 8 function(s). +If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 ++----------------------------------------+------------------------------------------------------------------------------+ +| Skipped Function | Reason for Skipping | ++=======================================================================================================================+ +| no_harness::doesnt_implement_arbitrary | Missing Arbitrary implementation for argument(s) x: DoesntImplementArbitrary | +|----------------------------------------+------------------------------------------------------------------------------| +| no_harness::unsupported_const_pointer | Missing Arbitrary implementation for argument(s) _y: *const i32 | +|----------------------------------------+------------------------------------------------------------------------------| +| no_harness::unsupported_generic | Generic Function | +|----------------------------------------+------------------------------------------------------------------------------| +| no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s) _y: *mut i32 | +|----------------------------------------+------------------------------------------------------------------------------| +| no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s) _: &() | +|----------------------------------------+------------------------------------------------------------------------------| +| no_harness::unsupported_ref | Missing Arbitrary implementation for argument(s) _y: &i32 | +|----------------------------------------+------------------------------------------------------------------------------| +| no_harness::unsupported_slice | Missing Arbitrary implementation for argument(s) _y: &[u8] | +|----------------------------------------+------------------------------------------------------------------------------| +| no_harness::unsupported_vec | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec | ++----------------------------------------+------------------------------------------------------------------------------+ + Autoharness: Checking function yes_harness::f_tuple against all possible inputs... Autoharness: Checking function yes_harness::f_maybe_uninit against all possible inputs... Autoharness: Checking function yes_harness::f_result against all possible inputs... @@ -133,25 +244,3 @@ Autoharness Summary: | yes_harness::f_u8 | #[kani::proof] | Success | +----------------------------------------------+---------------------------+---------------------+ Complete - 42 successfully verified functions, 0 failures, 42 total. - -Kani did not generate automatic harnesses for the following functions. -If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 -+----------------------------------------+------------------------------------------------------+ -| Skipped Function | Reason for Skipping | -+===============================================================================================+ -| no_harness::doesnt_implement_arbitrary | Missing Arbitrary implementation for argument(s): x | -|----------------------------------------+------------------------------------------------------| -| no_harness::unsupported_const_pointer | Missing Arbitrary implementation for argument(s): _y | -|----------------------------------------+------------------------------------------------------| -| no_harness::unsupported_generic | Generic Function | -|----------------------------------------+------------------------------------------------------| -| no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s): _y | -|----------------------------------------+------------------------------------------------------| -| no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s): _ | -|----------------------------------------+------------------------------------------------------| -| no_harness::unsupported_ref | Missing Arbitrary implementation for argument(s): _y | -|----------------------------------------+------------------------------------------------------| -| no_harness::unsupported_slice | Missing Arbitrary implementation for argument(s): _y | -|----------------------------------------+------------------------------------------------------| -| no_harness::unsupported_vec | Missing Arbitrary implementation for argument(s): _y | -+----------------------------------------+------------------------------------------------------+ diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected index 8d1e15f4d92e..d1727ed86d03 100644 --- a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected @@ -1,3 +1,20 @@ +Kani generated automatic harnesses for 5 function(s): ++-------------------------+ +| Chosen Function | ++=========================+ +| oob_safe_array_access | +|-------------------------| +| oob_unsafe_array_access | +|-------------------------| +| integer_overflow | +|-------------------------| +| panic | +|-------------------------| +| unchecked_mul | ++-------------------------+ + +Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). + Autoharness: Checking function panic against all possible inputs... panic.assertion\ - Status: FAILURE\ @@ -72,5 +89,3 @@ Autoharness Summary: Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). Complete - 0 successfully verified functions, 5 failures, 5 total. - -Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). diff --git a/tests/script-based-pre/cargo_autoharness_include/include.expected b/tests/script-based-pre/cargo_autoharness_include/include.expected index 4c0192e92448..2f5e75ef5a3c 100644 --- a/tests/script-based-pre/cargo_autoharness_include/include.expected +++ b/tests/script-based-pre/cargo_autoharness_include/include.expected @@ -1,3 +1,20 @@ +Kani generated automatic harnesses for 1 function(s): ++-----------------+ +| Chosen Function | ++=================+ +| include::simple | ++-----------------+ + +Kani did not generate automatic harnesses for 2 function(s). +If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 ++------------------+--------------------------------+ +| Skipped Function | Reason for Skipping | ++===================================================+ +| excluded::simple | Did not match provided filters | +|------------------+--------------------------------| +| include::generic | Generic Function | ++------------------+--------------------------------+ + Autoharness: Checking function include::simple against all possible inputs... VERIFICATION:- SUCCESSFUL @@ -11,13 +28,3 @@ Autoharness Summary: | include::simple | #[kani::proof] | Success | +-------------------+---------------------------+---------------------+ Complete - 1 successfully verified functions, 0 failures, 1 total. - -Kani did not generate automatic harnesses for the following functions. -If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 -+------------------+--------------------------------+ -| Skipped Function | Reason for Skipping | -+===================================================+ -| excluded::simple | Did not match provided filters | -|------------------+--------------------------------| -| include::generic | Generic Function | -+------------------+--------------------------------+ diff --git a/tests/script-based-pre/cargo_autoharness_termination/termination.expected b/tests/script-based-pre/cargo_autoharness_termination/termination.expected index 0b36a4dbe67b..62aaf328f3d5 100644 --- a/tests/script-based-pre/cargo_autoharness_termination/termination.expected +++ b/tests/script-based-pre/cargo_autoharness_termination/termination.expected @@ -1,3 +1,16 @@ +Kani generated automatic harnesses for 3 function(s): ++--------------------------------+ +| Chosen Function | ++================================+ +| unwind_bound::infinite_loop | +|--------------------------------| +| unwind_bound::gcd_recursion | +|--------------------------------| +| timeout::check_harness_timeout | ++--------------------------------+ + +Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). + Autoharness: Checking function timeout::check_harness_timeout against all possible inputs... CBMC failed VERIFICATION:- FAILED @@ -38,5 +51,3 @@ Autoharness Summary: Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). Complete - 0 successfully verified functions, 3 failures, 3 total. - -Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s).