Autoharness: verify all formatting trait implementations

[srivatsansamraj]

fmt_impl_self_ty recognises Debug and Display implementations, whose &mut Formatter argument is supplied by a model that formats a nondeterministic self value into a discarding sink (#4701). The other seven formatting traits went through the general path and were skipped for that argument: 41 fmt methods on an autoharness --list --std run, 33 of them in core.

This extends the same mechanism to Binary, Octal, LowerHex, UpperHex, LowerExp, UpperExp and Pointer. Only Debug, Display and Pointer carry a diagnostic item, so the rest are matched by name inside core::fmt.

As for Debug and Display, the self type must implement or derive Arbitrary. Of the 41, 20 gain a harness (NonZero, Wrapping, Saturating, Box/Rc/Arc of a primitive, and compiler_builtins' numeric types) and 21 on references and raw pointers (&i32, *const i32, NonNull, Unique, Atomic<*mut _>) stay skipped, now reported for the self type rather than the Formatter.

Pointer needs one extra step. format_args!("{value:p}") with value: &T selects impl Pointer for &T, which formats the reference's address rather than delegating to T, so the model would never reach the implementation under test. Its model formats through a local wrapper whose Pointer::fmt calls <T as Pointer>::fmt directly.

• FmtTrait gains the seven variants and a model() mapping; AutomaticHarnessPass holds one map of models instead of a field per trait.
• Seven check_*_fmt models in kani_core, beside the existing two.
• cargo_autoharness_fmt_impls gains one type per trait, each failing on its own assert. A model dispatched to the wrong trait does not resolve for that type, so a swap fails to generate rather than passing.
• Docs.

Part of #3832; follows #4701.

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

[Copilot]

🟡 Changes recommended

Raw-pointer formatting remains ineligible, and the regression test cannot detect swapped trait-to-model mappings.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

Extends autoharness verification from Debug and Display to all standard formatting traits.

Changes:

• Adds trait-specific formatting models and dispatch.
• Expands regression coverage for seven additional traits.
• Updates autoharness documentation.

File summaries

File	Description
tests/script-based-pre/cargo_autoharness_fmt_impls/src/lib.rs	Adds formatting trait test implementations.
tests/script-based-pre/cargo_autoharness_fmt_impls/fmt-impls.expected	Adds expected failures and harness results.
library/kani_core/src/lib.rs	Adds trait-specific formatting models.
kani-compiler/src/kani_middle/transform/automatic.rs	Dispatches through a formatting-model map.
kani-compiler/src/kani_middle/mod.rs	Recognizes and maps additional formatting traits.
kani-compiler/src/kani_middle/kani_functions.rs	Registers the new models.
kani-compiler/src/kani_middle/codegen_units.rs	Generalizes formatting harness documentation.
docs/src/reference/experimental/autoharness.md	Documents expanded formatting support.

Review details

Suppressed comments (3)

kani-compiler/src/kani_middle/mod.rs:1050

• The match arms should follow the same alphabetical order as the enum variants and their KaniModel counterparts, rather than retaining the old two variants first.

            FmtTrait::Debug => KaniModel::CheckDebugFmt,
            FmtTrait::Display => KaniModel::CheckDisplayFmt,
            FmtTrait::Binary => KaniModel::CheckBinaryFmt,

kani-compiler/src/kani_middle/mod.rs:1035

• Keep the formatting-trait variants alphabetically ordered, consistent with the adjacent KaniModel formatting variants in kani_functions.rs:108-125; appending Binary after Display leaves this enum out of order.

    Debug,
    Display,
    Binary,

docs/src/reference/experimental/autoharness.md:296

• The documented limitation now covers all nine formatting traits, but {:#?} is only the alternate Debug syntax; the other traits use forms such as {:#b}, {:#x}, and {:#p}. Please describe this as the generic alternate flag (or list the trait-specific forms) so the documentation does not imply that only Debug's alternate path is excluded.

  with the trait's bare specifier (`{:?}`, `{}`, `{:x}`, ...) would produce. Code paths that a `fmt`
  implementation takes only for a non-default width, precision, fill, alignment, sign, or the
  alternate (`{:#?}`) flag are therefore not covered.

• Files reviewed: 8/8 changed files
• Comments generated: 2
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.