Autoharness: metadata improvements and enable standard library application

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -613,7 +613,7 @@ impl GotoCodegenResults {
             // 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![],
-            autoharness_skipped_fns: None,
+            autoharness_md: None,
         }
     }
 

kani-compiler/src/kani_middle/codegen_units.rs

@@ -18,7 +18,7 @@ use crate::kani_middle::resolve::expect_resolve_fn;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
 use crate::kani_queries::QueryDb;
 use kani_metadata::{
-    ArtifactType, AssignsContract, AutoHarnessSkipReason, AutoHarnessSkippedFns, HarnessKind,
+    ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind,
     HarnessMetadata, KaniMetadata,
 };
 use rustc_hir::def_id::DefId;
@@ -32,6 +32,7 @@ use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fs::File;
 use std::io::BufWriter;
 use std::path::{Path, PathBuf};
+use std::sync::OnceLock;
 use tracing::debug;
 
 /// An identifier for the harness function.
@@ -40,6 +41,8 @@ type Harness = Instance;
 /// A set of stubs.
 pub type Stubs = HashMap<FnDef, FnDef>;
 
+static AUTOHARNESS_MD: OnceLock<AutoHarnessMetadata> = OnceLock::new();
+
 /// Store some relevant information about the crate compilation.
 #[derive(Clone, Debug)]
 struct CrateInfo {
@@ -49,7 +52,6 @@ struct CrateInfo {
 
 /// We group the harnesses that have the same stubs.
 pub struct CodegenUnits {
-    autoharness_skipped_fns: Option<AutoHarnessSkippedFns>,
     crate_info: CrateInfo,
     harness_info: HashMap<Harness, HarnessMetadata>,
     units: Vec<CodegenUnit>,
@@ -74,12 +76,7 @@ impl CodegenUnits {
                 let units = group_by_stubs(tcx, &all_harnesses);
                 validate_units(tcx, &units);
                 debug!(?units, "CodegenUnits::new");
-                CodegenUnits {
-                    units,
-                    harness_info: all_harnesses,
-                    crate_info,
-                    autoharness_skipped_fns: None,
-                }
+                CodegenUnits { units, harness_info: all_harnesses, crate_info }
             }
             ReachabilityType::AllFns => {
                 let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename);
@@ -95,6 +92,11 @@ impl CodegenUnits {
                     args,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
                 );
+                let chosen_fn_names =
+                    chosen.iter().map(|func| func.name().clone()).collect::<Vec<_>>();
+                AUTOHARNESS_MD
+                    .set(AutoHarnessMetadata { chosen: chosen_fn_names, skipped })
+                    .expect("Initializing the autoharness metdata failed");
 
                 let automatic_harnesses = get_all_automatic_harnesses(
                     tcx,
@@ -117,21 +119,11 @@ impl CodegenUnits {
 
                 // No need to validate the units again because validation only checks stubs, and we haven't added any stubs.
                 debug!(?units, "CodegenUnits::new");
-                CodegenUnits {
-                    units,
-                    harness_info: all_harnesses,
-                    crate_info,
-                    autoharness_skipped_fns: Some(skipped),
-                }
+                CodegenUnits { units, harness_info: all_harnesses, crate_info }
             }
             _ => {
                 // Leave other reachability type handling as is for now.
-                CodegenUnits {
-                    units: vec![],
-                    harness_info: HashMap::default(),
-                    crate_info,
-                    autoharness_skipped_fns: None,
-                }
+                CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info }
             }
         }
     }
@@ -176,7 +168,7 @@ impl CodegenUnits {
             unsupported_features: vec![],
             test_harnesses,
             contracted_functions: gen_contracts_metadata(tcx),
-            autoharness_skipped_fns: self.autoharness_skipped_fns.clone(),
+            autoharness_md: AUTOHARNESS_MD.get().cloned(),
         }
     }
 }
@@ -432,7 +424,8 @@ fn automatic_harness_partition(
                         var.argument_index.is_some_and(|arg_idx| idx + 1 == usize::from(arg_idx))
                     })
                     .map_or("_".to_string(), |debug_info| debug_info.name.to_string());
-                problematic_args.push(arg_name)
+                let arg_type = format!("{}", arg.ty);
+                problematic_args.push((arg_name, arg_type))
             }
         }
         if !problematic_args.is_empty() {

kani-driver/src/args/autoharness_args.rs

@@ -4,7 +4,7 @@
 
 use std::path::PathBuf;
 
-use crate::args::{ValidateArgs, VerificationArgs};
+use crate::args::{ValidateArgs, VerificationArgs, validate_std_path};
 use clap::{Error, Parser, error::ErrorKind};
 use kani_metadata::UnstableFeature;
 
@@ -54,6 +54,11 @@ pub struct StandaloneAutoharnessArgs {
     #[command(flatten)]
     pub common_autoharness_args: CommonAutoharnessArgs,
 
+    /// Pass this flag to run the `autoharness` subcommand on the standard library.
+    /// Ensure that the provided `input` is the `library` folder.
+    #[arg(long)]
+    pub std: bool,
+
     #[command(flatten)]
     pub verify_opts: VerificationArgs,
 }
@@ -99,7 +104,10 @@ impl ValidateArgs for StandaloneAutoharnessArgs {
                 ),
             ));
         }
-        if !self.input.is_file() {
+
+        if self.std {
+            validate_std_path(&self.input)?;
+        } else if !self.input.is_file() {
             return Err(Error::raw(
                 ErrorKind::InvalidValue,
                 format!(

kani-driver/src/args/list_args.rs

@@ -4,7 +4,7 @@
 
 use std::path::PathBuf;
 
-use crate::args::{CommonArgs, ValidateArgs};
+use crate::args::{CommonArgs, ValidateArgs, validate_std_path};
 use clap::{Error, Parser, ValueEnum, error::ErrorKind};
 use kani_metadata::UnstableFeature;
 
@@ -79,39 +79,7 @@ impl ValidateArgs for StandaloneListArgs {
         }
 
         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(())
-                }
-            }
+            validate_std_path(&self.input)
         } else if self.input.is_file() {
             Ok(())
         } else {

kani-driver/src/args/mod.rs

@@ -20,7 +20,7 @@ use clap::builder::{PossibleValue, TypedValueParser};
 use clap::{ValueEnum, error::ContextKind, error::ContextValue, error::Error, error::ErrorKind};
 use kani_metadata::CbmcSolver;
 use std::ffi::OsString;
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 use std::str::FromStr;
 use std::time::Duration;
 use strum::VariantNames;
@@ -789,6 +789,42 @@ impl ValidateArgs for VerificationArgs {
     }
 }
 
+pub(crate) fn validate_std_path(std_path: &Path) -> Result<(), Error> {
+    if !std_path.exists() {
+        Err(Error::raw(
+            ErrorKind::InvalidValue,
+            format!(
+                "Invalid argument: `<STD_PATH>` argument `{}` does not exist",
+                std_path.display()
+            ),
+        ))
+    } else if !std_path.is_dir() {
+        Err(Error::raw(
+            ErrorKind::InvalidValue,
+            format!(
+                "Invalid argument: `<STD_PATH>` argument `{}` is not a directory",
+                std_path.display()
+            ),
+        ))
+    } else {
+        let full_path = std_path.canonicalize()?;
+        let dir = full_path.file_stem().unwrap();
+        if dir != "library" {
+            Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: Expected `<STD_PATH>` to point to the `library` folder \
+                containing the standard library crates.\n\
+                Found `{}` folder instead",
+                    dir.to_string_lossy()
+                ),
+            ))
+        } else {
+            Ok(())
+        }
+    }
+}
+
 /// clap parser for `CbmcSolver`
 #[derive(Clone, Debug)]
 pub struct CbmcSolverValueParser(Vec<PossibleValue>);

kani-driver/src/args/std_args.rs

@@ -3,7 +3,7 @@
 
 //! Implements the `verify-std` subcommand handling.
 
-use crate::args::{ValidateArgs, VerificationArgs};
+use crate::args::{ValidateArgs, VerificationArgs, validate_std_path};
 use clap::error::ErrorKind;
 use clap::{Error, Parser};
 use kani_metadata::UnstableFeature;
@@ -40,38 +40,6 @@ impl ValidateArgs for VerifyStdArgs {
             ));
         }
 
-        if !self.std_path.exists() {
-            Err(Error::raw(
-                ErrorKind::InvalidValue,
-                format!(
-                    "Invalid argument: `<STD_PATH>` argument `{}` does not exist",
-                    self.std_path.display()
-                ),
-            ))
-        } else if !self.std_path.is_dir() {
-            Err(Error::raw(
-                ErrorKind::InvalidValue,
-                format!(
-                    "Invalid argument: `<STD_PATH>` argument `{}` is not a directory",
-                    self.std_path.display()
-                ),
-            ))
-        } else {
-            let full_path = self.std_path.canonicalize()?;
-            let dir = full_path.file_stem().unwrap();
-            if dir != "library" {
-                Err(Error::raw(
-                    ErrorKind::InvalidValue,
-                    format!(
-                        "Invalid argument: Expected `<STD_PATH>` to point to the `library` folder \
-                    containing the standard library crates.\n\
-                    Found `{}` folder instead",
-                        dir.to_string_lossy()
-                    ),
-                ))
-            } else {
-                Ok(())
-            }
-        }
+        validate_std_path(&self.std_path)
     }
 }