Update autoharness_analyzer for current AutoHarnessSkipReason variants

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.

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": "<reason>"}`.
+/// 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())]);
+    }
+}

scripts/autoharness_analyzer/src/make_tables.rs

@@ -85,8 +85,28 @@ fn skipped_overview_table(autoharness_md: &AutoHarnessMetadata) -> Result<Markdo
     )?)
 }
 
+/// Return the (name, type) pairs behind a `MissingArbitraryImpl` skip, if that is the reason.
+fn missing_arbitrary_args(reason: &AutoHarnessSkipReason) -> 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<MarkdownTable> {
     // 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());