From 41274fc93450a8418752074dacf3028459fc859d Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Mar 2025 11:33:16 -0400 Subject: [PATCH 1/6] print argument types for missing Arbitrary implementations --- .../src/kani_middle/codegen_units.rs | 3 +- kani-driver/src/autoharness/mod.rs | 29 +++++++++----- kani_metadata/src/lib.rs | 4 +- .../cargo_autoharness_filter/filter.expected | 38 +++++++++---------- 4 files changed, 42 insertions(+), 32 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index a0f63463053d..c5c634c15bde 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -432,7 +432,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/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 69dd8b561103..e31597e2a730 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -59,17 +59,26 @@ fn print_skipped_fns(metadata: Vec) { 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(", "))]) + skipped_fns.add_rows(skipped_md.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, })); } diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index 2fe1038647c1..33ef5a422a5b 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -51,9 +51,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, diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected index f324effe3d9b..f98ee0e9ca93 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -136,22 +136,22 @@ 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 | -+----------------------------------------+------------------------------------------------------+ ++----------------------------------------+------------------------------------------------------------------------------+ +| 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 | ++----------------------------------------+------------------------------------------------------------------------------+ From b90c1b47a3fac39bb6424ee2e4a7356caeee57cf Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Mar 2025 12:42:39 -0400 Subject: [PATCH 2/6] Store chosen autoharness functions in KaniMetadata This refactor lets us print full autoharness metadata when --only-codegen is provided. Before this change, we only knew which functions we have autoharnesses for once verification finishes. --- .../compiler_interface.rs | 2 +- .../src/kani_middle/codegen_units.rs | 34 +++++++------------ kani-driver/src/autoharness/mod.rs | 9 +++-- kani-driver/src/metadata.rs | 2 +- kani_metadata/src/lib.rs | 18 ++++++---- 5 files changed, 33 insertions(+), 32 deletions(-) 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 c5c634c15bde..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(), } } } diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index e31597e2a730..7856b3cbc281 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -58,8 +58,8 @@ fn print_skipped_fns(metadata: Vec) { skipped_fns.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)| { + let skipped = md.autoharness_md.unwrap().skipped; + skipped_fns.add_rows(skipped.into_iter().filter_map(|(func, reason)| { match reason { AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => Some(vec![ func, @@ -89,7 +89,10 @@ fn print_skipped_fns(metadata: Vec) { return; } - println!("\nKani did not generate automatic harnesses for the following functions."); + println!( + "\nKani did not generate automatic harnesses for {} functions.", + skipped_fns.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" ); 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 33ef5a422a5b..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. @@ -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). From afbe148a8aa7f9557e1d7f51f0e78b1db325ad33 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Mar 2025 14:20:10 -0400 Subject: [PATCH 3/6] print chosen and skipped fns before verification --- kani-driver/src/autoharness/mod.rs | 60 +++++--- .../contracts.expected | 19 ++- .../dependencies.expected | 12 +- .../exclude.expected | 27 ++-- .../cargo_autoharness_filter/filter.expected | 133 +++++++++++++++--- .../harnesses_fail.expected | 19 ++- .../include.expected | 27 ++-- .../termination.expected | 15 +- 8 files changed, 242 insertions(+), 70 deletions(-) diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 7856b3cbc281..aefc7ea4bddc 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -26,10 +26,10 @@ pub fn autoharness_cargo(args: CargoAutoharnessArgs) -> Result<()> { args.common_autoharness_args.exclude_function, ); 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<()> { @@ -46,20 +46,24 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { } 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 + 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.autoharness_md.unwrap().skipped; - skipped_fns.add_rows(skipped.into_iter().filter_map(|(func, reason)| { + 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, @@ -82,21 +86,37 @@ fn print_skipped_fns(metadata: Vec) { })); } - 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 {} functions.", - skipped_fns.row_count() - ); + 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/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_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 f98ee0e9ca93..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: 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 | -+----------------------------------------+------------------------------------------------------------------------------+ 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). From 5e0c5042109f77511756fe4fb86d6d30d5a35531 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Mar 2025 14:27:44 -0400 Subject: [PATCH 4/6] print kani version for cargo --- kani-driver/src/autoharness/mod.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index aefc7ea4bddc..4c7fa69b0d00 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -25,6 +25,9 @@ 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)?; if !session.args.common_args.quiet { print_metadata(project.metadata.clone()); From 519099a9f489c29ec3711430d739d418db4b0574 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Mar 2025 15:02:23 -0400 Subject: [PATCH 5/6] add unsafe block to fix warning, c.f. https://github.com/rust-lang/rust/pull/112038 --- tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) } } } From d121010be73992cc083342e4e198d7b7e4f12eb1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 18 Mar 2025 17:47:44 -0400 Subject: [PATCH 6/6] add --std flag to autoharness --- kani-driver/src/args/autoharness_args.rs | 12 ++++++-- kani-driver/src/args/list_args.rs | 36 ++-------------------- kani-driver/src/args/mod.rs | 38 +++++++++++++++++++++++- kani-driver/src/args/std_args.rs | 36 ++-------------------- kani-driver/src/autoharness/mod.rs | 8 ++++- 5 files changed, 58 insertions(+), 72 deletions(-) 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 4c7fa69b0d00..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; @@ -48,7 +49,12 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { print_kani_version(InvocationType::Standalone); } - let project = project::standalone_project(&args.input, args.crate_name, &session)?; + 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()); }