Upgrade Rust toolchain to nightly-2026-06-01

cprover_bindings/src/goto_program/symbol_table.rs

@@ -54,7 +54,7 @@ impl SymbolTable {
         assert!(
             self.lookup(symbol.name).is_none(),
             "Tried to insert symbol which already existed\n\t: {:?}\n\t",
-            &symbol
+            symbol
         );
         self.symbol_table.insert(symbol.name, symbol);
     }

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -206,7 +206,7 @@ impl CodegenBackend for LlbcCodegenBackend {
         .to_owned()
     }
 
-    fn codegen_crate<'tcx>(&self, tcx: TyCtxt<'tcx>, _crate_info: &CrateInfo) -> Box<dyn Any> {
+    fn codegen_crate<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Box<dyn Any> {
         let ret_val = rustc_internal::run(tcx, || {
             // Queries shouldn't change today once codegen starts.
             let queries = QUERY_DB.with(|db| db.borrow().clone());
@@ -296,6 +296,7 @@ impl CodegenBackend for LlbcCodegenBackend {
         ongoing_codegen: Box<dyn Any>,
         _sess: &Session,
         _filenames: &OutputFilenames,
+        _crate_info: &CrateInfo,
     ) -> (CompiledModules, FxIndexMap<WorkProductId, WorkProduct>) {
         match ongoing_codegen
             .downcast::<(CompiledModules, FxIndexMap<WorkProductId, WorkProduct>)>()

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -1644,7 +1644,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     fn translate_rvalue(&mut self, rvalue: &Rvalue) -> CharonRvalue {
         trace!("translate_rvalue: {rvalue:?}");
         match rvalue {
-            Rvalue::Use(operand) => CharonRvalue::Use(self.translate_operand(operand)),
+            Rvalue::Use(operand, _) => CharonRvalue::Use(self.translate_operand(operand)),
             Rvalue::Repeat(_operand, _) => todo!(),
             Rvalue::Ref(_region, kind, place) => {
                 CharonRvalue::Ref(self.translate_place(&place), translate_borrow_kind(kind))

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -187,8 +187,8 @@ impl ProjectedPlace {
         assert!(
             Self::check_fat_ptr_typ(&fat_ptr_goto_expr, &fat_ptr_mir_typ, ctx),
             "\n{:?}\n{:?}",
-            &fat_ptr_goto_expr,
-            &fat_ptr_mir_typ
+            fat_ptr_goto_expr,
+            fat_ptr_mir_typ
         );
         Ok(ProjectedPlace { goto_expr, mir_typ_or_variant, fat_ptr_goto_expr, fat_ptr_mir_typ })
     }

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -556,6 +556,11 @@ impl GotocCtx<'_, '_> {
             let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index, loc);
             let variant_expr = variant_proj.goto_expr.clone();
             let layout = self.layout_of_stable(res_ty);
+            // `Variants::Multiple` stores a `VariantLayout`, which has no `FieldsShape` and so no
+            // field order, so ask rustc for the variant's own layout. `variant_layout` is what the
+            // type side (`codegen_enum_cases`) uses too, so the operands below are ordered exactly
+            // like the goto struct's components.
+            let variant_layout;
             let fields = match &layout.variants {
                 Variants::Empty => {
                     unreachable!("Aggregate expression for uninhabited enum with no variants")
@@ -570,8 +575,12 @@ impl GotocCtx<'_, '_> {
                     }
                     &layout.fields
                 }
-                Variants::Multiple { variants, .. } => {
-                    &variants[rustc_internal::internal(self.tcx, variant_index)].fields
+                Variants::Multiple { .. } => {
+                    variant_layout = self.variant_layout(
+                        rustc_internal::internal(self.tcx, res_ty),
+                        rustc_internal::internal(self.tcx, variant_index),
+                    );
+                    &variant_layout.fields
                 }
             };
 
@@ -749,7 +758,19 @@ impl GotocCtx<'_, '_> {
         let res_ty = self.rvalue_ty_stable(rv);
         debug!(?rv, ?res_ty, "codegen_rvalue");
         match rv {
-            Rvalue::Use(p) => self.codegen_operand_stable(p),
+            Rvalue::Use(p, _) => self.codegen_operand_stable(p),
+            // `Reborrow` is the new user-definable reborrowing of ADTs (`CoerceShared`). It is
+            // documented as a bitwise copy today, but the same docs anticipate it changing memory
+            // layout, so report it as unsupported rather than silently modelling it as a copy.
+            Rvalue::Reborrow(..) => {
+                let typ = self.codegen_ty_stable(res_ty);
+                self.codegen_unimplemented_expr(
+                    "Rvalue::Reborrow",
+                    typ,
+                    loc,
+                    "https://github.com/model-checking/kani/issues/4189",
+                )
+            }
             Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
                 let place_ref = self.codegen_place_ref_stable(p, loc);
@@ -978,8 +999,7 @@ impl GotocCtx<'_, '_> {
                     let niche_val = self.codegen_get_niche(e, offset.bytes() as usize, discr_type);
                     let relative_discr =
                         wrapping_sub(&niche_val, u64::try_from(*niche_start).unwrap());
-                    let relative_max =
-                        niche_variants.end().as_u32() - niche_variants.start().as_u32();
+                    let relative_max = niche_variants.last.as_u32() - niche_variants.start.as_u32();
                     let is_niche = if relative_max == 0 {
                         relative_discr.clone().is_zero()
                     } else {
@@ -994,7 +1014,7 @@ impl GotocCtx<'_, '_> {
                             relative_discr.cast_to(result_type.clone())
                         };
                         relative_discr.plus(Expr::int_constant(
-                            niche_variants.start().as_u32(),
+                            niche_variants.start.as_u32(),
                             result_type.clone(),
                         ))
                     };

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -305,7 +305,6 @@ impl GotocCtx<'_, '_> {
             }
             StatementKind::PlaceMention(_) => todo!(),
             StatementKind::FakeRead(..)
-            | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType { .. }
             | StatementKind::Nop
             | StatementKind::ConstEvalCounter => Stmt::skip(location),
@@ -485,7 +484,7 @@ impl GotocCtx<'_, '_> {
                         let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal);
                         let discr_ty = self.codegen_ty(discr_ty);
                         let niche_value =
-                            variant_index_internal.as_u32() - niche_variants.start().as_u32();
+                            variant_index_internal.as_u32() - niche_variants.start.as_u32();
                         let niche_value = (niche_value as u128).wrapping_add(*niche_start);
                         trace!(val=?niche_value, typ=?discr_ty, "codegen_set_discriminant niche");
                         let value = if niche_value == 0
@@ -973,7 +972,7 @@ fn collect_rvalue_places<'a>(rvalue: &'a Rvalue, places: &mut Vec<&'a Place>) {
         }
     };
     match rvalue {
-        Rvalue::Use(op)
+        Rvalue::Use(op, _)
         | Rvalue::Repeat(op, _)
         | Rvalue::Cast(_, op, _)
         | Rvalue::UnaryOp(_, op) => push_operand(op, places),
@@ -985,7 +984,8 @@ fn collect_rvalue_places<'a>(rvalue: &'a Rvalue, places: &mut Vec<&'a Place>) {
         | Rvalue::AddressOf(_, place)
         | Rvalue::Len(place)
         | Rvalue::CopyForDeref(place)
-        | Rvalue::Discriminant(place) => places.push(place),
+        | Rvalue::Discriminant(place)
+        | Rvalue::Reborrow(_, _, place) => places.push(place),
         Rvalue::Aggregate(_, operands) => {
             for op in operands {
                 push_operand(op, places);