diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index 744fd17d3b68..89970abe0b6b 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -15,7 +15,7 @@ pub struct CargoListArgs { pub common_args: CommonArgs, /// Output format - #[clap(long, default_value = "markdown")] + #[clap(long, default_value = "pretty")] pub format: Format, } @@ -33,7 +33,7 @@ pub struct StandaloneListArgs { pub common_args: CommonArgs, /// Output format - #[clap(long, default_value = "markdown")] + #[clap(long, default_value = "pretty")] pub format: Format, /// Pass this flag to run the `list` command on the standard library. @@ -46,6 +46,8 @@ pub struct StandaloneListArgs { #[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. Markdown, /// Print output in JSON format. diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 2be3ff58f2fc..66ff247ddc82 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -143,7 +143,7 @@ pub enum StandaloneSubcommand { Playback(Box), /// Verify the rust standard library. VerifyStd(Box), - /// Execute the list subcommand + /// List contracts and harnesses. List(Box), } @@ -171,7 +171,7 @@ pub enum CargoKaniSubcommand { /// Execute concrete playback testcases of a local package. Playback(Box), - /// List metadata relevant to verification, e.g., harnesses. + /// List contracts and harnesses. List(Box), } diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index e9db880a146f..50ee19f069c0 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -11,7 +11,7 @@ use crate::{ list_args::{CargoListArgs, Format, StandaloneListArgs}, }, list::Totals, - list::output::{json, markdown}, + list::output::output_list_results, project::{Project, cargo_project, standalone_project, std_project}, session::KaniSession, version::print_kani_version, @@ -72,10 +72,13 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { contracted_functions: contracted_functions.len(), }; - match format { - Format::Markdown => markdown(standard_harnesses, contracted_functions, totals), - Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals), - } + output_list_results( + standard_harnesses, + contract_harnesses, + contracted_functions, + totals, + format, + ) } pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index 47f7601292f1..0f8842e10852 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -4,43 +4,48 @@ use std::{ collections::{BTreeMap, BTreeSet}, + fmt::Display, fs::File, io::BufWriter, }; -use crate::{list::Totals, version::KANI_VERSION}; +use crate::{args::list_args::Format, list::Totals, 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, MarkdownTableError}; +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"; -/// Construct the table of contracts information. +/// 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, -) -> Result { +) -> (Vec, Vec>) { const NO_HARNESSES_MSG: &str = "NONE"; const FUNCTION_HEADER: &str = "Function"; const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])"; const TOTALS_HEADER: &str = "Total"; - let mut table_rows: Vec> = vec![]; + let header = + vec![String::new(), FUNCTION_HEADER.to_string(), CONTRACT_HARNESSES_HEADER.to_string()]; - for cf in contracted_functions { - let first_harness = cf.harnesses.first().map_or(NO_HARNESSES_MSG, |v| v).to_string(); - let first_row = vec![String::new(), cf.function.clone(), first_harness]; - table_rows.push(first_row); + let mut rows: Vec> = vec![]; - for subsequent_harness in cf.harnesses.iter().skip(1) { - let row = vec![String::new(), cf.function.clone(), subsequent_harness.to_string()]; - table_rows.push(row); + for cf in contracted_functions { + let mut row = vec![String::new(), cf.function]; + if cf.harnesses.is_empty() { + row.push(NO_HARNESSES_MSG.to_string()); + } else { + row.push(cf.harnesses.join(", ")); } + rows.push(row); } let totals_row = vec![ @@ -48,20 +53,16 @@ fn construct_contracts_table( totals.contracted_functions.to_string(), totals.contract_harnesses.to_string(), ]; - table_rows.push(totals_row); - - let table = - MarkdownTable::new(Some(vec!["", FUNCTION_HEADER, CONTRACT_HARNESSES_HEADER]), table_rows)?; + rows.push(totals_row); - Ok(table) + (header, rows) } -// /// Output results as a table printed to the terminal. -pub fn markdown( +/// Print results to the terminal. +fn print_results( + table: Option, standard_harnesses: BTreeMap>, - contracted_functions: BTreeSet, - totals: Totals, -) -> Result<()> { +) { const CONTRACTS_SECTION: &str = "Contracts:"; const HARNESSES_SECTION: &str = "Standard Harnesses (#[kani::proof]):"; const NO_CONTRACTS_MSG: &str = "No contracts or contract harnesses found."; @@ -69,12 +70,11 @@ pub fn markdown( print_ln_bold!("\n{CONTRACTS_SECTION}"); - if contracted_functions.is_empty() { - println!("{NO_CONTRACTS_MSG}"); + if let Some(table) = table { + println!("{table}"); } else { - let table = construct_contracts_table(contracted_functions, totals)?; - println!("{}", table); - }; + println!("{NO_CONTRACTS_MSG}"); + } print_ln_bold!("\n{HARNESSES_SECTION}"); if standard_harnesses.is_empty() { @@ -91,12 +91,10 @@ pub fn markdown( } println!(); - - Ok(()) } /// Output results as a JSON file. -pub fn json( +fn json( standard_harnesses: BTreeMap>, contract_harnesses: BTreeMap>, contracted_functions: BTreeSet, @@ -124,3 +122,38 @@ pub fn json( 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), + } +}