Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Audit: Atomic intrinsics #850

Merged
merged 7 commits into from
Feb 22, 2022
Merged
Show file tree
Hide file tree
Changes from 6 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,7 @@ pub enum BinaryOperand {
Ashr,
Bitand,
Bitor,
Bitnand,
Bitxor,
Div,
Equal,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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() {
Expand Down Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions cprover_bindings/src/irep/to_irep.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
40 changes: 20 additions & 20 deletions docs/src/limitations.md
Original file line number Diff line number Diff line change
Expand Up @@ -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) |
Expand All @@ -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) |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand Down
Original file line number Diff line number Diff line change
@@ -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() {
Expand Down
Original file line number Diff line number Diff line change
@@ -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,
Expand Down
Original file line number Diff line number Diff line change
@@ -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,
Expand Down
Original file line number Diff line number Diff line change
@@ -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,
Expand Down
80 changes: 80 additions & 0 deletions tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs
Original file line number Diff line number Diff line change
@@ -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));
}
}
Loading