Analyze the impl body a trait-dispatched call resolves to - #237
Draft
coord-e wants to merge 1 commit into
Draft
Conversation
A generic impl of a trait method is registered as a deferred def, whose body is analyzed only when its type is asked for. A call dispatched through the trait takes its type from the trait method instead, where the spec is annotated, so nothing ever asked for the impl method's type: its body went unchecked while every caller assumed the trait's `ensures`. Ask for it at the call site, and instantiate the trait ref in `trait_item_ty` with the analyzed instantiation so the impl method's expected type is the trait's spec for that instantiation rather than one carrying the impl's own type parameters. Closes #190 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PvA5f69BEE7xw9MR6SLeMX
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
2 participants
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.
Closes #190.
A generic
implof a trait method is registered as a deferred def, whose body is analyzed only when its type is asked for. A call dispatched through the trait takes its type from the trait method instead — that is where the spec is annotated — so nothing ever asked for the impl method's type: its body went unchecked while every caller assumed the trait'sensures, and an always-panicking program verified assafe.Changes
src/analyze/basic_block.rs: whenfn_def_tyanswers from the registered callee type, also analyze the body the call resolves to (analyze_resolved_impl_body, a no-op unless resolution lands on a different def). The impl method's expected type is the trait's spec, so running its body against that type is the missing check.src/analyze/local_def.rs:trait_item_tyinstantiates the impl's trait ref with the instantiation being analyzed rather than the identity one, so the trait spec is translated at concrete types.Analyzer::newnow defaultsgeneric_argsto the identity instantiation, which keeps that instantiation well-formed for a def whose generic arguments were never set.tests/ui/{pass,fail}/trait_generic_impl.rs: a genericimplof a spec'd trait method, with theensuressatisfied and violated.Verification
cargo test(328 UI tests),cargo fmt --all -- --checkandcargo clippy -- -D warningsall pass, with Z3 5.0.0 and the CI-pinned COAR image.Beyond the added test pair, checked by hand: the issue's reproduction and its
assert!(false)-with-unused-result variant are both rejected; a satisfied body, a boundedimpl<T: Base>, and two instantiations (W<i32>andW<bool>) all verify, and each is rejected once its body breaks the postcondition.Generated by Claude Code