Merge branch 'main' into thanh-llbc

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")]
@@ -44,20 +42,22 @@ 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 diagnostic messages in a user friendly format.
+    /// Print output in human-readable format.
     Pretty,
-    /// Print diagnostic messages in JSON format.
+    /// Write output to a Markdown file.
+    Markdown,
+    /// Write output to a JSON file.
     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},
-    list::Totals,
-    list::output::{json, pretty},
+    args::{
+        VerificationArgs,
+        list_args::{CargoListArgs, StandaloneListArgs},
+    },
+    list::ListMetadata,
+    list::output::output_list_results,
     project::{Project, cargo_project, standalone_project, std_project},
     session::KaniSession,
     version::print_kani_version,
@@ -17,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<KaniMetadata>, format: Format) -> Result<()> {
+fn process_metadata(metadata: Vec<KaniMetadata>) -> 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.
@@ -26,14 +29,14 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
 
     let mut contracted_functions: BTreeSet<ContractedFunction> = 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);
@@ -45,7 +48,7 @@ fn process_metadata(metadata: Vec<KaniMetadata>, 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);
@@ -63,31 +66,34 @@ fn process_metadata(metadata: Vec<KaniMetadata>, 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(),
-    };
-
-    match format {
-        Format::Pretty => pretty(standard_harnesses, contracted_functions, totals),
-        Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals),
+    ListMetadata {
+        standard_harnesses,
+        standard_harnesses_count,
+        contract_harnesses,
+        contract_harnesses_count,
+        contracted_functions,
     }
 }
 
-pub fn list_cargo(args: CargoListArgs) -> Result<()> {
-    let session = KaniSession::new(args.verify_opts)?;
-    if !session.args.common_args.quiet {
+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 !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) -> Result<()> {
-    let session = KaniSession::new(args.verify_opts)?;
-    if !session.args.common_args.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 !quiet {
         print_kani_version(InvocationType::Standalone);
     }
 
@@ -97,5 +103,7 @@ pub fn list_standalone(args: StandaloneListArgs) -> Result<()> {
         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)
 }

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<String, BTreeSet<String>>,
+    // Total number of #[kani::proof] harnesses
+    standard_harnesses_count: usize,
+    // Files mapped to their #[kani::proof_for_contract] harnesses
+    contract_harnesses: BTreeMap<String, BTreeSet<String>>,
+    // Total number of #[kani:proof_for_contract] harnesses
+    contract_harnesses_count: usize,
+    // Set of all functions under contract
+    contracted_functions: BTreeSet<ContractedFunction>,
 }