Upgrade toolchain to 2025-08-10 (#4289)

Culprit PR: rust-lang/rust#144192

The upstream PR adds a new generic argument `U` for some atomic
intrinsics, so our tests need to include those.

Solely changing the tests to infer the generic argument makes
compilation succeed, but [this `atomic_xor`
harness](https://github.com/model-checking/kani/blob/41849d25092483d1dd92d472cc8c457908903927/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs#L70)
fails with this error:

```
thread 'rustc' (1068557) panicked at cprover_bindings/src/goto_program/expr.rs:1147:9:
BinaryOperation Expression does not typecheck 
Bitor 
Expr { value: Dereference(Expr { value: Symbol { identifier: "_RINvNtNtCslIVxtpUQXYK_4core4sync6atomic9atomic_orOxjECs63P9ci4LCSm_4main::1::var_1::dst" }, typ: Pointer { typ: Pointer { typ: Signedbv { width: 64 } } }, location: None, size_of_annotation: None }), typ: Pointer { typ: Signedbv { width: 64 } }, location: None, size_of_annotation: None } 
Expr { value: Symbol { identifier: "_RINvNtNtCslIVxtpUQXYK_4core4sync6atomic9atomic_orOxjECs63P9ci4LCSm_4main::1::var_2::val" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::sync::atomic::atomic_or::<*mut i64, usize>
_RINvNtNtCslIVxtpUQXYK_4core4sync6atomic9atomic_orOxjECs63P9ci4LCSm_4main
[Kani] current codegen location: Loc { file: "/Users/cmzech/.rustup/toolchains/nightly-2025-08-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs", function: None, start_line: 4183, start_col: Some(1), end_line: 4183, end_col: Some(81), pragmas: [] }
```

This happens because `codegen_atomic_binop` currently handles the case
where `T` is a pointer by checking if `var2` is a pointer, then casting
`var1` and `var2` to `size_t`:

https://github.com/model-checking/kani/blob/41849d25092483d1dd92d472cc8c457908903927/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs#L241-L245
But rust-lang/rust#144192 makes this change to
`fetch_xor`:

```diff
diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs
index 546f3d91a80..44a6895f90a 100644
--- a/library/core/src/sync/atomic.rs
+++ b/library/core/src/sync/atomic.rs
     pub fn fetch_xor(&self, val: usize, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
-        unsafe { atomic_xor(self.p.get(), core::ptr::without_provenance_mut(val), order).cast() }
+        unsafe { atomic_xor(self.p.get(), val, order).cast() }
     }
 
```
since `var2` is no longer a pointer, we hit the else case, and thus the
solution from #3047 no longer
takes effect.

The solution is to instead check if `var1` is a pointer. We also remove
the cast of `var2` to a size_t, since per the new documentation:

> `U` must be the same as `T` if that is an integer type, or `usize` if
`T` is a pointer type.

`U` is guaranteed to be a `usize` if `T` is a pointer, and we [codegen
usizes as `size_t`s
already](https://github.com/model-checking/kani/blob/41849d25092483d1dd92d472cc8c457908903927/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs#L713
).

Resolves #4284

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

Author: carolynzech

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -217,14 +217,16 @@ impl GotocCtx<'_> {
         // -------------------------
         //
         // In fetch functions of atomic_ptr such as https://doc.rust-lang.org/std/sync/atomic/struct.AtomicPtr.html#method.fetch_byte_add,
-        // the type of var2 can be pointer (invalid_mut).
-        // In such case, atomic binops are transformed as follows to avoid typecheck failure.
+        // the type of var1 is a pointer.
+        // In this case, var2 is guaranteed to be a usize,
+        // c.f. https://github.com/rust-lang/rust/blob/a1531335fe2807715fff569904d99602022643a7/library/core/src/intrinsics/mod.rs#L203
+        // We transform such binops as follows to avoid typecheck failure.
         // -------------------------
         // var = atomic_op(var1, var2)
         // -------------------------
         // unsigned char tmp;
         // tmp = *var1;
-        // *var1 = (typeof var1)op((size_t)*var1, (size_t)var2);
+        // *var1 = (typeof var1)op((size_t)*var1, var2);
         // var = tmp;
         // -------------------------
         //
@@ -238,9 +240,9 @@ impl GotocCtx<'_> {
                 let (tmp, decl_stmt) =
                     self.decl_temp_variable(var1.typ().clone(), Some(var1.to_owned()), loc);
                 let var2 = fargs.remove(0);
-                let op_expr = if var2.typ().is_pointer() {
+                let op_expr = if var1.typ().is_pointer() {
                     (var1.clone().cast_to(Type::c_size_t()))
-                        .$op(var2.cast_to(Type::c_size_t()))
+                        .$op(var2)
                         .with_location(loc)
                         .cast_to(var1.typ().clone())
                 } else {

rust-toolchain.toml

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

tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs

@@ -5,7 +5,7 @@
 // Specifically, it checks that Kani correctly handles atomic_ptr's fetch methods, in which the second argument is a pointer type.
 // These methods were not correctly handled as explained in https://github.com/model-checking/kani/issues/3042.
 
-#![feature(strict_provenance_atomic_ptr, strict_provenance)]
+#![feature(strict_provenance_atomic_ptr)]
 use std::sync::atomic::{AtomicPtr, Ordering};
 
 #[kani::proof]

tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs

@@ -25,11 +25,11 @@ fn main() {
     let c = 1 as u8;
 
     unsafe {
-        let x1 = atomic_xadd::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
-        let x2 = atomic_xadd::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
-        let x3 = atomic_xadd::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
-        let x4 = atomic_xadd::<_, { AtomicOrdering::Release }>(ptr_a4, b);
-        let x5 = atomic_xadd::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
+        let x1 = atomic_xadd::<_, _, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_xadd::<_, _, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_xadd::<_, _, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_xadd::<_, _, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_xadd::<_, _, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 0);
         assert!(x2 == 0);

tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs

@@ -24,11 +24,11 @@ fn main() {
     let b = 0 as u8;
 
     unsafe {
-        let x1 = atomic_and::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
-        let x2 = atomic_and::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
-        let x3 = atomic_and::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
-        let x4 = atomic_and::<_, { AtomicOrdering::Release }>(ptr_a4, b);
-        let x5 = atomic_and::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
+        let x1 = atomic_and::<_, _, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_and::<_, _, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_and::<_, _, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_and::<_, _, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_and::<_, _, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 1);
         assert!(x2 == 1);

tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs

@@ -24,11 +24,11 @@ fn main() {
     let b = u8::MAX as u8;
 
     unsafe {
-        let x1 = atomic_nand::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
-        let x2 = atomic_nand::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
-        let x3 = atomic_nand::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
-        let x4 = atomic_nand::<_, { AtomicOrdering::Release }>(ptr_a4, b);
-        let x5 = atomic_nand::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
+        let x1 = atomic_nand::<_, _, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_nand::<_, _, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_nand::<_, _, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_nand::<_, _, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_nand::<_, _, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 0);
         assert!(x2 == 0);
@@ -42,11 +42,11 @@ fn main() {
         assert!(*ptr_a4 == b);
         assert!(*ptr_a5 == b);
 
-        let x1 = atomic_nand::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
-        let x2 = atomic_nand::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
-        let x3 = atomic_nand::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
-        let x4 = atomic_nand::<_, { AtomicOrdering::Release }>(ptr_a4, b);
-        let x5 = atomic_nand::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
+        let x1 = atomic_nand::<_, _, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_nand::<_, _, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_nand::<_, _, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_nand::<_, _, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_nand::<_, _, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == b);
         assert!(x2 == b);

tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs

@@ -25,11 +25,11 @@ fn main() {
     let c = 1 as u8;
 
     unsafe {
-        let x1 = atomic_or::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
-        let x2 = atomic_or::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
-        let x3 = atomic_or::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
-        let x4 = atomic_or::<_, { AtomicOrdering::Release }>(ptr_a4, b);
-        let x5 = atomic_or::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
+        let x1 = atomic_or::<_, _, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_or::<_, _, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_or::<_, _, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_or::<_, _, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_or::<_, _, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 1);
         assert!(x2 == 1);

tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs

@@ -25,11 +25,11 @@ fn main() {
     let c = 0 as u8;
 
     unsafe {
-        let x1 = atomic_xsub::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
-        let x2 = atomic_xsub::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
-        let x3 = atomic_xsub::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
-        let x4 = atomic_xsub::<_, { AtomicOrdering::Release }>(ptr_a4, b);
-        let x5 = atomic_xsub::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
+        let x1 = atomic_xsub::<_, _, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_xsub::<_, _, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_xsub::<_, _, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_xsub::<_, _, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_xsub::<_, _, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 1);
         assert!(x2 == 1);

tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs

@@ -24,11 +24,11 @@ fn main() {
     let b = 1 as u8;
 
     unsafe {
-        let x1 = atomic_xor::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
-        let x2 = atomic_xor::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
-        let x3 = atomic_xor::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
-        let x4 = atomic_xor::<_, { AtomicOrdering::Release }>(ptr_a4, b);
-        let x5 = atomic_xor::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
+        let x1 = atomic_xor::<_, _, { AtomicOrdering::SeqCst }>(ptr_a1, b);
+        let x2 = atomic_xor::<_, _, { AtomicOrdering::Acquire }>(ptr_a2, b);
+        let x3 = atomic_xor::<_, _, { AtomicOrdering::AcqRel }>(ptr_a3, b);
+        let x4 = atomic_xor::<_, _, { AtomicOrdering::Release }>(ptr_a4, b);
+        let x5 = atomic_xor::<_, _, { AtomicOrdering::Relaxed }>(ptr_a5, b);
 
         assert!(x1 == 1);
         assert!(x2 == 1);