Skip to content

Commit 115a8e0

Browse files
claudecoord-e
authored andcommitted
Do not drop moved-out owned locals at the move site
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 drop-point analysis treats a local's last use as its drop site. For a value moved into an aggregate (e.g. a closure moved into a tuple), this dropped the moved-out temporary at the move site, prematurely resolving the captured reference's prophecy (final == current) to its construction value. The later call mutating through the closure then contradicted that, making the environment inconsistent and any following assertion vacuously "safe". Owned (non-reference) locals whose ownership is transferred away by a move are now excluded from the drop set: their drop obligation belongs to the destination. Moved references are left untouched since ReborrowVisitor/ RustCallVisitor turn them into reborrows, so the source remains live. https://claude.ai/code/session_01HHar2z2xTNwffns5SF7wRe cargo fmt https://claude.ai/code/session_01HHar2z2xTNwffns5SF7wRe Pair closure_field_mut with a passing counterpart Add tests/ui/pass/closure_field_mut.rs asserting the true post-condition (call_count == 1) and switch the fail case to the mutation-dependent assert!(call_count == 0), so the pair directly demonstrates that the field closure's mutation is tracked rather than only that the spurious contradiction is gone. https://claude.ai/code/session_01HHar2z2xTNwffns5SF7wRe
1 parent 29ec090 commit 115a8e0

3 files changed

Lines changed: 89 additions & 0 deletions

File tree

src/analyze/basic_block/drop_point.rs

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,47 @@ pub struct DropPointsBuilder<'mir, 'tcx> {
5757
bb_ins_cache: HashMap<BasicBlock, DenseBitSet<Local>>,
5858
}
5959

60+
/// Locals whose ownership is fully transferred away by the statement (or
61+
/// terminator) at `statement_index`. Such a local is left uninitialized, so its
62+
/// drop obligation (including resolving any mutable-borrow prophecies it owns)
63+
/// moves to the destination and it must not be dropped at the move site.
64+
///
65+
/// Only owned (non-reference) operands are reported: `move`d references are
66+
/// turned into reborrows by `ReborrowVisitor`/`RustCallVisitor`, so the source
67+
/// local remains live and must still be dropped.
68+
fn moved_locals<'tcx>(
69+
body: &Body<'tcx>,
70+
bb: BasicBlock,
71+
statement_index: usize,
72+
) -> DenseBitSet<Local> {
73+
struct Visitor<'a, 'tcx> {
74+
body: &'a Body<'tcx>,
75+
locals: DenseBitSet<Local>,
76+
}
77+
impl<'tcx> mir::visit::Visitor<'tcx> for Visitor<'_, 'tcx> {
78+
fn visit_operand(&mut self, operand: &mir::Operand<'tcx>, _location: mir::Location) {
79+
if let mir::Operand::Move(place) = operand {
80+
if place.projection.is_empty() && !self.body.local_decls[place.local].ty.is_ref() {
81+
self.locals.insert(place.local);
82+
}
83+
}
84+
}
85+
}
86+
let mut visitor = Visitor {
87+
body,
88+
locals: DenseBitSet::new_empty(body.local_decls.len()),
89+
};
90+
let loc = mir::Location::START;
91+
let data = &body.basic_blocks[bb];
92+
use mir::visit::Visitor as _;
93+
if statement_index < data.statements.len() {
94+
visitor.visit_statement(&data.statements[statement_index], loc);
95+
} else if let Some(tmnt) = &data.terminator {
96+
visitor.visit_terminator(tmnt, loc);
97+
}
98+
visitor.locals
99+
}
100+
60101
fn def_local<'tcx>(data: &mir::BasicBlockData<'tcx>, statement_index: usize) -> Option<Local> {
61102
struct Visitor {
62103
local: Option<Local>,
@@ -135,6 +176,7 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
135176
t.insert(def);
136177
}
137178
t.subtract(&last_live_locals);
179+
t.subtract(&moved_locals(self.body, bb, statement_index));
138180
t
139181
};
140182
last_live_locals = live_locals;

tests/ui/fail/closure_field_mut.rs

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
//@error-in-other-file: Unsat
2+
//@compile-flags: -C debug-assertions=off
3+
4+
// Fail counterpart of tests/ui/pass/closure_field_mut.rs.
5+
// Regression test for https://github.com/coord-e/thrust/issues/41.
6+
//
7+
// A closure capturing `&mut` stored in a tuple field used to make thrust derive
8+
// a contradictory environment: the moved-out closure temporary was dropped at
9+
// its move site, prematurely resolving the captured reference's prophecy to its
10+
// construction value, which then contradicted the mutation performed by the
11+
// call. That contradiction unsoundly proved any following assertion (including
12+
// the issue's original `assert!(false)`) unreachable.
13+
//
14+
// The closure sets `call_count` to 1, so the assertion below must be rejected.
15+
16+
fn main() {
17+
let mut call_count = 0;
18+
let mut s = (
19+
|| {
20+
call_count = 1;
21+
},
22+
0,
23+
);
24+
(s.0)();
25+
assert!(call_count == 0);
26+
}

tests/ui/pass/closure_field_mut.rs

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
//@check-pass
2+
//@compile-flags: -C debug-assertions=off
3+
4+
// Pass counterpart of tests/ui/fail/closure_field_mut.rs.
5+
// Regression test for https://github.com/coord-e/thrust/issues/41.
6+
//
7+
// A closure capturing `&mut` stored in a tuple field mutates the captured
8+
// variable when called through the field. thrust must track that mutation, so
9+
// the (true) post-condition below verifies.
10+
11+
fn main() {
12+
let mut call_count = 0;
13+
let mut s = (
14+
|| {
15+
call_count = 1;
16+
},
17+
0,
18+
);
19+
(s.0)();
20+
assert!(call_count == 1);
21+
}

0 commit comments

Comments
 (0)