Support atomic exchange primitives

compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs

@@ -280,6 +280,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" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_acq" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "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,25 @@
+// 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() {
+    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,37 @@
+// 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);
+    }
+}