Execute drop glue for Drop terminators by Stevengre · Pull Request #999 · runtimeverification/mir-semantics

Stevengre · 2026-03-23T12:01:34Z

Summary

interior-mut-fail.rs should pass under rustc, but KMIR failed on the second RefCell::borrow_mut() by reaching panic_already_borrowed(noBody).

The root cause was not RefCell writeback. It was that KMIR still treated MIR Drop terminators as no-ops, and the pre-proof SMIR reduction also discarded drop_in_place::<...> bodies because Drop was not modeled as a reachability edge.

This PR fixes that by:

preserving reachable drop glue during SMIR reduction by adding Drop-based edges to call_edges
executing Drop terminators through the normal call path using reachable drop_in_place::<T> bodies

After that, the temporary RefMut guard from the first borrow_mut() is actually dropped, the borrow flag is released, and interior-mut passes.

Additional fixes

While validating the initial change, this PR also fixed two follow-up issues that the new drop-glue path exposed:

preserve drop glue reachability for Downcast + Field projections, so enum variant fields keep the correct drop_in_place::<FieldTy> edge
treat NoOpSym drop-glue shims as real no-op calls, instead of letting them fall through as unknown or ordinary body-less calls

It also adds minimal bridge rules for the newly exposed PointerOffset + Field + Union projection path so the updated drop-glue execution can complete without getting stuck.

Follow-up

Issue #1011 tracks the follow-up refactor to unify #traverseProjection's representation invariant and remove the temporary bridge rules introduced here.

Stevengre · 2026-04-01T14:16:42Z

These two #traverseProjection bridge rules are intentional stopgaps for PR #999. They close the newly exposed PointerOffset + Field + Union path needed by drop-glue execution, but they are not meant to be the long-term shape of traversal semantics. I opened #1011 to track the follow-up refactor: unify #traverseProjection's representation invariant, move the traversal toward a more function-like structure, and remove the round-trip bridge rules added here.

Stevengre · 2026-04-01T14:23:24Z

I re-ran iterator-simple in several variants to check whether the two new #traverseProjection bridge rules are actually needed.

Command used:

uv run pytest src/tests/integration/test_integration.py -v --timeout=600 -k 'iterator-simple'

Results:

origin/master: PASSED (1 passed, 271 deselected in 61.64s)
current PR head: PASSED (1 passed, 271 deselected in 62.09s)
current PR head with both new bridge rules removed from rt/data.md: FAILED (1 failed, 271 deselected in 66.40s)
current PR head with only the Range(ListItem(Union(...))) -> Union(...) rule kept: FAILED (1 failed, 271 deselected in 65.14s)
current PR head with only the VAL -> Range(ListItem(VAL)) rule kept: FAILED (1 failed, 271 deselected in 65.27s)

The failures are not generic snapshot drift. They get stuck in different places:

With only the VAL -> Range(ListItem(VAL)) rule kept, the proof stops at:

#traverseProjection(..., Range(ListItem(Union(...))), projectionElemField(...), ...)

This is the case that needs the Range(ListItem(Union(...))) -> Union(...) bridge.

With only the Range(ListItem(Union(...))) -> Union(...) rule kept, the proof gets a bit further but then stops at:

#traverseProjection(..., Integer(1, 32, true), ...)

That is, after unwrapping the Union, traversal still needs to continue through a PointerOffset path on a singleton non-Range value. Without the VAL -> Range(ListItem(VAL)) bridge, the shared range-based PointerOffset rules do not apply.

So the effect of the two rules is complementary:

VAL -> Range(ListItem(VAL)) lets the PointerOffset path reuse the shared range-based traversal logic for singleton values.
Range(ListItem(Union(...))) -> Union(...) unwraps that singleton range again when the next projection step is Field, so the existing Union + Field rules can match.

In other words, after this PR starts executing real drop glue, iterator-simple reaches a PointerOffset + Field + Union projection shape that origin/master never had to complete. Without these bridge rules, the proof regresses from #EndProgram to a stuck #traverseProjection term; and the split checks above show that each rule is closing a different gap in that path.

The longer-term cleanup is still tracked in #1011, but based on this comparison these two rules are doing necessary work in PR #999 rather than just papering over an unrelated difference.

Stevengre · 2026-04-01T14:57:17Z

I ran the same kind of A/B check for termReturnIgnored by removing just that rule from kmir.md and rebuilding the semantics.

Commands used:

uv run pytest src/tests/integration/test_integration.py -v --timeout=600 -k 'interior-mut or iterator-simple'
uv run pytest src/tests/integration/test_run_smir_random.py -v -k 'complex-types'

Results:

current PR head: both commands passed
current PR head with only termReturnIgnored removed: both commands still passed
- test_integration.py -k 'interior-mut or iterator-simple': 4 passed, 268 deselected in 265.89s
- test_run_smir_random.py -k 'complex-types': 10 passed, 10 deselected in 56.67s

So unlike the two #traverseProjection bridge rules, I could not reproduce a current regression that specifically requires termReturnIgnored.

The likely reason is that, in the current PR, the only explicit producer of place(local(-1), .ProjectionElems) on a call frame is the drop-glue path:

#callDropGlue(...)
=> #execTerminatorCall(..., place(local(-1), .ProjectionElems), ...)

But the drop glue functions we are actually exercising here return ()/no meaningful value, so they appear to come back through termReturnNone rather than termReturnSome. In other words, the sentinel destination exists, but the tested paths do not currently try to write a real return value into it.

Based on these runs, termReturnIgnored looks more like a defensive/general rule for ignored-return calls than something this PR's current regressions demonstrably depend on. I have not found a real test in this branch that fails when this rule is removed.

Stevengre · 2026-04-02T02:26:30Z

One more note on termReturnIgnored, since this one is less obvious than the projection bridge rules.

Its job is to handle return paths where the caller intentionally does not consume the callee's return value. In KMIR that case is represented by the sentinel destination:

place(local(-1), .ProjectionElems)

Without termReturnIgnored, such returns fall through to the normal writeback path:

#setLocalValue(DEST, #decrementRef(VAL))

but #setLocalValue only accepts real local indices (0 <= I < size(LOCALS)), so trying to write back to local(-1) can get stuck.

I confirmed this is not just theoretical: after removing termReturnIgnored, a full test_integration.py run stopped with a real regression at test_prove[ptr-cast-wrapper-to-array].

So the purpose of the rule is simply: if the destination is the ignored-return sentinel, skip writeback and continue directly to the caller's target block.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: dafd5f50b8

ℹ️ 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".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ce96db106e

ℹ️ 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".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 0950dccd96

ℹ️ 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".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ae3e60adb6

ℹ️ 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".

dkcumming

I like what you have here. But there are the concerns I mention in the comments. But aside from that I do wonder if this would be a good addition in the SmirJson, there could be a field added for drop_functions, and it could be populated as part of visiting a TerminatorKind::Drop. Upstream Rust does not serialise this, but we can add a side table if it would be useful. Would save doing it in python and might be useful for others.

I would like the opinion of @jberthold if you have time

dkcumming · 2026-04-07T19:49:37Z

+  // Temporary bridge rule: after PointerOffset lifts a single value to Range(ListItem(...)),
+  // unwrap a Union head element so the existing Union + Field rules below can keep running.
+  rule <k> #traverseProjection(
+             DEST,
+             Range(ListItem(Union(_, _) #as VALUE) _REST:List),
+             projectionElemField(IDX, TY) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... </k> // TODO mark context?
+    [preserves-definedness, priority(100)]


I am concerned to add these temporary rules. I feel getting these mix ups with the projections is indicative that we are handing the pointers wrong, and by adding rules like this we suppress the underlying problem. I know they are temporary, but a bandaid added and forgotten could cause deep confusion later...

I agree with the concern, and I do not want these bridge rules to become permanent sediment.

For this PR they are only meant as a narrow regression fix for the newly exercised drop-glue path. I opened follow-up issue #1011 to track the real cleanup: #1011

The plan there is to refactor #traverseProjection around a single representation invariant and then delete these round-trip bridge rules rather than leave them in place indefinitely.

Agree with both, requiring this rule indicates a problem with how pointers are handled. It is specialised to Union and Field but maybe it applies more generally?

dkcumming · 2026-04-07T21:27:57Z

For clarity, this is the drop terminator routine for std::cell:BorrowRef which is from interior-mut-fail.smir.dot

Stevengre · 2026-04-08T08:31:30Z

But aside from that I do wonder if this would be a good addition in the SmirJson, there could be a field added for drop_functions, and it could be populated as part of visiting a TerminatorKind::Drop. Upstream Rust does not serialise this, but we can add a side table if it would be useful. Would save doing it in python and might be useful for others.

@dkcumming

I think this could make sense as a separate upstream improvement, but I would prefer to keep it out of #999.

My current view is that stable-mir-json should provide complete enough information for downstream consumers, so if drop_functions is broadly useful then adding it there could be a good direction. But that would be a cross-repo schema/export change, whereas #999 is currently fixing a concrete regression in mir-semantics.

So I would prefer to treat that as a follow-up design discussion or separate issue/PR rather than fold it into this one.

jberthold · 2026-04-08T08:39:28Z

+  // Temporary bridge rule: after PointerOffset lifts a single value to Range(ListItem(...)),
+  // unwrap a Union head element so the existing Union + Field rules below can keep running.
+  rule <k> #traverseProjection(
+             DEST,
+             Range(ListItem(Union(_, _) #as VALUE) _REST:List),
+             projectionElemField(IDX, TY) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... </k> // TODO mark context?
+    [preserves-definedness, priority(100)]


Agree with both, requiring this rule indicates a problem with how pointers are handled. It is specialised to Union and Field but maybe it applies more generally?

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 9821acb11a

ℹ️ 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".

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c7c7548ab6

ℹ️ 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".

The two bridge rules added in bed3503 (Union-unwrap for Field, and bare-value-to-Range for PointerOffset) treated a symptom rather than the root cause. The real issue is in how removeIndexTail and #typeProjection interact during pointer construction and PtrToPtr casts for slice types. Removing these rules exposes the underlying stuck state so the proper fix can be validated against it. See #1011 for the planned structural fix.

The iterator-simple test exposes a stuck state in #traverseProjection caused by the interaction between removeIndexTail and #typeProjection for slice-of-MaybeUninit pointer casts. Mark as -fail with show snapshot until the root cause in pointer projection construction is resolved. See #1011.

The consP rule that merged ConstantIndex with PointerOffset was a workaround for a deeper issue: removeIndexTail in #mkAggregate(aggregateKindRawPtr) strips the element-extraction CI(0) when constructing fat pointers from thin pointers, but #typeProjection later adds per-element navigation projections (Field for MaybeUninit→ManuallyDrop→T) that assume the element has already been extracted. Removing removeIndexTail preserves the CI(0) through the fat pointer construction, allowing the subsequent #typeProjection projections to correctly navigate into individual array elements. The consP HACK rule is also removed as it is no longer needed and was conceptually unsound (merging projections from different semantic levels). The iterator-simple test now reaches a different stuck state: PointerOffset(1,0) applied to a scalar Integer after successful element navigation, which is closer to the real remaining issue (projection ordering between CI and PointerOffset). See #1011.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 60b5e5a842

ℹ️ 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".

Add integration test for Subslice projection on an owned array of Drop types. The `let [first, rest @ ..]` pattern generates a Subslice that changes the type from [Droppable; 3] to [Droppable; 2], exercising an unsupported code path in _projected_ty() and K semantics. Marked as expected-fail with show snapshot.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 8c27c7e9a6

ℹ️ 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".

Revert the experimental removal of bridge rules, consP HACK rule, and removeIndexTail. These are workarounds for a deeper design issue in how #typeProjection interacts with PointerOffset for slice-to-slice PtrToPtr casts (tracked in #1011), and removing them without the proper fix causes regressions. Restore iterator-simple.rs as a passing test.

Add unit test demonstrating that _projected_ty() returns the original array type for Subslice projections, causing call_edges to miss the drop_in_place::<[T; M]> edge and reduce_to() to incorrectly prune the required drop glue. Add integration test subslice-drop-partial-move.rs that generates Drop(arr.Subslice(1,3,false)) in the MIR — the exact pattern described in the Codex review comment.

_projected_ty() returned the original array type for Subslice projections, so call_edges missed drop glue for subslice drops like Drop(local.Subslice(1,3,false)) and reduce_to() pruned the required drop_in_place::<[T; M]> function. Compute the result array length from the Subslice parameters (to - from for from_end=false, len - from - to for from_end=true) and search the type table for a matching ArrayType with the same element type and length.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 7fb84c93e2

ℹ️ 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".

Stevengre changed the title ~~Execute drop glue for terminators~~ Execute drop glue for Drop terminators Mar 23, 2026

Stevengre force-pushed the codex/fix-interior-mut-drop-glue branch from 0577e22 to f2ccd0c Compare April 1, 2026 09:52

Stevengre mentioned this pull request Apr 1, 2026

Unify #traverseProjection value representation to eliminate singleton Range round-trips #1011

Open

8 tasks

Stevengre marked this pull request as ready for review April 2, 2026 02:51

Stevengre requested review from dkcumming and mariaKt April 2, 2026 02:51

Stevengre self-assigned this Apr 2, 2026

chatgpt-codex-connector Bot reviewed Apr 2, 2026

View reviewed changes

Comment thread kmir/src/kmir/smir.py

chatgpt-codex-connector Bot reviewed Apr 2, 2026

View reviewed changes

Comment thread kmir/src/kmir/smir.py Outdated

Stevengre force-pushed the codex/fix-interior-mut-drop-glue branch from ce96db1 to 71e9f53 Compare April 3, 2026 05:39

chatgpt-codex-connector Bot reviewed Apr 3, 2026

View reviewed changes

Comment thread kmir/src/kmir/kdist/mir-semantics/kmir.md Outdated

chatgpt-codex-connector Bot reviewed Apr 3, 2026

View reviewed changes

Comment thread kmir/src/kmir/smir.py Outdated

dkcumming reviewed Apr 7, 2026

View reviewed changes

jberthold reviewed Apr 8, 2026

View reviewed changes

Stevengre force-pushed the codex/fix-interior-mut-drop-glue branch 3 times, most recently from 058ed6d to cada2a8 Compare April 10, 2026 01:53

Stevengre mentioned this pull request Apr 10, 2026

Split #traverseProjection write-back from path reconstruction #1055

Closed

chatgpt-codex-connector Bot reviewed Apr 15, 2026

View reviewed changes

Comment thread kmir/src/kmir/smir.py

Stevengre added 5 commits April 16, 2026 12:00

fix(kmir): execute drop glue for drop terminators

c6f1b0d

test(kmir): drop redundant interior-mut show output

e9e918d

fix(ci): satisfy mypy for drop-glue reachability

5e64648

fix(smir): preserve drop glue edges for downcast fields

83eb9b5

fix(kmir): handle noop drop-glue calls

e70f00e

Stevengre added 14 commits April 16, 2026 12:00

test(kmir): refresh complex-types random snapshots

e869bb7

docs(kmir): mark bridge projection rules as temporary

d099d10

docs(kmir): clarify bridge projection comments

81ee256

docs(kmir): explain ignored return sentinel

da9b180

docs(test): clarify downcast drop-glue fixture

4f4c96b

fix(smir): preserve drop glue edges for index projections

432a60b

fix(ci): satisfy isort for test_kompile imports

77ed24a

fix(kmir): preserve move effects for noop calls

4f34cdc

fix(smir): accept core drop glue names

9802073

fix(kmir): consume noop call operands explicitly

591638b

Restore termDrop name and drop iterator-simple show snapshot

910ae06

Fix NoOp move handling and drop glue setup

45f8743

test(prove-rs): add noop drop_in_place move repro

c6d1d10

Fix local(-1) sentinel comment to reflect actual semantics

c7c7548

Stevengre force-pushed the codex/fix-interior-mut-drop-glue branch from c0bc575 to c7c7548 Compare April 16, 2026 04:00

chatgpt-codex-connector Bot reviewed Apr 16, 2026

View reviewed changes

Comment thread kmir/src/kmir/smir.py

Stevengre added 3 commits April 16, 2026 15:50

chatgpt-codex-connector Bot reviewed Apr 16, 2026

View reviewed changes

Comment thread kmir/src/kmir/kdist/mir-semantics/rt/data.md Outdated

Stevengre force-pushed the codex/fix-interior-mut-drop-glue branch from c7e3a5d to 575b6ed Compare April 16, 2026 08:46

Stevengre force-pushed the codex/fix-interior-mut-drop-glue branch from 575b6ed to 8c27c7e Compare April 16, 2026 08:48

chatgpt-codex-connector Bot reviewed Apr 16, 2026

View reviewed changes

Comment thread kmir/src/kmir/smir.py

Comment thread kmir/src/kmir/kdist/mir-semantics/rt/data.md Outdated

Stevengre added 3 commits April 16, 2026 17:10

Stevengre force-pushed the codex/fix-interior-mut-drop-glue branch from 89291c4 to 7fb84c9 Compare April 16, 2026 09:23

chatgpt-codex-connector Bot reviewed Apr 16, 2026

View reviewed changes

Comment thread kmir/src/kmir/kdist/mir-semantics/kmir.md

Stevengre marked this pull request as draft April 16, 2026 10:01

Conversation

Stevengre commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Additional fixes

Follow-up

Uh oh!

Stevengre commented Apr 1, 2026

Uh oh!

Stevengre commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Stevengre commented Apr 1, 2026

Uh oh!

Stevengre commented Apr 2, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

dkcumming left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

dkcumming Apr 7, 2026

Choose a reason for hiding this comment

Uh oh!

Stevengre Apr 8, 2026

Choose a reason for hiding this comment

Uh oh!

jberthold Apr 8, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

dkcumming commented Apr 7, 2026

Uh oh!

Stevengre commented Apr 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jberthold Apr 8, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

Stevengre commented Mar 23, 2026 •

edited

Loading

Stevengre commented Apr 1, 2026 •

edited

Loading

Stevengre commented Apr 8, 2026 •

edited

Loading