change tests to json; sort output

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -9,7 +9,6 @@ use crate::kani_middle::analysis;
 use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
 use crate::kani_middle::check_reachable_items;
 use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits};
-use crate::kani_middle::list::collect_contracted_fns;
 use crate::kani_middle::metadata::gen_test_metadata;
 use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
@@ -342,10 +341,7 @@ impl CodegenBackend for GotocCodegenBackend {
                         results.harnesses.push(metadata);
                     }
                 }
-                ReachabilityType::None => {
-                    let units = CodegenUnits::new(&queries, tcx);
-                    units.write_metadata(&queries, tcx);
-                }
+                ReachabilityType::None => {}
                 ReachabilityType::PubFns => {
                     let unit = CodegenUnit::default();
                     let transformer = BodyTransformation::new(&queries, tcx, &unit);
@@ -384,7 +380,7 @@ impl CodegenBackend for GotocCodegenBackend {
                     write_file(
                         &base_filename,
                         ArtifactType::Metadata,
-                        &results.generate_metadata(tcx),
+                        &results.generate_metadata(),
                         queries.args().output_pretty_json,
                     );
                 }
@@ -623,7 +619,7 @@ impl GotoCodegenResults {
         }
     }
     /// Method that generates `KaniMetadata` from the given compilation results.
-    pub fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata {
+    pub fn generate_metadata(&self) -> KaniMetadata {
         // Maps the goto-context "unsupported features" data into the KaniMetadata "unsupported features" format.
         // TODO: Do we really need different formats??
         let unsupported_features = self
@@ -655,7 +651,10 @@ impl GotoCodegenResults {
             proof_harnesses: proofs,
             unsupported_features,
             test_harnesses: tests,
-            contracted_functions: collect_contracted_fns(tcx),
+            // We don't collect the functions under contract because the logic assumes that, if contract attributes are present,
+            // they are well-formed, which Kani only checks if we run verification or the list subcommand (i.e., for ReachabilityType::Harnesses).
+            // In those cases, we use the CodegenUnits object to generate the metadata instead of this function.
+            contracted_functions: vec![],
         }
     }
 

kani-compiler/src/kani_middle/codegen_units.rs

@@ -9,8 +9,7 @@
 
 use crate::args::ReachabilityType;
 use crate::kani_middle::attributes::is_proof_harness;
-use crate::kani_middle::list::collect_contracted_fns;
-use crate::kani_middle::metadata::gen_proof_metadata;
+use crate::kani_middle::metadata::{gen_proof_metadata, gen_contracts_metadata};
 use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::resolve::expect_resolve_fn;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
@@ -115,7 +114,7 @@ impl CodegenUnits {
             proof_harnesses,
             unsupported_features: vec![],
             test_harnesses,
-            contracted_functions: collect_contracted_fns(tcx),
+            contracted_functions: gen_contracts_metadata(tcx),
         }
     }
 }

kani-compiler/src/kani_middle/metadata.rs

@@ -3,15 +3,22 @@
 //! This module handles Kani metadata generation. For example, generating HarnessMetadata for a
 //! given function.
 
+use std::collections::HashMap;
 use std::path::Path;
 
 use crate::kani_middle::attributes::test_harness_name;
+use crate::kani_middle::attributes::{
+    matches_diagnostic as matches_function, ContractAttributes, KaniAttributes,
+};
+use crate::kani_middle::{find_closure_in_body, InternalDefId, SourceLocation};
+use kani_metadata::ContractedFunction;
 use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
 use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::CrateDef;
-
-use super::{attributes::KaniAttributes, SourceLocation};
+use stable_mir::mir::{Body, TerminatorKind};
+use stable_mir::ty::{RigidTy, TyKind};
+use stable_mir::{CrateDef, CrateItems};
 
 pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
     let def = instance.def;
@@ -39,6 +46,83 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
     }
 }
 
+/// Map each function under contract to its contract harnesses
+fn fns_to_contract_harnesses(tcx: TyCtxt) -> HashMap<InternalDefId, Vec<String>> {
+    // We work with stable_mir::CrateItem instead of stable_mir::Instance to include generic items
+    let crate_items: CrateItems = stable_mir::all_local_items();
+
+    let mut fns_to_harnesses: HashMap<InternalDefId, Vec<String>> = HashMap::new();
+
+    for item in crate_items {
+        let def_id = rustc_internal::internal(tcx, item.def_id());
+        let fn_name = tcx.def_path_str(def_id);
+        let attributes = KaniAttributes::for_item(tcx, def_id);
+
+        if attributes.has_contract() {
+            fns_to_harnesses.insert(def_id, vec![]);
+        } else if let Some((_, target_def_id, _)) = attributes.interpret_for_contract_attribute() {
+            if let Some(harnesses) = fns_to_harnesses.get_mut(&target_def_id) {
+                harnesses.push(fn_name);
+            } else {
+                fns_to_harnesses.insert(target_def_id, vec![fn_name]);
+            }
+        }
+    }
+
+    fns_to_harnesses
+}
+
+/// Count the number of contracts in `check_body`, where `check_body` is the body of the
+/// kanitool::checked_with closure (c.f. kani_macros::sysroot::contracts).
+/// In this closure, preconditions are denoted by kani::assume() calls and postconditions by kani::assert() calls.
+/// The number of contracts is the number of times these functions are called inside the closure
+fn count_contracts(tcx: TyCtxt, check_body: &Body) -> usize {
+    let mut count = 0;
+
+    for bb in &check_body.blocks {
+        if let TerminatorKind::Call { ref func, .. } = bb.terminator.kind {
+            let fn_ty = func.ty(check_body.locals()).unwrap();
+            if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() {
+                if let Ok(instance) = Instance::resolve(fn_def, &args) {
+                    // For each precondition or postcondition, increment the count
+                    if matches_function(tcx, instance.def, "KaniAssume")
+                        || matches_function(tcx, instance.def, "KaniAssert")
+                    {
+                        count += 1;
+                    }
+                }
+            }
+        }
+    }
+    count
+}
+
+/// Collects contract and contract harness metadata.
+///
+/// For each function with contracts (or that is a target of a contract harness),
+/// construct a ContractedFunction object for it.
+pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
+    let mut contracted_fns = vec![];
+    for (fn_def_id, harnesses) in fns_to_contract_harnesses(tcx) {
+        let attrs: ContractAttributes =
+            KaniAttributes::for_item(tcx, fn_def_id).contract_attributes().unwrap();
+        let body: Body = rustc_internal::stable(tcx.optimized_mir(fn_def_id));
+        let check_body: Body =
+            find_closure_in_body(&body, attrs.checked_with.as_str()).unwrap().body().unwrap();
+
+        let total_contracts = count_contracts(tcx, &check_body);
+
+        contracted_fns.push(ContractedFunction {
+            function: tcx.def_path_str(fn_def_id),
+            file: SourceLocation::new(rustc_internal::stable(tcx.def_span(fn_def_id))).filename,
+            harnesses,
+            total_contracts,
+        });
+    }
+
+    contracted_fns
+}
+
 /// Create the harness metadata for a test description.
 #[allow(dead_code)]
 pub fn gen_test_metadata(

kani-compiler/src/kani_middle/mod.rs

@@ -32,7 +32,6 @@ pub mod attributes;
 pub mod codegen_units;
 pub mod coercion;
 mod intrinsics;
-pub mod list;
 pub mod metadata;
 pub mod points_to;
 pub mod provide;

kani-driver/src/list/collect_metadata.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // This module invokes the compiler to gather the metadata for the list subcommand, then post-processes the output.
 
-use std::collections::BTreeMap;
+use std::collections::{BTreeMap, BTreeSet};
 
 use crate::{
     args::list_args::{CargoListArgs, Format, StandaloneListArgs},
@@ -18,9 +18,9 @@ use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata};
 
 fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
     // Map each file to a vector of its harnesses
-    let mut standard_harnesses: BTreeMap<String, Vec<String>> = BTreeMap::new();
-    let mut contract_harnesses: BTreeMap<String, Vec<String>> = BTreeMap::new();
-    let mut contracted_functions: Vec<ContractedFunction> = vec![];
+    let mut standard_harnesses: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
+    let mut contract_harnesses: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
+    let mut contracted_functions: BTreeSet<ContractedFunction> = BTreeSet::new();
 
     let mut total_standard_harnesses = 0;
     let mut total_contract_harnesses = 0;
@@ -33,20 +33,20 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
                     total_standard_harnesses += 1;
                     if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file)
                     {
-                        harnesses.push(harness_meta.pretty_name);
+                        harnesses.insert(harness_meta.pretty_name);
                     } else {
                         standard_harnesses
-                            .insert(harness_meta.original_file, vec![harness_meta.pretty_name]);
+                            .insert(harness_meta.original_file, BTreeSet::from([harness_meta.pretty_name]));
                     }
                 }
                 HarnessKind::ProofForContract { .. } => {
                     total_contract_harnesses += 1;
                     if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file)
                     {
-                        harnesses.push(harness_meta.pretty_name);
+                        harnesses.insert(harness_meta.pretty_name);
                     } else {
                         contract_harnesses
-                            .insert(harness_meta.original_file, vec![harness_meta.pretty_name]);
+                            .insert(harness_meta.original_file, BTreeSet::from([harness_meta.pretty_name]));
                     }
                 }
                 HarnessKind::Test => {}
@@ -60,9 +60,6 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
         contracted_functions.extend(kani_meta.contracted_functions.into_iter());
     }
 
-    // Print in alphabetical order
-    contracted_functions.sort_by_key(|cf| cf.function.clone());
-
     let totals = Totals {
         standard_harnesses: total_standard_harnesses,
         contract_harnesses: total_contract_harnesses,

kani-driver/src/list/output.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // This module handles outputting the result for the list subcommand
 
-use std::{collections::BTreeMap, fs::File, io::BufWriter};
+use std::{collections::{BTreeMap, BTreeSet}, fs::File, io::BufWriter};
 
 use crate::{list::Totals, version::KANI_VERSION};
 use anyhow::Result;
@@ -14,10 +14,11 @@ use serde_json::json;
 // 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";
 
 pub fn pretty(
-    standard_harnesses: BTreeMap<String, Vec<String>>,
-    contracted_functions: Vec<ContractedFunction>,
+    standard_harnesses: BTreeMap<String, BTreeSet<String>>,
+    contracted_functions: BTreeSet<ContractedFunction>,
     totals: Totals,
 ) -> Result<()> {
     fn format_contract_harnesses(harnesses: &mut [String]) -> String {
@@ -80,14 +81,12 @@ pub fn pretty(
 }
 
 pub fn json(
-    standard_harnesses: BTreeMap<String, Vec<String>>,
-    contract_harnesses: BTreeMap<String, Vec<String>>,
-    contracted_functions: Vec<ContractedFunction>,
+    standard_harnesses: BTreeMap<String, BTreeSet<String>>,
+    contract_harnesses: BTreeMap<String, BTreeSet<String>>,
+    contracted_functions: BTreeSet<ContractedFunction>,
     totals: Totals,
 ) -> Result<()> {
-    let filename = "kani-list.json";
-
-    let out_file = File::create(filename).unwrap();
+    let out_file = File::create(JSON_FILENAME).unwrap();
     let writer = BufWriter::new(out_file);
 
     let json_obj = json!({

kani_metadata/src/lib.rs

@@ -35,7 +35,7 @@ pub struct KaniMetadata {
     pub contracted_functions: Vec<ContractedFunction>,
 }
 
-#[derive(Debug, Clone, Serialize, Deserialize)]
+#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord)]
 pub struct ContractedFunction {
     /// The fully qualified name the user gave to the function (i.e. includes the module path).
     pub function: String,