Repository navigation
Autoharness: skip fns whose const {} blocks depend on a substituted type - #4981
Open
acearyanarun wants to merge 1 commit into
Open
acearyanarun wants to merge 1 commit into
acearyanarun wants to merge 1 commit into
Conversation
… 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
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
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#4820 stopped a
const {}precondition on a const parameter from aborting an autoharness run. As #4826 describes, the same unrecoverableE0080was 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 bareDefIds. 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. Aconst {}block (AnonConstwithNonTypeSystemInline) 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_ZSTare reached by nearly every function over slices and collections. Treating them as preconditions would skip all of those (slice_lenin 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_typepins this).Std skip-count impact (requested in #4826)
kani autoharness --std --listover the nightly-2026-09-25 library, on aarch64-darwin, excludingcore_arch::(on main it crashes on SVE tuples; see #4964):const {}block, e.g.TypeId::of,needs_drop,type_name,RawVec'sconst { assert!(..) },read_unaligned,mem::zeroed.Arbitraryor trait bounds now report the const-block reason, because the check runs first, and are listed under their generic rather than instantiated name.Testing
cargo_autoharness_generics: both shapes from autoharness: E0080 can still abort a run when the substituted *type* decides aconst {}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/expectedupdated for the reworded skip message.script-based-pre90/91 locally.codegen_cachehit anEINTRonechounder parallel load; it passes in isolation and passed in an earlier full run.cargo test -p kani-compiler,clippy -D warnings,kani-fmt --checkall 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.