Fix unsoundness from closure capturing &mut in a struct/tuple field (#41)

[coord-e]

Summary

Fixes #41. A closure capturing &mut stored in a tuple/struct field made thrust derive a contradictory environment and unsoundly accept programs that can panic (the issue's assert!(false) was proven unreachable).

Root cause

The drop-point analysis (src/analyze/basic_block/drop_point.rs) treats a local's last use as its drop site, based purely on liveness. When a value is moved into an aggregate (e.g. a closure moved into a tuple via _2 = (move _3, 0)), the moved-out temporary _3 was still dropped at the move site. Dropping a value containing a &mut asserts final == current on the captured reference, which prematurely resolves its prophecy to the construction-time value (0). The subsequent (s.0)() call mutates through the closure (final = 1), contradicting the pinned 0. An inconsistent environment makes any following assertion vacuously "safe" — the unsoundness.

Fix

Exclude owned (non-reference) locals whose ownership is transferred away by a move from the drop set — their drop obligation belongs to the destination. Moved references are deliberately left untouched, because ReborrowVisitor/RustCallVisitor rewrite them into reborrows, so the source local stays live and must still be dropped. (Restricting to non-reference types is essential: suppressing all moved-local drops regresses cases like closure_mut_0, where the original MIR moves a &mut that thrust reborrows.)

https://claude.ai/code/session_01HHar2z2xTNwffns5SF7wRe

---

Generated by Claude Code

[Copilot]

Pull request overview

Fixes a soundness bug in Thrust’s implicit drop-point analysis where moved (owned) locals could still be treated as dropped at the move site, producing contradictory environments when closures capturing &mut are stored in tuple/struct fields.

Changes:

• Add tracking of locals whose ownership is transferred via move and exclude them from implicit drop points (for non-reference types).
• Add UI regression tests covering both the accepted (“pass”) and rejected (“fail”) variants of the closure-in-field mutation scenario.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
src/analyze/basic_block/drop_point.rs	Excludes moved (owned) locals from implicit drop sets to avoid premature drops at move sites.
tests/ui/pass/closure_field_mut.rs	Regression test ensuring closure mutation through a tuple field is tracked and accepted when asserted correctly.
tests/ui/fail/closure_field_mut.rs	Regression test ensuring incorrect post-call assertions are rejected (avoids vacuous acceptance via inconsistent env).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.