Track drop points by MIR Place, splitting partially-moved locals (fix #121, #122)

[coord-e]

Supersedes #154 and #124. Fixes #121 and #122.

Motivation

• Replace the previous ad-hoc Local-only drop-point representation with MIR Place so implicit drops are tracked at the correct place granularity (the Track drop points by MIR Place #154 generalization).
• On top of that, fix the Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121/Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122 double-resolution bug. #154 alone generalized the representation but did not fix the underlying issue: a local with a partial field move (e.g. move (_2.0)) was still dropped wholesale, so the drop walked into the moved-out sub-place and resolved the &mut prophecy it owns a second time. The two resolutions contradict (final = 1 ∧ final = 2), making the clause body unsatisfiable, after which any assertion — including false ones — "verifies".

Description

• DropPoints is generic over the MIR lifetime and stores mir::Place<'tcx> in before_statements, after_statements, after_terminator, and after_terminator_extra. Liveness-derived Local sets are converted to Places in the builder, and the basic-block Analyzer routes all implicit-drop handling through drop_place/drop_after_terminator working on mir::Place<'tcx>.
• The fix lives in the drop-point production, not the env drop-walk. partial_moves collects the sub-places moved out of each local somewhere in the body; expand_owned_places then splits a to-be-dropped local along its type into the maximal still-owned sub-places, carving out moved-out subtrees while still dropping their owned siblings. A wholly-moved place expands to nothing; a place with no moved-out descendant is emitted whole (preserving prior behavior). Reference-typed moves are left in place, since ReborrowVisitor/RustCallVisitor turn them into reborrows and the source keeps owning its prophecy.
• Drop-point places are collected into HashSet instead of Vec, removing the manual dedup bookkeeping.

Testing

• New pass/fail regression tests for both shapes:
  • partial_move_drop.rs — Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121's partial-move-into-local (let b = s.0;).
  • partial_move_field_call.rs — Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122's partial-move-into-call (owned (&mut i64,) field passed to a function).
  • Each false-assertion variant now reports Unsat (rejected) where Track drop points by MIR Place #154 alone wrongly accepted it; the true-assertion companions still verify, confirming the drop is not over-suppressed.
• Full UI suite: 270 passed, 0 failed (pcsat solver via Docker, z3 4.15.4), plus doc-tests.
• cargo fmt --all -- --check, cargo clippy -- -D warnings, and git diff --check are clean.

🤖 Generated with Claude Code

---

Generated by Claude Code