Autoharness: --list option

kani-compiler/src/kani_middle/codegen_units.rs

@@ -36,7 +36,7 @@ use std::sync::OnceLock;
 use tracing::debug;
 
 /// An identifier for the harness function.
-type Harness = Instance;
+pub type Harness = Instance;
 
 /// A set of stubs.
 pub type Stubs = HashMap<FnDef, FnDef>;
@@ -92,8 +92,7 @@ impl CodegenUnits {
                     args,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
                 );
-                let chosen_fn_names =
-                    chosen.iter().map(|func| func.name().clone()).collect::<Vec<_>>();
+                let chosen_fn_names = chosen.iter().map(|func| func.name()).collect::<Vec<_>>();
                 AUTOHARNESS_MD
                     .set(AutoHarnessMetadata { chosen: chosen_fn_names, skipped })
                     .expect("Initializing the autoharness metdata failed");
@@ -167,7 +166,7 @@ impl CodegenUnits {
             proof_harnesses,
             unsupported_features: vec![],
             test_harnesses,
-            contracted_functions: gen_contracts_metadata(tcx),
+            contracted_functions: gen_contracts_metadata(tcx, &self.harness_info),
             autoharness_md: AUTOHARNESS_MD.get().cloned(),
         }
     }

kani-compiler/src/kani_middle/metadata.rs

@@ -7,6 +7,7 @@ use std::collections::HashMap;
 use std::path::Path;
 
 use crate::kani_middle::attributes::{KaniAttributes, test_harness_name};
+use crate::kani_middle::codegen_units::Harness;
 use crate::kani_middle::{SourceLocation, stable_fn_def};
 use kani_metadata::ContractedFunction;
 use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
@@ -47,7 +48,10 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
 ///
 /// 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> {
+pub fn gen_contracts_metadata(
+    tcx: TyCtxt,
+    harness_info: &HashMap<Harness, HarnessMetadata>,
+) -> 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();
 
@@ -61,8 +65,8 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
         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()
+        // This logic finds manual contract harnesses only (automatic harnesses are a Kani intrinsic, not crate items annotated with the proof_for_contract attribute).
+        } else if let Some((_, 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")
@@ -73,7 +77,9 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
                 fn_to_data.insert(
                     target_def_id,
                     ContractedFunction {
-                        function: target_name.to_string(),
+                        // Note that we use the item's fully qualified-name, rather than the target name specified in the attribute.
+                        // This is necessary for the automatic contract harness lookup, see below.
+                        function: item.name(),
                         file,
                         harnesses: vec![function],
                     },
@@ -82,6 +88,24 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
         }
     }
 
+    // Find automatically generated contract harnesses (if the `autoharness` subcommand is running)
+    for (harness, metadata) in harness_info {
+        if !metadata.is_automatically_generated {
+            continue;
+        }
+        if let HarnessKind::ProofForContract { target_fn } = &metadata.attributes.kind {
+            // FIXME: This is a bit hacky. We can't resolve the target_fn to a DefId because we need somewhere to start the name resolution from.
+            // For a manual harness, we could just start from the harness, but since automatic harnesses are Kani intrinsics, we can't resolve the target starting from them.
+            // Instead, we rely on the fact that the ContractedFunction objects store the function's fully qualified name,
+            // and that `gen_automatic_proof_metadata` uses the fully qualified name as well.
+            // Once we implement multiple automatic harnesses for a single function, we will have to revise the HarnessMetadata anyway,
+            // and then we can revisit the idea of storing the target_fn's DefId somewhere.
+            let (_, target_cf) =
+                fn_to_data.iter_mut().find(|(_, cf)| &cf.function == target_fn).unwrap();
+            target_cf.harnesses.push(harness.name());
+        }
+    }
+
     fn_to_data.into_values().collect()
 }
 

kani-driver/src/args/autoharness_args.rs

@@ -4,6 +4,7 @@
 
 use std::path::PathBuf;
 
+use crate::args::list_args::Format;
 use crate::args::{ValidateArgs, VerificationArgs, validate_std_path};
 use clap::{Error, Parser, error::ErrorKind};
 use kani_metadata::UnstableFeature;
@@ -29,6 +30,13 @@ pub struct CommonAutoharnessArgs {
     pub exclude_function: Vec<String>,
     // TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches,
     // like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though.
+    /// Run the `list` subcommand after generating the automatic harnesses. Requires -Z list. Note that this option implies --only-codegen.
+    #[arg(long)]
+    pub list: bool,
+
+    /// The format of the `list` output. Requires --list.
+    #[arg(long, default_value = "pretty", requires = "list")]
+    pub format: Format,
 }
 
 /// Automatically verify functions in a crate.
@@ -76,6 +84,24 @@ impl ValidateArgs for CargoAutoharnessArgs {
             ));
         }
 
+        if self.common_autoharness_args.list
+            && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List),
+            ));
+        }
+
+        if self.common_autoharness_args.format == Format::Pretty
+            && self.verify_opts.common_args.quiet
+        {
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.",
+            ));
+        }
+
         if self
             .verify_opts
             .common_args
@@ -105,6 +131,24 @@ impl ValidateArgs for StandaloneAutoharnessArgs {
             ));
         }
 
+        if self.common_autoharness_args.list
+            && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List),
+            ));
+        }
+
+        if self.common_autoharness_args.format == Format::Pretty
+            && self.verify_opts.common_args.quiet
+        {
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.",
+            ));
+        }
+
         if self.std {
             validate_std_path(&self.input)?;
         } else if !self.input.is_file() {

kani-driver/src/args/list_args.rs

@@ -64,6 +64,13 @@ impl ValidateArgs for CargoListArgs {
             ));
         }
 
+        if self.format == Format::Pretty && self.common_args.quiet {
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.",
+            ));
+        }
+
         Ok(())
     }
 }
@@ -78,6 +85,13 @@ impl ValidateArgs for StandaloneListArgs {
             ));
         }
 
+        if self.format == Format::Pretty && self.common_args.quiet {
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.",
+            ));
+        }
+
         if self.std {
             validate_std_path(&self.input)
         } else if self.input.is_file() {

kani-driver/src/autoharness/mod.rs

@@ -4,11 +4,15 @@
 use std::str::FromStr;
 
 use crate::args::Timeout;
-use crate::args::autoharness_args::{CargoAutoharnessArgs, StandaloneAutoharnessArgs};
+use crate::args::autoharness_args::{
+    CargoAutoharnessArgs, CommonAutoharnessArgs, StandaloneAutoharnessArgs,
+};
 use crate::call_cbmc::VerificationStatus;
 use crate::call_single_file::to_rustc_arg;
 use crate::harness_runner::HarnessResult;
-use crate::project::{standalone_project, std_project};
+use crate::list::collect_metadata::process_metadata;
+use crate::list::output::output_list_results;
+use crate::project::{Project, standalone_project, std_project};
 use crate::session::KaniSession;
 use crate::{InvocationType, print_kani_version, project, verify_project};
 use anyhow::Result;
@@ -20,30 +24,18 @@ const LOOP_UNWIND_DEFAULT: u32 = 20;
 
 pub fn autoharness_cargo(args: CargoAutoharnessArgs) -> Result<()> {
     let mut session = KaniSession::new(args.verify_opts)?;
-    session.enable_autoharness();
-    session.add_default_bounds();
-    session.add_auto_harness_args(
-        args.common_autoharness_args.include_function,
-        args.common_autoharness_args.exclude_function,
-    );
+    setup_session(&mut session, &args.common_autoharness_args);
+
     if !session.args.common_args.quiet {
         print_kani_version(InvocationType::CargoKani(vec![]));
     }
     let project = project::cargo_project(&mut session, false)?;
-    if !session.args.common_args.quiet {
-        print_metadata(project.metadata.clone());
-    }
-    if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
+    postprocess_project(project, session, args.common_autoharness_args)
 }
 
 pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> {
     let mut session = KaniSession::new(args.verify_opts)?;
-    session.enable_autoharness();
-    session.add_default_bounds();
-    session.add_auto_harness_args(
-        args.common_autoharness_args.include_function,
-        args.common_autoharness_args.exclude_function,
-    );
+    setup_session(&mut session, &args.common_autoharness_args);
 
     if !session.args.common_args.quiet {
         print_kani_version(InvocationType::Standalone);
@@ -55,14 +47,41 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> {
         standalone_project(&args.input, args.crate_name, &session)?
     };
 
+    postprocess_project(project, session, args.common_autoharness_args)
+}
+
+/// Execute autoharness-specific KaniSession configuration.
+fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAutoharnessArgs) {
+    session.enable_autoharness();
+    session.add_default_bounds();
+    session.add_auto_harness_args(
+        &common_autoharness_args.include_function,
+        &common_autoharness_args.exclude_function,
+    );
+}
+
+/// After generating the automatic harnesses, postprocess metadata and run verification.
+fn postprocess_project(
+    project: Project,
+    session: KaniSession,
+    common_autoharness_args: CommonAutoharnessArgs,
+) -> Result<()> {
     if !session.args.common_args.quiet {
-        print_metadata(project.metadata.clone());
+        print_autoharness_metadata(project.metadata.clone());
+    }
+    if common_autoharness_args.list {
+        let list_metadata = process_metadata(project.metadata.clone());
+        return output_list_results(
+            list_metadata,
+            common_autoharness_args.format,
+            session.args.common_args.quiet,
+        );
     }
     if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
 }
 
 /// Print automatic harness metadata to the terminal.
-fn print_metadata(metadata: Vec<KaniMetadata>) {
+fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
     let mut chosen_table = PrettyTable::new();
     chosen_table.set_header(vec!["Chosen Function"]);
 
@@ -135,7 +154,7 @@ impl KaniSession {
     }
 
     /// Add the compiler arguments specific to the `autoharness` subcommand.
-    pub fn add_auto_harness_args(&mut self, included: Vec<String>, excluded: Vec<String>) {
+    pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) {
         for func in included {
             self.pkg_args
                 .push(to_rustc_arg(vec![format!("--autoharness-include-function {}", func)]));

kani-driver/src/list/collect_metadata.rs

@@ -20,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>) -> ListMetadata {
+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.

kani-driver/src/list/mod.rs

@@ -6,9 +6,9 @@ use kani_metadata::ContractedFunction;
 use std::collections::{BTreeMap, BTreeSet};
 
 pub mod collect_metadata;
-mod output;
+pub mod output;
 
-struct ListMetadata {
+pub struct ListMetadata {
     // Files mapped to their #[kani::proof] harnesses
     standard_harnesses: BTreeMap<String, BTreeSet<String>>,
     // Total number of #[kani::proof] harnesses

tests/script-based-pre/cargo_autoharness_list/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_list"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_autoharness_list/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: list.sh
+expected: list.expected

tests/script-based-pre/cargo_autoharness_list/list.expected

@@ -0,0 +1,26 @@
+Kani generated automatic harnesses for 3 function(s):
++---------------------------+
+| Chosen Function           |
++===========================+
+| f_u8                      |
+|---------------------------|
+| has_recursion_gcd         |
+|---------------------------|
+| verify::has_recursion_gcd |
++---------------------------+
+
+Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s).
+
+Contracts:
++-------+---------------------------+-----------------------------------------------------------------------------+
+|       | Function                  | Contract Harnesses (#[kani::proof_for_contract])                            |
++=================================================================================================================+
+|       | has_recursion_gcd         | my_harness, my_harness_2, kani::internal::automatic_harness                 |
+|-------+---------------------------+-----------------------------------------------------------------------------|
+|       | verify::has_recursion_gcd | verify::my_harness, verify::my_harness_2, kani::internal::automatic_harness |
+|-------+---------------------------+-----------------------------------------------------------------------------|
+| Total | 2                         | 6                                                                           |
++-------+---------------------------+-----------------------------------------------------------------------------+
+
+Standard Harnesses (#[kani::proof]):
+1. f_u8

tests/script-based-pre/cargo_autoharness_list/list.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z autoharness --list -Z list -Z function-contracts