diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 88ee89a44a4e..1524cb736482 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/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" + | "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), diff --git a/src/test/cbmc/Atomics/Stable/Exchange/main.rs b/src/test/cbmc/Atomics/Stable/Exchange/main.rs new file mode 100644 index 000000000000..70e26fb1c7af --- /dev/null +++ b/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 + // 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); +} diff --git a/src/test/cbmc/Atomics/Unstable/AtomicXchg/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicXchg/main.rs new file mode 100644 index 000000000000..92fc0fc752af --- /dev/null +++ b/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); + } +}