Upgrade Rust toolchain to 2025-12-31

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

@@ -1708,6 +1708,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             Operand::Constant(constant) => CharonOperand::Const(self.translate_constant(constant)),
             Operand::Copy(place) => CharonOperand::Copy(self.translate_place(&place)),
             Operand::Move(place) => CharonOperand::Move(self.translate_place(&place)),
+            // `Operand::RuntimeChecks` (rust-lang/rust#148766) is not yet modeled by the
+            // experimental LLBC backend.
+            Operand::RuntimeChecks(_) => todo!(),
         }
     }
 

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

@@ -70,7 +70,14 @@ impl GotocCtx<'_, '_> {
                 Some(format!(
                     "{}:{}",
                     loc.filename().expect("recursion location wrapper should have a file name"),
-                    static_item.name(),
+                    // The `--nondet-static-exclude` value must match the static's
+                    // pretty name in the goto model. Since rust-lang/rust#149401,
+                    // `name()` is crate-qualified for local items, but the pretty
+                    // name is kept crate-relative (see `readable_name`), so strip
+                    // the crate prefix here too; otherwise the recursion tracker
+                    // `REENTRY` is not excluded from `--nondet-static` and gets
+                    // havocked, breaking contract-recursion checking.
+                    crate::kani_middle::strip_local_crate_prefix(static_item.name()),
                 ))
             } else {
                 None

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

@@ -5,6 +5,7 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
+use crate::kani_middle::readable_name;
 use cbmc::InternString;
 use cbmc::InternedString;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
@@ -32,7 +33,13 @@ impl GotocCtx<'_, '_> {
             }
             let base_name = self.codegen_var_base_name(&lc);
             let name = self.codegen_var_name(&lc);
-            let var_type = self.codegen_ty_stable(ldata.ty);
+            // Unsized-by-value arguments (`unsized_fn_params`) are represented as fat pointers,
+            // consistent with `fn_typ` and `codegen_local`.
+            let var_type = if self.is_unsized_by_value_arg(lc) {
+                self.codegen_ty_ref_stable(ldata.ty)
+            } else {
+                self.codegen_ty_stable(ldata.ty)
+            };
             let loc = self.codegen_span_stable(ldata.span);
             // Indices [1, N] represent the function parameters where N is the number of parameters.
             // Except that ZST fields are not included as parameters.
@@ -220,7 +227,7 @@ impl GotocCtx<'_, '_> {
             &fname,
             self.fn_typ(instance, &body),
             None,
-            instance.name(),
+            readable_name(instance),
             self.codegen_span_stable(instance.def.span()),
         );
         if !self.symbol_table.contains((&fname).into()) {

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

@@ -43,19 +43,24 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
                     self,
                     self.codegen_place_stable(place, Location::none())
                 );
-                // If the operand itself is a Dynamic (like when passing a boxed closure),
-                // we need to pull off the fat pointer. In that case, the rustc kind() on
-                // both the operand and the inner type are Dynamic.
-                // Consider moving this check elsewhere in:
-                // https://github.com/model-checking/kani/issues/277
+                // If the operand is itself an unsized value passed by value (a `Dynamic` boxed
+                // closure, or a slice/`str` via `unsized_fn_params`), the value is the fat
+                // pointer, so pull it off the projection rather than the (pointee) goto_expr.
                 match self.operand_ty_stable(operand).kind() {
-                    TyKind::RigidTy(RigidTy::Dynamic(..)) => projection.fat_ptr_goto_expr.unwrap(),
+                    TyKind::RigidTy(RigidTy::Dynamic(..))
+                    | TyKind::RigidTy(RigidTy::Slice(..))
+                    | TyKind::RigidTy(RigidTy::Str) => projection.fat_ptr_goto_expr.unwrap(),
                     _ => projection.goto_expr,
                 }
             }
             Operand::Constant(constant) => {
                 self.codegen_const(&constant.const_, self.codegen_span_stable(constant.span))
             }
+            // Runtime checks (`ub_checks()`, `contract_checks()`, `overflow_checks()`) were
+            // moved from `Rvalue::NullaryOp(NullOp::RuntimeChecks(..))` to `Operand::RuntimeChecks`
+            // by rust-lang/rust#148766. Kani does not enable these source-level checks (it inserts
+            // its own), so evaluate them to `false` as before.
+            Operand::RuntimeChecks(_) => Expr::c_false(),
         }
     }
 

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

@@ -397,7 +397,27 @@ impl GotocCtx<'_, '_> {
 
         // Otherwise, simply look up the local by the var name.
         let vname = self.codegen_var_name(&l);
-        Expr::symbol_expression(vname, self.codegen_ty_stable(local_ty))
+        // Unsized-by-value arguments (`unsized_fn_params`, e.g. `fn f(self: [T])`) are
+        // represented as fat pointers rather than as the (incomplete) unsized type itself.
+        // See `fn_typ` and `codegen_declare_variables`.
+        let typ = if self.is_unsized_by_value_arg(l) {
+            self.codegen_ty_ref_stable(local_ty)
+        } else {
+            self.codegen_ty_stable(local_ty)
+        };
+        Expr::symbol_expression(vname, typ)
+    }
+
+    /// Returns true if `local` is a by-value function argument of an unsized type
+    /// (via the `unsized_fn_params` feature, e.g. `fn f(self: [T])` or `fn f(self: str)`).
+    ///
+    /// Such arguments cannot be represented directly (the unsized type codegens to an
+    /// incomplete `FlexibleArray`, which cannot be a function parameter or carry the
+    /// length/vtable metadata), so Kani represents them as fat pointers.
+    pub fn is_unsized_by_value_arg(&self, local: Local) -> bool {
+        local >= 1
+            && local <= self.current_fn().arg_count()
+            && self.is_unsized(rustc_internal::internal(self.tcx, self.local_ty_stable(local)))
     }
 
     /// A projection is an operation that translates an lvalue to another lvalue.
@@ -684,7 +704,11 @@ impl GotocCtx<'_, '_> {
                 // Just return the address of the place dereferenced.
                 address_of
             }
-        } else if place_ty == pointee_type(self.local_ty_stable(place.local)).unwrap() {
+        } else if self.is_unsized_by_value_arg(place.local) && place.projection.is_empty() {
+            // `&self` where `self` is an unsized-by-value argument: the reference is the
+            // fat pointer that the argument is represented by (see `codegen_place_stable`).
+            projection.fat_ptr_goto_expr.unwrap()
+        } else if pointee_type(self.local_ty_stable(place.local)).is_some_and(|p| place_ty == p) {
             // Just return the fat pointer if this is a simple &(*local).
             projection.fat_ptr_goto_expr.unwrap()
         } else {
@@ -716,10 +740,21 @@ impl GotocCtx<'_, '_> {
     ) -> Result<ProjectedPlace, Box<UnimplementedData>> {
         debug!(?place, "codegen_place");
         let initial_expr = self.codegen_local(place.local, loc);
-        let initial_typ = TypeOrVariant::Type(self.local_ty_stable(place.local));
-        debug!(?initial_typ, ?initial_expr, "codegen_place");
-        let initial_projection =
-            ProjectedPlace::try_new(initial_expr, initial_typ, None, None, self);
+        let local_ty = self.local_ty_stable(place.local);
+        let initial_projection = if self.is_unsized_by_value_arg(place.local) {
+            // The local holds a fat pointer to the unsized value (see `codegen_local`).
+            // Model the place as the pointee of that fat pointer, i.e. `*(&local)`, by
+            // treating the local as a value of pointer type and applying a `Deref`
+            // projection. This reuses the existing fat-pointer projection logic so that
+            // reads, indexing, and `&self` recover the data pointer and length/vtable.
+            let ptr_ty = Ty::new_ptr(local_ty, Mutability::Not);
+            let base = ProjectedPlace::try_from_ty(initial_expr, ptr_ty, self);
+            self.codegen_projection(base, &ProjectionElem::Deref, loc)
+        } else {
+            let initial_typ = TypeOrVariant::Type(local_ty);
+            ProjectedPlace::try_new(initial_expr, initial_typ, None, None, self)
+        };
+        debug!(?local_ty, ?initial_projection, "codegen_place");
         let result = place
             .projection
             .iter()

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

@@ -23,7 +23,7 @@ use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_public::abi::{Primitive, Scalar, ValueAbi};
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{
-    AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
+    AggregateKind, BinOp, CastKind, Operand, Place, PointerCoercion, Rvalue, UnOp,
 };
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
@@ -824,7 +824,6 @@ impl GotocCtx<'_, '_> {
             Rvalue::CheckedBinaryOp(op, e1, e2) => {
                 self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty)
             }
-            Rvalue::NullaryOp(NullOp::RuntimeChecks(_)) => Expr::c_false(),
             Rvalue::ShallowInitBox(operand, content_ty) => {
                 // The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box<T>.
                 // See https://github.com/rust-lang/compiler-team/issues/460 for more details.
@@ -1321,7 +1320,7 @@ impl GotocCtx<'_, '_> {
     ) -> Expr {
         debug!(cast=?coercion, op=?operand, ?loc, "codegen_pointer_cast");
         match coercion {
-            PointerCoercion::ReifyFnPointer => match self.operand_ty_stable(operand).kind() {
+            PointerCoercion::ReifyFnPointer(_) => match self.operand_ty_stable(operand).kind() {
                 TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
                     let instance = Instance::resolve(def, &args).unwrap();
                     // We need to handle this case in a special way because `codegen_operand_stable` compiles FnDefs to dummy structs.

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

@@ -26,6 +26,9 @@ impl Debug for SourceRegion {
     }
 }
 
+// The `Err` type of `span_to_source`'s callback is rustc's `SpanSnippetError`,
+// which clippy now flags as large; we cannot shrink it, so allow the lint.
+#[allow(clippy::result_large_err)]
 fn ensure_non_empty_span(source_map: &SourceMap, span: Span) -> Option<Span> {
     if !span.is_empty() {
         return Some(span);

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

@@ -4,7 +4,7 @@
 //! This file contains functions related to codegenning MIR static variables into gotoc
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use crate::kani_middle::is_interior_mut;
+use crate::kani_middle::{is_interior_mut, readable_name};
 use rustc_public::CrateDef;
 use rustc_public::mir::mono::{Instance, StaticDef};
 use tracing::debug;
@@ -34,7 +34,7 @@ impl GotocCtx<'_, '_> {
         // Unique mangled monomorphized name.
         let symbol_name = instance.mangled_name();
         // Pretty name which may include function name.
-        let pretty_name = instance.name();
+        let pretty_name = readable_name(instance);
         debug!(?def, ?symbol_name, ?pretty_name, "declare_static");
 
         let typ = self.codegen_ty_stable(instance.ty());

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

@@ -771,9 +771,9 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         match &layout.fields {
-            FieldsShape::Arbitrary { offsets, memory_index } => {
+            FieldsShape::Arbitrary { offsets, in_memory_order } => {
                 assert_eq!(flds.len(), offsets.len());
-                assert_eq!(offsets.len(), memory_index.len());
+                assert_eq!(offsets.len(), in_memory_order.len());
                 let mut final_fields = Vec::with_capacity(flds.len());
                 let mut offset = initial_offset;
                 for idx in layout.fields.index_by_increasing_offset() {
@@ -1591,10 +1591,16 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
                         let (name, _) = self.codegen_spread_arg_name(&lc);
                         ident = name;
                     }
-                    Some(
+                    // Unsized-by-value arguments (`unsized_fn_params`, e.g. `fn f(self: [T])`)
+                    // cannot be a parameter of their (incomplete) unsized type, and the length /
+                    // vtable metadata must be carried somewhere, so represent them as fat pointers.
+                    // `codegen_local` / `codegen_place_stable` recover the pointee accordingly.
+                    let param_ty = if self.is_unsized(rustc_internal::internal(self.tcx, ty)) {
+                        self.codegen_ty_ref_stable(ty)
+                    } else {
                         self.codegen_ty_stable(ty)
-                            .as_parameter(Some(ident.clone().into()), Some(ident.into())),
-                    )
+                    };
+                    Some(param_ty.as_parameter(Some(ident.clone().into()), Some(ident.into())))
                 }
             })
             .collect();

kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs

@@ -24,6 +24,8 @@ pub struct CurrentFnCtx<'tcx> {
     instance_internal: InstanceInternal<'tcx>,
     /// A list of local declarations used to retrieve MIR component types.
     locals: Vec<LocalDecl>,
+    /// The number of formal arguments of the current function (locals `1..=arg_count`).
+    arg_count: usize,
     /// A list of pretty names for locals that corrspond to user variables.
     local_names: HashMap<Local, InternedString>,
     /// Collection of variables that are used in a reference or address-of expression.
@@ -58,9 +60,10 @@ impl MirVisitor for AddressTakenLocalsCollector {
 impl<'tcx> CurrentFnCtx<'tcx> {
     pub fn new(instance: Instance, gcx: &GotocCtx<'tcx, '_>, body: &Body) -> Self {
         let instance_internal = rustc_internal::internal(gcx.tcx, instance);
-        let readable_name = instance.name();
+        let readable_name = crate::kani_middle::readable_name(instance);
         let name = instance.mangled_name();
         let locals = body.locals().to_vec();
+        let arg_count = body.arg_locals().len();
         let local_names = body
             .var_debug_info
             .iter()
@@ -74,6 +77,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
             instance_internal,
             krate: instance.def.krate().name,
             locals,
+            arg_count,
             local_names,
             address_taken_locals: visitor.address_taken_locals,
             name,
@@ -126,6 +130,12 @@ impl<'tcx> CurrentFnCtx<'tcx> {
         &self.locals
     }
 
+    /// The number of formal arguments of the current function; locals `1..=arg_count()`
+    /// are the arguments.
+    pub fn arg_count(&self) -> usize {
+        self.arg_count
+    }
+
     pub fn local_name(&self, local: Local) -> Option<InternedString> {
         self.local_names.get(&local).copied()
     }

kani-compiler/src/kani_middle/analysis.rs

@@ -168,7 +168,6 @@ impl From<&Rvalue> for Key {
             Rvalue::Cast(_, _, _) => Key("Cast"),
             Rvalue::BinaryOp(..) => Key("BinaryOp"),
             Rvalue::CheckedBinaryOp(..) => Key("CheckedBinaryOp"),
-            Rvalue::NullaryOp(_) => Key("NullaryOp"),
             Rvalue::UnaryOp(_, _) => Key("UnaryOp"),
             Rvalue::Discriminant(_) => Key("Discriminant"),
             Rvalue::Aggregate(_, _) => Key("Aggregate"),

kani-compiler/src/kani_middle/attributes.rs

@@ -833,15 +833,15 @@ impl<'tcx> KaniAttributes<'tcx> {
                                     rustc_internal::internal(self.tcx, original_res.span()),
                                     format!(
                                     "`{}` does not have a body",
-                                    original_res.name()
+                                    crate::kani_middle::strip_local_crate_prefix(original_res.name())
                                 ));
                             }
                             if r_bad {
                                 err = err.with_span_note(
                                     rustc_internal::internal(self.tcx, replace_res.span()),
                                     format!(
                                     "`{}` does not have a body",
-                                    replace_res.name()
+                                    crate::kani_middle::strip_local_crate_prefix(replace_res.name())
                                 ));
                             }
                             err = err.with_help(

kani-compiler/src/kani_middle/codegen_units.rs

@@ -106,7 +106,10 @@ impl CodegenUnits {
                 );
                 AUTOHARNESS_MD
                     .set(AutoHarnessMetadata {
-                        chosen: chosen.iter().map(|func| func.name()).collect::<BTreeSet<_>>(),
+                        chosen: chosen
+                            .iter()
+                            .map(|func| crate::kani_middle::strip_local_crate_prefix(func.name()))
+                            .collect::<BTreeSet<_>>(),
                         skipped,
                     })
                     .expect("Initializing the autoharness metadata failed");
@@ -301,7 +304,7 @@ fn apply_transitivity(tcx: TyCtxt, harness: Harness, stubs: Stubs) -> Stubs {
                     format!(
                         "Cannot stub `{}`. Stub configuration for harness `{}` has a cycle",
                         orig.name(),
-                        harness.def.name(),
+                        crate::kani_middle::strip_local_crate_prefix(harness.def.name()),
                     ),
                 );
                 break;
@@ -452,7 +455,12 @@ fn automatic_harness_partition(
         }
 
         // Preprend the crate name so that users can filter out entire crates using the existing function filter flags.
-        let name = format!("{crate_name}::{}", instance.name());
+        // `instance.name()` is already crate-qualified for local items (rust-lang/rust#149401),
+        // so strip that prefix first to avoid double-qualifying (`crate::crate::fn`).
+        let name = format!(
+            "{crate_name}::{}",
+            crate::kani_middle::strip_local_crate_prefix(instance.name())
+        );
         let body = instance.body().unwrap();
 
         if is_proof_harness(tcx, instance)
@@ -503,7 +511,7 @@ fn automatic_harness_partition(
 
     for func in crate_fns {
         if let Some(reason) = skip_reason(func) {
-            skipped.insert(func.name(), reason);
+            skipped.insert(crate::kani_middle::strip_local_crate_prefix(func.name()), reason);
         } else {
             chosen.push(Instance::try_from(func).unwrap());
         }