List Subcommand Improvements (#3729)

Improvements to the list subcommand.

- Print the location of the JSON file for `--format=json` (#3633)
- Use `CommonArgs` instead of `VerificationArgs` (#3632)
- Add a Markdown option. The pretty table is nice for smaller packages,
but as we progress with the standard library verification effort, it's
too massive to be easily readable. In this case, it's better to print a
markdown table and then just read it in a markdown editor. (Once this PR
is merged, the [kani list workflow
step](model-checking/verify-rust-std#146) will
use the markdown option).

Resolves #3632, #3633

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: carolynzech

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>,
 }