Autoharness: constructor-based value generation (--constructor-args)

Cargo.lock

@@ -288,7 +288,7 @@ checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527"
 
 [[package]]
 name = "charon"
-version = "0.1.88"
+version = "0.1.73"
 dependencies = [
  "annotate-snippets",
  "anstream 0.6.21",

docs/src/reference/experimental/autoharness.md

@@ -79,6 +79,22 @@ Autoharness also accepts a `--list` argument, which runs the [list subcommand](.
 
 For a full list of options, run `kani autoharness --help`.
 
+### Constructor-based generation (--constructor-args)
+
+By default, when a type does not implement `Arbitrary`, Kani synthesizes values field by field.
+For types whose private fields carry a representation invariant (e.g. a date type storing a
+packed, validated ordinal), raw field synthesis can produce values that violate the invariant,
+causing false alarms in every harness that generates the type. With `--constructor-args`, Kani
+instead generates values of private-field struct types by calling one of the type's public
+constructors with nondeterministic arguments, assuming success for constructors returning
+`Option<Self>` or `Result<Self, E>`. Constructors that are doc-hidden, unsafe, zero-argument,
+or generic are not considered.
+
+This option is opt-in because it under-approximates: harnesses whose values are generated this
+way are marked "(ctor)" in the output, and their verification results only cover values
+reachable through the chosen constructor; a bug that requires a different value will not be
+found.
+
 ## Example
 Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:
 ```rust

kani-compiler/src/args.rs

@@ -111,6 +111,15 @@ pub struct Arguments {
     /// See kani_driver::autoharness_args for documentation.
     #[arg(long = "autoharness-exclude-pattern", num_args(1))]
     pub autoharness_excluded_patterns: Vec<String>,
+    /// If we are running the autoharness subcommand, whether to generate harnesses for
+    /// functions whose arguments require bounded nondeterministic values (e.g. slice
+    /// references). See kani_driver::autoharness_args for documentation.
+    #[arg(long = "autoharness-bounded-arguments")]
+    pub autoharness_bounded_arguments: bool,
+
+    /// Enable constructor-based nondeterministic value generation for autoharness.
+    #[arg(long = "autoharness-constructor-args")]
+    pub autoharness_constructor_args: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/kani_middle/codegen_units.rs

@@ -108,7 +108,9 @@ impl CodegenUnits {
                     .set(AutoHarnessMetadata {
                         chosen: chosen
                             .iter()
-                            .map(|func| crate::kani_middle::strip_local_crate_prefix(func.name()))
+                            .map(|(func, _)| {
+                                crate::kani_middle::strip_local_crate_prefix(func.name())
+                            })
                             .collect::<BTreeSet<_>>(),
                         skipped,
                     })
@@ -361,13 +363,13 @@ fn determine_targets(
 /// the AutomaticHarnessPass will later transform the bodies of these instances to actually verify the function.
 fn get_all_automatic_harnesses(
     tcx: TyCtxt,
-    verifiable_fns: Vec<Instance>,
+    verifiable_fns: Vec<(Instance, bool)>,
     kani_harness_intrinsic: FnDef,
     base_filename: &Path,
 ) -> HashMap<Harness, HarnessMetadata> {
     verifiable_fns
         .into_iter()
-        .map(|fn_to_verify| {
+        .map(|(fn_to_verify, is_ctor_based)| {
             // Set the generic arguments of the harness to be the function it is verifying
             // so that later, in AutomaticHarnessPass, we can retrieve the function to verify
             // and generate the harness body accordingly.
@@ -381,6 +383,7 @@ fn get_all_automatic_harnesses(
                 base_filename,
                 &fn_to_verify,
                 harness.mangled_name(),
+                is_ctor_based,
             );
             (harness, metadata)
         })
@@ -417,7 +420,7 @@ fn automatic_harness_partition(
     args: &Arguments,
     crate_name: &str,
     kani_any_def: FnDef,
-) -> (Vec<Instance>, BTreeMap<String, AutoHarnessSkipReason>) {
+) -> (Vec<(Instance, bool)>, BTreeMap<String, AutoHarnessSkipReason>) {
     let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::<FxHashSet<_>>();
     // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions
     // (c.f. https://github.com/model-checking/kani/issues/4189)
@@ -513,7 +516,20 @@ fn automatic_harness_partition(
         if let Some(reason) = skip_reason(func) {
             skipped.insert(crate::kani_middle::strip_local_crate_prefix(func.name()), reason);
         } else {
-            chosen.push(Instance::try_from(func).unwrap());
+            let instance = Instance::try_from(func).unwrap();
+            let is_ctor_based = args.autoharness_constructor_args
+                && instance.body().is_some_and(|body| {
+                    body.arg_locals().iter().any(|arg| {
+                        crate::kani_middle::uses_ctor_generation(
+                            tcx,
+                            arg.ty,
+                            kani_any_def,
+                            &mut FxHashMap::default(),
+                            &mut vec![],
+                        )
+                    })
+                });
+            chosen.push((instance, is_ctor_based));
         }
     }
 

kani-compiler/src/kani_middle/metadata.rs

@@ -42,6 +42,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         contract: Default::default(),
         has_loop_contracts: false,
         is_automatically_generated: false,
+        is_ctor_based: false,
     }
 }
 
@@ -121,6 +122,7 @@ pub fn gen_automatic_proof_metadata(
     base_name: &Path,
     fn_to_verify: &Instance,
     harness_mangled_name: String,
+    is_ctor_based: bool,
 ) -> HarnessMetadata {
     let def = fn_to_verify.def;
     let pretty_name = readable_name(*fn_to_verify);
@@ -159,5 +161,6 @@ pub fn gen_automatic_proof_metadata(
         contract: Default::default(),
         has_loop_contracts: false,
         is_automatically_generated: true,
+        is_ctor_based,
     }
 }