Audit: Atomic intrinsics (#850)

* Moved atomic intrinsics tests, added description

* Add support for `atomic_nand*`

* Support for `atomic_singlethreadfence` and variants

* Add missing test for `atomic_cxchgweak`

* Add negative tests for min & max atomics

* Update doc with missing intrinsics

cprover_bindings/src/goto_program/expr.rs

@@ -160,6 +160,7 @@ pub enum BinaryOperand {
     Ashr,
     Bitand,
     Bitor,
+    Bitnand,
     Bitxor,
     Div,
     Equal,
@@ -837,6 +838,8 @@ impl Expr {
             Bitand | Bitor | Bitxor => {
                 lhs.typ == rhs.typ && (lhs.typ.is_integer() || lhs.typ.is_vector())
             }
+            // Bitwise ops (no vector support)
+            Bitnand => lhs.typ == rhs.typ && lhs.typ.is_integer(),
             // Comparisons
             Ge | Gt | Le | Lt => {
                 lhs.typ == rhs.typ
@@ -881,7 +884,7 @@ impl Expr {
             // Boolean ops
             And | Implies | Or | Xor => Type::bool(),
             // Bitwise ops
-            Bitand | Bitor | Bitxor => lhs.typ.clone(),
+            Bitand | Bitnand | Bitor | Bitxor => lhs.typ.clone(),
             // Comparisons
             Ge | Gt | Le | Lt => {
                 if lhs.typ.is_vector() {
@@ -966,6 +969,11 @@ impl Expr {
         self.binop(Bitand, e)
     }
 
+    /// `~ (self & e)`
+    pub fn bitnand(self, e: Expr) -> Expr {
+        self.binop(Bitnand, e)
+    }
+
     /// `self | e`
     pub fn bitor(self, e: Expr) -> Expr {
         self.binop(Bitor, e)

cprover_bindings/src/irep/to_irep.rs

@@ -54,6 +54,7 @@ impl ToIrepId for BinaryOperand {
             BinaryOperand::And => IrepId::And,
             BinaryOperand::Ashr => IrepId::Ashr,
             BinaryOperand::Bitand => IrepId::Bitand,
+            BinaryOperand::Bitnand => IrepId::Bitnand,
             BinaryOperand::Bitor => IrepId::Bitor,
             BinaryOperand::Bitxor => IrepId::Bitxor,
             BinaryOperand::Div => IrepId::Div,

docs/src/limitations.md

@@ -245,16 +245,16 @@ atomic_load | Partial | See [Atomics](#atomics) |
 atomic_load_acq | Partial | See [Atomics](#atomics) |
 atomic_load_relaxed | Partial | See [Atomics](#atomics) |
 atomic_load_unordered | Partial | See [Atomics](#atomics) |
-atomic_max | Partial | See [Atomics](#atomics) |
-atomic_max_acq | Partial | See [Atomics](#atomics) |
-atomic_max_acqrel | Partial | See [Atomics](#atomics) |
-atomic_max_rel | Partial | See [Atomics](#atomics) |
-atomic_max_relaxed | Partial | See [Atomics](#atomics) |
-atomic_min | Partial | See [Atomics](#atomics) |
-atomic_min_acq | Partial | See [Atomics](#atomics) |
-atomic_min_acqrel | Partial | See [Atomics](#atomics) |
-atomic_min_rel | Partial | See [Atomics](#atomics) |
-atomic_min_relaxed | Partial | See [Atomics](#atomics) |
+atomic_max | No | See [Atomics](#atomics) |
+atomic_max_acq | No | See [Atomics](#atomics) |
+atomic_max_acqrel | No | See [Atomics](#atomics) |
+atomic_max_rel | No | See [Atomics](#atomics) |
+atomic_max_relaxed | No | See [Atomics](#atomics) |
+atomic_min | No | See [Atomics](#atomics) |
+atomic_min_acq | No | See [Atomics](#atomics) |
+atomic_min_acqrel | No | See [Atomics](#atomics) |
+atomic_min_rel | No | See [Atomics](#atomics) |
+atomic_min_relaxed | No | See [Atomics](#atomics) |
 atomic_nand | Partial | See [Atomics](#atomics) |
 atomic_nand_acq | Partial | See [Atomics](#atomics) |
 atomic_nand_acqrel | Partial | See [Atomics](#atomics) |
@@ -273,16 +273,16 @@ atomic_store | Partial | See [Atomics](#atomics) |
 atomic_store_rel | Partial | See [Atomics](#atomics) |
 atomic_store_relaxed | Partial | See [Atomics](#atomics) |
 atomic_store_unordered | Partial | See [Atomics](#atomics) |
-atomic_umax | Partial | See [Atomics](#atomics) |
-atomic_umax_acq | Partial | See [Atomics](#atomics) |
-atomic_umax_acqrel | Partial | See [Atomics](#atomics) |
-atomic_umax_rel | Partial | See [Atomics](#atomics) |
-atomic_umax_relaxed | Partial | See [Atomics](#atomics) |
-atomic_umin | Partial | See [Atomics](#atomics) |
-atomic_umin_acq | Partial | See [Atomics](#atomics) |
-atomic_umin_acqrel | Partial | See [Atomics](#atomics) |
-atomic_umin_rel | Partial | See [Atomics](#atomics) |
-atomic_umin_relaxed | Partial | See [Atomics](#atomics) |
+atomic_umax | No | See [Atomics](#atomics) |
+atomic_umax_acq | No | See [Atomics](#atomics) |
+atomic_umax_acqrel | No | See [Atomics](#atomics) |
+atomic_umax_rel | No | See [Atomics](#atomics) |
+atomic_umax_relaxed | No | See [Atomics](#atomics) |
+atomic_umin | No | See [Atomics](#atomics) |
+atomic_umin_acq | No | See [Atomics](#atomics) |
+atomic_umin_acqrel | No | See [Atomics](#atomics) |
+atomic_umin_rel | No | See [Atomics](#atomics) |
+atomic_umin_relaxed | No | See [Atomics](#atomics) |
 atomic_xadd | Partial | See [Atomics](#atomics) |
 atomic_xadd_acq | Partial | See [Atomics](#atomics) |
 atomic_xadd_acqrel | Partial | See [Atomics](#atomics) |

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

@@ -335,11 +335,20 @@ 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_nand" => codegen_atomic_binop!(bitnand),
+            "atomic_nand_acq" => codegen_atomic_binop!(bitnand),
+            "atomic_nand_acqrel" => codegen_atomic_binop!(bitnand),
+            "atomic_nand_rel" => codegen_atomic_binop!(bitnand),
+            "atomic_nand_relaxed" => codegen_atomic_binop!(bitnand),
             "atomic_or" => codegen_atomic_binop!(bitor),
             "atomic_or_acq" => codegen_atomic_binop!(bitor),
             "atomic_or_acqrel" => codegen_atomic_binop!(bitor),
             "atomic_or_rel" => codegen_atomic_binop!(bitor),
             "atomic_or_relaxed" => codegen_atomic_binop!(bitor),
+            "atomic_singlethreadfence" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_singlethreadfence_acq" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_singlethreadfence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_singlethreadfence_rel" => self.codegen_atomic_noop(intrinsic, loc),
             "atomic_store" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_store_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),

tests/kani/Atomics/Stable/CompareExchange/main.rs → tests/kani/Intrinsics/Atomic/Stable/CompareExchange/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_cxchg` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {
@@ -25,7 +29,7 @@ fn main() {
     let a8 = AtomicBool::new(true);
     let a9 = AtomicBool::new(true);
 
-    // compare_exchange is the stable version of atomic_cxchg
+    // `compare_exchange` is the stable version of `atomic_cxchg`
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#1094-1115
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#2410-2437
     // Combinations other than the ones included here result in panic

tests/kani/Atomics/Stable/Exchange/main.rs → tests/kani/Intrinsics/Atomic/Stable/Exchange/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_xchg` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {
@@ -9,7 +13,7 @@ fn main() {
     let a4 = AtomicBool::new(true);
     let a5 = AtomicBool::new(true);
 
-    // swap is the stable version of atomic_xchg
+    // `swap` is the stable version of `atomic_xchg`
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#435
     assert!(a1.swap(false, Ordering::Acquire) == true);
     assert!(a2.swap(false, Ordering::AcqRel) == true);

tests/kani/Atomics/Stable/Fence/main.rs → tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_fence` and other variants (stable version) can be
+// processed.
+
 use std::sync::atomic::{fence, Ordering};
 
 fn main() {

tests/kani/Atomics/Stable/FetchAdd/main.rs → tests/kani/Intrinsics/Atomic/Stable/FetchAdd/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_xadd` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicIsize, Ordering};
 
 fn main() {
@@ -11,7 +15,7 @@ fn main() {
     let a4 = AtomicIsize::new(0);
     let a5 = AtomicIsize::new(0);
 
-    // fetch_add is the stable version of atomic_add
+    // `fetch_add` is the stable version of `atomic_xadd`
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#1717-1724
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#2379-2392
     assert!(a1.fetch_add(1, Ordering::Acquire) == 0);

tests/kani/Atomics/Stable/FetchAnd/main.rs → tests/kani/Intrinsics/Atomic/Stable/FetchAnd/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_and` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {
@@ -13,7 +17,7 @@ fn main() {
     let a4 = AtomicBool::new(true);
     let a5 = AtomicBool::new(true);
 
-    // fetch_and is the stable version of atomic_and
+    // `fetch_and` is the stable version of `atomic_and`
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#623-629
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#2468-2481
     assert!(a1.fetch_and(false, Ordering::Acquire) == true);

tests/kani/Atomics/Stable/FetchOr/main.rs → tests/kani/Intrinsics/Atomic/Stable/FetchOr/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_or` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {
@@ -13,7 +17,7 @@ fn main() {
     let a4 = AtomicBool::new(true);
     let a5 = AtomicBool::new(true);
 
-    // fetch_or is the stable version of atomic_or
+    // `fetch_or` is the stable version of `atomic_or`
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#715-721
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#2498-2511
     assert!(a1.fetch_or(false, Ordering::Acquire) == true);

tests/kani/Atomics/Stable/FetchSub/main.rs → tests/kani/Intrinsics/Atomic/Stable/FetchSub/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_xsub` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicIsize, Ordering};
 
 fn main() {
@@ -11,7 +15,7 @@ fn main() {
     let a4 = AtomicIsize::new(1);
     let a5 = AtomicIsize::new(1);
 
-    // fetch_sub is the stable version of atomic_sub
+    // `fetch_sub` is the stable version of `atomic_xsub`
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#1748-1755
     // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#2395-2408
     assert!(a1.fetch_sub(1, Ordering::Acquire) == 1);

tests/kani/Atomics/Stable/FetchXor/main.rs → tests/kani/Intrinsics/Atomic/Stable/FetchXor/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_xor` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {
@@ -13,7 +17,7 @@ fn main() {
     let a4 = AtomicBool::new(true);
     let a5 = AtomicBool::new(true);
 
-    // fetch_xor is the stable version of atomic_xor
+    // `fetch_xor` is the stable version of `atomic_xor`
     assert!(a1.fetch_xor(true, Ordering::Acquire) == true);
     assert!(a2.fetch_xor(true, Ordering::Release) == true);
     assert!(a3.fetch_xor(true, Ordering::AcqRel) == true);

tests/kani/Atomics/Stable/Load/main.rs → tests/kani/Intrinsics/Atomic/Stable/Load/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_load` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {

tests/kani/Atomics/Stable/Store/main.rs → tests/kani/Intrinsics/Atomic/Stable/Store/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_store` and other variants (stable version) return the
+// expected result.
+
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {

tests/kani/Atomics/Unstable/AtomicAdd/main.rs → tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_xsub` and other variants (unstable version) return the
+// expected result.
+
 #![feature(core_intrinsics)]
 use std::intrinsics::{
     atomic_xadd, atomic_xadd_acq, atomic_xadd_acqrel, atomic_xadd_rel, atomic_xadd_relaxed,

tests/kani/Atomics/Unstable/AtomicAnd/main.rs → tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_and` and other variants (unstable version) return the
+// expected result.
+
 #![feature(core_intrinsics)]
 use std::intrinsics::{
     atomic_and, atomic_and_acq, atomic_and_acqrel, atomic_and_rel, atomic_and_relaxed,

tests/kani/Atomics/Unstable/AtomicCxchg/main.rs → tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs

@@ -1,5 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_cxchg` and other variants (unstable version) return the
+// expected result.
+
 #![feature(core_intrinsics)]
 use std::intrinsics::{
     atomic_cxchg, atomic_cxchg_acq, atomic_cxchg_acq_failrelaxed, atomic_cxchg_acqrel,

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

@@ -0,0 +1,80 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_cxchgweak` and other variants (unstable version) return
+// the expected result.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    atomic_cxchgweak, atomic_cxchgweak_acq, atomic_cxchgweak_acq_failrelaxed,
+    atomic_cxchgweak_acqrel, atomic_cxchgweak_acqrel_failrelaxed, atomic_cxchgweak_failacq,
+    atomic_cxchgweak_failrelaxed, atomic_cxchgweak_rel, atomic_cxchgweak_relaxed,
+};
+
+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 mut a6 = 0 as u8;
+    let mut a7 = 0 as u8;
+    let mut a8 = 0 as u8;
+    let mut a9 = 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 ptr_a6: *mut u8 = &mut a6;
+    let ptr_a7: *mut u8 = &mut a7;
+    let ptr_a8: *mut u8 = &mut a8;
+    let ptr_a9: *mut u8 = &mut a9;
+
+    unsafe {
+        // Stores a value if the current value is the same as the old value
+        // Returns (val, ok) where
+        //  * val: the old value
+        //  * ok:  bool indicating whether the operation was successful or not
+        let x1 = atomic_cxchgweak(ptr_a1, 0, 1);
+        let x2 = atomic_cxchgweak_acq(ptr_a2, 0, 1);
+        let x3 = atomic_cxchgweak_acq_failrelaxed(ptr_a3, 0, 1);
+        let x4 = atomic_cxchgweak_acqrel(ptr_a4, 0, 1);
+        let x5 = atomic_cxchgweak_acqrel_failrelaxed(ptr_a5, 0, 1);
+        let x6 = atomic_cxchgweak_failacq(ptr_a6, 0, 1);
+        let x7 = atomic_cxchgweak_failrelaxed(ptr_a7, 0, 1);
+        let x8 = atomic_cxchgweak_rel(ptr_a8, 0, 1);
+        let x9 = atomic_cxchgweak_relaxed(ptr_a9, 0, 1);
+
+        assert!(x1 == (0, true));
+        assert!(x2 == (0, true));
+        assert!(x3 == (0, true));
+        assert!(x4 == (0, true));
+        assert!(x5 == (0, true));
+        assert!(x6 == (0, true));
+        assert!(x7 == (0, true));
+        assert!(x8 == (0, true));
+        assert!(x9 == (0, true));
+
+        let y1 = atomic_cxchgweak(ptr_a1, 1, 1);
+        let y2 = atomic_cxchgweak_acq(ptr_a2, 1, 1);
+        let y3 = atomic_cxchgweak_acq_failrelaxed(ptr_a3, 1, 1);
+        let y4 = atomic_cxchgweak_acqrel(ptr_a4, 1, 1);
+        let y5 = atomic_cxchgweak_acqrel_failrelaxed(ptr_a5, 1, 1);
+        let y6 = atomic_cxchgweak_failacq(ptr_a6, 1, 1);
+        let y7 = atomic_cxchgweak_failrelaxed(ptr_a7, 1, 1);
+        let y8 = atomic_cxchgweak_rel(ptr_a8, 1, 1);
+        let y9 = atomic_cxchgweak_relaxed(ptr_a9, 1, 1);
+
+        assert!(y1 == (1, true));
+        assert!(y2 == (1, true));
+        assert!(y3 == (1, true));
+        assert!(y4 == (1, true));
+        assert!(y5 == (1, true));
+        assert!(y6 == (1, true));
+        assert!(y7 == (1, true));
+        assert!(y8 == (1, true));
+        assert!(y9 == (1, true));
+    }
+}