diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index fd949f8eef552..11245c49b5d4f 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -176,12 +176,14 @@ jobs: # Step 3: Add output to job summary - name: Add Autoharness Analyzer output to job summary run: | + pushd scripts/autoharness_analyzer echo "# Autoharness Failure Summary" >> "$GITHUB_STEP_SUMMARY" echo "## Crate core, all functions" >> "$GITHUB_STEP_SUMMARY" - cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + cat core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" echo "## Crate core, unsafe functions" >> "$GITHUB_STEP_SUMMARY" - cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + cat core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" echo "## Crate std, all functions" >> "$GITHUB_STEP_SUMMARY" - cat autoharness_analyzer/std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + cat std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" echo "## Crate std, unsafe functions" >> "$GITHUB_STEP_SUMMARY" - cat autoharness_analyzer/std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + cat std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + popd diff --git a/.gitignore b/.gitignore index 4bafa69269a57..39ad701a8883f 100644 --- a/.gitignore +++ b/.gitignore @@ -22,6 +22,7 @@ Session.vim /kani_build/ /target library/target +scripts/autoharness_analyzer/target/ *.rlib *.rmeta *.mir diff --git a/scripts/autoharness_analyzer/Cargo.toml b/scripts/autoharness_analyzer/Cargo.toml new file mode 100644 index 0000000000000..ced4df4b5dab3 --- /dev/null +++ b/scripts/autoharness_analyzer/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "autoharness_analyzer" +version = "0.1.0" +edition = "2021" + +[dependencies] +anyhow = "1.0.97" +clap = {version = "4.5.37", features = ["derive"] } +serde = { version = "1.0.219", features = ["derive"] } +serde_json = "1.0.140" +strum = "0.27.1" +strum_macros = "0.27.1" +to_markdown_table = "0.1.5" diff --git a/scripts/autoharness_analyzer/README.md b/scripts/autoharness_analyzer/README.md new file mode 100644 index 0000000000000..4304f4ecd5700 --- /dev/null +++ b/scripts/autoharness_analyzer/README.md @@ -0,0 +1,16 @@ +Invoke with: +``` +cargo run metadata/ scanner_results/ +``` + +The metadata/ folder contains the kani-metadata.json files produced by running: + +``` +kani autoharness --std ./library -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts --only-codegen --no-assert-contracts -j --output-format=terse -Z unstable-options -Z autoharness --cbmc-args --object-bits 12 +``` + +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. + +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 new file mode 100644 index 0000000000000..b4095d4db44fc --- /dev/null +++ b/scripts/autoharness_analyzer/src/main.rs @@ -0,0 +1,167 @@ +use anyhow::Result; +use clap::Parser; +use make_tables::compute_metrics; +use parse_scanner_output::process_scan_fns; +use serde::{Deserialize, Serialize}; +use serde_json::Value; +use std::{ + collections::{BTreeMap, HashMap}, + fs, + path::Path, +}; +use strum_macros::{Display, EnumString}; + +mod make_tables; +mod parse_scanner_output; + +#[derive(Parser, Debug)] +struct Args { + /// Path to directory with kani_metadata.json files + #[arg(required = true)] + metadata_dir_path: String, + + /// Scanner results directory path + #[arg(required = true)] + scanner_results_path: String, + + /// Generate per-crate tables instead of combined data + #[arg(long)] + per_crate: bool, + + /// Process only the specified crate + #[arg(long, value_name = "CRATE")] + for_crate: Option, + + /// Show precise types in the output tables + #[arg(long)] + show_precise_types: bool, + + /// Only output data for unsafe functions + #[arg(long)] + unsafe_fns_only: bool, +} +#[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. +#[derive(Debug, Clone, Serialize, Deserialize, Display, EnumString)] +pub enum AutoHarnessSkipReason { + /// The function is generic. + #[strum(serialize = "Generic Function")] + GenericFn, + /// A Kani-internal function: already a harness, implementation of a Kani associated item or Kani contract instrumentation functions). + #[strum(serialize = "Kani implementation")] + KaniImpl, + /// At least one of the function's arguments does not implement kani::Arbitrary + /// (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<(String, String)>), + /// The function does not have a body. + #[strum(serialize = "The function does not have a body")] + NoBody, + /// The function doesn't match the user's provided filters. + #[strum(serialize = "Did not match provided filters")] + UserFilter, +} + +impl Default for AutoHarnessMetadata { + fn default() -> Self { + Self::new() + } +} + +impl AutoHarnessMetadata { + pub fn new() -> Self { + Self { + chosen: Vec::new(), + skipped: BTreeMap::new(), + } + } + + pub fn extend(&mut self, other: AutoHarnessMetadata) { + self.chosen.extend(other.chosen); + self.skipped.extend(other.skipped); + } +} + +fn main() -> Result<()> { + let args = Args::parse(); + + // Collection of data from all crates + let mut cross_crate_fn_to_row_data = HashMap::new(); + let mut cross_crate_autoharness_md = AutoHarnessMetadata::new(); + + // Iterate over all kani-metadata.json files; one per crate + for entry in fs::read_dir(&args.metadata_dir_path)? { + let entry = entry?; + let path = entry.path(); + if !path.to_string_lossy().contains("kani-metadata.json") { + continue; + } + + let kani_md_file_data = + std::fs::read_to_string(&path).unwrap_or_else(|_| panic!("Unable to read {:?}", path)); + let v: Value = serde_json::from_str(&kani_md_file_data)?; + let crate_name = v["crate_name"].as_str().unwrap(); + + // Skip if a specific crate was requested and this isn't it + if let Some(ref target_crate) = args.for_crate { + if target_crate != crate_name { + continue; + } + } + + println!("Processing crate {crate_name}"); + + let scanner_fn_csv = format!( + "{}/{}_scan_functions.csv", + args.scanner_results_path, crate_name + ); + let scanner_fn_csv_path = Path::new(&scanner_fn_csv); + let fn_to_row_data = process_scan_fns(scanner_fn_csv_path)?; + + let autoharness_md: AutoHarnessMetadata = + serde_json::from_value(v["autoharness_md"].clone())?; + + if args.per_crate { + // Process each crate separately + compute_metrics( + crate_name, + &autoharness_md, + &fn_to_row_data, + args.show_precise_types, + args.unsafe_fns_only, + )?; + } else if args.for_crate.is_some() { + return compute_metrics( + crate_name, + &autoharness_md, + &fn_to_row_data, + args.show_precise_types, + args.unsafe_fns_only, + ); + } else { + cross_crate_fn_to_row_data.extend(fn_to_row_data); + cross_crate_autoharness_md.extend(autoharness_md); + } + } + + // Process combined data if not doing per-crate or single-crate analysis + if !args.per_crate { + compute_metrics( + "all_crates", + &cross_crate_autoharness_md, + &cross_crate_fn_to_row_data, + args.show_precise_types, + args.unsafe_fns_only, + )?; + } + + Ok(()) +} diff --git a/scripts/autoharness_analyzer/src/make_tables.rs b/scripts/autoharness_analyzer/src/make_tables.rs new file mode 100644 index 0000000000000..b97de96bc1e06 --- /dev/null +++ b/scripts/autoharness_analyzer/src/make_tables.rs @@ -0,0 +1,255 @@ +use anyhow::Result; + +use std::{ + collections::{BTreeMap, HashMap, HashSet}, + fs::File, + io::Write, + path::Path, +}; + +use to_markdown_table::MarkdownTable; + +use crate::{parse_scanner_output::ScanFnsRow, AutoHarnessMetadata, AutoHarnessSkipReason}; + +/// Create Markdown tables with the analysis results +fn chosen_overview_table( + autoharness_md: &AutoHarnessMetadata, + fn_to_row_data: &HashMap, +) -> Result { + let mut safe_count = 0; + let mut safe_abstractions_count = 0; + let mut unsafe_count = 0; + + for fn_name in &autoharness_md.chosen { + if let Some(record) = fn_to_row_data.get(fn_name) { + if record.is_unsafe { + unsafe_count += 1; + } else if record.has_unsafe_ops { + safe_abstractions_count += 1; + } else { + safe_count += 1; + } + } else { + // See https://github.com/model-checking/verify-rust-std/pull/350#discussion_r2091698600 + // for examples of when such discrepancies appear + println!( + "[WARNING] Function {} is in in autoharness metadata but absent in scanner tool output", + fn_name + ); + } + } + + Ok(MarkdownTable::new( + Some(vec!["Functions with Automatic Harnesses", "Count"]), + vec![ + vec!["Safe Functions".into(), safe_count.to_string()], + vec![ + "Safe Abstractions".into(), + safe_abstractions_count.to_string(), + ], + vec!["Unsafe Functions".into(), unsafe_count.to_string()], + vec![ + "Total".into(), + (safe_count + safe_abstractions_count + unsafe_count).to_string(), + ], + ], + )?) +} + +fn skipped_overview_table(autoharness_md: &AutoHarnessMetadata) -> Result { + // Map the String representation of each `AutoharnessSkipReason` to the number of times it appears + // We convert to a string first so that we treat all MissingArbitraryImpls as the same key, instead of differentiating on its vector contents. + let mut skip_reason_count: BTreeMap = BTreeMap::new(); + + for reason in autoharness_md.skipped.values() { + *skip_reason_count.entry(reason.to_string()).or_insert(0) += 1; + } + + // Sort in decreasing order by count so that most popular categories are in the first rows + let mut sorted_by_count = skip_reason_count.into_iter().collect::>(); + sorted_by_count.sort_by(|(_, count_a), (_, count_b)| count_b.cmp(count_a)); + + Ok(MarkdownTable::new( + Some(vec![ + "Reason function was skipped".to_string(), + "# of functions skipped for this reason".to_string(), + ]), + sorted_by_count + .iter() + .map(|(reason, count)| vec![reason.to_string(), count.to_string()]) + .chain(std::iter::once(vec![ + "Total".to_string(), + autoharness_md.skipped.len().to_string(), + ])) + .collect(), + )?) +} + +fn skipped_breakdown_table( + autoharness_md: &AutoHarnessMetadata, + show_precise_types: bool, +) -> Result { + // Rust type -- &mut i32, &mut u32, bool, etc. + type PreciseType = String; + // Grouping of PreciseTypes into larger categories, e.g. &mut i32 and &mut u32 are both in the same category of mutable reference + type TypeCategory = String; + // Count occurrences of TypeCategories across function arguments + type Count = u32; + + // The order is important; mutable references must come before immutable ones, + // so that we check for starting with &mut before falling back on checking for just & + let type_categories = ["&mut", "&", "*const", "*mut"].map(TypeCategory::from); + // Map each type category to (number of occurrences, list of precise types matching the category) + // e.g. if we encounter two &mut i32s and one &mut u32, we'd have &mut: (3, {&mut i32, &mut u32}) + let mut category_to_types: HashMap)> = + HashMap::new(); + + let mut insert_category = |category: TypeCategory, arg_type: PreciseType| { + if let Some((count, precise_types)) = category_to_types.get_mut(&category) { + *count += 1; + precise_types.insert(arg_type); + } else { + category_to_types.insert(category, (1, HashSet::from([arg_type.clone()]))); + } + }; + + for reason in autoharness_md.skipped.values() { + if let AutoHarnessSkipReason::MissingArbitraryImpl(args) = reason { + for (_, arg_type) in args { + let mut is_categorized = false; + for category in &type_categories { + if arg_type.starts_with(category) { + insert_category(category.clone(), arg_type.clone()); + is_categorized = true; + // break to avoid categorizing mutable references as immutable ones as well + break; + } + } + if !is_categorized { + // If arg_type doesn't fit into one of the predefined categories, + // create a TypeCategory and PreciseType for it by splitting on the last double semicolon + // e.g. if arg_type is "num::saturating::Saturating", produce new TypeCategory "num::saturating" and PreciseType "Saturating" + if let Some((type_category, precise_type)) = arg_type.rsplit_once("::") { + insert_category(type_category.into(), precise_type.into()); + } else { + insert_category("other".into(), arg_type.clone()); + } + } + } + } + } + + // Sort in decreasing order by count so that most popular categories are in the first rows + let mut sorted_by_count = category_to_types.into_iter().collect::>(); + sorted_by_count.sort_by(|(_, (count_a, _)), (_, (count_b, _))| count_b.cmp(count_a)); + + let total_precise_types = sorted_by_count + .iter() + .map(|(_, (_, precise_types))| precise_types.len()) + .sum::(); + + Ok(MarkdownTable::new( + Some(if show_precise_types { + vec![ + "Unsupported Type Category".to_string(), + "# of occurences".to_string(), + "Precise Types".to_string(), + ] + } else { + vec![ + "Unsupported Type Category".to_string(), + "# of occurences".to_string(), + ] + }), + sorted_by_count + .into_iter() + .map(|(category, (count, precise_types))| { + if show_precise_types { + vec![ + category.to_string(), + count.to_string(), + precise_types + .iter() + .map(|precise_type| precise_type.to_string()) + .collect::>() + .join(", "), + ] + } else { + vec![category.to_string(), count.to_string()] + } + }) + .chain(std::iter::once(if show_precise_types { + vec![ + "Total".to_string(), + total_precise_types.to_string(), + "".to_string(), + ] + } else { + vec!["Total".to_string(), total_precise_types.to_string()] + })) + .collect(), + )?) +} + +fn write_table_to_file(out_file: &mut File, table: &MarkdownTable) -> Result<()> { + let mut table_as_string = table.to_string(); + table_as_string.push('\n'); + Ok(out_file.write_all(table_as_string.as_bytes())?) +} + +pub fn compute_metrics( + crate_name: &str, + autoharness_md: &AutoHarnessMetadata, + fn_to_row_data: &HashMap, + show_precise_types: bool, + unsafe_fns_only: bool, +) -> Result<()> { + let unsafe_metadata = if unsafe_fns_only { + AutoHarnessMetadata { + chosen: autoharness_md + .chosen + .iter() + .filter(|fn_name| { + fn_to_row_data + .get(*fn_name) + .map(|row| row.is_unsafe) + .unwrap_or(false) + }) + .cloned() + .collect(), + skipped: autoharness_md + .skipped + .iter() + .filter(|(fn_name, _)| { + fn_to_row_data + .get(*fn_name) + .map(|row| row.is_unsafe) + .unwrap_or(false) + }) + .map(|(k, v)| (k.clone(), v.clone())) + .collect(), + } + } else { + autoharness_md.clone() + }; + + 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 out_path = Path::new(&format!( + "{}{}_autoharness_data", + crate_name, + if unsafe_fns_only { "_unsafe" } else { "" } + )) + .with_extension("md"); + let mut out_file = File::create(&out_path)?; + + 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)?; + + println!("Wrote results to {}", out_path.to_string_lossy()); + + Ok(()) +} diff --git a/scripts/autoharness_analyzer/src/parse_scanner_output.rs b/scripts/autoharness_analyzer/src/parse_scanner_output.rs new file mode 100644 index 0000000000000..243134a0c3d80 --- /dev/null +++ b/scripts/autoharness_analyzer/src/parse_scanner_output.rs @@ -0,0 +1,87 @@ +use anyhow::bail; +use anyhow::Result; +use serde::Deserialize; +use std::collections::HashMap; +use std::fs::File; +use std::io::BufRead; +use std::io::BufReader; +use std::path::Path; + +// Parse the CSV files that the Kani `scanner` tool outputs +// and store which functions are safe and unsafe + +// Number of columns in {crate_name}_scan_functions.csv. +const SCANNER_COLS: usize = 6; + +/// Single row of data in {crate_name}_scan_functions.csv +#[derive(Debug, Deserialize)] +#[allow(dead_code)] +pub struct ScanFnsRow { + pub name: String, + pub is_unsafe: bool, + pub has_unsafe_ops: bool, + has_unsupported_input: bool, + has_loop_or_iterator: bool, +} + +pub fn process_scan_fns(file_path: &Path) -> Result> { + let file = File::open(file_path).unwrap_or_else(|_| panic!("Cannot open file {:?}", file_path)); + let reader = BufReader::new(file); + let mut fn_to_row_data = HashMap::new(); + + for (index, line) in reader.lines().enumerate().skip(1) { + let line = line?; + + // The entries are split by semicolons, but we can't just split by that since the function names can also include semicolons + // e.g. the row "ptr::mut_ptr::::as_mut_ptr";false;false;true;false. + // So split by ;true or ;false instead--whichever comes first--then take everything before the match as the function name + let true_index = line.find(";true"); + let false_index = line.find(";false"); + + let split_index = match (true_index, false_index) { + (Some(t), Some(f)) => t.min(f), + (Some(t), None) => t, + (None, Some(f)) => f, + (None, None) => bail!("Invalid format in line {}: {}", index + 1, line), + }; + + let (name, rest) = line.split_at(split_index); + let mut fields = vec![name]; + // Now that we've found the function name, the rest is just booleans, so we can split by ; to get the rest + fields.extend(rest[1..].split(';')); + + parse_row(&mut fn_to_row_data, fields, index + 1)?; + } + + Ok(fn_to_row_data) +} + +fn parse_row( + rows: &mut HashMap, + fields: Vec<&str>, + line_number: usize, +) -> Result<()> { + if fields.len() != SCANNER_COLS { + bail!( + "Expected {} fields, got {} in line {}. Fields: {:?}", + SCANNER_COLS, + fields.len(), + line_number, + fields + ); + } + + let fn_name = fields[0].to_string(); + rows.insert( + fn_name.clone(), + ScanFnsRow { + name: fn_name, + is_unsafe: fields[1].parse().unwrap_or(false), + has_unsafe_ops: fields[2].parse().unwrap_or(false), + has_unsupported_input: fields[3].parse().unwrap_or(false), + has_loop_or_iterator: fields[4].parse().unwrap_or(false), + }, + ); + + Ok(()) +} diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 1abe73df88b12..24326cd2ced0c 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -358,14 +358,14 @@ main() { ./std-analysis.sh $build_dir popd echo "Running autoharness-analyzer command..." - git clone --depth 1 https://github.com/carolynzech/autoharness_analyzer - cd autoharness_analyzer + pushd scripts/autoharness_analyzer cargo run -- --per-crate \ - ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ + ../../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ /tmp/std_lib_analysis/results/ cargo run -- --per-crate --unsafe-fns-only \ - ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ + ../../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ /tmp/std_lib_analysis/results/ + popd fi }