List Subcommand: include crate name

kani-driver/src/list/collect_metadata.rs

@@ -10,69 +10,64 @@ use crate::{
         VerificationArgs,
         list_args::{CargoListArgs, StandaloneListArgs},
     },
-    list::ListMetadata,
     list::output::output_list_results,
+    list::{FileName, HarnessName, ListMetadata},
     project::{Project, cargo_project, standalone_project, std_project},
     session::KaniSession,
     version::print_kani_version,
 };
 use anyhow::Result;
-use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata};
+use kani_metadata::{ContractedFunction, HarnessKind, HarnessMetadata, KaniMetadata};
 
 /// Process the KaniMetadata output from kani-compiler and output the list subcommand results
-pub 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.
-    let mut standard_harnesses: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
-    let mut contract_harnesses: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
+pub fn process_metadata(metadata: Vec<KaniMetadata>) -> BTreeSet<ListMetadata> {
+    let mut list_metadata: BTreeSet<ListMetadata> = BTreeSet::new();
+
+    let insert = |harness_meta: HarnessMetadata,
+                  map: &mut BTreeMap<FileName, BTreeSet<HarnessName>>,
+                  count: &mut usize| {
+        *count += 1;
+        if let Some(harnesses) = map.get_mut(&harness_meta.original_file) {
+            harnesses.insert(harness_meta.pretty_name);
+        } else {
+            map.insert(harness_meta.original_file, BTreeSet::from([harness_meta.pretty_name]));
+        };
+    };
 
-    let mut contracted_functions: BTreeSet<ContractedFunction> = BTreeSet::new();
+    for kani_meta in metadata {
+        // We use ordered maps and sets so that the output is in lexicographic order (and consistent across invocations).
+        let mut standard_harnesses: BTreeMap<FileName, BTreeSet<HarnessName>> = BTreeMap::new();
+        let mut contract_harnesses: BTreeMap<FileName, BTreeSet<HarnessName>> = BTreeMap::new();
+        let mut contracted_functions: BTreeSet<ContractedFunction> = BTreeSet::new();
 
-    let mut standard_harnesses_count = 0;
-    let mut contract_harnesses_count = 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 => {
-                    standard_harnesses_count += 1;
-                    if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file)
-                    {
-                        harnesses.insert(harness_meta.pretty_name);
-                    } else {
-                        standard_harnesses.insert(
-                            harness_meta.original_file,
-                            BTreeSet::from([harness_meta.pretty_name]),
-                        );
-                    }
+                    insert(harness_meta, &mut standard_harnesses, &mut standard_harnesses_count);
                 }
                 HarnessKind::ProofForContract { .. } => {
-                    contract_harnesses_count += 1;
-                    if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file)
-                    {
-                        harnesses.insert(harness_meta.pretty_name);
-                    } else {
-                        contract_harnesses.insert(
-                            harness_meta.original_file,
-                            BTreeSet::from([harness_meta.pretty_name]),
-                        );
-                    }
+                    insert(harness_meta, &mut contract_harnesses, &mut contract_harnesses_count);
                 }
                 HarnessKind::Test => {}
             }
         }
 
         contracted_functions.extend(kani_meta.contracted_functions.into_iter());
-    }
 
-    ListMetadata {
-        standard_harnesses,
-        standard_harnesses_count,
-        contract_harnesses,
-        contract_harnesses_count,
-        contracted_functions,
+        list_metadata.insert(ListMetadata {
+            crate_name: kani_meta.crate_name,
+            standard_harnesses,
+            standard_harnesses_count,
+            contract_harnesses,
+            contract_harnesses_count,
+            contracted_functions,
+        });
     }
+
+    list_metadata
 }
 
 pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> {

kani-driver/src/list/mod.rs

@@ -8,15 +8,41 @@ use std::collections::{BTreeMap, BTreeSet};
 pub mod collect_metadata;
 pub mod output;
 
+type FileName = String;
+type HarnessName = String;
+
+/// Metadata for the list subcommand for a given crate.
+/// It is important that crate_name is the first field so that `Ord` orders two ListMetadata objects by crate name.
+#[derive(PartialEq, Eq, PartialOrd, Ord)]
 pub struct ListMetadata {
+    crate_name: String,
     // Files mapped to their #[kani::proof] harnesses
-    standard_harnesses: BTreeMap<String, BTreeSet<String>>,
+    standard_harnesses: BTreeMap<FileName, BTreeSet<HarnessName>>,
     // 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>>,
+    contract_harnesses: BTreeMap<FileName, BTreeSet<HarnessName>>,
     // Total number of #[kani:proof_for_contract] harnesses
     contract_harnesses_count: usize,
     // Set of all functions under contract
     contracted_functions: BTreeSet<ContractedFunction>,
 }
+
+/// Given a collection of ListMetadata objects, merge them into a single ListMetadata object.
+pub fn merge_list_metadata<T>(collection: T) -> ListMetadata
+where
+    T: Extend<ListMetadata>,
+    T: IntoIterator<Item = ListMetadata>,
+{
+    collection
+        .into_iter()
+        .reduce(|mut acc, item| {
+            acc.standard_harnesses.extend(item.standard_harnesses);
+            acc.standard_harnesses_count += item.standard_harnesses_count;
+            acc.contract_harnesses.extend(item.contract_harnesses);
+            acc.contract_harnesses_count += item.contract_harnesses_count;
+            acc.contracted_functions.extend(item.contracted_functions);
+            acc
+        })
+        .expect("Cannot merge empty collection of ListMetadata objects")
+}