Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1 +1,4 @@
target/
mir_dump/
*.mir
rust_out
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
@@ -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" ]
17 changes: 12 additions & 5 deletions src/analyze.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,10 +34,16 @@ mod local_def;
// TODO: organize structure and remove cross dependency between refine
pub use did_cache::DefIdCache;

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());
Expand All @@ -52,8 +58,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
Expand Down
5 changes: 4 additions & 1 deletion src/analyze/basic_block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -354,6 +354,9 @@ 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(_) => {
PlaceTypeBuilder::default().build(rty::Type::bool(), chc::Term::bool(false))
}
};
tracing::debug!(operand = ?operand, ty = %ty.display(), "operand_type");
ty
Expand Down Expand Up @@ -485,7 +488,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
}
Rvalue::Cast(
mir::CastKind::PointerCoercion(
mir_ty::adjustment::PointerCoercion::ReifyFnPointer,
mir_ty::adjustment::PointerCoercion::ReifyFnPointer(_),
_,
),
operand,
Expand Down
121 changes: 96 additions & 25 deletions src/analyze/local_def.rs
Original file line number Diff line number Diff line change
Expand Up @@ -294,7 +294,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 {
Expand All @@ -311,11 +311,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)
}
Expand Down Expand Up @@ -526,15 +529,81 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
return Some((lhs_local, *place));
}

// nightly-2026+: CopyForDeref was replaced by plain Use(Copy(place)) for &mut T.
// Detect copies of &mut T reached through struct-field projections — these are deref
// aliases created so the result can be immediately dereffed (e.g. closure captures).
// We require a non-empty projection ending with a Field to avoid matching plain
// copies like `return_val = copy param` which are genuine transfers, not deref aliases.
if let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue {
let proj = place.projection.as_slice();
if let Some(mir::ProjectionElem::Field(..)) = proj.last() {
let place_ty = place.ty(&self.body.local_decls, self.tcx).ty;
if matches!(
place_ty.kind(),
mir_ty::TyKind::Ref(_, _, mir::Mutability::Mut)
) {
return Some((lhs_local, *place));
}
}
}

// nightly-2026+: box deref uses plain `copy (*box_local)` instead of CopyForDeref.
// Box<T> is not Copy, so `lhs = copy <box-place>` in optimized MIR must be the
// elaborated box deref pattern (reaching through the raw pointer alias from Transmute).
// The box may be reached through a reference (e.g. `copy (*ref_to_box)`), so we check
// the type of the full place after projections, not just the local's type.
if let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue {
if let Some((rest, [mir::ProjectionElem::Deref])) =
place.projection.as_slice().split_last_chunk::<1>()
{
if rest.is_empty() {
let place_ty = place.ty(&self.body.local_decls, self.tcx).ty;
if place_ty.is_box() {
return Some((lhs_local, *place));
}
}
}
}

let unique_did = self.ctx.def_ids.unique()?;
let nonnull_did = self.ctx.def_ids.nonnull()?;

use mir::ProjectionElem::Field;
use rustc_abi::FieldIdx;
const ZERO_FIELD: FieldIdx = FieldIdx::from_u32(0);

// nightly-2026+: box deref split into two statements. The pre-optimization MIR copies
// the NonNull field directly (instead of going through CopyForDeref/Transmute chain):
// _nonnull = copy box_place.Field(0, Unique<T>).Field(0, NonNull<T>)
// _ptr = Transmute(_nonnull) as *const T
// Detect the first statement and map _nonnull → box_place so the Transmute can be handled.
if let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue {
if let Some((rest, [Field(ZERO_FIELD, ty0), Field(ZERO_FIELD, ty1)])) =
place.projection.as_slice().split_last_chunk::<2>()
{
let rest_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() {
if let Some(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)
&& matches!(ty1.kind(), mir_ty::TyKind::Adt(def, args)
if def.did() == nonnull_did && args.type_at(0) == inner_ty)
{
return Some((lhs_local, rest_place));
}
}
}
}
}

// Box deref pattern: `(_box.0.0 as *const T) Transmute`
// projection = [..., Field(0, Unique<T>), Field(0, NonNull<T>)], transmuted to *const T
// Two variants:
// Old: projection = [..., Field(0, Unique<T>), Field(0, NonNull<T>)], transmuted to *const T
// New (nightly-2026+): operand is a Box<T> local (NonNull was pre-fetched separately)
let mir::Rvalue::Cast(mir::CastKind::Transmute, mir::Operand::Copy(place), cast_ty) =
&rvalue
else {
Expand All @@ -543,31 +612,33 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
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)])) =
// Old pattern: last two projections are Field(0,Unique).Field(0,NonNull).
if let Some((rest, [Field(ZERO_FIELD, ty0), Field(ZERO_FIELD, ty1)])) =
place.projection.as_slice().split_last_chunk::<2>()
else {
return None;
};
let rest_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;
let rest_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() {
if let Some(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)
&& matches!(ty1.kind(), mir_ty::TyKind::Adt(def, args)
if def.did() == nonnull_did && args.type_at(0) == inner_ty)
{
return Some((lhs_local, rest_place));
}
}
}
}
if !matches!(ty1.kind(), mir_ty::TyKind::Adt(def, args)
if def.did() == nonnull_did && args.type_at(0) == inner_ty)
{
return None;
// New pattern (nightly-2026+): operand is already a Box<T> (after NonNull pre-fetch).
let place_ty = place.ty(&self.body.local_decls, self.tcx).ty;
if place_ty.is_box() {
return Some((lhs_local, *place));
}
Some((lhs_local, rest_place))
None
}

fn unelaborate_derefs(&mut self) {
Expand Down
15 changes: 8 additions & 7 deletions src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
});
}

Expand All @@ -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);
Expand Down Expand Up @@ -90,7 +94,7 @@ fn thrust_macros_path() -> Option<std::path::PathBuf> {
None
}

pub fn main() {
pub fn main() -> std::process::ExitCode {
let mut args = std::env::args().collect::<Vec<_>>();

use tracing_subscriber::{filter::EnvFilter, prelude::*};
Expand All @@ -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 {}))
}
5 changes: 1 addition & 4 deletions src/refine/env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1013,10 +1013,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(),
Expand Down
2 changes: 1 addition & 1 deletion src/rty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,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);
removed
}
}
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/adt_discr.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix
//@compile-flags: -C debug-assertions=off

pub enum X {
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/annot_formula_fn.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix

#[thrust::formula_fn]
fn _thrust_requires_rand_except(x: i64) -> bool {
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/annot_preds.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix
//@compile-flags: -Adead_code -C debug-assertions=off

#[thrust::predicate]
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/annot_preds_trait.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix
//@compile-flags: -Adead_code -C debug-assertions=off

// A is represented as Tuple<Int> in SMT-LIB2 format.
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/annot_preds_trait_multi.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix
//@compile-flags: -Adead_code -C debug-assertions=off

#[thrust_macros::context]
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/extern_spec_take.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix

#[thrust::extern_spec_fn]
#[thrust_macros::requires(true)]
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/fn_poly_param_order.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix

fn select<T, U, V>(a: T, b: U, c: V, which: i32) -> T {
if which == 0 {
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/iterators/range.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix
//@compile-flags: -C debug-assertions=off
//@rustc-env: THRUST_SOLVER_ARGS=

Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/just_rec.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix
//@compile-flags: -C debug-assertions=off

#[thrust::trusted]
Expand Down
1 change: 1 addition & 0 deletions tests/ui/fail/split.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@error-in-other-file: Unsat
//@no-rustfix
//@compile-flags: -C debug-assertions=off

#[thrust::trusted]
Expand Down
1 change: 1 addition & 0 deletions tests/ui/pass/iterators/fixed_filter_loop_none.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
//@check-pass
//@compile-flags: -C debug-assertions=off
//@rustc-env: THRUST_SOLVER_ARGS=

struct Range {
start: i64,
Expand Down
Loading