Autoharness: support generic functions

[tautschnig]

Description

Autoharness now generates harnesses for generic functions. For each generic function, it verifies a single monomorphic instantiation: every type parameter is substituted with the first candidate from a fixed list of primitive types (i32, u32, usize, bool, char) such that all of the function's trait bounds are satisfied — checked properly with the trait solver (rustc_trait_selection::ObligationCtxt) — and lifetime parameters are erased. Functions whose bounds no candidate satisfies (e.g. bounds on user traits with no primitive impls) and functions with const generic parameters are still skipped with the existing "Generic Function" reason.

This handles arbitrary numbers of generic parameters, methods of generic impl blocks (whose impl-level parameters are instantiated too), impl Trait argument position (anonymous type parameters), and generic functions with contracts. For contract harnesses, the harness metadata now stores the definition-level name of the target function rather than the instantiated one, since gen_contracts_metadata matches target_fn against definition-level ContractedFunction names (this previously had no observable effect because generic functions never reached that code path).

Design note on soundness of the reported result: verifying foo::<i32> is an underapproximation of foo's behaviors for all instantiations. The summary table makes this explicit by displaying the instantiated name (foo::<i32>), and the documentation spells out that a successful result covers only the chosen instantiation. Verifying one instantiation per function (rather than a set) keeps verification cost proportional to crate size; extending this to user-configurable instantiation sets is possible follow-up work.

Testing

New script-based test cargo_autoharness_generics covering: unbounded and bounded type parameters, bound-driven candidate selection (impl Into<u64> + Copy correctly skips i32 and picks u32), multiple type parameters, lifetimes, methods of generic impl blocks, a generic function with a contract (verified as proof_for_contract), a genuine bug found at the chosen instantiation (arithmetic overflow), and graceful skipping of unsatisfiable bounds and const generics.

Updated cargo_autoharness_filter/include/exclude tests, whose generic example functions are now instantiated and verified instead of skipped.

Manually verified no regressions in all autoharness and autoderive script-based tests and kani-compiler unit tests.

Note: the two functions previously used to exercise multi-parameter generics in a prototype branch ICE'd the compiler ("type parameter U/#1 out of range"); both are covered by the new test and verify correctly.

Towards #3832 (ticks the "Generics" box, the last unchecked entry together with #4677 and #4678).

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

[Copilot]

Pull request overview

Adds support for generating automatic harnesses for generic functions by selecting a single monomorphic instantiation per function (based on a fixed primitive candidate list and trait-bound satisfaction via the trait solver), and updates related metadata, docs, and script-based tests to reflect the new behavior.

Changes:

• Instantiate generic functions for autoharness using primitive candidates and trait-solver checking; erase lifetimes and keep skipping const generics/unsatisfiable bounds.
• Fix contract-harness metadata to store the definition-level target function name (to match contract metadata lookup behavior).
• Add/refresh script-based tests and documentation for generic-function autoharness behavior and output.

Reviewed changes

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

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_include/src/lib.rs	Updates include test source comment to reflect generic instantiation behavior.
tests/script-based-pre/cargo_autoharness_include/include.expected	Updates expected output to include instantiated generic function verification.
tests/script-based-pre/cargo_autoharness_generics/src/lib.rs	Adds new script-based test crate covering generic instantiation cases and edge cases.
tests/script-based-pre/cargo_autoharness_generics/generics.sh	Adds script to run cargo kani autoharness with contracts enabled for the new test.
tests/script-based-pre/cargo_autoharness_generics/generics.expected	Adds expected summary lines for generic instantiation successes/failure and skips.
tests/script-based-pre/cargo_autoharness_generics/config.yml	Registers the new script-based test (expects failure exit code due to intentional bug).
tests/script-based-pre/cargo_autoharness_generics/Cargo.toml	Adds manifest for the new test crate.
tests/script-based-pre/cargo_autoharness_filter/src/lib.rs	Adjusts filter test inputs to include a generic function now expected to be harnessed.
tests/script-based-pre/cargo_autoharness_filter/filter.expected	Updates expected output counts and entries to include instantiated generic function.
tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs	Updates exclude test source comment to reflect generic instantiation behavior.
tests/script-based-pre/cargo_autoharness_exclude/exclude.expected	Updates expected output to include instantiated generic function verification.
kani-compiler/src/main.rs	Adds rustc_infer / rustc_trait_selection extern crates required for trait-solver usage.
kani-compiler/src/kani_middle/metadata.rs	Switches contract harness metadata to use definition-level target function names.
kani-compiler/src/kani_middle/codegen_units.rs	Implements generic instantiation candidate selection and predicate checking for autoharness eligibility.
docs/src/reference/experimental/autoharness.md	Documents the new “single-instantiation” behavior and its underapproximation implications.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.