diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 5f56c69a9041..01ba2c8caeaa 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -308,7 +308,7 @@ impl GotocCtx<'_> { } Intrinsic::AtomicFence(_) => self.codegen_atomic_noop(intrinsic_str, loc), - Intrinsic::AtomicLoad(_) => self.codegen_atomic_load(intrinsic_str, fargs, place, 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), diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 5d9ab8221453..94b9462612b1 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -23,7 +23,7 @@ pub enum Intrinsic { AtomicCxchg(String), AtomicCxchgWeak(String), AtomicFence(String), - AtomicLoad(String), + AtomicLoad, AtomicMax(String), AtomicMin(String), AtomicNand(String), @@ -483,9 +483,9 @@ fn try_match_atomic(intrinsic_instance: &Instance) -> Option { } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence_") { assert_sig_matches!(sig, => RigidTy::Tuple(_)); Some(Intrinsic::AtomicFence(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_load_") { + } else if intrinsic_str == "atomic_load" { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); - Some(Intrinsic::AtomicLoad(suffix.into())) + 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())) diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 9276ae03e744..a3526d9979d8 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -227,7 +227,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } // All `atomic_load` intrinsics take `src` as an argument. // This is equivalent to `destination = *src`. - Intrinsic::AtomicLoad(_) => { + Intrinsic::AtomicLoad => { let src_set = self.successors_for_deref(state, args[0].node.clone()); let destination_set = state.resolve_place(*destination, self.instance); state.extend(&destination_set, &state.successors(&src_set)); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 1bd4566ab96a..ea3c5db5c216 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -286,7 +286,7 @@ impl MirVisitor for CheckUninitVisitor { Intrinsic::AtomicAnd(_) | Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) - | Intrinsic::AtomicLoad(_) + | Intrinsic::AtomicLoad | Intrinsic::AtomicMax(_) | Intrinsic::AtomicMin(_) | Intrinsic::AtomicNand(_) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e862b5493379..a8bff2547b44 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-05-30" +channel = "nightly-2025-06-02" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs index 78b9dd2fdea0..6bc98252dc45 100644 --- a/tests/expected/uninit/atomic/atomic.rs +++ b/tests/expected/uninit/atomic/atomic.rs @@ -21,7 +21,9 @@ fn local_atomic_uninit() { std::intrinsics::atomic_store_relaxed(ptr, 1); } 1 => { - std::intrinsics::atomic_load_relaxed(ptr as *const u8); + std::intrinsics::atomic_load::<_, { std::intrinsics::AtomicOrdering::Relaxed }>( + ptr as *const u8, + ); } _ => { std::intrinsics::atomic_cxchg_relaxed_relaxed(ptr, 1, 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs index b646c8326229..5f3fc29c0571 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs @@ -5,7 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{atomic_load_acquire, atomic_load_relaxed, atomic_load_seqcst}; +use std::intrinsics::{AtomicOrdering, atomic_load}; #[kani::proof] fn main() { @@ -18,9 +18,9 @@ fn main() { let ptr_a3: *const u8 = &a3; unsafe { - let x1 = atomic_load_seqcst(ptr_a1); - let x2 = atomic_load_acquire(ptr_a2); - let x3 = atomic_load_relaxed(ptr_a3); + let x1 = atomic_load::<_, { AtomicOrdering::SeqCst }>(ptr_a1); + let x2 = atomic_load::<_, { AtomicOrdering::Acquire }>(ptr_a2); + let x3 = atomic_load::<_, { AtomicOrdering::Relaxed }>(ptr_a3); assert!(x1 == 1); assert!(x2 == 1); diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index e7276867a2a5..eea065176dfa 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -42,7 +42,7 @@ mod verify { echo "[TEST] Modify library" echo "${CORE_CODE}" >> ${TMP_DIR}/library/core/src/lib.rs -echo "${STD_CODE}" >> ${TMP_DIR}/library/std/src/num.rs +echo "${STD_CODE}" >> ${TMP_DIR}/library/std/src/num/mod.rs # Note: Prepending with sed doesn't work on MacOs the same way it does in linux. # sed -i '1s/^/#![cfg_attr(kani, feature(kani))]\n/' ${TMP_DIR}/library/std/src/lib.rs