Repository navigation
Conversation
dropping_formula_for_term treated any pointer field whose pointee is an enum with the same datatype symbol as a recursive variant and skipped it. The symbol is shared by every instantiation of a generic enum, so a non-recursive nesting such as Option<&mut Option<i64>> or Option<Box<Option<&mut i64>>> lost the drop of its inner value and the &mut inside was never resolved, havocking the borrowed owner. Compare the pointee's sort with the dropped enum's sort instead, which includes the type arguments. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XWq7RJmc4iTGM8H7fsjtAT
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![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: 28acdfa015
ℹ️ 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".
|
|
||
| if let Some(p) = field_type.as_pointer() { | ||
| if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) { | ||
| if p.elem.ty.to_sort() == ty.to_sort() { |
There was a problem hiding this comment.
When a recursive enum permutes its type arguments, exact sort equality never identifies the recursive field. For example, enum E<T, U> { Value(T, U), Next(Box<E<U, T>>) } is valid Rust, but dropping E<i32, bool> recursively alternates between E<i32, bool> and E<bool, i32> here until Thrust overflows its stack. The previous symbol comparison stopped this recursion, so the recursion guard needs to track datatype cycles rather than only an identical instantiated sort.
Useful? React with 👍 / 👎.
This branch has not been deployed
2 participants
Fixes #341.
dropping_formula_for_termskipped any variant field that points to an enum with the same datatype symbol, treating it as a recursive variant. Every instantiation of a generic enum shares that symbol. So for non-recursive nestings likeOption<&mut Option<i64>>orOption<Box<Option<&mut i64>>>, the inner value's drop was skipped, the&mutinside was never resolved, and the borrowed owner was havoc'd. As a result, correct programs were rejected asUnsat.This change compares the pointee's sort with the dropped enum's sort instead, so type arguments are taken into account. Genuinely recursive fields such as
Box<List>inListstill have equal sorts and are still skipped (#173 is unchanged).Tests
tests/ui/{pass,fail}/enum_nested_same_enum_mut_drop.rs.cargo testpasses locally: 402 UI tests, with z3 5.0.0 and the pinned PCSat.Generated by Claude Code