update to 6/10

Author: Carolyn Zech

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/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

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/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

rust-toolchain.toml

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