Add support for atomic_min* and atomic_umin* intrinsics

cprover_bindings/src/goto_program/expr.rs

@@ -1080,6 +1080,14 @@ impl Expr {
     pub fn r_ok(self, e: Expr) -> Expr {
         self.binop(ROk, e)
     }
+
+    // Expressions defined on top of other expressions
+
+    /// `min(self, e)`
+    pub fn min(self, e: Expr) -> Expr {
+        let cmp = self.clone().lt(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_min" => codegen_atomic_binop!(min),
+            "atomic_min_acq" => codegen_atomic_binop!(min),
+            "atomic_min_acqrel" => codegen_atomic_binop!(min),
+            "atomic_min_rel" => codegen_atomic_binop!(min),
+            "atomic_min_relaxed" => codegen_atomic_binop!(min),
             "atomic_nand" => codegen_atomic_binop!(bitnand),
             "atomic_nand_acq" => codegen_atomic_binop!(bitnand),
             "atomic_nand_acqrel" => codegen_atomic_binop!(bitnand),
@@ -430,6 +435,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_umin" => codegen_atomic_binop!(min),
+            "atomic_umin_acq" => codegen_atomic_binop!(min),
+            "atomic_umin_acqrel" => codegen_atomic_binop!(min),
+            "atomic_umin_rel" => codegen_atomic_binop!(min),
+            "atomic_umin_relaxed" => codegen_atomic_binop!(min),
             "atomic_xadd" => codegen_atomic_binop!(plus),
             "atomic_xadd_acq" => codegen_atomic_binop!(plus),
             "atomic_xadd_acqrel" => codegen_atomic_binop!(plus),

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

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_min` and other variants (unstable version) return the
+// expected result.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    atomic_min, atomic_min_acq, atomic_min_acqrel, atomic_min_rel, atomic_min_relaxed,
+};
+
+#[kani::proof]
+fn main() {
+    let mut a1 = 1 as u8;
+    let mut a2 = 1 as u8;
+    let mut a3 = 1 as u8;
+    let mut a4 = 1 as u8;
+    let mut a5 = 1 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 = 0 as u8;
+
+    unsafe {
+        let x1 = atomic_min(ptr_a1, b);
+        let x2 = atomic_min_acq(ptr_a2, b);
+        let x3 = atomic_min_acqrel(ptr_a3, b);
+        let x4 = atomic_min_rel(ptr_a4, b);
+        let x5 = atomic_min_relaxed(ptr_a5, b);
+
+        assert!(x1 == 1);
+        assert!(x2 == 1);
+        assert!(x3 == 1);
+        assert!(x4 == 1);
+        assert!(x5 == 1);
+
+        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/AtomicUmin/main.rs

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