Support atomic compare/exhange primitives

compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs

@@ -286,6 +286,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "atomic_xadd_acqrel" => codegen_atomic_binop!(plus),
             "atomic_xadd_rel" => codegen_atomic_binop!(plus),
             "atomic_xadd_relaxed" => codegen_atomic_binop!(plus),
+            "atomic_xchg"
+            | "atomic_xchg_acq"
+            | "atomic_xchg_acqrel"
+            | "atomic_xchg_rel"
+            | "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_xor" => codegen_atomic_binop!(bitxor),
             "atomic_xor_acq" => codegen_atomic_binop!(bitxor),
             "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor),

src/test/cbmc/Atomics/Stable/Exchange/main.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use std::sync::atomic::{AtomicBool, Ordering};
+
+fn main() {
+    // pub fn compare_exchange(
+    //     &self,
+    //     current: bool,
+    //     new: bool,
+    //     success: Ordering,
+    //     failure: Ordering
+    // ) -> Result<bool, bool>
+    // Stores a value into the bool if the current value is the same
+    // as the current value.
+    // The return value is a result indicating whether the new value
+    // was written and containing the previous value. On success this
+    // value is guaranteed to be equal to current.
+    let a1 = AtomicBool::new(true);
+    let a2 = AtomicBool::new(true);
+    let a3 = AtomicBool::new(true);
+    let a4 = AtomicBool::new(true);
+    let a5 = AtomicBool::new(true);
+
+
+    // 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);
+    assert!(a3.swap(false, Ordering::Relaxed) == true);
+    assert!(a4.swap(false, Ordering::Release) == true);
+    assert!(a5.swap(false, Ordering::SeqCst) == true);
+
+    assert!(a1.load(Ordering::Relaxed) == false);
+    assert!(a2.load(Ordering::Relaxed) == false);
+    assert!(a3.load(Ordering::Relaxed) == false);
+    assert!(a4.load(Ordering::Relaxed) == false);
+    assert!(a5.load(Ordering::Relaxed) == false);
+}

src/test/cbmc/Atomics/Unstable/AtomicXchg/main.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    atomic_xchg, atomic_xchg_acq, atomic_xchg_acqrel,
+    atomic_xchg_rel, atomic_xchg_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 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;
+
+    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
+        assert!(atomic_xchg(ptr_a1, 1) == 0);
+        assert!(atomic_xchg(ptr_a1, 0) == 1);
+        assert!(atomic_xchg_acq(ptr_a2, 1) == 0);
+        assert!(atomic_xchg_acq(ptr_a2, 0) == 1);
+        assert!(atomic_xchg_acqrel(ptr_a3, 1) == 0);
+        assert!(atomic_xchg_acqrel(ptr_a3, 0) == 1);
+        assert!(atomic_xchg_rel(ptr_a4, 1) == 0);
+        assert!(atomic_xchg_rel(ptr_a4, 0) == 1);
+        assert!(atomic_xchg_relaxed(ptr_a5, 1) == 0);
+        assert!(atomic_xchg_relaxed(ptr_a5, 0) == 1);
+    }
+}