List Subcommand (Implementation)

Cargo.lock

@@ -191,6 +191,15 @@ version = "1.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0"
 
+[[package]]
+name = "colour"
+version = "2.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b536eebcabe54980476d120a182f7da2268fe02d22575cca99cee5fdda178280"
+dependencies = [
+ "winapi",
+]
+
 [[package]]
 name = "comfy-table"
 version = "7.1.1"
@@ -496,6 +505,7 @@ dependencies = [
  "anyhow",
  "cargo_metadata",
  "clap",
+ "colour",
  "comfy-table",
  "console",
  "glob",
@@ -1045,6 +1055,7 @@ version = "1.0.128"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8"
 dependencies = [
+ "indexmap",
  "itoa",
  "memchr",
  "ryu",

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

@@ -2,15 +2,16 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use crate::codegen_cprover_gotoc::{GotocCtx, codegen::ty_stable::pointee_type_stable};
 use crate::kani_middle::attributes::KaniAttributes;
+use crate::kani_middle::find_closure_in_body;
 use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
+use stable_mir::mir::Local;
 use stable_mir::mir::mono::{Instance, MonoItem};
-use stable_mir::mir::{Local, VarDebugInfoContents};
-use stable_mir::ty::{FnDef, RigidTy, TyKind};
+use stable_mir::ty::{RigidTy, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {
     /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
@@ -87,33 +88,24 @@ impl<'tcx> GotocCtx<'tcx> {
         recursion_tracker
     }
 
+    fn find_closure(&mut self, inside: Instance, name: &str) -> Option<Instance> {
+        let body = self.transformer.body(self.tcx, inside);
+        find_closure_in_body(&body, name)
+    }
+
     /// Find the modifies recursively since we may have a recursion wrapper.
     /// I.e.: [recursion_wrapper ->]? check -> modifies.
     fn find_modifies(&mut self, instance: Instance) -> Option<Instance> {
         let contract_attrs =
             KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?;
-        let mut find_closure = |inside: Instance, name: &str| {
-            let body = self.transformer.body(self.tcx, inside);
-            body.var_debug_info.iter().find_map(|var_info| {
-                if var_info.name.as_str() == name {
-                    let ty = match &var_info.value {
-                        VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(),
-                        VarDebugInfoContents::Const(const_op) => const_op.ty(),
-                    };
-                    if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() {
-                        return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap());
-                    }
-                }
-                None
-            })
-        };
         let check_instance = if contract_attrs.has_recursion {
-            let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?;
-            find_closure(recursion_check, contract_attrs.checked_with.as_str())?
+            let recursion_check =
+                self.find_closure(instance, contract_attrs.recursion_check.as_str())?;
+            self.find_closure(recursion_check, contract_attrs.checked_with.as_str())?
         } else {
-            find_closure(instance, contract_attrs.checked_with.as_str())?
+            self.find_closure(instance, contract_attrs.checked_with.as_str())?
         };
-        find_closure(check_instance, contract_attrs.modifies_wrapper.as_str())
+        self.find_closure(check_instance, contract_attrs.modifies_wrapper.as_str())
     }
 
     /// Convert the Kani level contract into a CBMC level contract by creating a

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -20,9 +20,8 @@ use cbmc::RoundingMode;
 use cbmc::goto_program::Location;
 use cbmc::irep::goto_binary_serde::write_goto_binary_file;
 use cbmc::{InternedString, MachineModel};
-use kani_metadata::UnsupportedFeature;
 use kani_metadata::artifact::convert_type;
-use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
+use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature};
 use kani_metadata::{AssignsContract, CompilerArtifactStub};
 use rustc_codegen_ssa::back::archive::{
     ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER,
@@ -644,6 +643,10 @@ impl GotoCodegenResults {
             proof_harnesses: proofs,
             unsupported_features,
             test_harnesses: tests,
+            // We don't collect the contracts metadata because the FunctionWithContractPass
+            // removes any contracts logic for ReachabilityType::Test or ReachabilityType::PubFns,
+            // which are the two ReachabilityTypes under which the compiler calls this function.
+            contracted_functions: vec![],
         }
     }
 

kani-compiler/src/kani_middle/codegen_units.rs

@@ -9,7 +9,7 @@
 
 use crate::args::ReachabilityType;
 use crate::kani_middle::attributes::is_proof_harness;
-use crate::kani_middle::metadata::gen_proof_metadata;
+use crate::kani_middle::metadata::{gen_contracts_metadata, gen_proof_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};
@@ -93,7 +93,7 @@ impl CodegenUnits {
 
     /// Write compilation metadata into a file.
     pub fn write_metadata(&self, queries: &QueryDb, tcx: TyCtxt) {
-        let metadata = self.generate_metadata();
+        let metadata = self.generate_metadata(tcx);
         let outpath = metadata_output_path(tcx);
         store_metadata(queries, &metadata, &outpath);
     }
@@ -103,14 +103,15 @@ impl CodegenUnits {
     }
 
     /// Generate [KaniMetadata] for the target crate.
-    fn generate_metadata(&self) -> KaniMetadata {
+    fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata {
         let (proof_harnesses, test_harnesses) =
             self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness());
         KaniMetadata {
             crate_name: self.crate_info.name.clone(),
             proof_harnesses,
             unsupported_features: vec![],
             test_harnesses,
+            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::{
+    ContractAttributes, KaniAttributes, matches_diagnostic as matches_function,
+};
+use crate::kani_middle::{InternalDefId, SourceLocation, find_closure_in_body};
+use kani_metadata::ContractedFunction;
 use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
 use rustc_middle::ty::TyCtxt;
-use stable_mir::CrateDef;
+use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-
-use super::{SourceLocation, attributes::KaniAttributes};
+use stable_mir::mir::{Body, TerminatorKind};
+use stable_mir::ty::{RigidTy, TyKind};
+use stable_mir::{CrateDef, CrateItems};
 
 /// Create the harness metadata for a proof harness for a given function.
 pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
@@ -40,6 +47,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

@@ -19,7 +19,8 @@ use rustc_span::source_map::respan;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use stable_mir::CrateDef;
-use stable_mir::mir::mono::MonoItem;
+use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::mir::{Body, VarDebugInfoContents};
 use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
 use stable_mir::visitor::{Visitable, Visitor as TyVisitor};
 use std::ops::ControlFlow;
@@ -238,3 +239,19 @@ pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option<FnDef> {
         None
     }
 }
+
+/// Find the user-declared closure by the name `name` in `body`.
+pub fn find_closure_in_body(body: &Body, name: &str) -> Option<Instance> {
+    body.var_debug_info.iter().find_map(|var_info| {
+        if var_info.name.as_str() == name {
+            let ty = match &var_info.value {
+                VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(),
+                VarDebugInfoContents::Const(const_op) => const_op.ty(),
+            };
+            if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() {
+                return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap());
+            }
+        }
+        None
+    })
+}

kani-driver/Cargo.toml

@@ -18,8 +18,9 @@ anyhow = "1"
 console = "0.15.1"
 once_cell = "1.19.0"
 serde = { version = "1", features = ["derive"] }
-serde_json = "1"
+serde_json = { version = "1", features = ["preserve_order"] }
 clap = { version = "4.4.11", features = ["derive"] }
+colour = "2.1.0"
 glob = "0.3"
 toml = "0.8"
 regex = "1.6"