diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index 89970abe0b6b..ebd97d01f2fb 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -42,15 +42,15 @@ pub struct StandaloneListArgs { pub std: bool, } -/// Message formats available for the subcommand. +/// Output formats available for the subcommand. #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] #[strum(serialize_all = "kebab-case")] pub enum Format { /// Print output in human-readable format. Pretty, - /// Print output in Markdown format. + /// Write output to a Markdown file. Markdown, - /// Print output in JSON format. + /// Write output to a JSON file. Json, } diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index 50ee19f069c0..a7901e997ab1 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -8,9 +8,9 @@ use crate::{ InvocationType, args::{ VerificationArgs, - list_args::{CargoListArgs, Format, StandaloneListArgs}, + list_args::{CargoListArgs, StandaloneListArgs}, }, - list::Totals, + list::ListMetadata, list::output::output_list_results, project::{Project, cargo_project, standalone_project, std_project}, session::KaniSession, @@ -20,7 +20,7 @@ use anyhow::Result; use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata}; /// Process the KaniMetadata output from kani-compiler and output the list subcommand results -fn process_metadata(metadata: Vec, format: Format) -> Result<()> { +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. @@ -29,14 +29,14 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { let mut contracted_functions: BTreeSet = BTreeSet::new(); - let mut total_standard_harnesses = 0; - let mut total_contract_harnesses = 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 => { - total_standard_harnesses += 1; + standard_harnesses_count += 1; if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file) { harnesses.insert(harness_meta.pretty_name); @@ -48,7 +48,7 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { } } HarnessKind::ProofForContract { .. } => { - total_contract_harnesses += 1; + contract_harnesses_count += 1; if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file) { harnesses.insert(harness_meta.pretty_name); @@ -66,36 +66,34 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { contracted_functions.extend(kani_meta.contracted_functions.into_iter()); } - let totals = Totals { - standard_harnesses: total_standard_harnesses, - contract_harnesses: total_contract_harnesses, - contracted_functions: contracted_functions.len(), - }; - - output_list_results( + ListMetadata { standard_harnesses, + standard_harnesses_count, contract_harnesses, + contract_harnesses_count, contracted_functions, - totals, - format, - ) + } } pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { + let quiet = args.common_args.quiet; verify_opts.common_args = args.common_args; let session = KaniSession::new(verify_opts)?; - if !session.args.common_args.quiet { + if !quiet { print_kani_version(InvocationType::CargoKani(vec![])); } let project = cargo_project(&session, false)?; - process_metadata(project.metadata, args.format) + let list_metadata = process_metadata(project.metadata); + + output_list_results(list_metadata, args.format, quiet) } pub fn list_standalone(args: StandaloneListArgs, mut verify_opts: VerificationArgs) -> Result<()> { + let quiet = args.common_args.quiet; verify_opts.common_args = args.common_args; let session = KaniSession::new(verify_opts)?; - if !session.args.common_args.quiet { + if !quiet { print_kani_version(InvocationType::Standalone); } @@ -105,5 +103,7 @@ pub fn list_standalone(args: StandaloneListArgs, mut verify_opts: VerificationAr standalone_project(&args.input, args.crate_name, &session)? }; - process_metadata(project.metadata, args.format) + let list_metadata = process_metadata(project.metadata); + + output_list_results(list_metadata, args.format, quiet) } diff --git a/kani-driver/src/list/mod.rs b/kani-driver/src/list/mod.rs index 0987a0e9c927..982c71d0120f 100644 --- a/kani-driver/src/list/mod.rs +++ b/kani-driver/src/list/mod.rs @@ -2,13 +2,21 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Implements the list subcommand logic +use kani_metadata::ContractedFunction; +use std::collections::{BTreeMap, BTreeSet}; + pub mod collect_metadata; mod output; -/// Stores the total count of standard harnesses, contract harnesses, -/// and functions under contract across all `KaniMetadata` objects. -struct Totals { - standard_harnesses: usize, - contract_harnesses: usize, - contracted_functions: usize, +struct ListMetadata { + // Files mapped to their #[kani::proof] harnesses + 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>, + // Total number of #[kani:proof_for_contract] harnesses + contract_harnesses_count: usize, + // Set of all functions under contract + contracted_functions: BTreeSet, } diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index 0f8842e10852..47b32bd6ed5e 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -3,31 +3,99 @@ //! This module handles outputting the result for the list subcommand use std::{ - collections::{BTreeMap, BTreeSet}, fmt::Display, fs::File, - io::BufWriter, + io::{BufWriter, Write}, + path::Path, }; -use crate::{args::list_args::Format, list::Totals, version::KANI_VERSION}; +use crate::{args::list_args::Format, list::ListMetadata, version::KANI_VERSION}; use anyhow::Result; -use colour::print_ln_bold; use comfy_table::Table as PrettyTable; -use kani_metadata::ContractedFunction; use serde_json::json; use to_markdown_table::MarkdownTable; // Represents the version of our JSON file format. // Increment this version (according to semantic versioning rules) whenever the JSON output format changes. const FILE_VERSION: &str = "0.1"; -const JSON_FILENAME: &str = "kani-list.json"; +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<()> { + match format { + Format::Pretty => pretty(list_metadata), + Format::Markdown => markdown(list_metadata, quiet), + Format::Json => json(list_metadata, quiet), + } +} + +/// 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) + }; + let output = format_results(table, &list_metadata); + println!("{}", 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); + + 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(); + if !quiet { + println!("Wrote list results to {}", std::fs::canonicalize(&out_path)?.display()); + } + Ok(()) +} + +/// Output results as a JSON file. +fn json(list_metadata: ListMetadata, 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 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, + "totals": { + "standard-harnesses": list_metadata.standard_harnesses_count, + "contract-harnesses": list_metadata.contract_harnesses_count, + "functions-under-contract": list_metadata.contracted_functions.len(), + } + }); + + serde_json::to_writer_pretty(writer, &json_obj)?; + + if !quiet { + println!("Wrote list results to {}", std::fs::canonicalize(out_path)?.display()); + } + + Ok(()) +} /// Construct the rows for the table of contracts information. /// Returns a tuple of the table header and the rows. -fn construct_contracts_table( - contracted_functions: BTreeSet, - totals: Totals, -) -> (Vec, Vec>) { +fn construct_contracts_table(list_metadata: &ListMetadata) -> (Vec, Vec>) { const NO_HARNESSES_MSG: &str = "NONE"; const FUNCTION_HEADER: &str = "Function"; const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])"; @@ -38,8 +106,8 @@ fn construct_contracts_table( let mut rows: Vec> = vec![]; - for cf in contracted_functions { - let mut row = vec![String::new(), cf.function]; + 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 { @@ -50,110 +118,43 @@ fn construct_contracts_table( let totals_row = vec![ TOTALS_HEADER.to_string(), - totals.contracted_functions.to_string(), - totals.contract_harnesses.to_string(), + list_metadata.contracted_functions.len().to_string(), + list_metadata.contract_harnesses_count.to_string(), ]; rows.push(totals_row); (header, rows) } -/// Print results to the terminal. -fn print_results( - table: Option, - standard_harnesses: BTreeMap>, -) { +/// 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."; - print_ln_bold!("\n{CONTRACTS_SECTION}"); + let mut output: Vec = vec![]; + output.push(format!("\n{CONTRACTS_SECTION}")); if let Some(table) = table { - println!("{table}"); + output.push(format!("{table}")); } else { - println!("{NO_CONTRACTS_MSG}"); + output.push(NO_CONTRACTS_MSG.to_string()); } - print_ln_bold!("\n{HARNESSES_SECTION}"); - if standard_harnesses.is_empty() { - println!("{NO_HARNESSES_MSG}"); + output.push(format!("\n{HARNESSES_SECTION}")); + if list_metadata.standard_harnesses.is_empty() { + output.push(NO_HARNESSES_MSG.to_string()); } let mut std_harness_index = 0; - for (_, harnesses) in standard_harnesses { + for harnesses in (&list_metadata.standard_harnesses).values() { for harness in harnesses { - println!("{}. {harness}", std_harness_index + 1); + output.push(format!("{}. {harness}", std_harness_index + 1)); std_harness_index += 1; } } - println!(); -} - -/// Output results as a JSON file. -fn json( - standard_harnesses: BTreeMap>, - contract_harnesses: BTreeMap>, - contracted_functions: BTreeSet, - totals: Totals, -) -> Result<()> { - let out_file = File::create(JSON_FILENAME).unwrap(); - let writer = BufWriter::new(out_file); - - let json_obj = json!({ - "kani-version": KANI_VERSION, - "file-version": FILE_VERSION, - "standard-harnesses": &standard_harnesses, - "contract-harnesses": &contract_harnesses, - "contracts": &contracted_functions, - "totals": { - "standard-harnesses": totals.standard_harnesses, - "contract-harnesses": totals.contract_harnesses, - "functions-under-contract": totals.contracted_functions, - } - }); - - serde_json::to_writer_pretty(writer, &json_obj)?; - - println!("Wrote list results to {}", std::fs::canonicalize(JSON_FILENAME)?.display()); - - Ok(()) -} - -/// Output the results of the list subcommand. -pub fn output_list_results( - standard_harnesses: BTreeMap>, - contract_harnesses: BTreeMap>, - contracted_functions: BTreeSet, - totals: Totals, - format: Format, -) -> Result<()> { - match format { - Format::Pretty => { - let table = if totals.contracted_functions == 0 { - None - } else { - let (header, rows) = construct_contracts_table(contracted_functions, totals); - let mut t = PrettyTable::new(); - t.set_header(header).add_rows(rows); - Some(t) - }; - print_results(table, standard_harnesses); - Ok(()) - } - Format::Markdown => { - let table = if totals.contracted_functions == 0 { - None - } else { - let (header, rows) = construct_contracts_table(contracted_functions, totals); - Some(MarkdownTable::new(Some(header), rows)?) - }; - print_results(table, standard_harnesses); - Ok(()) - } - Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals), - } + output.join("\n") }