Autoharness: try () when instantiating generic functions

[wodex1nhaoIeng]

Summary

AutoHarness currently skips some generic functions because () is missing from the base list of candidate types used for generic instantiation.

This change adds () to that list. The existing trait solver still verifies that the selected type satisfies all bounds, and Kani already has a complete Arbitrary implementation for ().

Context

The standard library implements Extend<()> for (). Some generic functions therefore require () as an item type. Trait-implementation discovery can find () as the concrete receiver type, but an unconstrained item type is chosen only from the base candidate list. Without (), valid generic instantiations are skipped.

The regression test exercises the standard library's unit and tuple Extend implementations and verifies:

• extend_unit::<()>
• extend_unit_pair::<(), ()>

The existing intentional buggy_add failure remains unchanged.

Related issue

• Contributes to #3832, the Automatic Harnesses tracking issue.
• This PR does not close the tracking issue.

Manual testing

Ran:

cargo build-dev
cargo run -p compiletest -- --suite script-based-pre --mode exec --force-rerun cargo_autoharness_generics
rustfmt --check --config-path rustfmt.toml kani-compiler/src/kani_middle/codegen_units.rs tests/script-based-pre/cargo_autoharness_generics/src/lib.rs

The focused regression passed. It generated and successfully verified the two new unit-based harnesses, reported 18 successful harnesses, and retained the existing intentional failure for buggy_add.

The full regression suite and whole-standard-library comparison were not run.

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

[feliperodri]

The mechanism checks out: on main a function whose bounds only () satisfies is skipped, and with this change it gets ::<()>. The new test fails without the change and passes with it.

The blocker is a side effect on functions that work today. choose_generic_instantiation caps the search at 256 solver queries. Appending () lengthens both the uniform pass and every slot of the cartesian pass, so existing solutions move later in the enumeration, and some move past the cap. Concretely, with traits implemented only by usize, u32 and u64, three_params<A: OnlyUsize, B: OnlyU32, C: OnlyU64> gets three_params::<usize, u32, u64> on main and is skipped with this PR. The message says no candidate satisfies the bounds, when in fact the search ran out of attempts first.

What would flip this to approval: add () in a way that can't change the outcome for functions that already get an instantiation. One option is a last-resort uniform () attempt after the existing search fails, which covers both new test cases. A test like three_params pinning a near-cap case would guard it.

Separately, which real function motivated this? The only examples are the test's own (): Extend<T> shapes. A std or crate function that's skipped today would make the value much easier to weigh.

[wodex1nhaoIeng]

I’ve revised the implementation locally to preserve the original candidate list, search order, and 256-query budget. Only after that search fails does it make one additional attempt with all type parameters set to ().

The motivating functions are the standard library’s tuple Extend methods: extend_one, extend_one_unchecked, and extend_reserve. Their bounds are satisfied when all item and collection type parameters are ().

I have not added mixed combinations involving () because an additional combinatorial search would increase the worst-case search cost. I’d leave that support and its performance tradeoffs for a follow-up.

I have also left out the proposed near-cap regression test in this revision. The preservation argument is structural: the original search is unchanged, and any previously successful instantiation returns before reaching the new fallback. This specifically avoids the candidate-displacement regression you identified. Would you still prefer a dedicated test to guard this property against future changes?