From c0712165a7331f5dcdbef3f74335d039550e0c0b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 11 Aug 2025 23:30:25 -0400 Subject: [PATCH] upgrade toolchain to 08/10/2025 --- .../codegen/intrinsic.rs | 12 ++++++----- rust-toolchain.toml | 2 +- .../Atomic/Stable/AtomicPtr/main.rs | 2 +- .../Atomic/Unstable/AtomicAdd/main.rs | 10 +++++----- .../Atomic/Unstable/AtomicAnd/main.rs | 10 +++++----- .../Atomic/Unstable/AtomicNand/main.rs | 20 +++++++++---------- .../Atomic/Unstable/AtomicOr/main.rs | 10 +++++----- .../Atomic/Unstable/AtomicSub/main.rs | 10 +++++----- .../Atomic/Unstable/AtomicXor/main.rs | 10 +++++----- 9 files changed, 44 insertions(+), 42 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 792ee2b0fade..ec1f7e0c19a0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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 { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index d73c66fde163..d345ea091e40 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-08-09" +channel = "nightly-2025-08-10" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs b/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs index 4e9d68619fd7..56c324487d59 100644 --- a/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs +++ b/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] diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs index 5789d9d62c0c..005f45a17da0 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs +++ b/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); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs index 8eccf86bce49..bf4dde1d0fc5 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs +++ b/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); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs index 4cae3c56988c..fa9b7ea0b842 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs +++ b/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); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs index aca7f25940b3..d0cde88267f4 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs +++ 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); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs index e57a3a12fe15..ded57405d164 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs +++ b/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); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs index 61a9e397e167..68449551ba39 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs +++ b/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);