pretty table and markdown table

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.

kani-driver/src/args/mod.rs

@@ -143,7 +143,7 @@ pub enum StandaloneSubcommand {
     Playback(Box<playback_args::KaniPlaybackArgs>),
     /// Verify the rust standard library.
     VerifyStd(Box<std_args::VerifyStdArgs>),
-    /// Execute the list subcommand
+    /// List contracts and harnesses.
     List(Box<list_args::StandaloneListArgs>),
 }
 
@@ -171,7 +171,7 @@ pub enum CargoKaniSubcommand {
     /// Execute concrete playback testcases of a local package.
     Playback(Box<playback_args::CargoPlaybackArgs>),
 
-    /// List metadata relevant to verification, e.g., harnesses.
+    /// List contracts and harnesses.
     List(Box<list_args::CargoListArgs>),
 }
 

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<KaniMetadata>, 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<()> {

kani-driver/src/list/output.rs

@@ -4,77 +4,77 @@
 
 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<ContractedFunction>,
     totals: Totals,
-) -> Result<MarkdownTable, MarkdownTableError> {
+) -> (Vec<String>, Vec<Vec<String>>) {
     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<String>> = 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<String>> = 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![
         TOTALS_HEADER.to_string(),
         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<T: Display>(
+    table: Option<T>,
     standard_harnesses: BTreeMap<String, BTreeSet<String>>,
-    contracted_functions: BTreeSet<ContractedFunction>,
-    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.";
     const NO_HARNESSES_MSG: &str = "No standard harnesses found.";
 
     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<String, BTreeSet<String>>,
     contract_harnesses: BTreeMap<String, BTreeSet<String>>,
     contracted_functions: BTreeSet<ContractedFunction>,
@@ -124,3 +122,38 @@ pub fn json(
 
     Ok(())
 }
+
+/// Output the results of the list subcommand.
+pub fn output_list_results(
+    standard_harnesses: BTreeMap<String, BTreeSet<String>>,
+    contract_harnesses: BTreeMap<String, BTreeSet<String>>,
+    contracted_functions: BTreeSet<ContractedFunction>,
+    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),
+    }
+}