Upgrade Rust toolchain to 2025-06-02 (#4123)

Relevant upstream PRs:
- rust-lang/rust#141507 (identified by
@tautschnig): replaces the atomic_load intrinstics
(`atomic_load_seqcst`, `atomic_load_acquire`, and `atomic_load_relaxed`)
by a new `atomic_load` intrinsic that is generic in the atomic ordering.
Update the Kani code and tests accordingly.
- rust-lang/rust#137574: Moved the `num` module
from `std/src/num.rs` to `std/src/num/mod.rs` which required updating
the corresponding path in the `script-based-pre/verify_std_cmd` test.

Resolves #4120

### Call-outs:
- Instead of replacing the `String` parameter of Kani's `AtomicLoad`
enum variant by `AtomicOrdering`, I opted to remove the parameter
altogether since Kani doesn't do anything with it at the moment. We can
easily add a parameter to that enum variant in the future if Kani needs
it.
- The upstream change to `atomic_load` is expected to be followed by
similar changes to all atomic intrinsics.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws

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),

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<Intrinsic> {
     } 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()))

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));

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(_)

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"]

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);

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);

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