Skip to content

Autoharness: skip fns whose const {} blocks depend on a substituted type - #4981

Open
acearyanarun wants to merge 1 commit into
model-checking:mainfrom
acearyanarun:autoharness-issue-4826
Open

acearyanarun wants to merge 1 commit into
model-checking:mainfrom
acearyanarun:autoharness-issue-4826

Conversation

@acearyanarun

Copy link
Copy Markdown

#4820 stopped a const {} precondition on a const parameter from aborting an autoharness run. As #4826 describes, the same unrecoverable E0080 was still reachable when the substituted type decides the block: either a const parameter reaching it through a type argument (inner::<[u8; N]>()) or a block guarded on a type parameter alone (const { [..][size_of::<T>()] }). Both abort the entire run.

The change

The reachability walk now carries (DefId, GenericArgsRef), expressed in terms of the candidate's own parameters, instead of bare DefIds. It follows calls, reified fn items, closures and coroutines whose instantiated arguments mention a type or const parameter. Instantiations with concrete arguments are still not followed. A const {} block (AnonConst with NonTypeSystemInline) counts as a possible precondition when its instantiated arguments mention a type or const parameter.

One deliberate departure from the issue's suggested direction: other unevaluated constants still count only when they mention a const parameter. Generic associated constants like <T as SizedTypeProperties>::IS_ZST are reached by nearly every function over slices and collections. Treating them as preconditions would skip all of those (slice_len in the test pins this boundary).

Carrying instantiated arguments is mostly about precision: a caller that reaches a guarded callee only through a concrete type is no longer skipped (concrete_second_type pins this).

Std skip-count impact (requested in #4826)

kani autoharness --std --list over the nightly-2026-09-25 library, on aarch64-darwin, excluding core_arch:: (on main it crashes on SVE tuples; see #4964):

  • Generated: 20,868 → 20,790 (−78, 0 gained). Every lost function reaches a type-dependent const {} block, e.g. TypeId::of, needs_drop, type_name, RawVec's const { assert!(..) }, read_unaligned, mem::zeroed.
  • The other changed skip rows are relabeling. Functions already skipped for missing Arbitrary or trait bounds now report the const-block reason, because the check runs first, and are listed under their generic rather than instantiated name.
  • The 1024-body search limit was never hit (checked with temporary instrumentation).

Testing

  • New cases in cargo_autoharness_generics: both shapes from autoharness: E0080 can still abort a run when the substituted *type* decides a const {} block #4826, a type-parameter variant, and three must-still-verify boundaries (concrete type argument, a concrete argument passed through an intermediate call, generic associated constants). The two boundary tests that pin design choices fail under their targeted mutations.
  • autoharness_comptime_intrinsic/expected updated for the reworded skip message.
  • script-based-pre 90/91 locally. codegen_cache hit an EINTR on echo under parallel load; it passes in isolation and passed in an earlier full run.
  • cargo test -p kani-compiler, clippy -D warnings, kani-fmt --check all pass.

Resolves #4826

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

… type

model-checking#4820 skips a const-generic candidate when it can reach a `const {}`
block parameterized by a const parameter, because a failing block makes
rustc emit an unrecoverable E0080 that aborts the whole autoharness run.
The same abort was still reachable in two shapes (model-checking#4826):

- a const parameter reaching the block through a type argument, as in
  `inner::<[u8; N]>()`, since only `GenericArgKind::Const` arguments
  were considered when following calls; and
- a block guarded on a type parameter alone, as in
  `const { assert!(size_of::<T>() >= 4) }`.

The reachability walk now carries each body's generic arguments,
instantiated in terms of the candidate's own parameters, instead of bare
`DefId`s, and follows calls, reified fn items, closures and coroutines
whose arguments mention any type or const parameter. Instantiations with
concrete arguments are still not followed. A `const {}` block counts as a
possible precondition when its instantiated arguments mention a type or
const parameter. Other unevaluated constants still count only when they
mention a const parameter: generic associated constants such as
`<T as SizedTypeProperties>::IS_ZST` are reached by most functions over
slices and collections, and treating them as preconditions would skip
those functions too.

Resolves model-checking#4826
@acearyanarun
acearyanarun requested review from a team as code owners October 6, 2026 08:42
@github-actions github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Oct 6, 2026
@acearyanarun

Copy link
Copy Markdown
Author

Hey @CYJ904 @Tianshu-Huang @wodex1nhaoIeng @srivatsansamraj, I opened #4981 for Milestone 33 / #4826. Can you guys take a look when you get a chance and sanity check the fix + numbers?

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

autoharness: E0080 can still abort a run when the substituted *type* decides a const {} block

1 participant