Autoharness: verify Debug and Display implementations

[tautschnig]

Description

The fmt methods of Debug/Display implementations were always skipped by autoharness: their &mut Formatter argument has no Arbitrary implementation, and Formatter cannot be synthesized (it wraps private state and a dyn Write sink). In the top-100 crates.io evaluation, Formatter arguments were the single largest "Missing Arbitrary" type (~1,900 skipped functions).

Rather than generating a Formatter, generate the harness the way user code exercises these implementations: format a nondeterministic value of the implementing type into a sink that discards the output, via two new models that call core::fmt::write(&mut DiscardingSink, format_args!(..., value)). The Formatter is constructed by the core formatting machinery — so it is always valid — and panics or undefined behavior inside the user's fmt are detected as usual (reachability follows the format_args! reference to the impl). The models are pure core and live in kani_core, available in both library flavors — no optional-model machinery needed.

Detection uses trait_impl_of_assoc plus the Debug/Display diagnostic items; eligibility requires the self type to implement (or be able to derive) Arbitrary. The self value is generated with kani::any through the shared call_kani_any_for_ty helper, so these harnesses are unbounded (full coverage of the self type — no --bounded-arguments interplay) and the self type's Invariant, if any, is assumed just like for a regular argument.

Both the eligibility check (automatic_harness_partition) and the harness generation (AutomaticHarnessPass) go through the same fmt_impl_self_ty predicate, so the two cannot disagree about which functions the formatting models handle.

A fmt method carrying a function contract is deliberately excluded: the automatic contract harness calls the function directly (and would therefore need a Formatter), and the formatting models reach fmt through a function pointer, where contract dispatch does not apply. Such a method is reported as skipped for its &mut Formatter argument, exactly as before this change.

Compiler-derived Debug implementations are verified too. That is consistent with how autoharness already treats other derived implementations (Clone::clone, PartialEq::eq, PartialOrd::partial_cmp, Default::default all get harnesses today), so no separate filter was added.

The documented limitations of the approach: the Formatter carries the default formatting parameters (so paths taken only for a non-default width/precision/fill/alignment/sign or the alternate {:#?} flag are not covered), the sink never fails (so ? write-error paths are not covered), and failures may point at a location inside core::fmt since the core formatting machinery is verified along with the fmt implementation.

Testing

New script-based test cargo_autoharness_fmt_impls, covering:

• a buggy Debug impl (assertion reachable — fails, with the panic message asserted in the expected output),
• a buggy Display impl (assertion reachable — fails), so that the Display model and its compiler branch are exercised by a failing harness too, not only by passing ones,
• a Display impl on a compiler-derived self type (passes),
• a Display impl on a self type with an Invariant (passes, i.e. the invariant is assumed — verified separately that the body is reached by negating the assertion),
• a compiler-derived Debug impl (passes),
• a self type that cannot be generated (skipped with the standard reason),
• a self type with a lifetime parameter (skipped),
• a fmt method under contract (skipped for its &mut Formatter argument).

Full script-based-pre suite (64 tests, including all 20 autoharness tests and verify_std_cmd, since kani_core is shared with the no_core flow), cargo test for kani-compiler/kani-driver/kani_metadata/cprover_bindings, clippy --all-targets, and kani-fmt --check all pass.

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.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[Copilot]

Pull request overview

Copilot reviewed 11 out of 11 changed files in this pull request and generated 1 comment.

[feliperodri]

Good catch — addressed. Added Level, a Display impl with a reachable failing assertion (the counterpart of Percent), and asserted Failed Checks: "invalid level" plus the Failure row in the expected output. The Display model and its compiler branch are now pinned by a failing harness, not only by ones that pass. Even keeps its (invariant-guaranteed) assertion, since its purpose is to check that the self type's Invariant is assumed.