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/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,16 @@
 //! 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::{KaniAttributes, test_harness_name};
+use crate::kani_middle::{SourceLocation, stable_fn_def};
+use kani_metadata::ContractedFunction;
 use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
 use rustc_middle::ty::TyCtxt;
-use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
-
-use super::{SourceLocation, attributes::KaniAttributes};
+use stable_mir::{CrateDef, CrateItems, DefId};
 
 /// 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 +41,48 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
     }
 }
 
+/// 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> {
+    // 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 fn_to_data: HashMap<DefId, ContractedFunction> = HashMap::new();
+
+    for item in crate_items {
+        let function = item.name();
+        let file = SourceLocation::new(item.span()).filename;
+        let attributes = KaniAttributes::for_def_id(tcx, item.def_id());
+
+        if attributes.has_contract() {
+            fn_to_data.insert(item.def_id(), ContractedFunction {
+                function,
+                file,
+                harnesses: vec![],
+            });
+        } else if let Some((target_name, internal_def_id, _)) =
+            attributes.interpret_for_contract_attribute()
+        {
+            let target_def_id = stable_fn_def(tcx, internal_def_id)
+                .expect("The target of a proof for contract should be a function definition")
+                .def_id();
+            if let Some(cf) = fn_to_data.get_mut(&target_def_id) {
+                cf.harnesses.push(function);
+            } else {
+                fn_to_data.insert(target_def_id, ContractedFunction {
+                    function: target_name.to_string(),
+                    file,
+                    harnesses: vec![function],
+                });
+            }
+        }
+    }
+
+    fn_to_data.into_values().collect()
+}
+
 /// Create the harness metadata for a test description.
 #[allow(dead_code)]
 pub fn gen_test_metadata(

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"

kani-driver/src/args/list_args.rs

@@ -0,0 +1,127 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Implements the subcommand handling of the list subcommand
+
+use std::path::PathBuf;
+
+use crate::args::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,
+
+    /// Output format
+    #[clap(long, default_value = "pretty")]
+    pub format: Format,
+}
+
+/// List information relevant to verification
+#[derive(Debug, Parser)]
+pub struct StandaloneListArgs {
+    /// Rust file to verify
+    #[arg(required = true)]
+    pub input: PathBuf,
+
+    #[arg(long, hide = true)]
+    pub crate_name: Option<String>,
+
+    #[command(flatten)]
+    pub verify_opts: VerificationArgs,
+
+    /// Output format
+    #[clap(long, default_value = "pretty")]
+    pub format: Format,
+
+    /// Pass this flag to run the `list` command on the standard library.
+    /// Ensure that the provided `path` is the `library` folder.
+    #[arg(long)]
+    pub std: bool,
+}
+
+/// Message 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.
+    Pretty,
+    /// Print diagnostic messages in JSON format.
+    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) {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `list` subcommand is unstable and requires -Z list",
+            ));
+        }
+
+        Ok(())
+    }
+}
+
+impl ValidateArgs for StandaloneListArgs {
+    fn validate(&self) -> Result<(), Error> {
+        self.verify_opts.validate()?;
+        if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `list` subcommand is unstable and requires -Z list",
+            ));
+        }
+
+        if self.std {
+            if !self.input.exists() {
+                Err(Error::raw(
+                    ErrorKind::InvalidValue,
+                    format!(
+                        "Invalid argument: `<input>` argument `{}` does not exist",
+                        self.input.display()
+                    ),
+                ))
+            } else if !self.input.is_dir() {
+                Err(Error::raw(
+                    ErrorKind::InvalidValue,
+                    format!(
+                        "Invalid argument: `<input>` argument `{}` is not a directory",
+                        self.input.display()
+                    ),
+                ))
+            } else {
+                let full_path = self.input.canonicalize()?;
+                let dir = full_path.file_stem().unwrap();
+                if dir != "library" {
+                    Err(Error::raw(
+                        ErrorKind::InvalidValue,
+                        format!(
+                            "Invalid argument: Expected `<input>` to point to the `library` folder \
+                        containing the standard library crates.\n\
+                        Found `{}` folder instead",
+                            dir.to_string_lossy()
+                        ),
+                    ))
+                } else {
+                    Ok(())
+                }
+            }
+        } else if self.input.is_file() {
+            Ok(())
+        } else {
+            Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: Input invalid. `{}` is not a regular file.",
+                    self.input.display()
+                ),
+            ))
+        }
+    }
+}

kani-driver/src/args/mod.rs

@@ -5,6 +5,7 @@
 pub mod assess_args;
 pub mod cargo;
 pub mod common;
+pub mod list_args;
 pub mod playback_args;
 pub mod std_args;
 
@@ -93,6 +94,8 @@ pub enum StandaloneSubcommand {
     Playback(Box<playback_args::KaniPlaybackArgs>),
     /// Verify the rust standard library.
     VerifyStd(Box<std_args::VerifyStdArgs>),
+    /// Execute the list subcommand
+    List(Box<list_args::StandaloneListArgs>),
 }
 
 #[derive(Debug, clap::Parser)]
@@ -118,6 +121,9 @@ 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(Box<list_args::CargoListArgs>),
 }
 
 // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext,
@@ -424,6 +430,7 @@ impl ValidateArgs for StandaloneArgs {
 
         match &self.command {
             Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?,
+            Some(StandaloneSubcommand::List(args)) => args.validate()?,
             // TODO: Invoke PlaybackArgs::validate()
             None | Some(StandaloneSubcommand::Playback(..)) => {}
         };
@@ -470,6 +477,7 @@ impl ValidateArgs for CargoKaniSubcommand {
             // Assess doesn't implement validation yet.
             CargoKaniSubcommand::Assess(_) => Ok(()),
             CargoKaniSubcommand::Playback(playback) => playback.validate(),
+            CargoKaniSubcommand::List(list) => list.validate(),
         }
     }
 }