From af427bdb117240793c97795d4d789665986b64c4 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 12 Oct 2026 21:37:42 +0000 Subject: [PATCH 1/2] Equate a parameter with its argument only when the body never assigns it `bind_locals` assumes that a non-flow parameter local still holds the function's argument and equates the two at every block with its own precondition. A parameter that is moved out and then re-initialized stays non-flow, because `reassign_local_mutabilities` marks a local mutable only when it is assigned while initialized, yet it holds a different value from then on. The equation then contradicts the incoming state at the next join point, so the function's postcondition becomes vacuous and callers verify panicking programs as safe. Skip the equation when the parameter local is the destination of any assignment in the body. Fixes #334 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01LhtkSy2XUScvjq9LXzmTQS --- src/analyze/basic_block.rs | 36 +++++++++++++++++++-- tests/ui/fail/fn_param_reinit_after_move.rs | 25 ++++++++++++++ tests/ui/pass/fn_param_reinit_after_move.rs | 25 ++++++++++++++ 3 files changed, 84 insertions(+), 2 deletions(-) create mode 100644 tests/ui/fail/fn_param_reinit_after_move.rs create mode 100644 tests/ui/pass/fn_param_reinit_after_move.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 97cc7f89..28532788 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -51,6 +51,33 @@ pub fn needs_own_precondition(body: &Body<'_>, bb: BasicBlock) -> bool { pred_term.successors().filter(|s| *s == bb).count() > 1 } +/// Whether `local` is the destination of an assignment anywhere in `body`. +fn is_assigned<'tcx>(body: &Body<'tcx>, local: Local) -> bool { + struct Visitor { + local: Local, + assigned: bool, + } + impl<'tcx> mir::visit::Visitor<'tcx> for Visitor { + fn visit_local( + &mut self, + local: Local, + ctxt: mir::visit::PlaceContext, + _location: mir::Location, + ) { + if local == self.local && ctxt.is_place_assignment() { + self.assigned = true; + } + } + } + let mut visitor = Visitor { + local, + assigned: false, + }; + use mir::visit::Visitor as _; + visitor.visit_body(body); + visitor.assigned +} + /// Whether every value of the integer type `inner` is also a value of the integer type `outer`. fn int_ty_includes<'tcx>( tcx: TyCtxt<'tcx>, @@ -1678,9 +1705,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // it no longer carries the relationship between a function's entry argument // (`OuterFnParam`) and its current local. The invariant cannot express both // views of the same argument with the current syntax. As an ad-hoc workaround, - // equate them when the local is non-flow, since its representation cannot change. + // equate them when the local is non-flow and never assigned, since it then + // still holds the argument. A non-flow local can be assigned again after being + // moved out. let local = analyze::local_of_function_param(outer_idx); - if !param_ty.to_sort().is_singleton() && self.env.is_non_flow_local(local) { + if !param_ty.to_sort().is_singleton() + && self.env.is_non_flow_local(local) + && !is_assigned(&self.body, local) + { assumption.body.push_conj( chc::Term::var(PlaceTypeVar::Var(var)) .equal_to(self.env.local_type(local).term), diff --git a/tests/ui/fail/fn_param_reinit_after_move.rs b/tests/ui/fail/fn_param_reinit_after_move.rs new file mode 100644 index 00000000..01c8d2b6 --- /dev/null +++ b/tests/ui/fail/fn_param_reinit_after_move.rs @@ -0,0 +1,25 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +struct S { + a: i64, +} + +impl thrust_models::Model for S { + type Ty = Self; +} + +fn id(x: i64) -> i64 { + x +} + +fn f(mut s: S) -> i64 { + let t = s; + s = S { a: id(t.a + 1) }; + if id(0) == 0 {} + s.a +} + +fn main() { + assert!(f(S { a: 0 }) == 0); +} diff --git a/tests/ui/pass/fn_param_reinit_after_move.rs b/tests/ui/pass/fn_param_reinit_after_move.rs new file mode 100644 index 00000000..a6841583 --- /dev/null +++ b/tests/ui/pass/fn_param_reinit_after_move.rs @@ -0,0 +1,25 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +struct S { + a: i64, +} + +impl thrust_models::Model for S { + type Ty = Self; +} + +fn id(x: i64) -> i64 { + x +} + +fn f(mut s: S) -> i64 { + let t = s; + s = S { a: id(t.a + 1) }; + if id(0) == 0 {} + s.a +} + +fn main() { + assert!(f(S { a: 0 }) == 1); +} From b896c632b22fa17b76addce8676f91f5f8f862e8 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 02:16:10 +0000 Subject: [PATCH 2/2] Track parameter assignments per block instead of per body Skipping the entry-argument equation whenever the body assigns the parameter anywhere also dropped it at blocks that no assignment can reach, such as a loop header before the parameter is moved out and re-initialized, so a loop invariant relating the parameter to its argument could no longer be established. Compute, once per body, which parameters may have been assigned on entry to each block by forward reachability from their assignment sites, and skip the equation only there. This also avoids rescanning the whole body for every parameter of every block. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01LhtkSy2XUScvjq9LXzmTQS --- src/analyze/basic_block.rs | 54 +++++++++++++++------ src/analyze/local_def.rs | 2 + tests/ui/fail/fn_param_reinit_after_loop.rs | 37 ++++++++++++++ tests/ui/pass/fn_param_reinit_after_loop.rs | 37 ++++++++++++++ 4 files changed, 116 insertions(+), 14 deletions(-) create mode 100644 tests/ui/fail/fn_param_reinit_after_loop.rs create mode 100644 tests/ui/pass/fn_param_reinit_after_loop.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 28532788..b37b2cb9 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -3,6 +3,7 @@ use std::collections::HashMap; use num_bigint::BigInt; use rustc_hir::def::DefKind; +use rustc_index::bit_set::DenseBitSet; use rustc_index::IndexVec; use rustc_middle::mir::{ self, BasicBlock, Body, Local, Operand, Rvalue, StatementKind, TerminatorKind, @@ -51,31 +52,46 @@ pub fn needs_own_precondition(body: &Body<'_>, bb: BasicBlock) -> bool { pred_term.successors().filter(|s| *s == bb).count() > 1 } -/// Whether `local` is the destination of an assignment anywhere in `body`. -fn is_assigned<'tcx>(body: &Body<'tcx>, local: Local) -> bool { +/// For each block, the parameters that may have been assigned since the function's entry when +/// control reaches the block. +pub fn params_assigned_on_entry(body: &Body<'_>) -> IndexVec> { struct Visitor { - local: Local, - assigned: bool, + arg_count: usize, + sites: Vec<(Local, BasicBlock)>, } impl<'tcx> mir::visit::Visitor<'tcx> for Visitor { fn visit_local( &mut self, local: Local, ctxt: mir::visit::PlaceContext, - _location: mir::Location, + location: mir::Location, ) { - if local == self.local && ctxt.is_place_assignment() { - self.assigned = true; + let is_param = (1..=self.arg_count).contains(&local.index()); + if is_param && ctxt.is_place_assignment() { + self.sites.push((local, location.block)); } } } let mut visitor = Visitor { - local, - assigned: false, + arg_count: body.arg_count, + sites: Vec::new(), }; use mir::visit::Visitor as _; visitor.visit_body(body); - visitor.assigned + + let mut assigned = IndexVec::from_elem_n( + DenseBitSet::new_empty(body.local_decls.len()), + body.basic_blocks.len(), + ); + for (local, site) in visitor.sites { + let mut worklist: Vec<_> = body.basic_blocks[site].terminator().successors().collect(); + while let Some(bb) = worklist.pop() { + if assigned[bb].insert(local) { + worklist.extend(body.basic_blocks[bb].terminator().successors()); + } + } + } + assigned } /// Whether every value of the integer type `inner` is also a value of the integer type `outer`. @@ -217,6 +233,7 @@ pub struct Analyzer<'tcx, 'ctx> { local_def_id: LocalDefId, drop_points: DropPoints, + assigned_params: DenseBitSet, basic_block: BasicBlock, body: Cow<'tcx, Body<'tcx>>, @@ -1705,13 +1722,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // it no longer carries the relationship between a function's entry argument // (`OuterFnParam`) and its current local. The invariant cannot express both // views of the same argument with the current syntax. As an ad-hoc workaround, - // equate them when the local is non-flow and never assigned, since it then - // still holds the argument. A non-flow local can be assigned again after being - // moved out. + // equate them when the local is non-flow and not assigned on any path to this + // block, since it then still holds the argument. A non-flow local can be + // assigned again after being moved out. let local = analyze::local_of_function_param(outer_idx); if !param_ty.to_sort().is_singleton() && self.env.is_non_flow_local(local) - && !is_assigned(&self.body, local) + && !self.assigned_params.contains(local) { assumption.body.push_conj( chc::Term::var(PlaceTypeVar::Var(var)) @@ -1750,6 +1767,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let tcx = ctx.tcx; let drop_points = DropPoints::default(); let body = Cow::Borrowed(tcx.optimized_mir(local_def_id.to_def_id())); + let assigned_params = DenseBitSet::new_empty(body.local_decls.len()); let env = ctx.new_env(); let local_decls = body.local_decls.clone(); let prophecy_vars = Default::default(); @@ -1759,6 +1777,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { tcx, local_def_id, drop_points, + assigned_params, basic_block, body, type_builder, @@ -1773,6 +1792,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self } + /// Sets the parameters that may have been assigned since the function's entry when control + /// reaches this block. + pub fn assigned_params(&mut self, assigned_params: DenseBitSet) -> &mut Self { + self.assigned_params = assigned_params; + self + } + pub fn body(&mut self, body: Body<'tcx>) -> &mut Self { self.local_decls = body.local_decls.clone(); self.body = Cow::Owned(body); diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 6a9cdf1b..f8ee5c7b 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -990,6 +990,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn analyze_basic_blocks(&mut self, expected_fn_ty: &rty::RefinedType) { let expected_fn_ty = expected_fn_ty.ty.as_function().unwrap(); + let assigned_params = analyze::basic_block::params_assigned_on_entry(&self.body); // Reverse postorder guarantees each block that inherits its precondition // is visited after the predecessor that lazily materialized its type. for (bb, data) in mir::traversal::reverse_postorder(&self.body) { @@ -1005,6 +1006,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .basic_block_analyzer(self.local_def_id, bb) .body(self.body.clone()) .drop_points(drop_points) + .assigned_params(assigned_params[bb].clone()) .run(&rty, expected_fn_ty); } } diff --git a/tests/ui/fail/fn_param_reinit_after_loop.rs b/tests/ui/fail/fn_param_reinit_after_loop.rs new file mode 100644 index 00000000..6b0fe6a9 --- /dev/null +++ b/tests/ui/fail/fn_param_reinit_after_loop.rs @@ -0,0 +1,37 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +struct S { + x: i64, +} + +impl thrust_models::Model for S { + type Ty = Self; +} + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +#[thrust::trusted] +fn rand() -> bool { + unimplemented!() +} + +fn id(x: i64) -> i64 { + x +} + +#[thrust_macros::ensures(result == a.x + 1)] +#[thrust_macros::context] +fn keep_argument(mut a: S) -> i64 { + let mut v = a.x; + while rand() { + thrust_macros::invariant!(|a: S, v: i64| v == a.x); + v = a.x; + } + let t = a; + a = S { x: id(t.x) }; + let _ = a.x; + v +} + +fn main() {} diff --git a/tests/ui/pass/fn_param_reinit_after_loop.rs b/tests/ui/pass/fn_param_reinit_after_loop.rs new file mode 100644 index 00000000..7c811a49 --- /dev/null +++ b/tests/ui/pass/fn_param_reinit_after_loop.rs @@ -0,0 +1,37 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +struct S { + x: i64, +} + +impl thrust_models::Model for S { + type Ty = Self; +} + +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(true)] +#[thrust::trusted] +fn rand() -> bool { + unimplemented!() +} + +fn id(x: i64) -> i64 { + x +} + +#[thrust_macros::ensures(result == a.x)] +#[thrust_macros::context] +fn keep_argument(mut a: S) -> i64 { + let mut v = a.x; + while rand() { + thrust_macros::invariant!(|a: S, v: i64| v == a.x); + v = a.x; + } + let t = a; + a = S { x: id(t.x) }; + let _ = a.x; + v +} + +fn main() {}