Repository navigation
Autoharness documentation is out of date and missing several features #4979
Description
Activity
@Tianshu-Huang cc.
Reacted by Tianshu HuangI'll take this. Since #4958 also touches this page, I'll start once it lands to avoid conflicts.
The new autoharness book chapter should follow this overall structure. It starts with the core idea, then covers the three phases (select → generate → verify/report), and ends by collecting the soundness caveats and the internals in one place each:
┌────────────────────────────────────┐ │ AUTOHARNESS: the core idea │ │ "for each fn: x = any(); f(x)" │ └─────────────────┬──────────────────┘ │ ┌──────────────────────────────────┼──────────────────────────────────┐ ▼ ▼ ▼ ┌────────────────┐ ┌─────────────────────────┐ ┌────────────────────┐ │ 1. SELECT │ │ 2. GENERATE │ │ 3. VERIFY & REPORT │ │ which fns? │ │ what goes in each │ │ run it, read it │ │ │ │ harness? │ │ │ ├────────────────┤ ├─────────────────────────┤ ├────────────────────┤ │ • include / │ │ 2a. ARGUMENTS │ │ • parallel / -j │ │ exclude regex│ │ Unbounded (default): │ │ • terse vs regular │ │ • --list │ │ ├ Arbitrary / derive │ │ • 60s timeout, │ │ • skip reasons │ │ ├ raw pointers │ │ unwind 20 │ │ • generics: │ │ ├ Box / Rc / Arc │ │ • summary table │ │ pick one │ │ ├ prim. slices / Vec │ │ • (bounded) / │ │ instantiation│ │ ├ Fn-bound closures │ │ (ctor) markers │ │ (Fn bounds, │ │ └ fmt-trait impls │ │ • bounds note │ │ SIMD, const) │ │ Opt-in (under-approx):│ └────────────────────┘ └────────────────┘ │ ├ --bounded-arguments │ │ └ --constructor-args │ │ 2b. ASSUMPTIONS │ │ ├ contracts (requires)│ │ ├ Invariant::is_safe │ │ ├ layout niches │ │ └ mined invariants │ │ 2c. CHECKS │ │ ├ UB / panics (always)│ │ ├ contracts (ensures) │ │ └ --check-invariants │ └─────────────────────────┘ │ ┌──────────────────────────────────┴──────────────────────────────────┐ ▼ ▼ ┌───────────────────────────────────────┐ ┌──────────────────────────────────────────┐ │ SOUNDNESS CAVEATS (what "Success" │ │ ARCHITECTURE (for contributors) │ │ does NOT mean) │ │ driver → partition → harness pass → │ │ • one monomorphization only │ │ codegen → CBMC → summary │ │ • no aliasing between args (#4750) │ │ (see the architecture diagram below) │ │ • bounded args only up to bound │ └──────────────────────────────────────────┘ │ • ctor may be vacuous (#4757) │ │ • mined-invariant heuristic (#4763) │ └───────────────────────────────────────┘Architecture diagram (for the contributors section)
┌──────────────────────────── kani-driver ────────────────────────────┐ │ args/autoharness_args.rs CLI: --include/--exclude-pattern, │ │ --bounded-arguments, --constructor-args, │ │ --check-invariants, --list, bounds │ │ autoharness/mod.rs setup_session(): parallel defaults, timeout, │ │ unwind, add_auto_harness_args() → --autoharness-*│ │ call_single_file.rs: adds those flags to the kani-compiler call │ └────────────────┬────────────────────────────────────────────────────┘ ▼ ┌──────────────────────────── kani-compiler ──────────────────────────┐ │ kani_middle/codegen_units.rs │ │ automatic_harness_partition() → chosen / skipped (+reasons) │ │ get_all_automatic_harnesses() → AutomaticHarnessIntrinsic::<fn> │ │ + gen_automatic_proof_metadata() │ │ kani_middle/transform/automatic.rs │ │ AutomaticHarnessPass dummy body → [contract init] args = any() │ │ [assume invariants] f(args) [checks] │ │ AutomaticArbitraryPass T::any() for derivable types │ │ codegen_cprover_gotoc → goto; KaniMetadata { autoharness_md, ... } │ └────────────────┬────────────────────────────────────────────────────┘ ▼ ┌──────────────────────────── kani-driver ────────────────────────────┐ │ postprocess_project(): chosen/skipped tables, --list stops here │ │ harness_runner.rs: CBMC per harness → print_autoharness_summary() │ └─────────────────────────────────────────────────────────────────────┘Reacted by Tianshu Huang@Tianshu-Huang I need more time to review #4958 so don't wait on it to be merged to start working on this one.
Reacted by Tianshu HuangThank you, the structure is clear!
I wrote my earlier reply last night, before our sync today. After the sync, the team decided that Sriv and I will take the verification-result analysis, and @CYJ904 @acearyanarun @wodex1nhaoIeng will work on this one.
- added 9 commits that reference this issue
on Oct 8, 2026
The autoharness reference page (
docs/src/reference/experimental/autoharness.md) is out of date with the implementation onmain. Some sections are now wrong, and several user-visible features are not documented at all.Incorrect / outdated content
Vecare no longer always bounded (Autoharness: unbounded slice, mutable slice and Vec arguments #4721).&[T],&mut [T]andVec<T>arguments whose element type is a primitive integer or float are generated as fresh allocations of nondeterministic length. They are eligible by default (no--bounded-argumentsneeded) and are not marked "(bounded)". Seeautomatic_harness_partitioninkani-compiler/src/kani_middle/codegen_units.rsandUnboundedModelsinkani-compiler/src/kani_middle/transform/automatic.rs. The "Bounded Arguments" and "Limitations > Arguments Implementing Arbitrary" sections currently say slices require--bounded-arguments.Fn/FnMut/FnOnceare no longer skipped. They are instantiated with nondeterministic closure models (fn_bound_candidates,resolve_deferred_fn_slotsandNondetFnModelsincodegen_units.rs). Arities 0-3 are supported; for reference-taking shapes only arity 1 and 2. The "Generic Functions" section should describe this and its limits.Undocumented features
Box<T>/Rc<T>/Arc<T>arguments whose pointee implements or can deriveArbitraryare supported and unbounded (SmartPointerModelsinkani-compiler/src/kani_middle/mod.rs; testcargo_autoharness_smart_pointers).Layout niche assumptions. Generated values of types with scalar valid ranges (e.g.
NonZero*,Duration's nanoseconds field) are constrained to their valid range (assume_scalar_niche). This is sound and needs no flag, but it explains why such types do not produce false alarms.Default verification settings.
kani autoharnesssets--harness-timeout 60sand--default-unwind 20(kani-driver/src/autoharness/mod.rs). The page only mentions the unwind bound in passing.The full list of skip reasons. Only "Generic Function" and "Requires --bounded-arguments" are documented. Missing:
Comptime(can only be called at compile time)KaniImplNoBodyUnsupportedVariadicUserFilterMissingArbitraryImplSee
AutoHarnessSkipReasoninkani_metadata/src/lib.rs.Additional generic-instantiation rejections:
simd_imin::<T>with a non-SIMDT;invalid_simd_instantiation).has_const_generic_precondition).Smaller CLI items:
kani autoharness --std(run on the standard library).--list --format <FORMAT>.--slice-bound,--string-bound,--bounded-arbitrary-bound) are rejected unless--bounded-argumentsis passed.Suggested restructuring
The page has grown feature by feature. Consider reorganizing it as:
--list, skip reasons)Vec, Fn-bound generics, niches--bounded-arguments,--constructor-argsInvariant, mined invariants /--check-invariants)