diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 9e4c26639f88..208b43479185 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -174,8 +174,8 @@ logf32 | Partial | Results are overapproximated | logf64 | Partial | Results are overapproximated | maxnumf32 | Yes | | maxnumf64 | Yes | | -min_align_of | Yes | | -min_align_of_val | Yes | | +align_of | Yes | | +align_of_val | Yes | | minnumf32 | Yes | | minnumf64 | Yes | | move_val_init | No | | diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 613c078cac0f..0ffc0cd8d5be 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -309,11 +309,11 @@ impl Intrinsic { assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool); Self::Likely } - "min_align_of" => { + "align_of" => { assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize)); Self::MinAlignOf } - "min_align_of_val" => { + "align_of_val" => { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize)); Self::MinAlignOfVal } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index b0e88c8f2fc0..cc5085af0b9a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-13" +channel = "nightly-2025-06-16" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs index ba482248898c..83f76816f257 100644 --- a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs +++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs @@ -1,11 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that we get the expected results for the `min_align_of_val` intrinsic +// Check that we get the expected results for the `align_of_val` intrinsic // with common data types. Note that these tests assume an x86_64 architecture, // which is the only architecture supported by Kani at the moment. #![feature(core_intrinsics)] -use std::intrinsics::min_align_of_val; +use std::intrinsics::align_of_val; struct MyStruct { val: u32, @@ -26,55 +26,55 @@ fn main() { #[cfg(target_arch = "x86_64")] unsafe { // Scalar types - assert!(min_align_of_val(&0i8) == 1); - assert!(min_align_of_val(&0i16) == 2); - assert!(min_align_of_val(&0i32) == 4); - assert!(min_align_of_val(&0i64) == 8); - assert!(min_align_of_val(&0i128) == 16); - assert!(min_align_of_val(&0isize) == 8); - assert!(min_align_of_val(&0u8) == 1); - assert!(min_align_of_val(&0u16) == 2); - assert!(min_align_of_val(&0u32) == 4); - assert!(min_align_of_val(&0u64) == 8); - assert!(min_align_of_val(&0u128) == 16); - assert!(min_align_of_val(&0usize) == 8); - assert!(min_align_of_val(&0f32) == 4); - assert!(min_align_of_val(&0f64) == 8); - assert!(min_align_of_val(&false) == 1); - assert!(min_align_of_val(&(0 as char)) == 4); + assert!(align_of_val(&0i8) == 1); + assert!(align_of_val(&0i16) == 2); + assert!(align_of_val(&0i32) == 4); + assert!(align_of_val(&0i64) == 8); + assert!(align_of_val(&0i128) == 16); + assert!(align_of_val(&0isize) == 8); + assert!(align_of_val(&0u8) == 1); + assert!(align_of_val(&0u16) == 2); + assert!(align_of_val(&0u32) == 4); + assert!(align_of_val(&0u64) == 8); + assert!(align_of_val(&0u128) == 16); + assert!(align_of_val(&0usize) == 8); + assert!(align_of_val(&0f32) == 4); + assert!(align_of_val(&0f64) == 8); + assert!(align_of_val(&false) == 1); + assert!(align_of_val(&(0 as char)) == 4); // Compound types (tuple and array) - assert!(min_align_of_val(&(0i32, 0i32)) == 4); - assert!(min_align_of_val(&[0i32; 5]) == 4); + assert!(align_of_val(&(0i32, 0i32)) == 4); + assert!(align_of_val(&[0i32; 5]) == 4); // Custom data types (struct and enum) - assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4); - assert!(min_align_of_val(&MyEnum::Variant) == 1); - assert!(min_align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4); + assert!(align_of_val(&MyStruct { val: 0u32 }) == 4); + assert!(align_of_val(&MyEnum::Variant) == 1); + assert!(align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4); } #[cfg(target_arch = "aarch64")] unsafe { // Scalar types - assert!(min_align_of_val(&0i8) == 1); - assert!(min_align_of_val(&0i16) == 2); - assert!(min_align_of_val(&0i32) == 4); - assert!(min_align_of_val(&0i64) == 8); - assert!(min_align_of_val(&0i128) == 16); - assert!(min_align_of_val(&0isize) == 8); - assert!(min_align_of_val(&0u8) == 1); - assert!(min_align_of_val(&0u16) == 2); - assert!(min_align_of_val(&0u32) == 4); - assert!(min_align_of_val(&0u64) == 8); - assert!(min_align_of_val(&0u128) == 16); - assert!(min_align_of_val(&0usize) == 8); - assert!(min_align_of_val(&0f32) == 4); - assert!(min_align_of_val(&0f64) == 8); - assert!(min_align_of_val(&false) == 1); - assert!(min_align_of_val(&(0 as char)) == 4); + assert!(align_of_val(&0i8) == 1); + assert!(align_of_val(&0i16) == 2); + assert!(align_of_val(&0i32) == 4); + assert!(align_of_val(&0i64) == 8); + assert!(align_of_val(&0i128) == 16); + assert!(align_of_val(&0isize) == 8); + assert!(align_of_val(&0u8) == 1); + assert!(align_of_val(&0u16) == 2); + assert!(align_of_val(&0u32) == 4); + assert!(align_of_val(&0u64) == 8); + assert!(align_of_val(&0u128) == 16); + assert!(align_of_val(&0usize) == 8); + assert!(align_of_val(&0f32) == 4); + assert!(align_of_val(&0f64) == 8); + assert!(align_of_val(&false) == 1); + assert!(align_of_val(&(0 as char)) == 4); // Compound types (tuple and array) - assert!(min_align_of_val(&(0i32, 0i32)) == 4); - assert!(min_align_of_val(&[0i32; 5]) == 4); + assert!(align_of_val(&(0i32, 0i32)) == 4); + assert!(align_of_val(&[0i32; 5]) == 4); // Custom data types (struct and enum) - assert!(min_align_of_val(&MyStruct { val: 0u32 }) == 4); - assert!(min_align_of_val(&MyEnum::Variant) == 1); - assert!(min_align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4); + assert!(align_of_val(&MyStruct { val: 0u32 }) == 4); + assert!(align_of_val(&MyEnum::Variant) == 1); + assert!(align_of_val(&CStruct { a: 0u8, b: 0i32 }) == 4); } } diff --git a/tests/kani/Intrinsics/ConstEval/align_of.rs b/tests/kani/Intrinsics/ConstEval/align_of.rs new file mode 100644 index 000000000000..06d8cd9b79a5 --- /dev/null +++ b/tests/kani/Intrinsics/ConstEval/align_of.rs @@ -0,0 +1,43 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we get the expected results for the `align_of` intrinsic +// with common data types +#![feature(core_intrinsics)] +use std::intrinsics::align_of; + +struct MyStruct {} + +enum MyEnum {} + +#[kani::proof] +fn main() { + // for the following types x86_64 and aarch64 agree on the alignment; see + // AlignOfVal/align_of_fat_ptr.rs for some example of where they don't agree + #[cfg(any(target_arch = "x86_64", target_arch = "aarch64"))] + { + // Scalar types + assert!(align_of::() == 1); + assert!(align_of::() == 2); + assert!(align_of::() == 4); + assert!(align_of::() == 8); + assert!(align_of::() == 16); + assert!(align_of::() == 8); + assert!(align_of::() == 1); + assert!(align_of::() == 2); + assert!(align_of::() == 4); + assert!(align_of::() == 8); + assert!(align_of::() == 16); + assert!(align_of::() == 8); + assert!(align_of::() == 4); + assert!(align_of::() == 8); + assert!(align_of::() == 1); + assert!(align_of::() == 4); + // Compound types (tuple and array) + assert!(align_of::<(i32, i32)>() == 4); + assert!(align_of::<[i32; 5]>() == 4); + // Custom data types (struct and enum) + assert!(align_of::() == 1); + assert!(align_of::() == 1); + } +} diff --git a/tests/kani/Intrinsics/ConstEval/min_align_of.rs b/tests/kani/Intrinsics/ConstEval/min_align_of.rs deleted file mode 100644 index 425f27084076..000000000000 --- a/tests/kani/Intrinsics/ConstEval/min_align_of.rs +++ /dev/null @@ -1,68 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Check that we get the expected results for the `min_align_of` intrinsic -// with common data types -#![feature(core_intrinsics)] -use std::intrinsics::min_align_of; - -struct MyStruct {} - -enum MyEnum {} - -#[kani::proof] -fn main() { - #[cfg(target_arch = "x86_64")] - { - // Scalar types - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 2); - assert!(min_align_of::() == 4); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 16); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 2); - assert!(min_align_of::() == 4); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 16); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 4); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 4); - // Compound types (tuple and array) - assert!(min_align_of::<(i32, i32)>() == 4); - assert!(min_align_of::<[i32; 5]>() == 4); - // Custom data types (struct and enum) - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 1); - } - - #[cfg(target_arch = "aarch64")] - { - // Scalar types - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 2); - assert!(min_align_of::() == 4); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 16); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 2); - assert!(min_align_of::() == 4); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 16); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 4); - assert!(min_align_of::() == 8); - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 4); - // Compound types (tuple and array) - assert!(min_align_of::<(i32, i32)>() == 4); - assert!(min_align_of::<[i32; 5]>() == 4); - // Custom data types (struct and enum) - assert!(min_align_of::() == 1); - assert!(min_align_of::() == 1); - } -}