Skip to content

Conversation

carolynzech
Copy link
Contributor

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 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:

let op_expr = if var2.typ().is_pointer() {
(var1.clone().cast_to(Type::c_size_t()))
.$op(var2.cast_to(Type::c_size_t()))
.with_location(loc)
.cast_to(var1.typ().clone())
But rust-lang/rust#144192 makes this change to fetch_xor:

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_ts already.

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.

@github-actions github-actions bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 12, 2025
@carolynzech carolynzech marked this pull request as ready for review August 12, 2025 06:13
@carolynzech carolynzech requested a review from a team as a code owner August 12, 2025 06:13
@tautschnig tautschnig added this pull request to the merge queue Aug 12, 2025
Merged via the queue into model-checking:main with commit fff9316 Aug 12, 2025
33 of 34 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Toolchain upgrade to nightly-2025-08-10 failed
2 participants