Analyze the impl body a trait-dispatched call resolves to - #237
Conversation
220e02c to
be42861
Compare
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
be42861 to
1133f50
Compare
There was a problem hiding this comment.
🟡 Changes recommended
Trait-item argument rebasing remains incomplete for generic methods and type-dependent contracts.
Once you've addressed the issues Copilot identified, you can request another Copilot review.
Pull request overview
Fixes a soundness gap by analyzing generic trait implementation bodies against trait contracts at dispatched call sites.
Changes:
- Resolves and analyzes the concrete implementation behind trait calls.
- Propagates generic instantiations into trait contract analysis.
- Adds passing and failing regression tests.
File summaries
| File | Description |
|---|---|
src/analyze/basic_block.rs |
Triggers analysis of resolved implementation methods. |
src/analyze/local_def.rs |
Propagates generic arguments during trait-type translation. |
tests/ui/pass/trait_generic_impl.rs |
Covers a conforming generic implementation. |
tests/ui/fail/trait_generic_impl.rs |
Rejects a contract-violating generic implementation. |
Review details
- Files reviewed: 4/4 changed files
- Comments generated: 1
- Review effort level: Balanced
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1133f502dc
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
`trait_item_ty` passed only the impl's trait ref arguments, which cover the trait's generics but not the method's own. Analyzing the impl body of a generic trait method therefore asked for the trait method's type with too few arguments and panicked with `type parameter out of range`. Inherited `requires`/`ensures` had the reverse problem: they were translated with the impl method's arguments, whose layout maps `Self` to the impl's first generic parameter. Build the trait method's arguments once, and extract the inherited annotations with them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PvA5f69BEE7xw9MR6SLeMX
|
@codex review |
|
Codex Review: Didn't find any major issues. Breezy! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
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, it now also asks for the type of the impl the call resolves to, which is what analyzes that impl's body. The impl method's expected type is the trait's spec, so running its body against it is the missing check. The lookup sits at the call site rather than indef_ty_with_argsso that it resolves in the caller body's typing env and reusesresolve_fn_def.src/analyze/local_def.rs:trait_item_argsbuilds the implemented trait method's arguments for the instantiation being analyzed — the instantiated trait ref followed by the impl method's own-parameter tail — and both the trait-item type lookup and the inheritedrequires/ensuresextraction use it.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.tests/ui/{pass,fail}/trait_generic_method.rs: the same for a trait method generic over a parameter of its own, which the newly reached path had to get right.Verification
cargo test(330 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 pairs, 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>, two instantiations (W<i32>andW<bool>), a non-generic method in a generic impl, and the method passed as a function value all verify or are rejected as they should be.