Autoharness: mine type invariants from a type's own assertions

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,19 @@ 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,
+
+    /// Check mined type invariants on values returned by autoharness-verified functions.
+    #[arg(long = "autoharness-check-invariants")]
+    pub autoharness_check_invariants: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -899,6 +899,94 @@ impl GotocHook for LoopInvariantRegister {
     }
 }
 
+/// Lower `kani::slice_validity_assume::<T>(ptr, len)` (KaniHook::SliceValidityAssume) to a
+/// quantified assumption constraining every element's raw bits to `T`'s layout niche:
+/// `assume(forall i. i < len ==> lo <= *(uN*)ptr + i <= hi)` (wrapping ranges use `||`).
+/// A no-op for element types without a niche (every bit pattern valid).
+///
+/// This is lowered directly to pure goto expressions rather than through `kani::forall!`:
+/// the closure-based quantifier lowering cannot substitute bodies containing checked
+/// arithmetic or bounds checks (it falls back to an unconstrained predicate), whereas the
+/// expressions built here are side-effect-free by construction.
+struct SliceValidityAssume;
+impl GotocHook for SliceValidityAssume {
+    fn hook_applies(
+        &self,
+        _tcx: TyCtxt,
+        _instance: Instance,
+        _instance_name: &str,
+        _kani_tool_attr: Option<&String>,
+    ) -> bool {
+        unreachable!("{UNEXPECTED_CALL}")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        instance: Instance,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let loc = gcx.codegen_span_stable(span);
+        let target = target.unwrap();
+        let goto_target = Stmt::goto(bb_label(target), loc);
+
+        let elem_ty = instance.args().0[0].expect_ty().to_owned();
+        let Some(niche) = crate::kani_middle::scalar_niche(gcx.tcx, elem_ty) else {
+            // Every bit pattern is valid: nothing to assume.
+            return goto_target;
+        };
+        let len = fargs.remove(1);
+        let ptr = fargs.remove(0);
+
+        // Fresh quantified variable of the same type as `len`.
+        let base_name = "kani_slice_validity_var".to_string();
+        let mut counter = 0;
+        let mut unique_name = format!("{base_name}_{counter}");
+        while gcx.symbol_table.lookup(&unique_name).is_some() {
+            counter += 1;
+            unique_name = format!("{base_name}_{counter}");
+        }
+        let qvar = {
+            let sym =
+                GotoSymbol::variable(unique_name.clone(), unique_name, len.typ().clone(), loc);
+            gcx.symbol_table.insert(sym.clone());
+            sym.to_expr()
+        };
+
+        // CBMC's quantifier handling binds byte-granularity dereferences reliably, but not
+        // wider ones (byte_extract at a symbolic index under a forall does not propagate),
+        // so the validity predicate is expressed over bytes:
+        // - 8-bit niches (bool, u8-based ranged types): direct range check on the byte;
+        // - NonZero-style niches (excluded zero, full top): OR over "some byte nonzero".
+        // Wider general ranges are not byte-decomposable this simply; the element classifier
+        // (kani_middle::slice_elem_unbounded_ok) never routes such types to this hook.
+        let byte_ty = Type::unsigned_int(8u64);
+        let byte_ptr = ptr.clone().cast_to(byte_ty.clone().to_pointer());
+        let valid = if niche.bits == 8 {
+            let elem = byte_ptr.plus(qvar.clone()).dereference();
+            let lo = Expr::int_constant(niche.start, byte_ty.clone());
+            let hi = Expr::int_constant(niche.end, byte_ty.clone());
+            if niche.start <= niche.end {
+                lo.le(elem.clone()).and(elem.le(hi))
+            } else {
+                lo.le(elem.clone()).or(elem.le(hi))
+            }
+        } else {
+            unreachable!(
+                "slice_validity_assume: element type with non-byte-decomposable niche                  should have been rejected by the classifier"
+            )
+        };
+        let domain = qvar.clone().lt(len).implies(valid);
+        let quantified = Expr::forall_expr(Type::Bool, qvar, domain);
+
+        Stmt::block(vec![gcx.codegen_assume(quantified, loc), goto_target], loc)
+    }
+}
+
 struct Forall;
 struct Exists;
 
@@ -1339,6 +1427,7 @@ pub fn fn_hooks() -> GotocHooks {
     let kani_lib_hooks = [
         (KaniHook::Assert, Rc::new(Assert) as Rc<dyn GotocHook>),
         (KaniHook::Assume, Rc::new(Assume)),
+        (KaniHook::SliceValidityAssume, Rc::new(SliceValidityAssume)),
         (KaniHook::Exists, Rc::new(Exists)),
         (KaniHook::Forall, Rc::new(Forall)),
         (KaniHook::Panic, Rc::new(Panic)),

kani-compiler/src/kani_middle/codegen_units.rs

@@ -9,7 +9,7 @@
 
 use crate::args::{Arguments, ReachabilityType};
 use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness};
-use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
+use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel};
 use crate::kani_middle::metadata::{
     gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata,
 };
@@ -103,12 +103,16 @@ impl CodegenUnits {
                     args,
                     &crate_info.name,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
+                    *kani_fns.get(&KaniHook::Assert.into()).unwrap(),
+                    kani_fns.contains_key(&KaniModel::AnySliceRefUnbounded.into()),
                 );
                 AUTOHARNESS_MD
                     .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 +365,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 +385,7 @@ fn get_all_automatic_harnesses(
                 base_filename,
                 &fn_to_verify,
                 harness.mangled_name(),
+                is_ctor_based,
             );
             (harness, metadata)
         })
@@ -417,7 +422,9 @@ fn automatic_harness_partition(
     args: &Arguments,
     crate_name: &str,
     kani_any_def: FnDef,
-) -> (Vec<Instance>, BTreeMap<String, AutoHarnessSkipReason>) {
+    kani_assert_def: FnDef,
+    unbounded_slice_available: bool,
+) -> (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)
@@ -478,6 +485,25 @@ fn automatic_harness_partition(
         // Note that we've already filtered out generic functions, so we know that each of these arguments has a concrete type.
         let mut problematic_args = vec![];
         for (idx, arg) in body.arg_locals().iter().enumerate() {
+            // Unbounded generation: slices (&[T], &mut [T]) and Vec<T> of primitive
+            // integer/float elements are generated as fresh allocations of
+            // nondeterministic size (results hold for all lengths), when the optional
+            // alloc-requiring models are present.
+            if unbounded_slice_available {
+                let slice_ok = match arg.ty.kind() {
+                    TyKind::RigidTy(RigidTy::Ref(_, inner, _)) => match inner.kind() {
+                        TyKind::RigidTy(RigidTy::Slice(elem)) => {
+                            crate::kani_middle::slice_elem_unbounded_ok(tcx, elem)
+                        }
+                        _ => false,
+                    },
+                    _ => crate::kani_middle::vec_elem_ty(arg.ty)
+                        .is_some_and(|elem| crate::kani_middle::slice_elem_unbounded_ok(tcx, elem)),
+                };
+                if slice_ok {
+                    continue;
+                }
+            }
             if !ty_arbitrary_cache.contains_key(&arg.ty) {
                 let impls_arbitrary =
                     implements_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache)
@@ -513,7 +539,21 @@ 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,
+                            kani_assert_def,
+                            &mut FxHashMap::default(),
+                            &mut vec![],
+                        )
+                    })
+                });
+            chosen.push((instance, is_ctor_based));
         }
     }
 

kani-compiler/src/kani_middle/kani_functions.rs

@@ -65,6 +65,12 @@ pub enum KaniModel {
     AlignOfDynObject,
     #[strum(serialize = "AlignOfValRawModel")]
     AlignOfVal,
+    #[strum(serialize = "AnySliceMutUnboundedModel")]
+    AnySliceMutUnbounded,
+    #[strum(serialize = "AnySliceRefUnboundedModel")]
+    AnySliceRefUnbounded,
+    #[strum(serialize = "AnyVecUnboundedModel")]
+    AnyVecUnbounded,
     #[strum(serialize = "AnyModel")]
     Any,
     #[strum(serialize = "CopyInitStateModel")]
@@ -129,6 +135,8 @@ pub enum KaniHook {
     AnyRaw,
     #[strum(serialize = "AssertHook")]
     Assert,
+    #[strum(serialize = "SliceValidityAssumeHook")]
+    SliceValidityAssume,
     #[strum(serialize = "AssumeHook")]
     Assume,
     #[strum(serialize = "CheckHook")]
@@ -162,6 +170,20 @@ pub enum KaniHook {
     UntrackedDeref,
 }
 
+impl KaniModel {
+    /// Whether this model may legitimately be absent. These models require `alloc` and are
+    /// only defined in the `kani` library, not in `core::kani` (the `no_core` flow used by
+    /// `kani verify-std`). Code retrieving optional models must handle their absence.
+    pub fn is_optional(&self) -> bool {
+        matches!(
+            self,
+            KaniModel::AnySliceMutUnbounded
+                | KaniModel::AnySliceRefUnbounded
+                | KaniModel::AnyVecUnbounded
+        )
+    }
+}
+
 impl From<KaniIntrinsic> for KaniFunction {
     fn from(value: KaniIntrinsic) -> Self {
         KaniFunction::Intrinsic(value)
@@ -271,7 +293,7 @@ pub fn validate_kani_functions(kani_funcs: &HashMap<KaniFunction, FnDef>) {
     {
         if let Some(fn_def) = kani_funcs.get(&func) {
             assert_eq!(KaniFunction::try_from(*fn_def), Ok(func), "Unexpected function marker");
-        } else {
+        } else if !matches!(func, KaniFunction::Model(model) if model.is_optional()) {
             tracing::error!(?func, "Missing kani function");
             missing += 1;
         }

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