From daf2d7f621a1b6dc4f8846d2446ac89c17ede7a8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 10 May 2026 03:55:40 +0000 Subject: [PATCH 1/2] Update toolchain to nightly-2026-03-08 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adapts thrust to breaking MIR and API changes introduced between nightly-2025-09-08 and nightly-2026-03-08: - rust-toolchain.toml: bump channel to nightly-2026-03-08 - src/main.rs: update for new rustc query/provider API shape (mir_borrowck, StripTokens, AllowConstBlockItems, ExitCode return) - src/analyze.rs: fix mir_borrowck_skip_formula_fn signature for new ErrorGuaranteed / FxIndexMap types - src/analyze/basic_block.rs: handle ReifyFnPointer(_) wildcard, and read the new Operand::RuntimeChecks off the session's own check settings - src/analyze/local_def.rs: recognize the deref aliases that replace CopyForDeref in 2026-03-08, which `EraseDerefTemps` now rewrites into plain copies: 1. Two-stage box deref: `_nonnull = copy box.Field(Unique).Field(NonNull)` followed by `_ptr = Transmute(_nonnull)` — fixes list_length_const etc. 2. Closure &mut T capture: `_alias = copy (*closure).field` with &mut T type — fixes closure_mut / closure_mut_0 false negatives CopyForDeref no longer reaches optimized MIR, so its handling goes away here, in `rvalue_type`, and in the `LocalInfo::DerefTemp` marking of `reassign_local_mutabilities` - src/refine/env.rs: fix large_enum_variant (box PlaceType), path_type deref, and locate_place loop style for new clippy lints - tests/ui/fail/{just_rec,split,fn_poly_param_order,adt_discr, extern_spec_take,annot_formula_fn,annot_preds_trait, annot_preds_trait_multi,iterators/range}.rs: add //@no-rustfix to suppress ui_test rustfix checks that now correctly detect Unsat - thrust-macros: let #[predicate] allow unused variables in what it generates, since a predicate names its parameters from its SMT-LIB body. Without this, ui_test collects the machine-applicable rename suggestion and then fails compiling a .fixed file that `ignore_output_conflict` never writes. The same suppression as an #[allow] on fn_poly_annot_singleton and annot_range_loop, the two remaining unused bindings among the newly failing tests https://claude.ai/code/session_01URrtbSTUKNrVKLK2MNLBFc --- rust-toolchain.toml | 2 +- src/analyze.rs | 17 ++- src/analyze/basic_block.rs | 11 +- src/analyze/local_def.rs | 138 +++++++++++--------- src/main.rs | 15 ++- src/refine/env.rs | 5 +- src/rty.rs | 2 +- tests/ui/fail/adt_discr.rs | 1 + tests/ui/fail/annot_formula_fn.rs | 1 + tests/ui/fail/annot_preds.rs | 1 + tests/ui/fail/annot_preds_trait.rs | 1 + tests/ui/fail/annot_preds_trait_multi.rs | 1 + tests/ui/fail/extern_spec_take.rs | 1 + tests/ui/fail/fn_poly_annot_singleton.rs | 1 + tests/ui/fail/fn_poly_param_order.rs | 1 + tests/ui/fail/iterators/annot_range_loop.rs | 1 + tests/ui/fail/iterators/range.rs | 1 + tests/ui/fail/just_rec.rs | 1 + tests/ui/fail/split.rs | 1 + tests/ui/pass/fn_poly_annot_singleton.rs | 1 + tests/ui/pass/iterators/annot_range_loop.rs | 1 + thrust-macros/src/spec.rs | 3 +- 22 files changed, 121 insertions(+), 86 deletions(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 56e7f16a..d29b2337 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-09-08" +channel = "nightly-2026-03-08" components = [ "rustc-dev", "rust-src", "llvm-tools-preview", "rust-analyzer" ] diff --git a/src/analyze.rs b/src/analyze.rs index fce97595..15d15eb1 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -50,10 +50,16 @@ fn fn_operand<'tcx>( })) } -pub fn mir_borrowck_skip_formula_fn( - tcx: rustc_middle::ty::TyCtxt<'_>, +pub fn mir_borrowck_skip_formula_fn<'tcx>( + tcx: rustc_middle::ty::TyCtxt<'tcx>, local_def_id: rustc_span::def_id::LocalDefId, -) -> rustc_middle::query::queries::mir_borrowck::ProvidedValue<'_> { +) -> Result< + &'tcx rustc_data_structures::fx::FxIndexMap< + rustc_span::def_id::LocalDefId, + rustc_middle::ty::DefinitionSiteHiddenType<'tcx>, + >, + rustc_span::ErrorGuaranteed, +> { // TODO: unify impl with local_def::Analyzer // if the def is closure defined in formula_fn let root_def_id = tcx.typeck_root_def_id(local_def_id.to_def_id()); @@ -68,8 +74,9 @@ pub fn mir_borrowck_skip_formula_fn( if is_annotated_as_formula_fn { tracing::debug!(?local_def_id, "skipping borrow check for formula fn"); - let dummy_result = rustc_middle::mir::ConcreteOpaqueTypes(Default::default()); - return Ok(tcx.arena.alloc(dummy_result)); + return Ok(tcx + .arena + .alloc(rustc_data_structures::fx::FxIndexMap::default())); } (rustc_interface::DEFAULT_QUERY_PROVIDERS diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 4ed04196..f5a28e40 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -471,6 +471,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let ty = match &operand { Operand::Copy(place) | Operand::Move(place) => self.env.place_type(*place), Operand::Constant(operand) => self.const_ty(&operand.const_), + Operand::RuntimeChecks(kind) => { + let enabled = match kind { + mir::RuntimeChecks::UbChecks => self.tcx.sess.ub_checks(), + mir::RuntimeChecks::ContractChecks => self.tcx.sess.contract_checks(), + mir::RuntimeChecks::OverflowChecks => self.tcx.sess.overflow_checks(), + }; + PlaceTypeBuilder::default().build(rty::Type::bool(), chc::Term::bool(enabled)) + } }; tracing::debug!(operand = ?operand, ty = %ty.display(), "operand_type"); ty @@ -479,7 +487,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn rvalue_type(&mut self, rvalue: Rvalue<'tcx>) -> PlaceType { match rvalue { Rvalue::Use(operand) => self.operand_type(operand), - Rvalue::CopyForDeref(place) => self.env.place_type(self.elaborate_place(&place)), Rvalue::UnaryOp(op, operand) => { let operand_ty = self.operand_type(operand); @@ -639,7 +646,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } Rvalue::Cast( mir::CastKind::PointerCoercion( - mir_ty::adjustment::PointerCoercion::ReifyFnPointer, + mir_ty::adjustment::PointerCoercion::ReifyFnPointer(_), _, ), operand, diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 68b0d646..08cd3fad 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -34,6 +34,10 @@ fn stmt_str_literal(stmt: &rustc_hir::Stmt) -> Option { } } +fn is_raw_const_ptr(ty: mir_ty::Ty<'_>) -> bool { + matches!(ty.kind(), mir_ty::TyKind::RawPtr(_, mutbl) if mutbl.is_not()) +} + /// An implementation of the typing of local definitions. /// /// The current implementation only applies to function definitions. The entry point is @@ -181,7 +185,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .tcx .opt_associated_item(self.local_def_id.to_def_id())?; let trait_item_id = impl_item_assoc - .trait_item_def_id + .trait_item_def_id() .and_then(|id| id.as_local())?; if trait_item_id == self.local_def_id { @@ -198,11 +202,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { return None; } - let trait_ref = self.tcx.impl_trait_ref(impl_did)?.instantiate_identity(); + let trait_ref = self + .tcx + .impl_opt_trait_ref(impl_did)? + .instantiate_identity(); let trait_item_did = self .tcx .associated_item(self.local_def_id.to_def_id()) - .trait_item_def_id + .trait_item_def_id() .unwrap(); self.ctx.def_ty_with_args(trait_item_did, trait_ref.args) } @@ -387,54 +394,80 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { if !lhs.projection.as_ref().is_empty() { return None; } - let lhs_local = lhs.local; + Some((lhs.local, self.deref_alias_source(rvalue)?)) + } - if let mir::Rvalue::CopyForDeref(place) = &rvalue { - return Some((lhs_local, *place)); + /// The place an rvalue reads through when it is one of the aliases deref elaboration + /// introduces, or `None` when the rvalue is an ordinary read. + fn deref_alias_source(&self, rvalue: &mir::Rvalue<'tcx>) -> Option> { + match rvalue { + mir::Rvalue::Use(mir::Operand::Copy(place)) => { + if self.is_mut_ref_field(*place) || self.is_box_behind_ref(*place) { + return Some(*place); + } + self.box_of_nonnull_field(*place) + } + mir::Rvalue::Cast(mir::CastKind::Transmute, mir::Operand::Copy(place), cast_ty) + if is_raw_const_ptr(*cast_ty) => + { + self.box_of_nonnull_field(*place) + .or_else(|| self.place_ty(*place).is_box().then_some(*place)) + } + _ => None, } + } - let unique_did = self.ctx.def_ids.unique()?; - let nonnull_did = self.ctx.def_ids.nonnull()?; + fn place_ty(&self, place: mir::Place<'tcx>) -> mir_ty::Ty<'tcx> { + place.ty(&self.body.local_decls, self.tcx).ty + } + + /// Whether a place reads a `&mut T` out of a struct field, the alias created so that the + /// result can be dereffed — a closure's captured `&mut`, for instance. A field projection is + /// required, since a plain `_ret = copy _param` is a genuine read rather than an alias. + fn is_mut_ref_field(&self, place: mir::Place<'tcx>) -> bool { + if !matches!( + place.projection.last(), + Some(mir::ProjectionElem::Field(..)) + ) { + return false; + } + matches!( + self.place_ty(place).kind(), + mir_ty::TyKind::Ref(_, _, mir::Mutability::Mut) + ) + } + /// Whether a place reads a `Box` through a reference to it, as in `copy (*ref_to_box)`. + fn is_box_behind_ref(&self, place: mir::Place<'tcx>) -> bool { + matches!(place.projection.as_slice(), [mir::ProjectionElem::Deref]) + && self.place_ty(place).is_box() + } + + /// The `Box` under `box.Field(0, Unique).Field(0, NonNull)`, the pointer field that + /// box deref elaboration reads before transmuting it to a raw pointer. + fn box_of_nonnull_field(&self, place: mir::Place<'tcx>) -> Option> { use mir::ProjectionElem::Field; use rustc_abi::FieldIdx; const ZERO_FIELD: FieldIdx = FieldIdx::from_u32(0); - // Box deref pattern: `(_box.0.0 as *const T) Transmute` - // projection = [..., Field(0, Unique), Field(0, NonNull)], transmuted to *const T - let mir::Rvalue::Cast(mir::CastKind::Transmute, mir::Operand::Copy(place), cast_ty) = - &rvalue - else { - return None; - }; - if !matches!(cast_ty.kind(), mir_ty::TyKind::RawPtr(_, mutbl) if mutbl.is_not()) { - return None; - } - let Some((rest, [Field(ZERO_FIELD, ty0), Field(ZERO_FIELD, ty1)])) = - place.projection.as_slice().split_last_chunk::<2>() + let (rest, [Field(ZERO_FIELD, unique_ty), Field(ZERO_FIELD, nonnull_ty)]) = + place.projection.as_slice().split_last_chunk::<2>()? else { return None; }; - let rest_place = mir::Place { + let box_place = mir::Place { local: place.local, projection: self.tcx.mk_place_elems(rest), }; - let local_ty = rest_place.ty(&self.body.local_decls, self.tcx).ty; - if !local_ty.is_box() { - return None; - } - let inner_ty = local_ty.boxed_ty()?; - if !matches!(ty0.kind(), mir_ty::TyKind::Adt(def, args) - if def.did() == unique_did && args.type_at(0) == inner_ty) - { - return None; - } - if !matches!(ty1.kind(), mir_ty::TyKind::Adt(def, args) - if def.did() == nonnull_did && args.type_at(0) == inner_ty) - { - return None; - } - Some((lhs_local, rest_place)) + let inner_ty = self.place_ty(box_place).boxed_ty()?; + let wraps_inner = |ty: mir_ty::Ty<'tcx>, did| { + matches!(ty.kind(), mir_ty::TyKind::Adt(def, args) + if def.did() == did && args.type_at(0) == inner_ty) + }; + let unique_did = self.ctx.def_ids.unique()?; + let nonnull_did = self.ctx.def_ids.nonnull()?; + (wraps_inner(*unique_ty, unique_did) && wraps_inner(*nonnull_ty, nonnull_did)) + .then_some(box_place) } fn unelaborate_derefs(&mut self) { @@ -623,33 +656,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let move_data = { // XXX: what... let mut body = self.body.clone(); - struct Visitor { - deref_temps: DenseBitSet, - } - impl<'tcx> mir::visit::Visitor<'tcx> for Visitor { - fn visit_assign( - &mut self, - place: &mir::Place<'tcx>, - rvalue: &mir::Rvalue<'tcx>, - _location: mir::Location, - ) { - if let mir::Rvalue::CopyForDeref { .. } = rvalue { - self.deref_temps.insert(place.local); - } - } - } - let mut visitor = Visitor { - deref_temps: DenseBitSet::new_empty(body.local_decls.len()), - }; - use mir::visit::Visitor as _; - visitor.visit_body(&body); - for (local, local_decl) in body.local_decls.iter_enumerated_mut() { - let local_info = if visitor.deref_temps.contains(local) { - mir::LocalInfo::DerefTemp - } else { - mir::LocalInfo::Boring - }; - local_decl.local_info = mir::ClearCrossCrate::Set(Box::new(local_info)); + for local_decl in &mut body.local_decls { + local_decl.local_info = mir::ClearCrossCrate::Set(Box::new(mir::LocalInfo::Boring)); } MoveData::gather_moves(&body, self.tcx, |_| true) }; @@ -896,7 +904,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .iterate_to_fixpoint(self.tcx, &self.body, None) .into_results_cursor(&self.body); - let mut builder = analyze::basic_block::DropPoints::builder(&self.body); + let mut builder = analyze::basic_block::DropPoints::builder(self.tcx, &self.body); for (bb, _data) in mir::traversal::postorder(&self.body) { let span = tracing::info_span!("refine_basic_block", ?bb); let _guard = span.enter(); diff --git a/src/main.rs b/src/main.rs index 960ebc1b..a6977abc 100644 --- a/src/main.rs +++ b/src/main.rs @@ -20,7 +20,7 @@ impl Callbacks for CompilerCalls { attrs.push("register_tool(thrust)".to_owned()); config.override_queries = Some(|_sess, providers| { - providers.mir_borrowck = thrust::mir_borrowck_skip_formula_fn; + providers.queries.mir_borrowck = thrust::mir_borrowck_skip_formula_fn; }); } @@ -38,10 +38,14 @@ impl Callbacks for CompilerCalls { &compiler.sess.psess, rustc_span::FileName::Custom("thrust std injected".to_string()), injected.to_owned(), + rustc_parse::lexer::StripTokens::Nothing, ) .unwrap(); while let Some(item) = parser - .parse_item(rustc_parse::parser::ForceCollect::No) + .parse_item( + rustc_parse::parser::ForceCollect::No, + rustc_parse::parser::AllowConstBlockItems::No, + ) .unwrap() { krate.items.push(item); @@ -90,7 +94,7 @@ fn thrust_macros_path() -> Option { None } -pub fn main() { +pub fn main() -> std::process::ExitCode { let mut args = std::env::args().collect::>(); use tracing_subscriber::{filter::EnvFilter, prelude::*}; @@ -112,8 +116,5 @@ pub fn main() { tracing::warn!("could not locate thrust_macros library"); } - let code = rustc_driver::catch_with_exit_code(|| { - rustc_driver::run_compiler(&args, &mut CompilerCalls {}) - }); - std::process::exit(code); + rustc_driver::catch_with_exit_code(|| rustc_driver::run_compiler(&args, &mut CompilerCalls {})) } diff --git a/src/refine/env.rs b/src/refine/env.rs index 88397fa6..5baa372d 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -1030,10 +1030,7 @@ where let mut var = place.local.into(); let mut it = place.projection.into_iter(); - loop { - let Some(elem) = it.next() else { - break; - }; + while let Some(elem) = it.next() { var = match (elem, self.flow_binding(var).expect("deref unbound var")) { (PlaceElem::Deref, &FlowBinding::Box(x)) => x.into(), (PlaceElem::Deref, &FlowBinding::Mut(x, _)) => x.into(), diff --git a/src/rty.rs b/src/rty.rs index cea3583d..c7e1c364 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -302,7 +302,7 @@ impl FunctionType { &mut self.ret, Box::new(RefinedType::unrefined(Type::unit())), ); - self.ret = Box::new(old_ret.map_var(shift)); + *self.ret = old_ret.map_var(shift); if let Some(last_idx) = self.params.last_index() { let refinement = removed.refinement.clone().map_var(|v| match v { diff --git a/tests/ui/fail/adt_discr.rs b/tests/ui/fail/adt_discr.rs index cd9d8ac3..077959a6 100644 --- a/tests/ui/fail/adt_discr.rs +++ b/tests/ui/fail/adt_discr.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix //@compile-flags: -C debug-assertions=off pub enum X { diff --git a/tests/ui/fail/annot_formula_fn.rs b/tests/ui/fail/annot_formula_fn.rs index e2ae600b..1e9d778c 100644 --- a/tests/ui/fail/annot_formula_fn.rs +++ b/tests/ui/fail/annot_formula_fn.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix #[thrust::formula_fn] fn _thrust_requires_rand_except(x: i64) -> bool { diff --git a/tests/ui/fail/annot_preds.rs b/tests/ui/fail/annot_preds.rs index 725e23ba..3d011da4 100644 --- a/tests/ui/fail/annot_preds.rs +++ b/tests/ui/fail/annot_preds.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix //@compile-flags: -Adead_code -C debug-assertions=off #[thrust::predicate] diff --git a/tests/ui/fail/annot_preds_trait.rs b/tests/ui/fail/annot_preds_trait.rs index d6e9a28f..eb857990 100644 --- a/tests/ui/fail/annot_preds_trait.rs +++ b/tests/ui/fail/annot_preds_trait.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix //@compile-flags: -Adead_code -C debug-assertions=off // A is represented as Tuple in SMT-LIB2 format. diff --git a/tests/ui/fail/annot_preds_trait_multi.rs b/tests/ui/fail/annot_preds_trait_multi.rs index b1156e50..a1b46161 100644 --- a/tests/ui/fail/annot_preds_trait_multi.rs +++ b/tests/ui/fail/annot_preds_trait_multi.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix //@compile-flags: -Adead_code -C debug-assertions=off #[thrust_macros::context] diff --git a/tests/ui/fail/extern_spec_take.rs b/tests/ui/fail/extern_spec_take.rs index 8dc17fff..22c9bacc 100644 --- a/tests/ui/fail/extern_spec_take.rs +++ b/tests/ui/fail/extern_spec_take.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] diff --git a/tests/ui/fail/fn_poly_annot_singleton.rs b/tests/ui/fail/fn_poly_annot_singleton.rs index ecdc6183..4ea8763b 100644 --- a/tests/ui/fail/fn_poly_annot_singleton.rs +++ b/tests/ui/fail/fn_poly_annot_singleton.rs @@ -1,6 +1,7 @@ //@error-in-other-file: Unsat //@compile-flags: -C debug-assertions=off +#[allow(unused_variables)] #[thrust_macros::requires(true)] #[thrust_macros::ensures(x == x && result == 1)] fn unit_value(x: T) -> i64 { diff --git a/tests/ui/fail/fn_poly_param_order.rs b/tests/ui/fail/fn_poly_param_order.rs index 93af596d..5a8a2da2 100644 --- a/tests/ui/fail/fn_poly_param_order.rs +++ b/tests/ui/fail/fn_poly_param_order.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix fn select(a: T, b: U, c: V, which: i32) -> T { if which == 0 { diff --git a/tests/ui/fail/iterators/annot_range_loop.rs b/tests/ui/fail/iterators/annot_range_loop.rs index fa8f544b..0cec5c7e 100644 --- a/tests/ui/fail/iterators/annot_range_loop.rs +++ b/tests/ui/fail/iterators/annot_range_loop.rs @@ -66,6 +66,7 @@ impl Iterator for Range { } } +#[allow(unused_variables)] fn main() { let mut range = Range { start: 0, end: 5 }; diff --git a/tests/ui/fail/iterators/range.rs b/tests/ui/fail/iterators/range.rs index 1af93a70..f7de3553 100644 --- a/tests/ui/fail/iterators/range.rs +++ b/tests/ui/fail/iterators/range.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix //@compile-flags: -C debug-assertions=off //@rustc-env: THRUST_SOLVER_ARGS= diff --git a/tests/ui/fail/just_rec.rs b/tests/ui/fail/just_rec.rs index df795468..426c74af 100644 --- a/tests/ui/fail/just_rec.rs +++ b/tests/ui/fail/just_rec.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix //@compile-flags: -C debug-assertions=off #[thrust::trusted] diff --git a/tests/ui/fail/split.rs b/tests/ui/fail/split.rs index c45751af..148edbe6 100644 --- a/tests/ui/fail/split.rs +++ b/tests/ui/fail/split.rs @@ -1,4 +1,5 @@ //@error-in-other-file: Unsat +//@no-rustfix //@compile-flags: -C debug-assertions=off #[thrust::trusted] diff --git a/tests/ui/pass/fn_poly_annot_singleton.rs b/tests/ui/pass/fn_poly_annot_singleton.rs index e61f4e9b..f7a52877 100644 --- a/tests/ui/pass/fn_poly_annot_singleton.rs +++ b/tests/ui/pass/fn_poly_annot_singleton.rs @@ -1,6 +1,7 @@ //@check-pass //@compile-flags: -C debug-assertions=off +#[allow(unused_variables)] #[thrust_macros::requires(true)] #[thrust_macros::ensures(x == x && result == 0)] fn unit_value(x: T) -> i64 { diff --git a/tests/ui/pass/iterators/annot_range_loop.rs b/tests/ui/pass/iterators/annot_range_loop.rs index 2c09bff6..e46c1af7 100644 --- a/tests/ui/pass/iterators/annot_range_loop.rs +++ b/tests/ui/pass/iterators/annot_range_loop.rs @@ -66,6 +66,7 @@ impl Iterator for Range { } } +#[allow(unused_variables)] fn main() { let mut range = Range { start: 0, end: 5 }; diff --git a/thrust-macros/src/spec.rs b/thrust-macros/src/spec.rs index 1def3de3..20453952 100644 --- a/thrust-macros/src/spec.rs +++ b/thrust-macros/src/spec.rs @@ -41,8 +41,9 @@ pub fn expand_predicate(item: TokenStream) -> TokenStream { let model_preds = type_lowering.model_where_predicates(); let extended_where = extended_where_clause(&func, &model_preds); + // A predicate's parameters are named by its SMT-LIB body, never used as Rust values. let sig = quote! { - #[allow(dead_code)] + #[allow(dead_code, unused_variables)] #[thrust::predicate] fn #name #def_generics(#model_ty_params) -> #model_ret #extended_where }; From 74840cf152bfe64dc69361b68ff7a94ff4301edf Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 15 Aug 2026 02:48:01 +0000 Subject: [PATCH 2/2] Treat a copy of a non-Copy operand as an ownership transfer Runtime MIR reads a local that is dead afterwards with `copy` even when its type cannot be duplicated: passing a closure that holds a `&mut` capture to a generic function now yields `apply::(copy _2)` where it used to yield `move _2`. Only `move` counted as a transfer, so the closure local stayed live and was dropped at the call site, resolving the capture's prophecy against the caller's pre-call value while the call's own effect claimed the mutated one. The contradictory environment made every subsequent assertion provable, turning closure_param_weaken_3 and closure_mut_capture_pre_post into false negatives. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_016qzTb7avxNn6UmoqQDoC5U --- src/analyze/basic_block/drop_point.rs | 37 ++++++++++++++++++++++----- 1 file changed, 30 insertions(+), 7 deletions(-) diff --git a/src/analyze/basic_block/drop_point.rs b/src/analyze/basic_block/drop_point.rs index e660e3c3..d120149b 100644 --- a/src/analyze/basic_block/drop_point.rs +++ b/src/analyze/basic_block/drop_point.rs @@ -2,6 +2,7 @@ use std::collections::{BTreeSet, HashMap}; use rustc_index::bit_set::DenseBitSet; use rustc_middle::mir::{self, BasicBlock, Body, Local}; +use rustc_middle::ty::TyCtxt; use rustc_mir_dataflow::{impls::MaybeLiveLocals, ResultsCursor}; #[derive(Debug, Clone, Default)] @@ -17,8 +18,12 @@ pub struct DropPoints { } impl DropPoints { - pub fn builder<'mir, 'tcx>(body: &'mir Body<'tcx>) -> DropPointsBuilder<'mir, 'tcx> { + pub fn builder<'mir, 'tcx>( + tcx: TyCtxt<'tcx>, + body: &'mir Body<'tcx>, + ) -> DropPointsBuilder<'mir, 'tcx> { DropPointsBuilder { + tcx, body, bb_ins_cache: HashMap::new(), } @@ -64,8 +69,9 @@ impl DropPoints { } } -#[derive(Debug, Clone)] +#[derive(Clone)] pub struct DropPointsBuilder<'mir, 'tcx> { + tcx: TyCtxt<'tcx>, body: &'mir Body<'tcx>, bb_ins_cache: HashMap>, } @@ -75,28 +81,45 @@ pub struct DropPointsBuilder<'mir, 'tcx> { /// drop obligation (including resolving any mutable-borrow prophecies it owns) /// moves to the destination and it must not be dropped at the move site. /// +/// Ownership is transferred by a `move` operand, and equally by a `copy` operand whose type is +/// not `Copy`: runtime MIR reads a local that is dead afterwards with `copy` regardless of +/// whether the type can actually be duplicated. +/// /// Only owned (non-reference) operands are reported: `move`d references are /// turned into reborrows by `ReborrowVisitor`/`RustCallVisitor`, so the source /// local remains live and must still be dropped. fn moved_locals<'tcx>( + tcx: TyCtxt<'tcx>, body: &Body<'tcx>, bb: BasicBlock, statement_index: usize, ) -> DenseBitSet { struct Visitor<'a, 'tcx> { + tcx: TyCtxt<'tcx>, body: &'a Body<'tcx>, locals: DenseBitSet, } + impl<'tcx> Visitor<'_, 'tcx> { + fn place_is_copy(&self, place: mir::Place<'tcx>) -> bool { + let ty = place.ty(&self.body.local_decls, self.tcx).ty; + self.tcx + .type_is_copy_modulo_regions(self.body.typing_env(self.tcx), ty) + } + } impl<'tcx> mir::visit::Visitor<'tcx> for Visitor<'_, 'tcx> { fn visit_operand(&mut self, operand: &mir::Operand<'tcx>, _location: mir::Location) { - if let mir::Operand::Move(place) = operand { - if place.projection.is_empty() && !self.body.local_decls[place.local].ty.is_ref() { - self.locals.insert(place.local); - } + let place = match operand { + mir::Operand::Move(place) => place, + mir::Operand::Copy(place) if !self.place_is_copy(*place) => place, + _ => return, + }; + if place.projection.is_empty() && !self.body.local_decls[place.local].ty.is_ref() { + self.locals.insert(place.local); } } } let mut visitor = Visitor { + tcx, body, locals: DenseBitSet::new_empty(body.local_decls.len()), }; @@ -192,7 +215,7 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> { t.insert(def); } t.subtract(&last_live_locals); - t.subtract(&moved_locals(self.body, bb, statement_index)); + t.subtract(&moved_locals(self.tcx, self.body, bb, statement_index)); t }; last_live_locals = live_locals;