Add support for atomic_max* and atomic_umax* intinsics

cprover_bindings/src/goto_program/expr.rs

@@ -1109,6 +1109,13 @@ impl Expr {
         let cmp = self.clone().lt(e.clone());
         cmp.ternary(self, e)
     }
+
+    /// `max(self, e)`
+    pub fn max(self, e: Expr) -> Expr {
+        assert!(!self.is_side_effect() && !e.is_side_effect());
+        let cmp = self.clone().gt(e.clone());
+        cmp.ternary(self, e)
+    }
 }
 
 /// Constructors for self operations

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

@@ -412,6 +412,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "atomic_load_acq" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
             "atomic_load_relaxed" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
             "atomic_load_unordered" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
+            "atomic_max" => codegen_atomic_binop!(max),
+            "atomic_max_acq" => codegen_atomic_binop!(max),
+            "atomic_max_acqrel" => codegen_atomic_binop!(max),
+            "atomic_max_rel" => codegen_atomic_binop!(max),
+            "atomic_max_relaxed" => codegen_atomic_binop!(max),
             "atomic_min" => codegen_atomic_binop!(min),
             "atomic_min_acq" => codegen_atomic_binop!(min),
             "atomic_min_acqrel" => codegen_atomic_binop!(min),
@@ -435,6 +440,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "atomic_store_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_store_unordered" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_umax" => codegen_atomic_binop!(max),
+            "atomic_umax_acq" => codegen_atomic_binop!(max),
+            "atomic_umax_acqrel" => codegen_atomic_binop!(max),
+            "atomic_umax_rel" => codegen_atomic_binop!(max),
+            "atomic_umax_relaxed" => codegen_atomic_binop!(max),
             "atomic_umin" => codegen_atomic_binop!(min),
             "atomic_umin_acq" => codegen_atomic_binop!(min),
             "atomic_umin_acqrel" => codegen_atomic_binop!(min),

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

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_max` and other variants (unstable version) return the
+// expected result.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    atomic_max, atomic_max_acq, atomic_max_acqrel, atomic_max_rel, atomic_max_relaxed,
+};
+
+#[kani::proof]
+fn main() {
+    let mut a1 = 0 as u8;
+    let mut a2 = 0 as u8;
+    let mut a3 = 0 as u8;
+    let mut a4 = 0 as u8;
+    let mut a5 = 0 as u8;
+
+    let ptr_a1: *mut u8 = &mut a1;
+    let ptr_a2: *mut u8 = &mut a2;
+    let ptr_a3: *mut u8 = &mut a3;
+    let ptr_a4: *mut u8 = &mut a4;
+    let ptr_a5: *mut u8 = &mut a5;
+
+    let b = 1 as u8;
+
+    unsafe {
+        let x1 = atomic_max(ptr_a1, b);
+        let x2 = atomic_max_acq(ptr_a2, b);
+        let x3 = atomic_max_acqrel(ptr_a3, b);
+        let x4 = atomic_max_rel(ptr_a4, b);
+        let x5 = atomic_max_relaxed(ptr_a5, b);
+
+        assert!(x1 == 0);
+        assert!(x2 == 0);
+        assert!(x3 == 0);
+        assert!(x4 == 0);
+        assert!(x5 == 0);
+
+        assert!(*ptr_a1 == b);
+        assert!(*ptr_a2 == b);
+        assert!(*ptr_a3 == b);
+        assert!(*ptr_a4 == b);
+        assert!(*ptr_a5 == b);
+    }
+}

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

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_umax` and other variants (unstable version) return the
+// expected result.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    atomic_umax, atomic_umax_acq, atomic_umax_acqrel, atomic_umax_rel, atomic_umax_relaxed,
+};
+
+#[kani::proof]
+fn main() {
+    let mut a1 = 0 as u8;
+    let mut a2 = 0 as u8;
+    let mut a3 = 0 as u8;
+    let mut a4 = 0 as u8;
+    let mut a5 = 0 as u8;
+
+    let ptr_a1: *mut u8 = &mut a1;
+    let ptr_a2: *mut u8 = &mut a2;
+    let ptr_a3: *mut u8 = &mut a3;
+    let ptr_a4: *mut u8 = &mut a4;
+    let ptr_a5: *mut u8 = &mut a5;
+
+    let b = 1 as u8;
+
+    unsafe {
+        let x1 = atomic_umax(ptr_a1, b);
+        let x2 = atomic_umax_acq(ptr_a2, b);
+        let x3 = atomic_umax_acqrel(ptr_a3, b);
+        let x4 = atomic_umax_rel(ptr_a4, b);
+        let x5 = atomic_umax_relaxed(ptr_a5, b);
+
+        assert!(x1 == 0);
+        assert!(x2 == 0);
+        assert!(x3 == 0);
+        assert!(x4 == 0);
+        assert!(x5 == 0);
+
+        assert!(*ptr_a1 == b);
+        assert!(*ptr_a2 == b);
+        assert!(*ptr_a3 == b);
+        assert!(*ptr_a4 == b);
+        assert!(*ptr_a5 == b);
+    }
+}