diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index 5a5ed290dcad..c0d452ee6051 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -10,69 +10,64 @@ use crate::{ VerificationArgs, list_args::{CargoListArgs, StandaloneListArgs}, }, - list::ListMetadata, list::output::output_list_results, + list::{FileName, HarnessName, ListMetadata}, project::{Project, cargo_project, standalone_project, std_project}, session::KaniSession, version::print_kani_version, }; use anyhow::Result; -use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata}; +use kani_metadata::{ContractedFunction, HarnessKind, HarnessMetadata, KaniMetadata}; /// Process the KaniMetadata output from kani-compiler and output the list subcommand results -pub fn process_metadata(metadata: Vec) -> ListMetadata { - // We use ordered maps and sets so that the output is in lexicographic order (and consistent across invocations). - - // Map each file to a vector of its harnesses. - let mut standard_harnesses: BTreeMap> = BTreeMap::new(); - let mut contract_harnesses: BTreeMap> = BTreeMap::new(); +pub fn process_metadata(metadata: Vec) -> BTreeSet { + let mut list_metadata: BTreeSet = BTreeSet::new(); + + let insert = |harness_meta: HarnessMetadata, + map: &mut BTreeMap>, + count: &mut usize| { + *count += 1; + if let Some(harnesses) = map.get_mut(&harness_meta.original_file) { + harnesses.insert(harness_meta.pretty_name); + } else { + map.insert(harness_meta.original_file, BTreeSet::from([harness_meta.pretty_name])); + }; + }; - let mut contracted_functions: BTreeSet = BTreeSet::new(); + for kani_meta in metadata { + // We use ordered maps and sets so that the output is in lexicographic order (and consistent across invocations). + let mut standard_harnesses: BTreeMap> = BTreeMap::new(); + let mut contract_harnesses: BTreeMap> = BTreeMap::new(); + let mut contracted_functions: BTreeSet = BTreeSet::new(); - let mut standard_harnesses_count = 0; - let mut contract_harnesses_count = 0; + let mut standard_harnesses_count = 0; + let mut contract_harnesses_count = 0; - for kani_meta in metadata { for harness_meta in kani_meta.proof_harnesses { match harness_meta.attributes.kind { HarnessKind::Proof => { - standard_harnesses_count += 1; - if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file) - { - harnesses.insert(harness_meta.pretty_name); - } else { - standard_harnesses.insert( - harness_meta.original_file, - BTreeSet::from([harness_meta.pretty_name]), - ); - } + insert(harness_meta, &mut standard_harnesses, &mut standard_harnesses_count); } HarnessKind::ProofForContract { .. } => { - contract_harnesses_count += 1; - if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file) - { - harnesses.insert(harness_meta.pretty_name); - } else { - contract_harnesses.insert( - harness_meta.original_file, - BTreeSet::from([harness_meta.pretty_name]), - ); - } + insert(harness_meta, &mut contract_harnesses, &mut contract_harnesses_count); } HarnessKind::Test => {} } } contracted_functions.extend(kani_meta.contracted_functions.into_iter()); - } - ListMetadata { - standard_harnesses, - standard_harnesses_count, - contract_harnesses, - contract_harnesses_count, - contracted_functions, + list_metadata.insert(ListMetadata { + crate_name: kani_meta.crate_name, + standard_harnesses, + standard_harnesses_count, + contract_harnesses, + contract_harnesses_count, + contracted_functions, + }); } + + list_metadata } pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { diff --git a/kani-driver/src/list/mod.rs b/kani-driver/src/list/mod.rs index 0a5aa523ea6a..d300908d476d 100644 --- a/kani-driver/src/list/mod.rs +++ b/kani-driver/src/list/mod.rs @@ -8,15 +8,41 @@ use std::collections::{BTreeMap, BTreeSet}; pub mod collect_metadata; pub mod output; +type FileName = String; +type HarnessName = String; + +/// Metadata for the list subcommand for a given crate. +/// It is important that crate_name is the first field so that `Ord` orders two ListMetadata objects by crate name. +#[derive(PartialEq, Eq, PartialOrd, Ord)] pub struct ListMetadata { + crate_name: String, // Files mapped to their #[kani::proof] harnesses - standard_harnesses: BTreeMap>, + standard_harnesses: BTreeMap>, // Total number of #[kani::proof] harnesses standard_harnesses_count: usize, // Files mapped to their #[kani::proof_for_contract] harnesses - contract_harnesses: BTreeMap>, + contract_harnesses: BTreeMap>, // Total number of #[kani:proof_for_contract] harnesses contract_harnesses_count: usize, // Set of all functions under contract contracted_functions: BTreeSet, } + +/// Given a collection of ListMetadata objects, merge them into a single ListMetadata object. +pub fn merge_list_metadata(collection: T) -> ListMetadata +where + T: Extend, + T: IntoIterator, +{ + collection + .into_iter() + .reduce(|mut acc, item| { + acc.standard_harnesses.extend(item.standard_harnesses); + acc.standard_harnesses_count += item.standard_harnesses_count; + acc.contract_harnesses.extend(item.contract_harnesses); + acc.contract_harnesses_count += item.contract_harnesses_count; + acc.contracted_functions.extend(item.contracted_functions); + acc + }) + .expect("Cannot merge empty collection of ListMetadata objects") +} diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index 47b32bd6ed5e..e91f71a6c25f 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -3,13 +3,18 @@ //! This module handles outputting the result for the list subcommand use std::{ + collections::BTreeSet, fmt::Display, fs::File, io::{BufWriter, Write}, path::Path, }; -use crate::{args::list_args::Format, list::ListMetadata, version::KANI_VERSION}; +use crate::{ + args::list_args::Format, + list::{ListMetadata, merge_list_metadata}, + version::KANI_VERSION, +}; use anyhow::Result; use comfy_table::Table as PrettyTable; use serde_json::json; @@ -21,7 +26,11 @@ const FILE_VERSION: &str = "0.1"; const OUTPUT_FILENAME: &str = "kani-list"; /// Output the results of the list subcommand. -pub fn output_list_results(list_metadata: ListMetadata, format: Format, quiet: bool) -> Result<()> { +pub fn output_list_results( + list_metadata: BTreeSet, + format: Format, + quiet: bool, +) -> Result<()> { match format { Format::Pretty => pretty(list_metadata), Format::Markdown => markdown(list_metadata, quiet), @@ -29,36 +38,64 @@ pub fn output_list_results(list_metadata: ListMetadata, format: Format, quiet: b } } -/// Print results to the terminal. -fn pretty(list_metadata: ListMetadata) -> Result<()> { - let table = if list_metadata.contracted_functions.is_empty() { - None - } else { - let (header, rows) = construct_contracts_table(&list_metadata); - let mut t = PrettyTable::new(); - t.set_header(header).add_rows(rows); - Some(t) +fn pretty_constructor(header: Vec, rows: Vec>) -> Result { + let mut t = PrettyTable::new(); + t.set_header(header).add_rows(rows); + Ok(t) +} + +fn markdown_constructor(header: Vec, rows: Vec>) -> Result { + Ok(MarkdownTable::new(Some(header), rows)?) +} + +/// Construct the "Contracts" and "Standard Harnesses" tables. +/// `table_constructor` is a function that, given the header and rows for the tables, creates a particular kind of table. +fn construct_output( + list_metadata: BTreeSet, + table_constructor: fn(Vec, Vec>) -> Result, +) -> Result<(String, String)> { + let contract_output = { + const CONTRACTS_SECTION: &str = "Contracts:"; + const NO_CONTRACTS_MSG: &str = "No contracts or contract harnesses found."; + let contract_table = if list_metadata.iter().all(|md| md.contracted_functions.is_empty()) { + None + } else { + let (header, rows) = construct_contracts_table(&list_metadata); + let t = table_constructor(header, rows)?; + Some(t) + }; + format_results(contract_table, CONTRACTS_SECTION.to_string(), NO_CONTRACTS_MSG.to_string()) }; - let output = format_results(table, &list_metadata); - println!("{}", output); + let standard_output = { + const HARNESSES_SECTION: &str = "Standard Harnesses (#[kani::proof]):"; + const NO_HARNESSES_MSG: &str = "No standard harnesses found."; + let standard_table = { + let (header, rows) = construct_standard_table(&list_metadata); + let t = table_constructor(header, rows)?; + Some(t) + }; + format_results(standard_table, HARNESSES_SECTION.to_string(), NO_HARNESSES_MSG.to_string()) + }; + Ok((contract_output, standard_output)) +} + +/// Print results to the terminal. +fn pretty(list_metadata: BTreeSet) -> Result<()> { + let (contract_output, standard_output) = construct_output(list_metadata, pretty_constructor)?; + println!("{}", contract_output); + println!("{}", standard_output); Ok(()) } /// Output results to a Markdown file. -fn markdown(list_metadata: ListMetadata, quiet: bool) -> Result<()> { - let table = if list_metadata.contracted_functions.is_empty() { - None - } else { - let (header, rows) = construct_contracts_table(&list_metadata); - Some(MarkdownTable::new(Some(header), rows)?) - }; - - let output = format_results(table, &list_metadata); +fn markdown(list_metadata: BTreeSet, quiet: bool) -> Result<()> { + let (contract_output, standard_output) = construct_output(list_metadata, markdown_constructor)?; let out_path = Path::new(OUTPUT_FILENAME).with_extension("md"); let mut out_file = File::create(&out_path).unwrap(); - out_file.write_all(output.as_bytes()).unwrap(); + out_file.write_all(contract_output.as_bytes()).unwrap(); + out_file.write_all(standard_output.as_bytes()).unwrap(); if !quiet { println!("Wrote list results to {}", std::fs::canonicalize(&out_path)?.display()); } @@ -66,21 +103,23 @@ fn markdown(list_metadata: ListMetadata, quiet: bool) -> Result<()> { } /// Output results as a JSON file. -fn json(list_metadata: ListMetadata, quiet: bool) -> Result<()> { +fn json(list_metadata: BTreeSet, quiet: bool) -> Result<()> { let out_path = Path::new(OUTPUT_FILENAME).with_extension("json"); let out_file = File::create(&out_path).unwrap(); let writer = BufWriter::new(out_file); + let combined_md = merge_list_metadata(list_metadata); + let json_obj = json!({ "kani-version": KANI_VERSION, "file-version": FILE_VERSION, - "standard-harnesses": &list_metadata.standard_harnesses, - "contract-harnesses": &list_metadata.contract_harnesses, - "contracts": &list_metadata.contracted_functions, + "standard-harnesses": combined_md.standard_harnesses, + "contract-harnesses": combined_md.contract_harnesses, + "contracts": combined_md.contracted_functions, "totals": { - "standard-harnesses": list_metadata.standard_harnesses_count, - "contract-harnesses": list_metadata.contract_harnesses_count, - "functions-under-contract": list_metadata.contracted_functions.len(), + "standard-harnesses": combined_md.standard_harnesses_count, + "contract-harnesses": combined_md.contract_harnesses_count, + "functions-under-contract": combined_md.contracted_functions.len(), } }); @@ -95,65 +134,95 @@ fn json(list_metadata: ListMetadata, quiet: bool) -> Result<()> { /// Construct the rows for the table of contracts information. /// Returns a tuple of the table header and the rows. -fn construct_contracts_table(list_metadata: &ListMetadata) -> (Vec, Vec>) { +fn construct_contracts_table( + list_metadata: &BTreeSet, +) -> (Vec, Vec>) { const NO_HARNESSES_MSG: &str = "NONE"; + const CRATE_NAME: &str = "Crate"; const FUNCTION_HEADER: &str = "Function"; const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])"; const TOTALS_HEADER: &str = "Total"; - let header = - vec![String::new(), FUNCTION_HEADER.to_string(), CONTRACT_HARNESSES_HEADER.to_string()]; + let header = vec![ + String::new(), + CRATE_NAME.to_string(), + FUNCTION_HEADER.to_string(), + CONTRACT_HARNESSES_HEADER.to_string(), + ]; let mut rows: Vec> = vec![]; - - for cf in &list_metadata.contracted_functions { - let mut row = vec![String::new(), cf.function.clone()]; - if cf.harnesses.is_empty() { - row.push(NO_HARNESSES_MSG.to_string()); - } else { - row.push(cf.harnesses.join(", ")); + let mut functions_under_contract_total = 0; + let mut contract_harnesses_total = 0; + + for crate_md in list_metadata { + for cf in &crate_md.contracted_functions { + let mut row = vec![String::new(), crate_md.crate_name.to_string(), cf.function.clone()]; + if cf.harnesses.is_empty() { + row.push(NO_HARNESSES_MSG.to_string()); + } else { + row.push(cf.harnesses.join(", ")); + } + rows.push(row); } - rows.push(row); + functions_under_contract_total += crate_md.contracted_functions.len(); + contract_harnesses_total += crate_md.contract_harnesses_count; } let totals_row = vec![ TOTALS_HEADER.to_string(), - list_metadata.contracted_functions.len().to_string(), - list_metadata.contract_harnesses_count.to_string(), + String::new(), + functions_under_contract_total.to_string(), + contract_harnesses_total.to_string(), ]; rows.push(totals_row); (header, rows) } -/// Format results as a String -fn format_results(table: Option, list_metadata: &ListMetadata) -> String { - const CONTRACTS_SECTION: &str = "Contracts:"; - const HARNESSES_SECTION: &str = "Standard Harnesses (#[kani::proof]):"; - const NO_CONTRACTS_MSG: &str = "No contracts or contract harnesses found."; - const NO_HARNESSES_MSG: &str = "No standard harnesses found."; +fn construct_standard_table( + list_metadata: &BTreeSet, +) -> (Vec, Vec>) { + const CRATE_NAME: &str = "Crate"; + const HARNESS_HEADER: &str = "Harness"; + const TOTALS_HEADER: &str = "Total"; - let mut output: Vec = vec![]; - output.push(format!("\n{CONTRACTS_SECTION}")); + let header = vec![String::new(), CRATE_NAME.to_string(), HARNESS_HEADER.to_string()]; - if let Some(table) = table { - output.push(format!("{table}")); - } else { - output.push(NO_CONTRACTS_MSG.to_string()); - } + let mut rows: Vec> = vec![]; - output.push(format!("\n{HARNESSES_SECTION}")); - if list_metadata.standard_harnesses.is_empty() { - output.push(NO_HARNESSES_MSG.to_string()); + let mut total = 0; + + for crate_md in list_metadata { + for harnesses in crate_md.standard_harnesses.values() { + for harness in harnesses { + rows.push(vec![ + String::new(), + crate_md.crate_name.to_string(), + harness.to_string(), + ]); + } + total += harnesses.len(); + } } - let mut std_harness_index = 0; + let totals_row = vec![TOTALS_HEADER.to_string(), String::new(), total.to_string()]; + rows.push(totals_row); + + (header, rows) +} - for harnesses in (&list_metadata.standard_harnesses).values() { - for harness in harnesses { - output.push(format!("{}. {harness}", std_harness_index + 1)); - std_harness_index += 1; - } +fn format_results( + table: Option, + section_name: String, + absent_name: String, +) -> String { + let mut output: Vec = vec![]; + output.push(format!("\n{section_name}")); + + if let Some(table) = table { + output.push(format!("{table}")); + } else { + output.push(absent_name); } output.join("\n") diff --git a/tests/script-based-pre/cargo_autoharness_list/list.expected b/tests/script-based-pre/cargo_autoharness_list/list.expected index 4c9feb73d184..06eccba6fef3 100644 --- a/tests/script-based-pre/cargo_autoharness_list/list.expected +++ b/tests/script-based-pre/cargo_autoharness_list/list.expected @@ -12,15 +12,21 @@ Kani generated automatic harnesses for 3 function(s): Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). Contracts: -+-------+---------------------------+-----------------------------------------------------------------------------+ -| | Function | Contract Harnesses (#[kani::proof_for_contract]) | -+=================================================================================================================+ -| | has_recursion_gcd | my_harness, my_harness_2, kani::internal::automatic_harness | -|-------+---------------------------+-----------------------------------------------------------------------------| -| | verify::has_recursion_gcd | verify::my_harness, verify::my_harness_2, kani::internal::automatic_harness | -|-------+---------------------------+-----------------------------------------------------------------------------| -| Total | 2 | 6 | -+-------+---------------------------+-----------------------------------------------------------------------------+ ++-------+------------------------+---------------------------+-----------------------------------------------------------------------------+ +| | Crate | Function | Contract Harnesses (#[kani::proof_for_contract]) | ++==========================================================================================================================================+ +| | cargo_autoharness_list | has_recursion_gcd | my_harness, my_harness_2, kani::internal::automatic_harness | +|-------+------------------------+---------------------------+-----------------------------------------------------------------------------| +| | cargo_autoharness_list | verify::has_recursion_gcd | verify::my_harness, verify::my_harness_2, kani::internal::automatic_harness | +|-------+------------------------+---------------------------+-----------------------------------------------------------------------------| +| Total | | 2 | 6 | ++-------+------------------------+---------------------------+-----------------------------------------------------------------------------+ Standard Harnesses (#[kani::proof]): -1. f_u8 ++-------+------------------------+---------+ +| | Crate | Harness | ++==========================================+ +| | cargo_autoharness_list | f_u8 | +|-------+------------------------+---------| +| Total | | 1 | ++-------+------------------------+---------+ diff --git a/tests/script-based-pre/cargo_list_md/list.expected b/tests/script-based-pre/cargo_list_md/list.expected index 9e913345e664..fcaf72a14d00 100644 --- a/tests/script-based-pre/cargo_list_md/list.expected +++ b/tests/script-based-pre/cargo_list_md/list.expected @@ -1,14 +1,16 @@ Contracts: -| | Function | Contract Harnesses (#[kani::proof_for_contract]) | -| ----- | ----------------------------- | -------------------------------------------------------------- | -| | example::implementation::bar | example::verify::check_bar | -| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | -| | example::implementation::func | example::verify::check_func | -| | example::prep::parse | NONE | -| Total | 4 | 4 | - +| | Crate | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ----- | ----------------------------- | -------------------------------------------------------------- | +| | lib | example::implementation::bar | example::verify::check_bar | +| | lib | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | lib | example::implementation::func | example::verify::check_func | +| | lib | example::prep::parse | NONE | +| Total | | 4 | 4 | Standard Harnesses (#[kani::proof]): -1. standard_harnesses::example::verify::check_modify -2. standard_harnesses::example::verify::check_new \ No newline at end of file +| | Crate | Harness | +| ----- | ----- | ------------------------------------------------- | +| | lib | standard_harnesses::example::verify::check_modify | +| | lib | standard_harnesses::example::verify::check_new | +| Total | | 2 | diff --git a/tests/script-based-pre/kani_list_md/list.expected b/tests/script-based-pre/kani_list_md/list.expected index eb4ca335d678..1184443beaa1 100644 --- a/tests/script-based-pre/kani_list_md/list.expected +++ b/tests/script-based-pre/kani_list_md/list.expected @@ -1,14 +1,16 @@ Contracts: -| | Function | Contract Harnesses (#[kani::proof_for_contract]) | -| ----- | ----------------------------- | -------------------------------------------------------------- | -| | example::implementation::bar | example::verify::check_bar | -| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | -| | example::implementation::func | example::verify::check_func | -| | example::prep::parse | NONE | -| Total | 4 | 4 | - +| | Crate | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ----- | ----------------------------- | -------------------------------------------------------------- | +| | lib | example::implementation::bar | example::verify::check_bar | +| | lib | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | lib | example::implementation::func | example::verify::check_func | +| | lib | example::prep::parse | NONE | +| Total | | 4 | 4 | Standard Harnesses (#[kani::proof]): -1. example::verify::check_modify -2. example::verify::check_new \ No newline at end of file +| | Crate | Harness | +| ----- | ----- | ----------------------------- | +| | lib | example::verify::check_modify | +| | lib | example::verify::check_new | +| Total | | 2 |