Add support for atomic_min* and atomic_umin* intrinsics (rust-lang#1212)

* Define `min` expression

* Add `atomic_min*` intrinsics

* Add test and remove negative ones

* Add support for `atomic_umin*`

* Add test for `umin` and remove negative ones

* Complete `is_side_effect` and use in `min`

* Use `any` instead of local function

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: adpaco-aws

cprover_bindings/src/goto_program/expr.rs

@@ -282,13 +282,33 @@ impl Expr {
             _ => false,
         }
     }
+
+    /// Returns whether an expression causes side effects or not
     pub fn is_side_effect(&self) -> bool {
-        match *self.value {
+        match &*self.value {
+            // These expressions always cause side effects
             Assign { .. }
             | FunctionCall { .. }
             | Nondet
             | SelfOp { .. }
             | StatementExpression { .. } => true,
+            // These expressions do not cause side effects, but the expressions
+            // they contain may do. All we need to do are recursive calls.
+            AddressOf(e) => e.is_side_effect(),
+            Array { elems } => elems.iter().any(|e| e.is_side_effect()),
+            ArrayOf { elem } => elem.is_side_effect(),
+            BinOp { op: _, lhs, rhs } => lhs.is_side_effect() || rhs.is_side_effect(),
+            ByteExtract { e, offset: _ } => e.is_side_effect(),
+            Dereference(e) => e.is_side_effect(),
+            If { c, t, e } => c.is_side_effect() || t.is_side_effect() || e.is_side_effect(),
+            Index { array, index } => array.is_side_effect() || index.is_side_effect(),
+            Member { lhs, field: _ } => lhs.is_side_effect(),
+            Struct { values } => values.iter().any(|e| e.is_side_effect()),
+            Typecast(e) => e.is_side_effect(),
+            Union { value, field: _ } => value.is_side_effect(),
+            UnOp { op: _, e } => e.is_side_effect(),
+            Vector { elems } => elems.iter().any(|e| e.is_side_effect()),
+            // The rest of expressions (constants) do not cause side effects
             _ => false,
         }
     }
@@ -1080,6 +1100,15 @@ 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 {
+        assert!(!self.is_side_effect() && !e.is_side_effect());
+        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/AtomicMin/min.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);
+    }
+}