vstd/std_specs/
atomic.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3use core::sync::atomic::*;
4
5// Supports the core::sync::atomic functions
6// This provides NO support for reasoning about the values inside the atomics.
7// If you need to do that, see `vstd::atomic` or `vstd::atomic_ghost` instead.
8#[verifier::external_type_specification]
9#[verifier::external_body]
10#[verifier::reject_recursive_types(T)]
11pub struct ExAtomic<T: AtomicPrimitive>(Atomic<T>);
12
13#[verifier::external_trait_specification]
14pub trait ExAtomicPrimitive: Sized + Copy {
15    type ExternalTraitSpecificationFor: AtomicPrimitive;
16}
17
18#[verifier::external_type_specification]
19pub struct ExOrdering(Ordering);
20
21macro_rules! atomic_specs_common {
22    ($at:ty, $ty:ty) => {
23        verus!{
24
25        pub assume_specification [ <$at>::new ](v: $ty) -> $at;
26
27        pub assume_specification [ <$at>::compare_exchange ](
28            atomic: &$at,
29            current: $ty,
30            new: $ty,
31            success: Ordering,
32            failure: Ordering,
33        ) -> Result<$ty, $ty>;
34
35        pub assume_specification [ <$at>::compare_exchange_weak ](
36            atomic: &$at,
37            current: $ty,
38            new: $ty,
39            success: Ordering,
40            failure: Ordering,
41        ) -> Result<$ty, $ty>;
42
43        pub assume_specification [ <$at>::fetch_and ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
44
45        pub assume_specification [ <$at>::fetch_nand ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
46
47        pub assume_specification [ <$at>::fetch_or ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
48
49        pub assume_specification [ <$at>::fetch_xor ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
50
51        pub assume_specification [ <$at>::load ](atomic: &$at, order: Ordering) -> $ty;
52
53        pub assume_specification [ <$at>::store ](atomic: &$at, val: $ty, order: Ordering);
54
55        pub assume_specification [ <$at>::swap ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
56
57        }
58    };
59}
60
61macro_rules! atomic_specs_int_specific {
62    ($at:ty, $ty:ty) => {
63        verus!{
64
65        pub assume_specification [ <$at>::fetch_add ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
66
67        pub assume_specification [ <$at>::fetch_sub ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
68
69        pub assume_specification [ <$at>::fetch_min ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
70
71        pub assume_specification [ <$at>::fetch_max ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
72
73        }
74    };
75}
76
77macro_rules! atomic_specs_int {
78    ($at:ty, $ty:ty) => {
79        atomic_specs_common!($at, $ty);
80        atomic_specs_int_specific!($at, $ty);
81    };
82}
83
84macro_rules! atomic_specs_bool {
85    ($at:ty, $ty:ty) => {
86        atomic_specs_common!($at, $ty);
87    };
88}
89
90atomic_specs_int!(AtomicU8, u8);
91atomic_specs_int!(AtomicU16, u16);
92atomic_specs_int!(AtomicU32, u32);
93#[cfg(target_has_atomic = "64")]
94atomic_specs_int!(AtomicU64, u64);
95atomic_specs_int!(AtomicUsize, usize);
96
97atomic_specs_int!(AtomicI8, i8);
98atomic_specs_int!(AtomicI16, i16);
99atomic_specs_int!(AtomicI32, i32);
100#[cfg(target_has_atomic = "64")]
101atomic_specs_int!(AtomicI64, i64);
102atomic_specs_int!(AtomicIsize, isize);
103
104atomic_specs_bool!(AtomicBool, bool);
vstd/std_specs/atomic.rs

vstd/std_specs/
atomic.rs
