List Subcommand Improvements

Cargo.lock

@@ -826,6 +826,7 @@ dependencies = [
  "strum_macros",
  "tempfile",
  "time",
+ "to_markdown_table",
  "tokio",
  "toml",
  "tracing",
@@ -1753,6 +1754,15 @@ dependencies = [
  "time-core",
 ]
 
+[[package]]
+name = "to_markdown_table"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8450ade61b78735ed7811cc14639462723d87a6cd748a41e7bfde554ac5033dd"
+dependencies = [
+ "thiserror",
+]
+
 [[package]]
 name = "tokio"
 version = "1.41.1"

kani-driver/Cargo.toml

@@ -17,6 +17,7 @@ cargo_metadata = "0.18.0"
 anyhow = "1"
 console = "0.15.1"
 once_cell = "1.19.0"
+to_markdown_table = "0.1.0"
 serde = { version = "1", features = ["derive"] }
 serde_json = { version = "1", features = ["preserve_order"] }
 clap = { version = "4.4.11", features = ["derive"] }

kani-driver/src/args/list_args.rs

@@ -4,17 +4,15 @@
 
 use std::path::PathBuf;
 
-use crate::args::ValidateArgs;
+use crate::args::{CommonArgs, ValidateArgs};
 use clap::{Error, Parser, ValueEnum, error::ErrorKind};
 use kani_metadata::UnstableFeature;
 
-use super::VerificationArgs;
-
 /// List information relevant to verification
 #[derive(Debug, Parser)]
 pub struct CargoListArgs {
     #[command(flatten)]
-    pub verify_opts: VerificationArgs,
+    pub common_args: CommonArgs,
 
     /// Output format
     #[clap(long, default_value = "pretty")]
@@ -32,7 +30,7 @@ pub struct StandaloneListArgs {
     pub crate_name: Option<String>,
 
     #[command(flatten)]
-    pub verify_opts: VerificationArgs,
+    pub common_args: CommonArgs,
 
     /// Output format
     #[clap(long, default_value = "pretty")]
@@ -48,16 +46,18 @@ pub struct StandaloneListArgs {
 #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)]
 #[strum(serialize_all = "kebab-case")]
 pub enum Format {
-    /// Print diagnostic messages in a user friendly format.
+    /// Print output in human-readable format.
     Pretty,
-    /// Print diagnostic messages in JSON format.
+    /// Print output in Markdown format.
+    Markdown,
+    /// Print output in JSON format.
     Json,
 }
 
 impl ValidateArgs for CargoListArgs {
     fn validate(&self) -> Result<(), Error> {
-        self.verify_opts.validate()?;
-        if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) {
+        self.common_args.validate()?;
+        if !self.common_args.unstable_features.contains(UnstableFeature::List) {
             return Err(Error::raw(
                 ErrorKind::MissingRequiredArgument,
                 "The `list` subcommand is unstable and requires -Z list",
@@ -70,8 +70,8 @@ impl ValidateArgs for CargoListArgs {
 
 impl ValidateArgs for StandaloneListArgs {
     fn validate(&self) -> Result<(), Error> {
-        self.verify_opts.validate()?;
-        if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) {
+        self.common_args.validate()?;
+        if !self.common_args.unstable_features.contains(UnstableFeature::List) {
             return Err(Error::raw(
                 ErrorKind::MissingRequiredArgument,
                 "The `list` subcommand is unstable and requires -Z list",

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

@@ -6,9 +6,12 @@ use std::collections::{BTreeMap, BTreeSet};
 
 use crate::{
     InvocationType,
-    args::list_args::{CargoListArgs, Format, StandaloneListArgs},
+    args::{
+        VerificationArgs,
+        list_args::{CargoListArgs, Format, StandaloneListArgs},
+    },
     list::Totals,
-    list::output::{json, pretty},
+    list::output::output_list_results,
     project::{Project, cargo_project, standalone_project, std_project},
     session::KaniSession,
     version::print_kani_version,
@@ -69,14 +72,18 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
         contracted_functions: contracted_functions.len(),
     };
 
-    match format {
-        Format::Pretty => pretty(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) -> Result<()> {
-    let session = KaniSession::new(args.verify_opts)?;
+pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
+    verify_opts.common_args = args.common_args;
+    let session = KaniSession::new(verify_opts)?;
     if !session.args.common_args.quiet {
         print_kani_version(InvocationType::CargoKani(vec![]));
     }
@@ -85,8 +92,9 @@ pub fn list_cargo(args: CargoListArgs) -> Result<()> {
     process_metadata(project.metadata, args.format)
 }
 
-pub fn list_standalone(args: StandaloneListArgs) -> Result<()> {
-    let session = KaniSession::new(args.verify_opts)?;
+pub fn list_standalone(args: StandaloneListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
+    verify_opts.common_args = args.common_args;
+    let session = KaniSession::new(verify_opts)?;
     if !session.args.common_args.quiet {
         print_kani_version(InvocationType::Standalone);
     }

kani-driver/src/list/output.rs

@@ -3,134 +3,78 @@
 //! This module handles outputting the result for the list subcommand
 
 use std::{
-    cmp::max,
     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;
 
 // 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,
-) -> Vec<String> {
+) -> (Vec<String>, Vec<Vec<String>>) {
     const NO_HARNESSES_MSG: &str = "NONE";
-
-    // Since the harnesses will be separated by newlines, the column length is equal to the length of the longest harness
-    fn column_len(harnesses: &[String]) -> usize {
-        harnesses.iter().map(|s| s.len()).max().unwrap_or(NO_HARNESSES_MSG.len())
-    }
-
-    // Contracts table headers
     const FUNCTION_HEADER: &str = "Function";
     const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])";
-
-    // Contracts table totals row
     const TOTALS_HEADER: &str = "Total";
-    let functions_total = totals.contracted_functions.to_string();
-    let harnesses_total = totals.contract_harnesses.to_string();
 
-    let mut table_rows: Vec<String> = vec![];
-    let mut max_function_fmt_width = max(FUNCTION_HEADER.len(), functions_total.len());
-    let mut max_contract_harnesses_fmt_width =
-        max(CONTRACT_HARNESSES_HEADER.len(), harnesses_total.len());
+    let header =
+        vec![String::new(), FUNCTION_HEADER.to_string(), CONTRACT_HARNESSES_HEADER.to_string()];
 
-    let mut data_rows: Vec<(String, Vec<String>)> = vec![];
+    let mut rows: Vec<Vec<String>> = vec![];
 
     for cf in contracted_functions {
-        max_function_fmt_width = max(max_function_fmt_width, cf.function.len());
-        max_contract_harnesses_fmt_width =
-            max(max_contract_harnesses_fmt_width, column_len(&cf.harnesses));
-
-        data_rows.push((cf.function, cf.harnesses));
-    }
-
-    let function_sep = "-".repeat(max_function_fmt_width);
-    let contract_harnesses_sep = "-".repeat(max_contract_harnesses_fmt_width);
-    let totals_sep = "-".repeat(TOTALS_HEADER.len());
-
-    let sep_row = format!("| {totals_sep} | {function_sep} | {contract_harnesses_sep} |");
-    table_rows.push(sep_row.clone());
-
-    let function_space = " ".repeat(max_function_fmt_width - FUNCTION_HEADER.len());
-    let contract_harnesses_space =
-        " ".repeat(max_contract_harnesses_fmt_width - CONTRACT_HARNESSES_HEADER.len());
-    let totals_space = " ".repeat(TOTALS_HEADER.len());
-
-    let header_row = format!(
-        "| {totals_space} | {FUNCTION_HEADER}{function_space} | {CONTRACT_HARNESSES_HEADER}{contract_harnesses_space} |"
-    );
-    table_rows.push(header_row);
-    table_rows.push(sep_row.clone());
-
-    for (function, harnesses) in data_rows {
-        let function_space = " ".repeat(max_function_fmt_width - function.len());
-        let first_harness = harnesses.first().map_or(NO_HARNESSES_MSG, |v| v);
-        let contract_harnesses_space =
-            " ".repeat(max_contract_harnesses_fmt_width - first_harness.len());
-
-        let first_row = format!(
-            "| {totals_space} | {function}{function_space} | {first_harness}{contract_harnesses_space} |"
-        );
-        table_rows.push(first_row);
-
-        for subsequent_harness in harnesses.iter().skip(1) {
-            let function_space = " ".repeat(max_function_fmt_width);
-            let contract_harnesses_space =
-                " ".repeat(max_contract_harnesses_fmt_width - subsequent_harness.len());
-            let row = format!(
-                "| {totals_space} | {function_space} | {subsequent_harness}{contract_harnesses_space} |"
-            );
-            table_rows.push(row);
+        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(", "));
         }
-
-        table_rows.push(sep_row.clone())
+        rows.push(row);
     }
 
-    let total_function_space = " ".repeat(max_function_fmt_width - functions_total.len());
-    let total_harnesses_space =
-        " ".repeat(max_contract_harnesses_fmt_width - harnesses_total.len());
+    let totals_row = vec![
+        TOTALS_HEADER.to_string(),
+        totals.contracted_functions.to_string(),
+        totals.contract_harnesses.to_string(),
+    ];
+    rows.push(totals_row);
 
-    let totals_row = format!(
-        "| {TOTALS_HEADER} | {functions_total}{total_function_space} | {harnesses_total}{total_harnesses_space} |"
-    );
-
-    table_rows.push(totals_row);
-    table_rows.push(sep_row.clone());
-
-    table_rows
+    (header, rows)
 }
 
-/// Output results as a table printed to the terminal.
-pub fn pretty(
+/// 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_rows = construct_contracts_table(contracted_functions, totals);
-        println!("{}", table_rows.join("\n"));
-    };
+        println!("{NO_CONTRACTS_MSG}");
+    }
 
     print_ln_bold!("\n{HARNESSES_SECTION}");
     if standard_harnesses.is_empty() {
@@ -147,12 +91,10 @@ pub fn pretty(
     }
 
     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>,
@@ -176,5 +118,42 @@ pub fn json(
 
     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<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),
+    }
+}