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

@@ -302,27 +302,25 @@ impl GotocCtx<'_> {
                 "Rust intrinsic assumption failed",
                 loc,
             ),
-            Intrinsic::AtomicAnd(_) => codegen_atomic_binop!(bitand),
-            Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => {
+            Intrinsic::AtomicAnd => codegen_atomic_binop!(bitand),
+            Intrinsic::AtomicCxchg | Intrinsic::AtomicCxchgWeak => {
                 self.codegen_atomic_cxchg(intrinsic_str, fargs, place, loc)
             }
 
-            Intrinsic::AtomicFence(_) => self.codegen_atomic_noop(intrinsic_str, loc),
+            Intrinsic::AtomicFence => self.codegen_atomic_noop(intrinsic_str, loc),
             Intrinsic::AtomicLoad => self.codegen_atomic_load(intrinsic_str, fargs, place, loc),
-            Intrinsic::AtomicMax(_) => codegen_atomic_binop!(max),
-            Intrinsic::AtomicMin(_) => codegen_atomic_binop!(min),
-            Intrinsic::AtomicNand(_) => codegen_atomic_binop!(bitnand),
-            Intrinsic::AtomicOr(_) => codegen_atomic_binop!(bitor),
-            Intrinsic::AtomicSingleThreadFence(_) => self.codegen_atomic_noop(intrinsic_str, loc),
-            Intrinsic::AtomicStore(_) => {
-                self.codegen_atomic_store(intrinsic_str, fargs, place, loc)
-            }
-            Intrinsic::AtomicUmax(_) => codegen_atomic_binop!(max),
-            Intrinsic::AtomicUmin(_) => codegen_atomic_binop!(min),
-            Intrinsic::AtomicXadd(_) => codegen_atomic_binop!(plus),
-            Intrinsic::AtomicXchg(_) => self.codegen_atomic_store(intrinsic_str, fargs, place, loc),
-            Intrinsic::AtomicXor(_) => codegen_atomic_binop!(bitxor),
-            Intrinsic::AtomicXsub(_) => codegen_atomic_binop!(sub),
+            Intrinsic::AtomicMax => codegen_atomic_binop!(max),
+            Intrinsic::AtomicMin => codegen_atomic_binop!(min),
+            Intrinsic::AtomicNand => codegen_atomic_binop!(bitnand),
+            Intrinsic::AtomicOr => codegen_atomic_binop!(bitor),
+            Intrinsic::AtomicSingleThreadFence => self.codegen_atomic_noop(intrinsic_str, loc),
+            Intrinsic::AtomicStore => self.codegen_atomic_store(intrinsic_str, fargs, place, loc),
+            Intrinsic::AtomicUmax => codegen_atomic_binop!(max),
+            Intrinsic::AtomicUmin => codegen_atomic_binop!(min),
+            Intrinsic::AtomicXadd => codegen_atomic_binop!(plus),
+            Intrinsic::AtomicXchg => self.codegen_atomic_store(intrinsic_str, fargs, place, loc),
+            Intrinsic::AtomicXor => codegen_atomic_binop!(bitxor),
+            Intrinsic::AtomicXsub => codegen_atomic_binop!(sub),
             Intrinsic::Bitreverse => {
                 self.codegen_expr_to_place_stable(place, fargs.remove(0).bitreverse(), loc)
             }
@@ -419,7 +417,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

@@ -19,23 +19,23 @@ pub enum Intrinsic {
     AssertMemUninitializedValid,
     AssertZeroValid,
     Assume,
-    AtomicAnd(String),
-    AtomicCxchg(String),
-    AtomicCxchgWeak(String),
-    AtomicFence(String),
+    AtomicAnd,
+    AtomicCxchg,
+    AtomicCxchgWeak,
+    AtomicFence,
     AtomicLoad,
-    AtomicMax(String),
-    AtomicMin(String),
-    AtomicNand(String),
-    AtomicOr(String),
-    AtomicSingleThreadFence(String),
-    AtomicStore(String),
-    AtomicUmax(String),
-    AtomicUmin(String),
-    AtomicXadd(String),
-    AtomicXchg(String),
-    AtomicXor(String),
-    AtomicXsub(String),
+    AtomicMax,
+    AtomicMin,
+    AtomicNand,
+    AtomicOr,
+    AtomicSingleThreadFence,
+    AtomicStore,
+    AtomicUmax,
+    AtomicUmin,
+    AtomicXadd,
+    AtomicXchg,
+    AtomicXor,
+    AtomicXsub,
     Bitreverse,
     BlackBox,
     Breakpoint,
@@ -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,59 +466,76 @@ 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_") {
-        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
-        Some(Intrinsic::AtomicAnd(suffix.into()))
-    } 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_") {
-        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_") {
-        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_") {
-        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
-        Some(Intrinsic::AtomicMax(suffix.into()))
-    } 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_") {
-        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
-        Some(Intrinsic::AtomicNand(suffix.into()))
-    } 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_") {
-        assert_sig_matches!(sig, => RigidTy::Tuple(_));
-        Some(Intrinsic::AtomicSingleThreadFence(suffix.into()))
-    } 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_") {
-        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
-        Some(Intrinsic::AtomicUmax(suffix.into()))
-    } 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_") {
-        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
-        Some(Intrinsic::AtomicXadd(suffix.into()))
-    } 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_") {
-        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
-        Some(Intrinsic::AtomicXor(suffix.into()))
-    } 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 {
-        None
+    match intrinsic_str.as_str() {
+        "atomic_and" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicAnd)
+        }
+        "atomic_cxchgweak" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
+            Some(Intrinsic::AtomicCxchgWeak)
+        }
+        "atomic_cxchg" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
+            Some(Intrinsic::AtomicCxchg)
+        }
+        "atomic_fence" => {
+            assert_sig_matches!(sig, => RigidTy::Tuple(_));
+            Some(Intrinsic::AtomicFence)
+        }
+        "atomic_load" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
+            Some(Intrinsic::AtomicLoad)
+        }
+        "atomic_max" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicMax)
+        }
+        "atomic_min" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicMin)
+        }
+        "atomic_nand" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicNand)
+        }
+        "atomic_or" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicOr)
+        }
+        "atomic_singlethreadfence" => {
+            assert_sig_matches!(sig, => RigidTy::Tuple(_));
+            Some(Intrinsic::AtomicSingleThreadFence)
+        }
+        "atomic_store" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_));
+            Some(Intrinsic::AtomicStore)
+        }
+        "atomic_umax" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicUmax)
+        }
+        "atomic_umin" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicUmin)
+        }
+        "atomic_xadd" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicXadd)
+        }
+        "atomic_xchg" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicXchg)
+        }
+        "atomic_xor" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicXor)
+        }
+        "atomic_xsub" => {
+            assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+            Some(Intrinsic::AtomicXsub)
+        }
+        _ => None,
     }
 }
 

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

@@ -218,7 +218,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
                         }
                         // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments.
                         // This is equivalent to `destination = *dst; *dst = src`.
-                        Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => {
+                        Intrinsic::AtomicCxchg | Intrinsic::AtomicCxchgWeak => {
                             let src_set = self.successors_for_operand(state, args[2].node.clone());
                             let dst_set = self.successors_for_deref(state, args[0].node.clone());
                             let destination_set = state.resolve_place(*destination, self.instance);
@@ -234,24 +234,24 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
                         }
                         // All `atomic_store` intrinsics take `dst, val` as arguments.
                         // This is equivalent to `*dst = val`.
-                        Intrinsic::AtomicStore(_) => {
+                        Intrinsic::AtomicStore => {
                             let dst_set = self.successors_for_deref(state, args[0].node.clone());
                             let val_set = self.successors_for_operand(state, args[1].node.clone());
                             state.extend(&dst_set, &val_set);
                         }
                         // All other `atomic` intrinsics take `dst, src` as arguments.
                         // This is equivalent to `destination = *dst; *dst = src`.
-                        Intrinsic::AtomicAnd(_)
-                        | Intrinsic::AtomicMax(_)
-                        | Intrinsic::AtomicMin(_)
-                        | Intrinsic::AtomicNand(_)
-                        | Intrinsic::AtomicOr(_)
-                        | Intrinsic::AtomicUmax(_)
-                        | Intrinsic::AtomicUmin(_)
-                        | Intrinsic::AtomicXadd(_)
-                        | Intrinsic::AtomicXchg(_)
-                        | Intrinsic::AtomicXor(_)
-                        | Intrinsic::AtomicXsub(_) => {
+                        Intrinsic::AtomicAnd
+                        | Intrinsic::AtomicMax
+                        | Intrinsic::AtomicMin
+                        | Intrinsic::AtomicNand
+                        | Intrinsic::AtomicOr
+                        | Intrinsic::AtomicUmax
+                        | Intrinsic::AtomicUmin
+                        | Intrinsic::AtomicXadd
+                        | Intrinsic::AtomicXchg
+                        | Intrinsic::AtomicXor
+                        | Intrinsic::AtomicXsub => {
                             let src_set = self.successors_for_operand(state, args[1].node.clone());
                             let dst_set = self.successors_for_deref(state, args[0].node.clone());
                             let destination_set = state.resolve_place(*destination, self.instance);
@@ -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
@@ -728,7 +727,7 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
             /* SIMD operations */
             true
         }
-        Intrinsic::AtomicFence(_) | Intrinsic::AtomicSingleThreadFence(_) => {
+        Intrinsic::AtomicFence | Intrinsic::AtomicSingleThreadFence => {
             /* Atomic fences */
             true
         }