From f13a8b503212cd1f241aea999cfe4c4dd599a94d Mon Sep 17 00:00:00 2001 From: Srivatsan Samraj <321934658+srivatsansamraj@users.noreply.github.com> Date: Mon, 7 Sep 2026 12:48:40 -0700 Subject: [PATCH] Update autoharness_analyzer for current AutoHarnessSkipReason variants Kani changed GenericFn to carry a String (model-checking/kani#4679) and added RequiresBoundedArguments (model-checking/kani#4691). The analyzer keeps its own copy of the enum, which did not follow, so it fails to deserialize metadata from current Kani. Match the enum, normalize the old bare "GenericFn" form so CI on the pinned Kani keeps working, and report RequiresBoundedArguments in its own table. Resolves #679 --- scripts/autoharness_analyzer/README.md | 2 + scripts/autoharness_analyzer/src/main.rs | 67 ++++++++++++++++++- .../autoharness_analyzer/src/make_tables.rs | 45 ++++++++++--- 3 files changed, 103 insertions(+), 11 deletions(-) diff --git a/scripts/autoharness_analyzer/README.md b/scripts/autoharness_analyzer/README.md index 4304f4ecd5700..daf14fd489be7 100644 --- a/scripts/autoharness_analyzer/README.md +++ b/scripts/autoharness_analyzer/README.md @@ -11,6 +11,8 @@ kani autoharness --std ./library -Z function-contracts -Z mem-predicates -Z floa on the standard library. The scanner_results/ directory contains the CSV files that the [scanner tool in Kani](https://github.com/model-checking/kani/tree/main/tools/scanner) produces. +Without `--bounded-arguments`, functions whose arguments are only supported with bounded values are skipped with `Requires --bounded-arguments for argument(s)` and summarized in their own type-category table. + The output is `autoharness_data.md`, which contains Markdown tables summarizing the autoharness application across all the crates in the standard library. One of the tables has a column for "Skipped Type Categories." Generally speaking, "precise types" are what we think of as actual Rust types, and "type categories" are my subjective sense of how to group those types further. For example, `&mut i32` and `&mut u32` are two precise types, but they're in the same type category `&mut`. See the code for exact details on how we create type categories; the TL;DR is that we have a few hardcoded ones for raw pointers and references, and the rest we create using a fully-qualified path splitting heuristic. diff --git a/scripts/autoharness_analyzer/src/main.rs b/scripts/autoharness_analyzer/src/main.rs index b4095d4db44fc..1beda1c47eebf 100644 --- a/scripts/autoharness_analyzer/src/main.rs +++ b/scripts/autoharness_analyzer/src/main.rs @@ -52,9 +52,11 @@ pub struct AutoHarnessMetadata { /// Reasons that Kani does not generate an automatic harness for a function. #[derive(Debug, Clone, Serialize, Deserialize, Display, EnumString)] pub enum AutoHarnessSkipReason { - /// The function is generic. + /// The function is generic and autoharness could not find a monomorphic instantiation to + /// verify. The payload gives the specific reason (e.g. const generic parameters, or trait + /// bounds that no candidate type satisfies). #[strum(serialize = "Generic Function")] - GenericFn, + GenericFn(String), /// A Kani-internal function: already a harness, implementation of a Kani associated item or Kani contract instrumentation functions). #[strum(serialize = "Kani implementation")] KaniImpl, @@ -65,6 +67,11 @@ pub enum AutoHarnessSkipReason { /// The function does not have a body. #[strum(serialize = "The function does not have a body")] NoBody, + /// The function's arguments are only supported with bounded nondeterministic values, and + /// the user did not pass --bounded-arguments. + /// (The Vec<(String, String)> contains the list of (name, type) tuples for each such argument.) + #[strum(serialize = "Requires --bounded-arguments for argument(s)")] + RequiresBoundedArguments(Vec<(String, String)>), /// The function doesn't match the user's provided filters. #[strum(serialize = "Did not match provided filters")] UserFilter, @@ -90,6 +97,23 @@ impl AutoHarnessMetadata { } } +/// Kani at the commit in `tool_config/kani-version.toml` predates model-checking/kani#4679 and +/// writes `GenericFn` as a bare string, while current Kani writes `{"GenericFn": ""}`. +/// Rewrite the old form so both deserialize into `GenericFn(String)`. +fn normalize_skip_reasons(mut autoharness_md: Value) -> Value { + if let Some(skipped) = autoharness_md + .get_mut("skipped") + .and_then(Value::as_object_mut) + { + for reason in skipped.values_mut() { + if reason.as_str() == Some("GenericFn") { + *reason = serde_json::json!({ "GenericFn": "" }); + } + } + } + autoharness_md +} + fn main() -> Result<()> { let args = Args::parse(); @@ -127,7 +151,7 @@ fn main() -> Result<()> { let fn_to_row_data = process_scan_fns(scanner_fn_csv_path)?; let autoharness_md: AutoHarnessMetadata = - serde_json::from_value(v["autoharness_md"].clone())?; + serde_json::from_value(normalize_skip_reasons(v["autoharness_md"].clone()))?; if args.per_crate { // Process each crate separately @@ -165,3 +189,40 @@ fn main() -> Result<()> { Ok(()) } + +#[cfg(test)] +mod tests { + use super::*; + + fn parse(skipped: &str) -> AutoHarnessMetadata { + let v: Value = serde_json::from_str(&format!( + r#"{{"chosen": [], "skipped": {{"f": {skipped}}}}}"# + )) + .unwrap(); + serde_json::from_value(normalize_skip_reasons(v)).unwrap() + } + + #[test] + fn generic_fn_old_form() { + let md = parse(r#""GenericFn""#); + assert!(matches!(md.skipped["f"], AutoHarnessSkipReason::GenericFn(ref s) if s.is_empty())); + } + + #[test] + fn generic_fn_new_form() { + let md = parse(r#"{"GenericFn": "no candidate instantiation"}"#); + assert!(matches!( + md.skipped["f"], + AutoHarnessSkipReason::GenericFn(ref s) if s == "no candidate instantiation" + )); + } + + #[test] + fn requires_bounded_arguments() { + let md = parse(r#"{"RequiresBoundedArguments": [["s", "&[u8]"]]}"#); + let AutoHarnessSkipReason::RequiresBoundedArguments(args) = &md.skipped["f"] else { + panic!("wrong variant"); + }; + assert_eq!(args, &[("s".to_string(), "&[u8]".to_string())]); + } +} diff --git a/scripts/autoharness_analyzer/src/make_tables.rs b/scripts/autoharness_analyzer/src/make_tables.rs index b97de96bc1e06..f3b1e47ebdedf 100644 --- a/scripts/autoharness_analyzer/src/make_tables.rs +++ b/scripts/autoharness_analyzer/src/make_tables.rs @@ -85,8 +85,28 @@ fn skipped_overview_table(autoharness_md: &AutoHarnessMetadata) -> Result Option<&Vec<(String, String)>> { + match reason { + AutoHarnessSkipReason::MissingArbitraryImpl(args) => Some(args), + _ => None, + } +} + +/// Return the (name, type) pairs behind a `RequiresBoundedArguments` skip, if that is the reason. +fn bounded_arguments_args(reason: &AutoHarnessSkipReason) -> Option<&Vec<(String, String)>> { + match reason { + AutoHarnessSkipReason::RequiresBoundedArguments(args) => Some(args), + _ => None, + } +} + +/// Count the argument types behind every skip reason that `args_of` selects, grouped into +/// type categories. `category_header` names the first column. fn skipped_breakdown_table( autoharness_md: &AutoHarnessMetadata, + category_header: &str, + args_of: fn(&AutoHarnessSkipReason) -> Option<&Vec<(String, String)>>, show_precise_types: bool, ) -> Result { // Rust type -- &mut i32, &mut u32, bool, etc. @@ -114,7 +134,7 @@ fn skipped_breakdown_table( }; for reason in autoharness_md.skipped.values() { - if let AutoHarnessSkipReason::MissingArbitraryImpl(args) = reason { + if let Some(args) = args_of(reason) { for (_, arg_type) in args { let mut is_categorized = false; for category in &type_categories { @@ -151,15 +171,12 @@ fn skipped_breakdown_table( Ok(MarkdownTable::new( Some(if show_precise_types { vec![ - "Unsupported Type Category".to_string(), + category_header.to_string(), "# of occurences".to_string(), "Precise Types".to_string(), ] } else { - vec![ - "Unsupported Type Category".to_string(), - "# of occurences".to_string(), - ] + vec![category_header.to_string(), "# of occurences".to_string()] }), sorted_by_count .into_iter() @@ -235,7 +252,18 @@ pub fn compute_metrics( let chosen_overview_table = chosen_overview_table(&unsafe_metadata, fn_to_row_data)?; let skipped_overview_table = skipped_overview_table(&unsafe_metadata)?; - let skipped_breakdown_table = skipped_breakdown_table(&unsafe_metadata, show_precise_types)?; + let missing_arbitrary_table = skipped_breakdown_table( + &unsafe_metadata, + "Unsupported Type Category", + missing_arbitrary_args, + show_precise_types, + )?; + let bounded_arguments_table = skipped_breakdown_table( + &unsafe_metadata, + "Type Category Requiring --bounded-arguments", + bounded_arguments_args, + show_precise_types, + )?; let out_path = Path::new(&format!( "{}{}_autoharness_data", @@ -247,7 +275,8 @@ pub fn compute_metrics( write_table_to_file(&mut out_file, &chosen_overview_table)?; write_table_to_file(&mut out_file, &skipped_overview_table)?; - write_table_to_file(&mut out_file, &skipped_breakdown_table)?; + write_table_to_file(&mut out_file, &missing_arbitrary_table)?; + write_table_to_file(&mut out_file, &bounded_arguments_table)?; println!("Wrote results to {}", out_path.to_string_lossy());