Update toolchain to 2025-06-13

cprover_bindings/src/irep/irep_id.rs

@@ -887,7 +887,7 @@ impl ToString for IrepId {
 }
 
 impl IrepId {
-    pub fn to_string_cow(&self) -> Cow<str> {
+    pub fn to_string_cow(&self) -> Cow<'_, str> {
         match self.to_owned_string() {
             Some(owned) => Cow::Owned(owned),
             None => Cow::Borrowed(self.to_static_string()),

docs/src/rust-feature-support/intrinsics.md

@@ -187,7 +187,6 @@ powf32 | Partial | Results are overapproximated |
 powf64 | Partial | Results are overapproximated |
 powif32 | Partial | Results are overapproximated |
 powif64 | Partial | Results are overapproximated |
-pref_align_of | Yes | |
 prefetch_read_data | No | |
 prefetch_read_instruction | No | |
 prefetch_write_data | No | |

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

@@ -419,7 +419,6 @@ impl GotocCtx<'_> {
             Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
             Intrinsic::PowIF32 => codegen_simple_intrinsic!(Powif),
             Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi),
-            Intrinsic::PrefAlignOf => codegen_intrinsic_const!(),
             Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
             Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
             Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc),

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

@@ -519,7 +519,7 @@ impl GotocCtx<'_> {
                 .index_by_increasing_offset()
                 .map(|idx| {
                     let field_ty = layout.field(self, idx).ty;
-                    if idx == *discriminant_field {
+                    if idx == (*discriminant_field).as_usize() {
                         Expr::int_constant(0, self.codegen_ty(field_ty))
                     } else {
                         self.codegen_operand_stable(&operands[idx])

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

@@ -914,7 +914,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     pretty_name,
                     type_and_layout,
                     "DirectFields".into(),
-                    Some(*discriminant_field),
+                    Some((*discriminant_field).as_usize()),
                 ),
             };
             let mut fields = vec![direct_fields];
@@ -1277,7 +1277,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // Contrary to coroutines, currently enums have only one field (the discriminant), the rest are in the variants:
                 assert!(layout.fields.count() <= 1);
                 // Contrary to coroutines, the discriminant is the first (and only) field for enums:
-                assert_eq!(*tag_field, 0);
+                assert_eq!((*tag_field).as_usize(), 0);
                 match tag_encoding {
                     TagEncoding::Direct => {
                         self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, name| {

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -20,7 +20,7 @@ use cbmc::{InternedString, MachineModel};
 use kani_metadata::artifact::convert_type;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature};
 use kani_metadata::{AssignsContract, CompilerArtifactStub};
-use rustc_abi::Endian;
+use rustc_abi::{Align, Endian};
 use rustc_codegen_ssa::back::archive::{
     ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER,
 };
@@ -511,10 +511,11 @@ fn check_options(session: &Session) {
     // a valid CBMC machine model in function `machine_model_from_session` from
     // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
     match session.target.options.min_global_align {
-        Some(1) => (),
+        Some(Align::ONE) => (),
         Some(align) => {
             let err_msg = format!(
-                "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}."
+                "Kani requires the target architecture option `min_global_align` to be 1, but it is {}.",
+                align.bytes()
             );
             session.dcx().err(err_msg);
         }
@@ -705,7 +706,7 @@ fn new_machine_model(sess: &Session) -> MachineModel {
     // We check these options in function `check_options` from
     // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
     // and error if their values are not the ones we expect.
-    let alignment = sess.target.options.min_global_align.unwrap_or(1);
+    let alignment = sess.target.options.min_global_align.map_or(1, |align| align.bytes());
     let is_big_endian = match sess.target.options.endian {
         Endian::Little => false,
         Endian::Big => true,

kani-compiler/src/intrinsics.rs

@@ -91,7 +91,6 @@ pub enum Intrinsic {
     PowF64,
     PowIF32,
     PowIF64,
-    PrefAlignOf,
     PtrGuaranteedCmp,
     PtrOffsetFrom,
     PtrOffsetFromUnsigned,
@@ -330,10 +329,6 @@ impl Intrinsic {
             "offset" => unreachable!(
                 "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
             ),
-            "pref_align_of" => {
-                assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize));
-                Self::PrefAlignOf
-            }
             "ptr_guaranteed_cmp" => {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::U8));
                 Self::PtrGuaranteedCmp
@@ -471,55 +466,55 @@ impl Intrinsic {
 fn try_match_atomic(intrinsic_instance: &Instance) -> Option<Intrinsic> {
     let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap();
     let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder();
-    if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and_") {
+    if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicAnd(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
         Some(Intrinsic::AtomicCxchgWeak(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
         Some(Intrinsic::AtomicCxchg(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence") {
         assert_sig_matches!(sig, => RigidTy::Tuple(_));
         Some(Intrinsic::AtomicFence(suffix.into()))
     } else if intrinsic_str == "atomic_load" {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
         Some(Intrinsic::AtomicLoad)
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicMax(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicMin(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicNand(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicOr(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence") {
         assert_sig_matches!(sig, => RigidTy::Tuple(_));
         Some(Intrinsic::AtomicSingleThreadFence(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_));
         Some(Intrinsic::AtomicStore(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicUmax(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicUmin(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicXadd(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicXchg(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicXor(suffix.into()))
-    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub_") {
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub") {
         assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
         Some(Intrinsic::AtomicXsub(suffix.into()))
     } else {

kani-compiler/src/kani_middle/coercion.rs

@@ -19,6 +19,7 @@ use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::{PseudoCanonicalInput, Ty, TyCtxt, TypingEnv};
 use rustc_smir::rustc_internal;
+use rustc_span::DUMMY_SP;
 use stable_mir::Symbol;
 use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 use tracing::trace;
@@ -245,7 +246,7 @@ fn custom_coerce_unsize_info<'tcx>(
     source_ty: Ty<'tcx>,
     target_ty: Ty<'tcx>,
 ) -> CustomCoerceUnsized {
-    let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None);
+    let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, DUMMY_SP);
 
     let trait_ref = TraitRef::new(tcx, def_id, tcx.mk_args_trait(source_ty, [target_ty.into()]));
 

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

@@ -669,7 +669,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::PowF64
         | Intrinsic::PowIF32
         | Intrinsic::PowIF64
-        | Intrinsic::PrefAlignOf
         | Intrinsic::PtrGuaranteedCmp
         | Intrinsic::PtrOffsetFrom
         | Intrinsic::PtrOffsetFromUnsigned

kani-compiler/src/kani_middle/provide.rs

@@ -28,15 +28,15 @@ fn should_override(args: &Arguments) -> bool {
 
 /// Returns the optimized code for the external function associated with `def_id` by
 /// running rustc's optimization passes followed by Kani-specific passes.
-fn run_mir_passes_extern(tcx: TyCtxt, def_id: DefId) -> &Body {
+fn run_mir_passes_extern(tcx: TyCtxt<'_>, def_id: DefId) -> &Body<'_> {
     tracing::debug!(?def_id, "run_mir_passes_extern");
     let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.extern_queries.optimized_mir)(tcx, def_id);
     run_kani_mir_passes(tcx, def_id, body)
 }
 
 /// Returns the optimized code for the local function associated with `def_id` by
 /// running rustc's optimization passes followed by Kani-specific passes.
-fn run_mir_passes(tcx: TyCtxt, def_id: LocalDefId) -> &Body {
+fn run_mir_passes(tcx: TyCtxt<'_>, def_id: LocalDefId) -> &Body<'_> {
     tracing::debug!(?def_id, "run_mir_passes");
     let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir)(tcx, def_id);
     run_kani_mir_passes(tcx, def_id.to_def_id(), body)

kani-compiler/src/kani_middle/resolve.rs

@@ -434,7 +434,9 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R
         let item = tcx.hir_item(item_id);
         if item.kind.ident().is_some_and(|ident| ident.as_str() == name) {
             match item.kind {
-                ItemKind::Use(use_path, UseKind::Single(_)) => use_path.res[0].opt_def_id(),
+                ItemKind::Use(use_path, UseKind::Single(_)) => {
+                    use_path.res.present_items().filter_map(|res| res.opt_def_id()).next()
+                }
                 ItemKind::ExternCrate(orig_name, _) => resolve_external(
                     tcx,
                     orig_name.as_ref().map(|sym| sym.as_str()).unwrap_or(name),
@@ -445,7 +447,7 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R
             if let ItemKind::Use(use_path, UseKind::Glob) = item.kind {
                 // Do not immediately try to resolve the path using this glob,
                 // since paths resolved via non-globs take precedence.
-                glob_imports.push(use_path.res[0]);
+                glob_imports.extend(use_path.res.present_items());
             }
             None
         }

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs

@@ -629,7 +629,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::PowF64
         | Intrinsic::PowIF32
         | Intrinsic::PowIF64
-        | Intrinsic::PrefAlignOf
         | Intrinsic::RawEq
         | Intrinsic::RotateLeft
         | Intrinsic::RotateRight

library/kani_macros/src/sysroot/contracts/helpers.rs

@@ -10,7 +10,7 @@ use syn::spanned::Spanned;
 use syn::{Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt, parse_quote};
 
 /// If an explicit return type was provided it is returned, otherwise `()`.
-pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow<syn::Type> {
+pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow<'_, syn::Type> {
     match return_type {
         syn::ReturnType::Default => Cow::Owned(syn::Type::Tuple(syn::TypeTuple {
             paren_token: syn::token::Paren::default(),

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-06-03"
+channel = "nightly-2025-06-13"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/arbitrary/ptrs/pointer_generator_error.expected

@@ -1,6 +1,9 @@
-error[E0080]: evaluation of `kani::PointerGenerator::<0>::VALID` failed\
+error[E0080]: evaluation panicked: PointerGenerator requires at least one byte.\
 
-evaluation panicked: PointerGenerator requires at least one byte.\
+|\
+| kani_core::kani_lib!(kani);\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation of `kani::PointerGenerator::<0>::VALID` failed here\
+|\
 
 note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\
 pointer_generator_error.rs\

tests/expected/uninit/atomic/atomic.rs

@@ -5,7 +5,7 @@
 #![feature(core_intrinsics)]
 
 use std::alloc::{Layout, alloc};
-use std::sync::atomic::{AtomicU8, Ordering};
+use std::intrinsics::{AtomicOrdering, atomic_cxchg, atomic_load, atomic_store};
 
 // Checks if memory initialization checks correctly fail when uninitialized memory is passed to
 // atomic intrinsics.
@@ -18,15 +18,15 @@ fn local_atomic_uninit() {
     unsafe {
         match kani::any() {
             0 => {
-                std::intrinsics::atomic_store_relaxed(ptr, 1);
+                atomic_store::<_, { AtomicOrdering::Relaxed }>(ptr, 1);
             }
             1 => {
-                std::intrinsics::atomic_load::<_, { std::intrinsics::AtomicOrdering::Relaxed }>(
-                    ptr as *const u8,
-                );
+                atomic_load::<_, { AtomicOrdering::Relaxed }>(ptr as *const u8);
             }
             _ => {
-                std::intrinsics::atomic_cxchg_relaxed_relaxed(ptr, 1, 1);
+                atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>(
+                    ptr, 1, 1,
+                );
             }
         };
     }

tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs

@@ -5,10 +5,7 @@
 // expected result.
 
 #![feature(core_intrinsics)]
-use std::intrinsics::{
-    atomic_xadd_acqrel, atomic_xadd_acquire, atomic_xadd_relaxed, atomic_xadd_release,
-    atomic_xadd_seqcst,
-};
+use std::intrinsics::{AtomicOrdering, atomic_xadd};
 
 #[kani::proof]
 fn main() {
@@ -28,11 +25,11 @@ fn main() {
     let c = 1 as u8;
 
     unsafe {
-        let x1 = atomic_xadd_seqcst(ptr_a1, b);
-        let x2 = atomic_xadd_acquire(ptr_a2, b);
-        let x3 = atomic_xadd_acqrel(ptr_a3, b);
-        let x4 = atomic_xadd_release(ptr_a4, b);
-        let x5 = atomic_xadd_relaxed(ptr_a5, b);
+        let x1 = atomic_xadd::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_xadd::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_xadd::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_xadd::<_, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_xadd::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 0);
         assert!(x2 == 0);

tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs

@@ -5,10 +5,7 @@
 // expected result.
 
 #![feature(core_intrinsics)]
-use std::intrinsics::{
-    atomic_and_acqrel, atomic_and_acquire, atomic_and_relaxed, atomic_and_release,
-    atomic_and_seqcst,
-};
+use std::intrinsics::{AtomicOrdering, atomic_and};
 
 #[kani::proof]
 fn main() {
@@ -27,11 +24,11 @@ fn main() {
     let b = 0 as u8;
 
     unsafe {
-        let x1 = atomic_and_seqcst(ptr_a1, b);
-        let x2 = atomic_and_acquire(ptr_a2, b);
-        let x3 = atomic_and_acqrel(ptr_a3, b);
-        let x4 = atomic_and_release(ptr_a4, b);
-        let x5 = atomic_and_relaxed(ptr_a5, b);
+        let x1 = atomic_and::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_and::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_and::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_and::<_, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_and::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 1);
         assert!(x2 == 1);