Update toolchain to 2025-11-13

creusot/src/analysis/borrows.rs

@@ -121,7 +121,7 @@ impl<'tcx> Analysis<'tcx> for Borrows<'_, '_, 'tcx> {
     }
 
     fn apply_primary_statement_effect(
-        &mut self,
+        &self,
         trans: &mut Self::Domain,
         stmt: &mir::Statement<'tcx>,
         location: Location,
@@ -162,7 +162,6 @@ impl<'tcx> Analysis<'tcx> for Borrows<'_, '_, 'tcx> {
 
             mir::StatementKind::FakeRead(..)
             | mir::StatementKind::SetDiscriminant { .. }
-            | mir::StatementKind::Deinit(..)
             | mir::StatementKind::Retag { .. }
             | mir::StatementKind::PlaceMention(..)
             | mir::StatementKind::AscribeUserType(..)
@@ -175,7 +174,7 @@ impl<'tcx> Analysis<'tcx> for Borrows<'_, '_, 'tcx> {
     }
 
     fn apply_primary_terminator_effect<'mir>(
-        &mut self,
+        &self,
         trans: &mut Self::Domain,
         terminator: &'mir mir::Terminator<'tcx>,
         location: Location,

creusot/src/analysis/liveness_no_drop.rs

@@ -60,7 +60,7 @@ impl<'a, 'tcx> Analysis<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
         // No variables are live until we observe a use
     }
     fn apply_primary_statement_effect(
-        &mut self,
+        &self,
         trans: &mut Self::Domain,
         statement: &mir::Statement<'tcx>,
         location: Location,
@@ -69,7 +69,7 @@ impl<'a, 'tcx> Analysis<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
     }
 
     fn apply_primary_terminator_effect<'mir>(
-        &mut self,
+        &self,
         trans: &mut Self::Domain,
         terminator: &'mir mir::Terminator<'tcx>,
         location: Location,
@@ -79,7 +79,7 @@ impl<'a, 'tcx> Analysis<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
     }
 
     fn apply_call_return_effect(
-        &mut self,
+        &self,
         trans: &mut Self::Domain,
         _block: mir::BasicBlock,
         return_places: CallReturnPlaces<'_, 'tcx>,
@@ -174,8 +174,7 @@ impl DefUse {
                 MutatingUseContext::Call
                 | MutatingUseContext::Yield
                 | MutatingUseContext::AsmOutput
-                | MutatingUseContext::Store
-                | MutatingUseContext::Deinit,
+                | MutatingUseContext::Store,
             ) => {
                 if place_contains_borrow_deref(place.as_ref(), &ctx.body, ctx.tcx) {
                     // Treat derefs of (mutable) borrows as a use of the base local.

creusot/src/analysis/not_final_places.rs

@@ -239,7 +239,7 @@ impl<'tcx> Analysis<'tcx> for NotFinalPlaces<'tcx> {
     fn initialize_start_block(&self, _: &mir::Body<'tcx>, _: &mut Self::Domain) {}
 
     fn apply_primary_statement_effect(
-        &mut self,
+        &self,
         trans: &mut Self::Domain,
         statement: &mir::Statement<'tcx>,
         location: mir::Location,
@@ -248,7 +248,7 @@ impl<'tcx> Analysis<'tcx> for NotFinalPlaces<'tcx> {
     }
 
     fn apply_primary_terminator_effect<'mir>(
-        &mut self,
+        &self,
         trans: &mut Self::Domain,
         terminator: &'mir mir::Terminator<'tcx>,
         location: mir::Location,

creusot/src/backend.rs

@@ -72,7 +72,7 @@ impl<'tcx> Why3Generator<'tcx> {
         debug!("translating {:?}", def_id);
 
         let translated_item = match self.item_type(def_id) {
-            ItemType::Impl if self.tcx.impl_trait_ref(def_id).is_some() => {
+            ItemType::Impl if self.tcx.impl_opt_trait_ref(def_id).is_some() => {
                 let modls = traits::lower_impl(self, def_id);
                 TranslatedItem::Impl { modls }
             }

creusot/src/backend/clone_map/elaborator.rs

@@ -662,7 +662,7 @@ fn traitref_of_item<'tcx>(
         return Some(TraitRef::new(tcx, cont, subst));
     }
 
-    let trait_ref = tcx.impl_trait_ref(cont)?.instantiate(tcx, subst);
+    let trait_ref = tcx.impl_opt_trait_ref(cont)?.instantiate(tcx, subst);
     Some(tcx.normalize_erasing_regions(typing_env, trait_ref))
 }
 

creusot/src/backend/dependency.rs

@@ -85,7 +85,7 @@ impl<'tcx> Dependency<'tcx> {
                     let mut name =
                         lowercase_prefix("f_", name.strip_suffix("_logic").unwrap_or(name));
                     let first_ty = if let Some(parent) = ctx.impl_of_assoc(did)
-                        && let Some(trait_ref) = ctx.impl_trait_ref(parent)
+                        && let Some(trait_ref) = ctx.impl_opt_trait_ref(parent)
                     {
                         // AssocFn in a trait impl: get the instantiated Self type
                         first_ty_arg(trait_ref.instantiate(ctx.tcx, subst).args)

creusot/src/backend/logic/vcgen.rs

@@ -630,7 +630,6 @@ impl<'tcx> VCGen<'_, 'tcx> {
                     def(ProjectionElem::Downcast(symbol, variant_idx))
                 }
                 ProjectionElem::OpaqueCast(ty) => def(ProjectionElem::OpaqueCast(ty)),
-                ProjectionElem::Subtype(ty) => def(ProjectionElem::Subtype(ty)),
                 ProjectionElem::UnwrapUnsafeBinder(ty) => {
                     def(ProjectionElem::UnwrapUnsafeBinder(ty))
                 }

creusot/src/backend/optimization/invariants.rs

@@ -124,7 +124,6 @@ fn place_to_term<'tcx>(
             ProjectionElem::Subslice { .. } => return None,
             ProjectionElem::Downcast(_, _) => return None,
             ProjectionElem::OpaqueCast(_) => return None,
-            ProjectionElem::Subtype(_) => return None,
             ProjectionElem::UnwrapUnsafeBinder(_) => return None,
         }
 

creusot/src/backend/projections.rs

@@ -240,7 +240,6 @@ pub(crate) fn projections_to_expr<'tcx, 'a>(
             ProjectionElem::ConstantIndex { .. }
             | ProjectionElem::Subslice { .. }
             | ProjectionElem::OpaqueCast(_)
-            | ProjectionElem::Subtype(_)
             | ProjectionElem::UnwrapUnsafeBinder(_) => {
                 ctx.dcx().span_bug(span, format!("Unsupported projection {proj:?}"))
             }
@@ -295,9 +294,7 @@ pub(crate) fn borrow_generated_id<'tcx, V: Debug>(
                 ctx.dcx().span_bug(span, format!("Unsupported projection {proj:?} in reborrow"))
             }
             // Nothing to do
-            ProjectionElem::Downcast(..)
-            | ProjectionElem::OpaqueCast(_)
-            | ProjectionElem::Subtype(_) => {}
+            ProjectionElem::Downcast(..) | ProjectionElem::OpaqueCast(_) => {}
         }
     }
     borrow_id
@@ -382,12 +379,7 @@ pub(crate) fn projections_term<'tcx, 'a, V: Debug>(
             (ProjectionElem::ConstantIndex { .. } | ProjectionElem::Subslice { .. }, _) => {
                 ctx.dcx().span_bug(span, "Array and slice patterns are currently not supported")
             }
-            (
-                ProjectionElem::OpaqueCast(_)
-                | ProjectionElem::Subtype(_)
-                | ProjectionElem::UnwrapUnsafeBinder(_),
-                _,
-            ) => {
+            (ProjectionElem::OpaqueCast(_) | ProjectionElem::UnwrapUnsafeBinder(_), _) => {
                 unreachable!("{el:?} unsupported projection.")
             }
         }

creusot/src/callbacks.rs

@@ -4,7 +4,6 @@ use rustc_driver::{Callbacks, Compilation};
 use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_interface::{Config, interface::Compiler};
 use rustc_middle::{mir, ty::TyCtxt};
-use rustc_span::ErrorGuaranteed;
 
 use std::{cell::RefCell, collections::HashMap, thread_local};
 
@@ -71,28 +70,43 @@ impl Callbacks for ToWhy {
     fn config(&mut self, config: &mut Config) {
         self.set_output_dir(config);
 
-        // HACK: remove this once `config.locale_resources` is defined as a Vec
-        let mut locale_resources = config.locale_resources.to_vec();
-        locale_resources.push(crate::DEFAULT_LOCALE_RESOURCE);
-        config.locale_resources = locale_resources;
+        config.locale_resources.push(crate::DEFAULT_LOCALE_RESOURCE);
         config.override_queries = Some(|_sess, providers| {
+            // Remove MIR of Pearlite code (logic functions, contracts, assertions, snapshots)
+            // One might wonder why not override `mir_promoted` instead: that would be too late because
+            // drops are inserted then, and that results in errors because many types are not Drop.
             providers.mir_built = |tcx, def_id| {
                 let mir = (rustc_interface::DEFAULT_QUERY_PROVIDERS.mir_built)(tcx, def_id);
                 let mut mir = mir.steal();
-                cleanup_spec_closures(tcx, def_id.to_def_id(), &mut mir);
+                cleanup_spec_closures(tcx, def_id, &mut mir);
                 tcx.alloc_steal_mir(mir)
             };
 
+            // Store borrow-checked bodies for translation
+            providers.mir_borrowck = |tcx, local_id| {
+                copy_mir_bodies(tcx, local_id);
+                (rustc_interface::DEFAULT_QUERY_PROVIDERS.mir_borrowck)(tcx, local_id)
+            };
+
+            // The `check_liveness` query is where unused variable warnings are emitted.
+            // We reintroduce the MIR of Pearlite code for this analysis.
+            // Then we remove it again for good.
+            providers.check_liveness = |tcx, local_id| {
+                restore_mir_for_liveness_check(tcx, local_id);
+                let value =
+                    (rustc_interface::DEFAULT_QUERY_PROVIDERS.check_liveness)(tcx, local_id);
+                cleanup_spec_closures_final(tcx, local_id);
+                value
+            };
+
+            // Remove ghost code for codegen
             providers.mir_drops_elaborated_and_const_checked = |tcx, def_id| {
                 let mir = (rustc_interface::DEFAULT_QUERY_PROVIDERS
                     .mir_drops_elaborated_and_const_checked)(tcx, def_id);
                 let mut mir = mir.steal();
                 remove_ghost_closures(tcx, &mut mir);
                 tcx.alloc_steal_mir(mir)
             };
-
-            providers.mir_borrowck = |tcx, def_id| mir_borrowck(tcx, def_id);
-            // TODO override mir_borrowck_const_arg
         });
 
         let previous = config.register_lints.take();
@@ -115,10 +129,7 @@ impl Callbacks for ToWhy {
     }
 }
 
-fn mir_borrowck<'tcx, 'a>(
-    tcx: TyCtxt<'tcx>,
-    def_id: LocalDefId,
-) -> Result<&'a mir::DefinitionSiteHiddenTypes<'tcx>, ErrorGuaranteed> {
+fn copy_mir_bodies<'tcx, 'a>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) {
     let opts = ConsumerOptions::RegionInferenceContext;
     let bodies_with_facts =
         rustc_borrowck::consumers::get_bodies_with_borrowck_facts(tcx, def_id, opts);
@@ -144,13 +155,10 @@ fn mir_borrowck<'tcx, 'a>(
             assert!(map.insert(def_id, body).is_none());
         }
     });
-
-    (rustc_interface::DEFAULT_QUERY_PROVIDERS.mir_borrowck)(tcx, def_id)
 }
 
 /// Try to retrieve the promoted MIR for a body from a thread local cache.
 /// The cache is populated when rustc runs the `mir_borrowck` query.
-/// After a body was retrieved, calling this function again for the same `def_id` will return `None`.
 pub fn get_body<'tcx, 'a>(
     tcx: TyCtxt<'tcx>,
     def_id: LocalDefId,