diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index dba9988..fa5702e 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2024-09-08"
+channel = "nightly-2025-03-08"
 components = [ "rustc-dev", "rust-src", "llvm-tools-preview", "rust-analyzer" ]
diff --git a/src/analyze.rs b/src/analyze.rs
index 75d2286..dbf6209 100644
--- a/src/analyze.rs
+++ b/src/analyze.rs
@@ -582,7 +582,7 @@ impl<'tcx> Analyzer<'tcx> {
         attr_path: &[Symbol],
     ) -> Option<DefId> {
         let map = self.tcx.hir();
-        let body = map.maybe_body_owned_by(local_def_id)?;
+        let body = self.tcx.hir_maybe_body_owned_by(local_def_id)?;
 
         let rustc_hir::ExprKind::Block(block, _) = body.value.kind else {
             return None;
diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs
index b94a1ef..ec8465c 100644
--- a/src/analyze/annot.rs
+++ b/src/analyze/annot.rs
@@ -1,7 +1,7 @@
 //! Supporting implementation for parsing Thrust annotations.
 
-use rustc_ast::ast::Attribute;
 use rustc_ast::tokenstream::TokenStream;
+use rustc_hir::Attribute;
 use rustc_index::IndexVec;
 use rustc_span::symbol::{Ident, Symbol};
 
@@ -198,31 +198,27 @@ impl ResultResolver {
 }
 
 pub fn extract_annot_tokens(attr: Attribute) -> TokenStream {
-    use rustc_ast::{AttrArgs, AttrKind, DelimArgs};
-
-    let AttrKind::Normal(attr) = &attr.kind else {
-        panic!("invalid attribute");
+    let Attribute::Unparsed(item) = attr else {
+        panic!("invalid attribute: expected unparsed");
     };
-
-    let AttrArgs::Delimited(DelimArgs { tokens, .. }, ..) = &attr.item.args else {
-        panic!("invalid attribute");
+    let rustc_hir::AttrArgs::Delimited(d) = item.args else {
+        panic!("invalid attribute: expected delimited args");
     };
-
-    tokens.clone()
+    d.tokens
 }
 
 pub fn split_param(ts: &TokenStream) -> (Ident, TokenStream) {
     use rustc_ast::token::TokenKind;
     use rustc_ast::tokenstream::TokenTree;
 
-    let mut cursor = ts.trees();
-    let (ident, _) = match cursor.next() {
+    let mut iter = ts.iter();
+    let (ident, _) = match iter.next() {
         Some(TokenTree::Token(t, _)) => t.ident().expect("expected parameter name"),
         _ => panic!("expected parameter name"),
     };
-    match cursor.next() {
+    match iter.next() {
         Some(TokenTree::Token(t, _)) if t.kind == TokenKind::Colon => {}
         _ => panic!("expected :"),
     }
-    (ident, cursor.cloned().collect())
+    (ident, iter.cloned().collect())
 }
diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index 2e292db..aae82be 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -17,7 +17,7 @@ pub struct FormulaFn<'tcx> {
     formula: chc::Formula<rty::FunctionParamIdx>,
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b FormulaFn<'_>
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &FormulaFn<'_>
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
@@ -141,8 +141,7 @@ pub struct AnnotFnTranslator<'tcx> {
 
 impl<'tcx> AnnotFnTranslator<'tcx> {
     pub fn new(tcx: TyCtxt<'tcx>, local_def_id: LocalDefId) -> Self {
-        let map = tcx.hir();
-        let body = map.body_owned_by(local_def_id);
+        let body = tcx.hir_body_owned_by(local_def_id);
         let generic_args = tcx.mk_args(&[]);
         let typeck = tcx.typeck(local_def_id);
         let def_ids = DefIdCache::new(tcx);
@@ -208,15 +207,15 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
     fn expr_ty(&self, expr: &'tcx rustc_hir::Expr<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.expr_ty(expr);
         let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
-        let param_env = mir_ty::ParamEnv::reveal_all();
-        self.tcx.normalize_erasing_regions(param_env, instantiated)
+        let typing_env = mir_ty::TypingEnv::fully_monomorphized();
+        self.tcx.normalize_erasing_regions(typing_env, instantiated)
     }
 
     fn pat_ty(&self, pat: &'tcx rustc_hir::Pat<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.pat_ty(pat);
         let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
-        let param_env = mir_ty::ParamEnv::reveal_all();
-        self.tcx.normalize_erasing_regions(param_env, instantiated)
+        let typing_env = mir_ty::TypingEnv::fully_monomorphized();
+        self.tcx.normalize_erasing_regions(typing_env, instantiated)
     }
 
     pub fn to_formula_fn(&self) -> FormulaFn<'tcx> {
@@ -427,7 +426,7 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                             let ExprKind::Closure(closure) = args[0].kind else {
                                 panic!("exists argument must be a closure");
                             };
-                            let closure_body = self.tcx.hir().body(closure.body);
+                            let closure_body = self.tcx.hir_body(closure.body);
 
                             let mut inner_translator = self.clone();
                             let mut vars = Vec::new();
@@ -487,10 +486,7 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                             .next()
                             .is_some()
                         {
-                            let param_env = self
-                                .tcx
-                                .param_env(self.local_def_id)
-                                .with_reveal_all_normalized(self.tcx);
+                            let typing_env = mir_ty::TypingEnv::fully_monomorphized();
                             let generic_args = self.typeck.node_args(func_expr.hir_id);
                             tracing::debug!(
                                 lhs = ?def_id,
@@ -503,7 +499,7 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                                 .instantiate(self.tcx, self.generic_args);
                             let instance = mir_ty::Instance::try_resolve(
                                 self.tcx,
-                                param_env,
+                                typing_env,
                                 def_id,
                                 generic_args,
                             )
diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index a95d205..bb71ee7 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -181,12 +181,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let bytes = alloc
             .inner()
             .inspect_with_uninit_and_ptr_outside_interpreter(range.clone());
-        let param_env = self.tcx.param_env(self.local_def_id);
-        let layout = self.tcx.layout_of(param_env.and(ty)).unwrap();
-        let lcx = mir_ty::layout::LayoutCx {
-            tcx: self.tcx,
-            param_env,
-        };
+        let typing_env = self.body.typing_env(self.tcx);
+        let layout = self.tcx.layout_of(typing_env.as_query_input(ty)).unwrap();
+        let lcx = mir_ty::layout::LayoutCx::new(self.tcx, typing_env);
         match ty.kind() {
             mir_ty::TyKind::Str => {
                 let content = std::str::from_utf8(bytes).unwrap();
@@ -271,9 +268,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 let global_alloc = self.tcx.global_alloc(prov.alloc_id());
                 match global_alloc {
                     mir::interpret::GlobalAlloc::Memory(alloc) => {
+                        let typing_env = self.body.typing_env(self.tcx);
                         let layout = self
                             .tcx
-                            .layout_of(mir_ty::ParamEnv::reveal_all().and(*elem))
+                            .layout_of(typing_env.as_query_input(*elem))
                             .unwrap();
                         let size = layout.size;
                         let range =
@@ -297,10 +295,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             mir::Const::Unevaluated(unevaluated, ty) => {
                 // since all constants are immutable in current setup,
                 // it should be okay to evaluate them here on-the-fly
-                let param_env = self.tcx.param_env(self.local_def_id);
+                let typing_env = self.body.typing_env(self.tcx);
                 let val = self
                     .tcx
-                    .const_eval_resolve(param_env, *unevaluated, rustc_span::DUMMY_SP)
+                    .const_eval_resolve(typing_env, *unevaluated, rustc_span::DUMMY_SP)
                     .unwrap();
                 self.const_value_ty(&val, ty)
             }
@@ -445,7 +443,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 }
             }
             Rvalue::Cast(
-                mir::CastKind::PointerCoercion(mir_ty::adjustment::PointerCoercion::ReifyFnPointer),
+                mir::CastKind::PointerCoercion(
+                    mir_ty::adjustment::PointerCoercion::ReifyFnPointer,
+                    _,
+                ),
                 operand,
                 _ty,
             ) => {
@@ -614,12 +615,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             tracing::debug!(?closure_def_id, "closure instance");
             (*closure_def_id, args)
         } else {
-            let param_env = self
-                .tcx
-                .param_env(self.local_def_id)
-                .with_reveal_all_normalized(self.tcx);
+            let typing_env = self.body.typing_env(self.tcx);
             let instance =
-                mir_ty::Instance::try_resolve(self.tcx, param_env, def_id, args).unwrap();
+                mir_ty::Instance::try_resolve(self.tcx, typing_env, def_id, args).unwrap();
             if let Some(instance) = instance {
                 (instance.def_id(), instance.args)
             } else {
@@ -852,7 +850,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         } = &term.kind
         {
             let destination = match destination {
-                p if p.projection.len() == 0 => p.local,
+                p if p.projection.is_empty() => p.local,
                 _ => unimplemented!(),
             };
             if self.is_defined(destination) {
@@ -955,7 +953,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         {
             if let Some((p, Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _))) = stmt.kind.as_assign()
             {
-                if p.projection.len() != 0 {
+                if !p.projection.is_empty() {
                     unimplemented!();
                 }
                 // TODO: is it appropriate to use builtin_deref here... maybe we should handle dereferencing logic in `refine`
@@ -1088,7 +1086,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
         let bb_ty = self.basic_block_ty(self.basic_block).clone();
         let params = &bb_ty.as_ref().params;
-        assert!(params.len() >= 1);
+        assert!(!params.is_empty());
         for (param_idx, param_rty) in params.iter_enumerated() {
             let param_ty = &param_rty.ty;
             if let Some(local) = bb_ty.local_of_param(param_idx) {
diff --git a/src/analyze/basic_block/drop_point.rs b/src/analyze/basic_block/drop_point.rs
index a9685c3..be08b10 100644
--- a/src/analyze/basic_block/drop_point.rs
+++ b/src/analyze/basic_block/drop_point.rs
@@ -1,6 +1,6 @@
 use std::collections::HashMap;
 
-use rustc_index::bit_set::BitSet;
+use rustc_index::bit_set::DenseBitSet;
 use rustc_middle::mir::{self, BasicBlock, Body, Local};
 use rustc_mir_dataflow::{impls::MaybeLiveLocals, ResultsCursor};
 
@@ -8,8 +8,8 @@ use rustc_mir_dataflow::{impls::MaybeLiveLocals, ResultsCursor};
 pub struct DropPoints {
     // TODO: ad-hoc
     pub before_statements: Vec<Local>,
-    after_statements: Vec<BitSet<Local>>,
-    after_terminator: HashMap<BasicBlock, BitSet<Local>>,
+    after_statements: Vec<DenseBitSet<Local>>,
+    after_terminator: HashMap<BasicBlock, DenseBitSet<Local>>,
 }
 
 impl DropPoints {
@@ -40,11 +40,11 @@ impl DropPoints {
         self.after_statements[statement_index].insert(local)
     }
 
-    pub fn after_statement(&self, statement_index: usize) -> BitSet<Local> {
+    pub fn after_statement(&self, statement_index: usize) -> DenseBitSet<Local> {
         self.after_statements[statement_index].clone()
     }
 
-    pub fn after_terminator(&self, target: &BasicBlock) -> BitSet<Local> {
+    pub fn after_terminator(&self, target: &BasicBlock) -> DenseBitSet<Local> {
         let mut t = self.after_terminator[target].clone();
         t.union(self.after_statements.last().unwrap());
         t
@@ -54,12 +54,10 @@ impl DropPoints {
 #[derive(Debug, Clone)]
 pub struct DropPointsBuilder<'mir, 'tcx> {
     body: &'mir Body<'tcx>,
-    bb_ins_cache: HashMap<BasicBlock, BitSet<Local>>,
+    bb_ins_cache: HashMap<BasicBlock, DenseBitSet<Local>>,
 }
 
-fn def_local<'a, 'tcx, T: mir::visit::MirVisitable<'tcx> + ?Sized>(
-    visitable: &'a T,
-) -> Option<Local> {
+fn def_local<'tcx>(data: &mir::BasicBlockData<'tcx>, statement_index: usize) -> Option<Local> {
     struct Visitor {
         local: Option<Local>,
     }
@@ -77,7 +75,13 @@ fn def_local<'a, 'tcx, T: mir::visit::MirVisitable<'tcx> + ?Sized>(
         }
     }
     let mut visitor = Visitor { local: None };
-    visitable.apply(mir::Location::START, &mut visitor);
+    let loc = mir::Location::START;
+    use mir::visit::Visitor as _;
+    if statement_index < data.statements.len() {
+        visitor.visit_statement(&data.statements[statement_index], loc);
+    } else if let Some(tmnt) = &data.terminator {
+        visitor.visit_terminator(tmnt, loc);
+    }
     visitor.local
 }
 
@@ -91,13 +95,13 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
 
         let mut after_terminator = HashMap::new();
         let mut after_statements = Vec::new();
-        after_statements.resize_with(data.statements.len() + 1, || BitSet::new_empty(0));
+        after_statements.resize_with(data.statements.len() + 1, || DenseBitSet::new_empty(0));
 
         results.seek_to_block_end(bb);
         let live_locals_after_terminator = results.get().clone();
 
         use rustc_data_structures::graph::Successors as _;
-        let mut ins = BitSet::new_empty(self.body.local_decls.len());
+        let mut ins = DenseBitSet::new_empty(self.body.local_decls.len());
         for succ_bb in self.body.basic_blocks.successors(bb) {
             self.bb_ins_cache.entry(succ_bb).or_insert_with(|| {
                 results.seek_to_block_start(succ_bb);
@@ -127,7 +131,7 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
             tracing::debug!(?live_locals, ?loc);
             after_statements[statement_index] = {
                 let mut t = live_locals.clone();
-                if let Some(def) = def_local(data.visitable(statement_index)) {
+                if let Some(def) = def_local(data, statement_index) {
                     t.insert(def);
                 }
                 t.subtract(&last_live_locals);
diff --git a/src/analyze/basic_block/visitor/rust_call.rs b/src/analyze/basic_block/visitor/rust_call.rs
index 73b6338..5310010 100644
--- a/src/analyze/basic_block/visitor/rust_call.rs
+++ b/src/analyze/basic_block/visitor/rust_call.rs
@@ -62,7 +62,7 @@ impl<'a, 'tcx, 'ctx> mir::visit::MutVisitor<'tcx> for RustCallVisitor<'a, 'tcx,
                     panic!("expected closure arg for fn trait");
                 };
                 let fn_sig = self.analyzer.ctx().fn_sig(*resolved_def_id);
-                if !matches!(fn_sig.abi, rustc_target::spec::abi::Abi::RustCall) {
+                if !matches!(fn_sig.abi, rustc_abi::ExternAbi::RustCall) {
                     self.super_terminator(terminator, location);
                     return;
                 }
diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs
index 8b749d1..c85038f 100644
--- a/src/analyze/crate_.rs
+++ b/src/analyze/crate_.rs
@@ -37,7 +37,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             use rustc_ast::tokenstream::TokenTree;
 
             let ts = analyze::annot::extract_annot_tokens(attrs.clone());
-            let tt = ts.trees().next().expect("string literal");
+            let tt = ts.iter().next().expect("string literal").clone();
 
             let raw_command = match tt {
                 TokenTree::Token(
@@ -206,7 +206,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 mir_ty::GenericParamDefKind::Const { .. } => {
                     unimplemented!()
                 }
-                mir_ty::GenericParamDefKind::Lifetime { .. } => self.tcx.lifetimes.re_erased.into(),
+                mir_ty::GenericParamDefKind::Lifetime => self.tcx.lifetimes.re_erased.into(),
             };
             args.push(arg);
         }
diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs
index bb6fb90..1d8fd6a 100644
--- a/src/analyze/did_cache.rs
+++ b/src/analyze/did_cache.rs
@@ -3,10 +3,10 @@
 use std::cell::OnceCell;
 use std::rc::Rc;
 
+use rustc_abi::FieldIdx;
 use rustc_middle::ty::TyCtxt;
 use rustc_span::def_id::DefId;
 use rustc_span::symbol::Symbol;
-use rustc_target::abi::FieldIdx;
 
 #[derive(Debug, Clone, Default)]
 struct DefIds {
@@ -80,14 +80,13 @@ impl<'tcx> DefIdCache<'tcx> {
     }
 
     fn annotated_def(&self, path: &[Symbol]) -> Option<DefId> {
-        let map = self.tcx.hir();
-        for item_id in map.items() {
+        for item_id in self.tcx.hir_free_items() {
             let def_id = item_id.owner_id.to_def_id();
             if self.tcx.get_attrs_by_path(def_id, path).next().is_some() {
                 return Some(def_id);
             }
 
-            let item = map.item(item_id);
+            let item = self.tcx.hir_item(item_id);
             if let rustc_hir::ItemKind::Trait(_, _, _, _, trait_item_refs) = item.kind {
                 for trait_item_ref in trait_item_refs {
                     let def_id = trait_item_ref.id.owner_id.to_def_id();
diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
index 5987228..089699b 100644
--- a/src/analyze/local_def.rs
+++ b/src/analyze/local_def.rs
@@ -2,7 +2,7 @@
 
 use std::collections::{HashMap, HashSet};
 
-use rustc_index::bit_set::BitSet;
+use rustc_index::bit_set::DenseBitSet;
 use rustc_index::IndexVec;
 use rustc_middle::mir::{self, BasicBlock, Body, Local};
 use rustc_middle::ty::{self as mir_ty, TyCtxt, TypeAndMut};
@@ -140,8 +140,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         // function's body
         use rustc_hir::{Block, Expr, ExprKind};
 
-        let hir_map = self.tcx.hir();
-        let hir_body = hir_map.maybe_body_owned_by(self.local_def_id).unwrap();
+        let hir_body = self.tcx.hir_maybe_body_owned_by(self.local_def_id).unwrap();
 
         let predicate_body = match hir_body.value {
             Expr {
@@ -441,7 +440,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let node = self.tcx.hir_node_by_def_id(self.local_def_id);
         let body_id = match node {
             rustc_hir::Node::Item(item) => {
-                let rustc_hir::ItemKind::Fn(_, _, body_id) = item.kind else {
+                let rustc_hir::ItemKind::Fn { body: body_id, .. } = item.kind else {
                     panic!("extern_spec_fn must be a function");
                 };
                 body_id
@@ -463,7 +462,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             _ => panic!("extern_spec_fn must be a function item or impl item"),
         };
 
-        let body = self.tcx.hir().body(body_id);
+        let body = self.tcx.hir_body(body_id);
 
         // The body is a block; the tail expression is the function call to the target.
         let rustc_hir::ExprKind::Block(block, _) = &body.value.kind else {
@@ -487,8 +486,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         };
 
         let args = typeck_result.node_args(hir_id);
-        let param_env = self.tcx.param_env(self.local_def_id);
-        let instance = mir_ty::Instance::try_resolve(self.tcx, param_env, def_id, args).unwrap();
+        let typing_env = self.body.typing_env(self.tcx);
+        let instance = mir_ty::Instance::try_resolve(self.tcx, typing_env, def_id, args).unwrap();
         if let Some(instance) = instance {
             instance.def_id()
         } else {
@@ -518,14 +517,28 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             return Some((lhs_local, *place));
         }
 
-        let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue else {
-            return None;
-        };
-
         let unique_did = self.ctx.def_ids.unique()?;
         let nonnull_did = self.ctx.def_ids.nonnull()?;
 
-        let (rest, chunk) = place.projection.as_slice().split_last_chunk::<3>()?;
+        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<T>), Field(0, NonNull<T>)], 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>()
+        else {
+            return None;
+        };
         let rest_place = mir::Place {
             local: place.local,
             projection: self.tcx.mk_place_elems(rest),
@@ -535,35 +548,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             return None;
         }
         let inner_ty = local_ty.boxed_ty()?;
-
-        use mir::ProjectionElem::Field;
-        use rustc_target::abi::FieldIdx;
-        const ZERO_FIELD: FieldIdx = FieldIdx::from_u32(0);
-        let [Field(ZERO_FIELD, ty0), Field(ZERO_FIELD, ty1), Field(ZERO_FIELD, ty2)] = chunk else {
-            return None;
-        };
-
-        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
-        ) {
+        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!(
-            ty2.kind(), mir_ty::TyKind::RawPtr(t, mutbl)
-            if *t == inner_ty && mutbl.is_not()
-        ) {
+        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))
     }
 
@@ -590,15 +584,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
     }
 
-    fn mut_locals<'a, T>(&self, visitable: &'a T) -> BitSet<Local>
-    where
-        T: mir::visit::MirVisitable<'tcx> + ?Sized,
-    {
+    fn mut_locals(
+        &self,
+        data: &mir::BasicBlockData<'tcx>,
+        statement_index: usize,
+    ) -> DenseBitSet<Local> {
         struct Visitor<'tcx, 'a> {
             tcx: TyCtxt<'tcx>,
             body: &'a Body<'tcx>,
 
-            locals: BitSet<Local>,
+            locals: DenseBitSet<Local>,
         }
         impl<'tcx> mir::visit::Visitor<'tcx> for Visitor<'tcx, '_> {
             fn visit_rvalue(&mut self, rvalue: &mir::Rvalue<'tcx>, location: mir::Location) {
@@ -636,9 +631,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let mut visitor = Visitor {
             tcx: self.tcx,
             body: &self.body,
-            locals: BitSet::new_empty(self.body.local_decls.len()),
+            locals: DenseBitSet::new_empty(self.body.local_decls.len()),
         };
-        visitable.apply(mir::Location::START, &mut visitor);
+        let loc = mir::Location::START;
+        use mir::visit::Visitor as _;
+        if statement_index < data.statements.len() {
+            visitor.visit_statement(&data.statements[statement_index], loc);
+        } else if let Some(tmnt) = &data.terminator {
+            visitor.visit_terminator(tmnt, loc);
+        }
         visitor.locals
     }
 
@@ -714,7 +715,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             // XXX: what...
             let mut body = self.body.clone();
             struct Visitor {
-                deref_temps: BitSet<Local>,
+                deref_temps: DenseBitSet<Local>,
             }
             impl<'tcx> mir::visit::Visitor<'tcx> for Visitor {
                 fn visit_assign(
@@ -729,7 +730,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 }
             }
             let mut visitor = Visitor {
-                deref_temps: BitSet::new_empty(body.local_decls.len()),
+                deref_temps: DenseBitSet::new_empty(body.local_decls.len()),
             };
             use mir::visit::Visitor as _;
             visitor.visit_body(&body);
@@ -741,22 +742,20 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 };
                 local_decl.local_info = mir::ClearCrossCrate::Set(Box::new(local_info));
             }
-            let param_env = self.tcx.param_env_reveal_all_normalized(self.local_def_id);
-            MoveData::gather_moves(&body, self.tcx, param_env, |_| true)
+            MoveData::gather_moves(&body, self.tcx, |_| true)
         };
         let tmp_body = self.body.clone();
         let mut results =
             rustc_mir_dataflow::impls::MaybeInitializedPlaces::new(self.tcx, &tmp_body, &move_data)
-                .into_engine(self.tcx, &self.body)
-                .iterate_to_fixpoint()
+                .iterate_to_fixpoint(self.tcx, &self.body, None)
                 .into_results_cursor(&tmp_body);
 
-        let mut zst_locals = BitSet::new_empty(self.body.local_decls.len());
+        let mut zst_locals = DenseBitSet::new_empty(self.body.local_decls.len());
         for (local, local_decl) in self.body.local_decls.iter_enumerated() {
             let ty = local_decl.ty;
             if self
                 .tcx
-                .layout_of(mir_ty::ParamEnv::reveal_all().and(ty))
+                .layout_of(self.body.typing_env(self.tcx).as_query_input(ty))
                 .map(|l| l.is_zst())
                 .unwrap_or(false)
             {
@@ -778,7 +777,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                     .iter()
                     .map(|p| results.analysis().move_data().move_paths[p].place.local)
                     .collect();
-                let mut_locals = self.mut_locals(data.visitable(statement_index));
+                let mut_locals = self.mut_locals(data, statement_index);
                 tracing::info!(
                     ?init_locals,
                     ?mut_locals,
@@ -800,8 +799,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     fn refine_basic_blocks(&mut self) {
         use rustc_mir_dataflow::Analysis as _;
         let mut results = rustc_mir_dataflow::impls::MaybeLiveLocals
-            .into_engine(self.tcx, &self.body)
-            .iterate_to_fixpoint()
+            .iterate_to_fixpoint(self.tcx, &self.body, None)
             .into_results_cursor(&self.body);
 
         let mut builder = analyze::basic_block::DropPoints::builder(&self.body);
diff --git a/src/annot.rs b/src/annot.rs
index 03965a2..a82d8ad 100644
--- a/src/annot.rs
+++ b/src/annot.rs
@@ -8,8 +8,8 @@
 //! The main entry point is [`AnnotParser`], which parses a [`TokenStream`] into a
 //! [`rty::RefinedType`] or a [`chc::Formula`].
 
-use rustc_ast::token::{BinOpToken, Delimiter, LitKind, Token, TokenKind};
-use rustc_ast::tokenstream::{RefTokenTreeCursor, Spacing, TokenStream, TokenTree};
+use rustc_ast::token::{Delimiter, LitKind, Token, TokenKind};
+use rustc_ast::tokenstream::{Spacing, TokenStream, TokenTree};
 use rustc_index::IndexVec;
 use rustc_span::symbol::Ident;
 use std::collections::HashMap;
@@ -95,7 +95,7 @@ pub trait Resolver {
     fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)>;
 }
 
-impl<'a, T> Resolver for &'a T
+impl<T> Resolver for &T
 where
     T: Resolver,
 {
@@ -253,15 +253,43 @@ impl<T> FormulaOrTerm<T> {
     }
 }
 
+struct TokenCursor {
+    trees: Vec<TokenTree>,
+    idx: usize,
+}
+
+impl TokenCursor {
+    fn from_stream(stream: TokenStream) -> Self {
+        TokenCursor {
+            trees: stream.iter().cloned().collect(),
+            idx: 0,
+        }
+    }
+
+    fn next(&mut self) -> Option<&TokenTree> {
+        if self.idx < self.trees.len() {
+            let t = &self.trees[self.idx];
+            self.idx += 1;
+            Some(t)
+        } else {
+            None
+        }
+    }
+
+    fn look_ahead(&self, n: usize) -> Option<&TokenTree> {
+        self.trees.get(self.idx + n)
+    }
+}
+
 /// A parser for refinement type annotations and formula annotations.
-struct Parser<'a, T> {
+struct Parser<T> {
     resolver: T,
     self_type_name: Option<String>,
-    cursor: RefTokenTreeCursor<'a>,
+    cursor: TokenCursor,
     formula_existentials: HashMap<String, chc::Sort>,
 }
 
-impl<'a, T> Parser<'a, T>
+impl<T> Parser<T>
 where
     T: Resolver,
 {
@@ -461,7 +489,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     self_type_name: self.self_type_name.clone(),
-                    cursor: s.trees(),
+                    cursor: TokenCursor::from_stream(s.clone()),
                     formula_existentials: self.formula_existentials.clone(),
                 };
                 let formula_or_term = parser.parse_formula_or_term_or_tuple()?;
@@ -502,7 +530,7 @@ where
                             let mut parser = Parser {
                                 resolver: self.boxed_resolver(),
                                 self_type_name: self.self_type_name.clone(),
-                                cursor: args.trees(),
+                                cursor: TokenCursor::from_stream(args),
                                 formula_existentials: self.formula_existentials.clone(),
                             };
                             let args = parser.parse_arg_terms()?;
@@ -528,7 +556,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     self_type_name: self.self_type_name.clone(),
-                    cursor: s.trees(),
+                    cursor: TokenCursor::from_stream(s),
                     formula_existentials: self.formula_existentials.clone(),
                 };
                 let args = parser.parse_arg_terms()?;
@@ -646,7 +674,7 @@ where
                     let mut parser = Parser {
                         resolver: self.boxed_resolver(),
                         self_type_name: self.self_type_name.clone(),
-                        cursor: args.trees(),
+                        cursor: TokenCursor::from_stream(args),
                         formula_existentials: self.formula_existentials.clone(),
                     };
                     let args = parser.parse_arg_terms()?;
@@ -695,14 +723,14 @@ where
     fn parse_prefix(&mut self) -> Result<FormulaOrTerm<T::Output>> {
         let formula_or_term =
             match self.look_ahead_token(0).map(|t| &t.kind) {
-                Some(TokenKind::BinOp(BinOpToken::Minus)) => {
+                Some(TokenKind::Minus) => {
                     self.consume();
                     let (operand, sort) = self.parse_postfix()?.into_term().ok_or_else(|| {
                         ParseAttrError::unexpected_formula("after unary - operator")
                     })?;
                     FormulaOrTerm::Term(operand.neg(), sort)
                 }
-                Some(TokenKind::BinOp(BinOpToken::Star)) => {
+                Some(TokenKind::Star) => {
                     self.consume();
                     let (operand, sort) = self.parse_postfix()?.into_term().ok_or_else(|| {
                         ParseAttrError::unexpected_formula("after unary * operator")
@@ -714,7 +742,7 @@ where
                     };
                     FormulaOrTerm::Term(t, s)
                 }
-                Some(TokenKind::BinOp(BinOpToken::Caret)) => {
+                Some(TokenKind::Caret) => {
                     self.consume();
                     let (operand, sort) = self.parse_postfix()?.into_term().ok_or_else(|| {
                         ParseAttrError::unexpected_formula("after unary ^ operator")
@@ -725,7 +753,7 @@ where
                         return Err(ParseAttrError::unsorted_op("^", sort));
                     }
                 }
-                Some(TokenKind::Not) => {
+                Some(TokenKind::Bang) => {
                     self.consume();
                     let formula_or_term = self.parse_postfix()?;
                     FormulaOrTerm::Not(Box::new(formula_or_term))
@@ -738,9 +766,7 @@ where
     fn parse_binop_1(&mut self) -> Result<FormulaOrTerm<T::Output>> {
         let mut formula_or_term = self.parse_prefix()?;
 
-        while let Some(TokenKind::BinOp(BinOpToken::Star)) =
-            self.look_ahead_token(0).map(|t| &t.kind)
-        {
+        while let Some(TokenKind::Star) = self.look_ahead_token(0).map(|t| &t.kind) {
             self.consume();
             let (lhs, _) = formula_or_term
                 .into_term()
@@ -760,7 +786,7 @@ where
 
         loop {
             match self.look_ahead_token(0).map(|t| &t.kind) {
-                Some(TokenKind::BinOp(BinOpToken::Plus)) => {
+                Some(TokenKind::Plus) => {
                     self.consume();
                     let (lhs, _) = formula_or_term
                         .into_term()
@@ -771,7 +797,7 @@ where
                         .ok_or_else(|| ParseAttrError::unexpected_formula("after + operator"))?;
                     formula_or_term = FormulaOrTerm::Term(lhs.add(rhs), chc::Sort::int())
                 }
-                Some(TokenKind::BinOp(BinOpToken::Minus)) => {
+                Some(TokenKind::Minus) => {
                     self.consume();
                     let (lhs, _) = formula_or_term
                         .into_term()
@@ -947,7 +973,7 @@ where
         match tt {
             TokenTree::Token(
                 Token {
-                    kind: TokenKind::BinOp(BinOpToken::And),
+                    kind: TokenKind::And,
                     ..
                 },
                 _,
@@ -995,7 +1021,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     self_type_name: self.self_type_name.clone(),
-                    cursor: ts.trees(),
+                    cursor: TokenCursor::from_stream(ts),
                     formula_existentials: self.formula_existentials.clone(),
                 };
                 let mut sorts = Vec::new();
@@ -1076,14 +1102,14 @@ where
             }
             TokenTree::Token(
                 Token {
-                    kind: TokenKind::Not,
+                    kind: TokenKind::Bang,
                     ..
                 },
                 _,
             ) => Ok(rty::Type::never()),
             TokenTree::Token(
                 Token {
-                    kind: TokenKind::BinOp(BinOpToken::And),
+                    kind: TokenKind::And,
                     ..
                 },
                 _,
@@ -1102,7 +1128,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     self_type_name: self.self_type_name.clone(),
-                    cursor: ts.trees(),
+                    cursor: TokenCursor::from_stream(ts),
                     formula_existentials: self.formula_existentials.clone(),
                 };
                 let mut rtys = Vec::new();
@@ -1139,7 +1165,7 @@ where
         let mut parser = Parser {
             resolver: self.boxed_resolver(),
             self_type_name: self.self_type_name.clone(),
-            cursor: ts.trees(),
+            cursor: TokenCursor::from_stream(ts),
             formula_existentials: self.formula_existentials.clone(),
         };
         let self_ident = if matches!(
@@ -1159,7 +1185,7 @@ where
             None
         };
         let ty = parser.parse_ty()?;
-        parser.expect_next_token(TokenKind::BinOp(BinOpToken::Or), "|")?;
+        parser.expect_next_token(TokenKind::Or, "|")?;
 
         let mut parser = Parser {
             resolver: RefinementResolver::new(self.boxed_resolver()),
@@ -1309,7 +1335,7 @@ where
         let mut parser = Parser {
             resolver: &self.resolver,
             self_type_name: self.self_type_name.clone(),
-            cursor: ts.trees(),
+            cursor: TokenCursor::from_stream(ts),
             formula_existentials: Default::default(),
         };
         let rty = parser.parse_rty()?;
@@ -1321,7 +1347,7 @@ where
         let mut parser = Parser {
             resolver: &self.resolver,
             self_type_name: self.self_type_name.clone(),
-            cursor: ts.trees(),
+            cursor: TokenCursor::from_stream(ts),
             formula_existentials: Default::default(),
         };
         let formula = parser.parse_annot_formula()?;
diff --git a/src/chc.rs b/src/chc.rs
index 5b884e5..5816639 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -30,7 +30,7 @@ impl std::fmt::Display for DatatypeSymbol {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b DatatypeSymbol
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &DatatypeSymbol
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -55,7 +55,7 @@ pub struct DatatypeSort {
     args: Vec<Sort>,
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b DatatypeSort
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &DatatypeSort
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
@@ -105,7 +105,7 @@ impl From<DatatypeSort> for Sort {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b Sort
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &Sort
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
@@ -326,7 +326,7 @@ impl std::fmt::Display for TermVarIdx {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b TermVarIdx
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &TermVarIdx
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -354,7 +354,7 @@ impl std::fmt::Display for Function {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b Function
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &Function
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -456,7 +456,7 @@ pub enum Term<V = TermVarIdx> {
     FormulaExistentialVar(Sort, String),
 }
 
-impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Term<V>
+impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &Term<V>
 where
     V: Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -798,7 +798,7 @@ impl std::fmt::Display for PredVarId {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b PredVarId
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &PredVarId
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -834,7 +834,7 @@ impl std::fmt::Display for KnownPred {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b KnownPred
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &KnownPred
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -933,7 +933,7 @@ impl std::fmt::Display for MatcherPred {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b MatcherPred
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &MatcherPred
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
@@ -979,7 +979,7 @@ impl std::fmt::Display for UserDefinedPred {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b UserDefinedPred
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &UserDefinedPred
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -1014,7 +1014,7 @@ impl std::fmt::Display for Pred {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b Pred
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &Pred
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
@@ -1113,7 +1113,7 @@ pub struct Atom<V = TermVarIdx> {
     pub args: Vec<Term<V>>,
 }
 
-impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Atom<V>
+impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &Atom<V>
 where
     V: Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -1266,7 +1266,7 @@ impl<V> From<Atom<V>> for Formula<V> {
     }
 }
 
-impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Formula<V>
+impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &Formula<V>
 where
     V: Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -1629,7 +1629,7 @@ where
     }
 }
 
-impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Body<V>
+impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &Body<V>
 where
     V: Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -1670,7 +1670,7 @@ pub struct Clause {
     pub debug_info: DebugInfo,
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b Clause
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &Clause
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
diff --git a/src/lib.rs b/src/lib.rs
index 14499d2..cbbe60b 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,5 +1,6 @@
 #![feature(rustc_private)]
 
+extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_borrowck;
 extern crate rustc_data_structures;
diff --git a/src/main.rs b/src/main.rs
index a4746d8..960ebc1 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -3,13 +3,13 @@
 extern crate rustc_ast;
 extern crate rustc_driver;
 extern crate rustc_interface;
+extern crate rustc_middle;
 extern crate rustc_parse;
 extern crate rustc_session;
 extern crate rustc_span;
 
-use rustc_driver::{Callbacks, Compilation, RunCompiler};
+use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::interface::{Compiler, Config};
-use rustc_interface::Queries;
 
 struct CompilerCalls {}
 
@@ -24,18 +24,15 @@ impl Callbacks for CompilerCalls {
         });
     }
 
-    fn after_crate_root_parsing<'tcx>(
+    fn after_crate_root_parsing(
         &mut self,
         compiler: &Compiler,
-        queries: &'tcx Queries<'tcx>,
+        krate: &mut rustc_ast::Crate,
     ) -> Compilation {
         if matches!(std::env::var("THRUST_NO_INJECT_STD").as_deref(), Ok("1")) {
             return Compilation::Continue;
         }
 
-        let mut result = queries.parse().unwrap();
-        let krate = result.get_mut();
-
         let injected = include_str!("../std.rs");
         let mut parser = rustc_parse::new_parser_from_source_str(
             &compiler.sess.psess,
@@ -55,14 +52,12 @@ impl Callbacks for CompilerCalls {
     fn after_analysis<'tcx>(
         &mut self,
         _compiler: &Compiler,
-        queries: &'tcx Queries<'tcx>,
+        tcx: rustc_middle::ty::TyCtxt<'tcx>,
     ) -> Compilation {
-        queries.global_ctxt().unwrap().enter(|tcx| {
-            let mut ctx = thrust::Analyzer::new(tcx);
-            ctx.register_well_known_defs();
-            ctx.crate_analyzer().run();
-            ctx.solve();
-        });
+        let mut ctx = thrust::Analyzer::new(tcx);
+        ctx.register_well_known_defs();
+        ctx.crate_analyzer().run();
+        ctx.solve();
         Compilation::Stop
     }
 }
@@ -117,7 +112,8 @@ pub fn main() {
         tracing::warn!("could not locate thrust_macros library");
     }
 
-    let code =
-        rustc_driver::catch_with_exit_code(|| RunCompiler::new(&args, &mut CompilerCalls {}).run());
+    let code = rustc_driver::catch_with_exit_code(|| {
+        rustc_driver::run_compiler(&args, &mut CompilerCalls {})
+    });
     std::process::exit(code);
 }
diff --git a/src/pretty.rs b/src/pretty.rs
index bb347d8..8fc3a98 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -53,7 +53,7 @@ pub struct PrettySlice<'a, T> {
     slice: &'a [T],
 }
 
-impl<'a, 'b, 'c, D, T> Pretty<'a, D, termcolor::ColorSpec> for &'c PrettySlice<'b, T>
+impl<'a, 'b, D, T> Pretty<'a, D, termcolor::ColorSpec> for &PrettySlice<'b, T>
 where
     &'b T: Pretty<'a, D, termcolor::ColorSpec>,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
diff --git a/src/refine/basic_block.rs b/src/refine/basic_block.rs
index ac39a1c..67439c9 100644
--- a/src/refine/basic_block.rs
+++ b/src/refine/basic_block.rs
@@ -19,7 +19,7 @@ pub struct BasicBlockType {
     pub(super) locals: IndexVec<rty::FunctionParamIdx, (Local, mir_ty::Mutability)>,
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b BasicBlockType
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &BasicBlockType
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
diff --git a/src/refine/env.rs b/src/refine/env.rs
index 77b7556..e7762e5 100644
--- a/src/refine/env.rs
+++ b/src/refine/env.rs
@@ -1,9 +1,9 @@
 use std::collections::{BTreeMap, HashMap};
 
 use pretty::{termcolor, Pretty};
+use rustc_abi::{FieldIdx, VariantIdx};
 use rustc_index::IndexVec;
 use rustc_middle::mir::{Local, Place, PlaceElem};
-use rustc_target::abi::{FieldIdx, VariantIdx};
 
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
@@ -49,7 +49,7 @@ impl std::fmt::Display for Var {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b Var
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &Var
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -200,7 +200,7 @@ impl std::fmt::Debug for PlaceTypeVar {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b PlaceTypeVar
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &PlaceTypeVar
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -294,7 +294,7 @@ pub trait EnumDefProvider {
     fn enum_def(&self, name: &chc::DatatypeSymbol) -> rty::EnumDatatypeDef;
 }
 
-impl<'a, T: EnumDefProvider> EnumDefProvider for &'a T {
+impl<T: EnumDefProvider> EnumDefProvider for &T {
     fn enum_def(&self, name: &chc::DatatypeSymbol) -> rty::EnumDatatypeDef {
         <T as EnumDefProvider>::enum_def(self, name)
     }
@@ -327,7 +327,7 @@ impl From<PlaceType> for rty::RefinedType<Var> {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b PlaceType
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &PlaceType
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
@@ -1036,7 +1036,7 @@ where
 
 #[derive(Debug, Clone)]
 enum Path {
-    PlaceTy(PlaceType),
+    PlaceTy(Box<PlaceType>),
     Local(Local),
     Deref(Box<Path>),
     TupleProj(Box<Path>, usize),
@@ -1081,7 +1081,7 @@ where
 {
     fn path_type(&self, path: &Path) -> PlaceType {
         match path {
-            Path::PlaceTy(pty) => pty.clone(),
+            Path::PlaceTy(pty) => *pty.clone(),
             Path::Local(local) => self.local_type(*local),
             Path::Deref(path) => self.path_type(path).deref(),
             Path::TupleProj(path, idx) => self.path_type(path).tuple_proj(*idx),
@@ -1160,7 +1160,7 @@ where
                 let Assumption {
                     existentials: assumption_existentials,
                     body: assumption_body,
-                } = self.dropping_assumption(&Path::PlaceTy(field_pty));
+                } = self.dropping_assumption(&Path::PlaceTy(Box::new(field_pty)));
                 // dropping assumption should not generate any existential
                 assert!(assumption_existentials.is_empty());
                 formula.push_conj(assumption_body);
diff --git a/src/refine/template.rs b/src/refine/template.rs
index b4ec137..f3db0e8 100644
--- a/src/refine/template.rs
+++ b/src/refine/template.rs
@@ -71,7 +71,7 @@ where
 pub struct TypeBuilder<'tcx> {
     tcx: mir_ty::TyCtxt<'tcx>,
     def_ids: DefIdCache<'tcx>,
-    param_env: mir_ty::ParamEnv<'tcx>,
+    typing_env: mir_ty::TypingEnv<'tcx>,
     /// Maps index in [`mir_ty::ParamTy`] to [`rty::TypeParamIdx`].
     /// These indices may differ because we skip lifetime parameters and they always need to be
     /// mapped when we translate a [`mir_ty::ParamTy`] to [`rty::ParamType`].
@@ -93,11 +93,11 @@ impl<'tcx> TypeBuilder<'tcx> {
                 mir_ty::GenericParamDefKind::Const { .. } => {}
             }
         }
-        let param_env = tcx.param_env_reveal_all_normalized(def_id);
+        let typing_env = mir_ty::TypingEnv::post_analysis(tcx, def_id);
         Self {
             tcx,
             def_ids,
-            param_env,
+            typing_env,
             param_idx_mapping,
         }
     }
@@ -161,7 +161,7 @@ impl<'tcx> TypeBuilder<'tcx> {
         let projection_ty = mir_ty::Ty::new_projection(self.tcx, model_ty_def_id, args);
         if let Ok(normalized_ty) = self
             .tcx
-            .try_normalize_erasing_regions(self.param_env, projection_ty)
+            .try_normalize_erasing_regions(self.typing_env, projection_ty)
         {
             return normalized_ty;
         }
@@ -279,8 +279,8 @@ impl<'tcx> TypeBuilder<'tcx> {
         sig: mir_ty::FnSig<'tcx>,
     ) -> FunctionTemplateTypeBuilder<'tcx, 'a, R> {
         let abi = match sig.abi {
-            rustc_target::spec::abi::Abi::Rust => rty::FunctionAbi::Rust,
-            rustc_target::spec::abi::Abi::RustCall => rty::FunctionAbi::RustCall,
+            rustc_abi::ExternAbi::Rust => rty::FunctionAbi::Rust,
+            rustc_abi::ExternAbi::RustCall => rty::FunctionAbi::RustCall,
             _ => unimplemented!("unsupported function ABI: {:?}", sig.abi),
         };
         FunctionTemplateTypeBuilder {
diff --git a/src/rty.rs b/src/rty.rs
index 7e45866..5cbe6d2 100644
--- a/src/rty.rs
+++ b/src/rty.rs
@@ -40,8 +40,8 @@
 use std::collections::{HashMap, HashSet};
 
 use pretty::{termcolor, Pretty};
+use rustc_abi::VariantIdx;
 use rustc_index::IndexVec;
-use rustc_target::abi::VariantIdx;
 
 use crate::chc;
 
@@ -74,7 +74,7 @@ impl std::fmt::Display for FunctionParamIdx {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b FunctionParamIdx
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &FunctionParamIdx
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -125,7 +125,7 @@ pub struct FunctionType {
     pub abi: FunctionAbi,
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b FunctionType
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &FunctionType
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
@@ -218,7 +218,7 @@ impl std::fmt::Display for RefKind {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b RefKind
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &RefKind
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -243,7 +243,7 @@ impl std::fmt::Display for PointerKind {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b PointerKind
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &PointerKind
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -274,7 +274,7 @@ pub struct PointerType<T> {
     pub elem: Box<RefinedType<T>>,
 }
 
-impl<'a, 'b, T, D> Pretty<'a, D, termcolor::ColorSpec> for &'b PointerType<T>
+impl<'a, T, D> Pretty<'a, D, termcolor::ColorSpec> for &PointerType<T>
 where
     T: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -386,7 +386,7 @@ pub struct TupleType<T> {
     pub elems: Vec<RefinedType<T>>,
 }
 
-impl<'a, 'b, T, D> Pretty<'a, D, termcolor::ColorSpec> for &'b TupleType<T>
+impl<'a, T, D> Pretty<'a, D, termcolor::ColorSpec> for &TupleType<T>
 where
     T: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -511,7 +511,7 @@ pub struct EnumType<T> {
     pub args: IndexVec<TypeParamIdx, RefinedType<T>>,
 }
 
-impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b EnumType<V>
+impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &EnumType<V>
 where
     V: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -612,7 +612,7 @@ pub struct ParamType {
     pub idx: TypeParamIdx,
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b ParamType
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ParamType
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -642,7 +642,7 @@ pub struct ArrayType<T> {
     pub elem: Box<RefinedType<T>>,
 }
 
-impl<'a, 'b, T, D> Pretty<'a, D, termcolor::ColorSpec> for &'b ArrayType<T>
+impl<'a, T, D> Pretty<'a, D, termcolor::ColorSpec> for &ArrayType<T>
 where
     T: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -769,7 +769,7 @@ impl<T> From<EnumType<T>> for Type<T> {
     }
 }
 
-impl<'a, 'b, T, D> Pretty<'a, D, termcolor::ColorSpec> for &'b Type<T>
+impl<'a, T, D> Pretty<'a, D, termcolor::ColorSpec> for &Type<T>
 where
     T: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -1029,7 +1029,7 @@ impl std::fmt::Display for Closed {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b Closed
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &Closed
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -1055,7 +1055,7 @@ impl std::fmt::Display for ExistentialVarIdx {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b ExistentialVarIdx
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ExistentialVarIdx
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
@@ -1076,7 +1076,7 @@ pub trait ShiftExistential {
 /// - `RefinedTypeVar::Value`: a variable `v` representing the value of the type
 /// - `RefinedTypeVar::Existential`: an existential variable `e`
 /// - `RefinedTypeVar::Free`: a variable from the outer scope, such as function parameters or
-///    variables bound in the environment
+///   variables bound in the environment
 #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum RefinedTypeVar<FV> {
     Value,
@@ -1116,7 +1116,7 @@ where
     }
 }
 
-impl<'a, 'b, D, FV> Pretty<'a, D, termcolor::ColorSpec> for &'b RefinedTypeVar<FV>
+impl<'a, D, FV> Pretty<'a, D, termcolor::ColorSpec> for &RefinedTypeVar<FV>
 where
     FV: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -1213,7 +1213,7 @@ where
     }
 }
 
-impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Formula<V>
+impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &Formula<V>
 where
     V: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -1409,7 +1409,7 @@ pub struct RefinedType<FV = Closed> {
     pub refinement: Refinement<FV>,
 }
 
-impl<'a, 'b, D, FV> Pretty<'a, D, termcolor::ColorSpec> for &'b RefinedType<FV>
+impl<'a, D, FV> Pretty<'a, D, termcolor::ColorSpec> for &RefinedType<FV>
 where
     FV: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
diff --git a/src/rty/params.rs b/src/rty/params.rs
index b76b6d1..ef05138 100644
--- a/src/rty/params.rs
+++ b/src/rty/params.rs
@@ -36,7 +36,7 @@ impl std::fmt::Display for TypeParamIdx {
     }
 }
 
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b TypeParamIdx
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &TypeParamIdx
 where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
diff --git a/thrust-macros/src/lib.rs b/thrust-macros/src/lib.rs
index e61b95a..b79e844 100644
--- a/thrust-macros/src/lib.rs
+++ b/thrust-macros/src/lib.rs
@@ -687,7 +687,7 @@ fn model_where_predicates(
                 let TypeParamBound::Trait(tb) = b else {
                     return false;
                 };
-                tb.path.segments.last().map_or(false, |s| {
+                tb.path.segments.last().is_some_and(|s| {
                     matches!(s.ident.to_string().as_str(), "Fn" | "FnOnce" | "FnMut")
                 })
             })