Fix codegen_atomic_binop for atomic_ptr (#3047)

Fetch functions of `atomic_ptr` calls atomic intrinsic functions with
pointer-type arguments (`invalid_mut`), which will cause typecheck
failures. The change in this commit add support of pointer-type
arguments into `codegen_atomic_binop` to fix the issue. The new
`codegen_atomic_binop` will cast pointer arguments to `size_t`, apply op
on them, and then cast the op result back to the pointer type.

The new test include all fetch functions of `atomic_ptr` except for
`fetch_ptr_add` and `fetch_ptr_sub`, which do not call intrinsic
functions.

Resolves #3042.

---------

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

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

@@ -239,6 +239,19 @@ impl<'tcx> GotocCtx<'tcx> {
  // *var1 = op(*var1, var2);
  // var = tmp;
  // -------------------------
+ //
+ // 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.
+ // -------------------------
+ // var = atomic_op(var1, var2)
+ // -------------------------
+ // unsigned char tmp;
+ // tmp = *var1;
+ // *var1 = (typeof var1)op((size_t)*var1, (size_t)var2);
+ // var = tmp;
+ // -------------------------
+ //
  // Note: Atomic arithmetic operations wrap around on overflow.
  macro_rules! codegen_atomic_binop {
  ($op: ident) => {{
@@ -249,7 +262,14 @@ impl<'tcx> GotocCtx<'tcx> {
  let (tmp, decl_stmt) =
  self.decl_temp_variable(var1.typ().clone(), Some(var1.to_owned()), loc);
  let var2 = fargs.remove(0);
- let op_expr = (var1.clone()).$op(var2).with_location(loc);
+ 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())
+ } else {
+ (var1.clone()).$op(var2).with_location(loc)
+ };
  let assign_stmt = (var1.clone()).assign(op_expr, loc);
  let res_stmt = self.codegen_expr_to_place_stable(place, tmp.clone());
  Stmt::atomic_block(vec![decl_stmt, assign_stmt, res_stmt], loc)

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

@@ -0,0 +1,72 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Test atomic intrinsics through the stable interface of atomic_ptr.
+// 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)]
+use std::sync::atomic::{AtomicPtr, Ordering};
+
+#[kani::proof]
+fn check_fetch_byte_add() {
+ let atom = AtomicPtr::<i64>::new(core::ptr::null_mut());
+ assert_eq!(atom.fetch_byte_add(1, Ordering::Relaxed).addr(), 0);
+ // Note: in units of bytes, not `size_of::<i64>()`.
+ assert_eq!(atom.load(Ordering::Relaxed).addr(), 1);
+}
+
+#[kani::proof]
+fn check_fetch_byte_sub() {
+ let atom = AtomicPtr::<i64>::new(core::ptr::invalid_mut(1));
+ assert_eq!(atom.fetch_byte_sub(1, Ordering::Relaxed).addr(), 1);
+ assert_eq!(atom.load(Ordering::Relaxed).addr(), 0);
+}
+
+#[kani::proof]
+fn check_fetch_and() {
+ let pointer = &mut 3i64 as *mut i64;
+ // A tagged pointer
+ let atom = AtomicPtr::<i64>::new(pointer.map_addr(|a| a | 1));
+ assert_eq!(atom.fetch_or(1, Ordering::Relaxed).addr() & 1, 1);
+ // Untag, and extract the previously tagged pointer.
+ let untagged = atom.fetch_and(!1, Ordering::Relaxed).map_addr(|a| a & !1);
+ assert_eq!(untagged, pointer);
+}
+
+#[kani::proof]
+fn check_fetch_or() {
+ let pointer = &mut 3i64 as *mut i64;
+
+ let atom = AtomicPtr::<i64>::new(pointer);
+ // Tag the bottom bit of the pointer.
+ assert_eq!(atom.fetch_or(1, Ordering::Relaxed).addr() & 1, 0);
+ // Extract and untag.
+ let tagged = atom.load(Ordering::Relaxed);
+ assert_eq!(tagged.addr() & 1, 1);
+ assert_eq!(tagged.map_addr(|p| p & !1), pointer);
+}
+
+#[kani::proof]
+fn check_fetch_update() {
+ let ptr: *mut _ = &mut 5;
+ let some_ptr = AtomicPtr::new(ptr);
+
+ let new: *mut _ = &mut 10;
+ assert_eq!(some_ptr.fetch_update(Ordering::SeqCst, Ordering::SeqCst, |_| None), Err(ptr));
+ let result = some_ptr.fetch_update(Ordering::SeqCst, Ordering::SeqCst, |x| {
+ if x == ptr { Some(new) } else { None }
+ });
+ assert_eq!(result, Ok(ptr));
+ assert_eq!(some_ptr.load(Ordering::SeqCst), new);
+}
+
+#[kani::proof]
+fn check_fetch_xor() {
+ let pointer = &mut 3i64 as *mut i64;
+ let atom = AtomicPtr::<i64>::new(pointer);
+
+ // Toggle a tag bit on the pointer.
+ atom.fetch_xor(1, Ordering::Relaxed);
+ assert_eq!(atom.load(Ordering::Relaxed).addr() & 1, 1);
+}