Autoharness: metadata improvements and enable standard library application (#3948)

Update the autoharness subcommand to:

- Print the types of the arguments that don't implement Arbitrary
- Print a table of the functions we chose to verify after codegen
finishes, and move the printing of the functions we skipped to be after
codegen as well, instead of after verification. This lets us iterate
faster to debug because we can pass `--only-codegen` and see
pretty-printed data instead of waiting for verification to finish.
- Add a `--std` flag which, when provided, runs autoharness against the
provided path to the standard library.

Towards #3832

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

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)
     }
 }