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]
14#[verifier::external_trait_private_bound(core::sync::atomic::private::Sealed)]
15pub trait ExAtomicPrimitive: Sized + Copy {
16    type ExternalTraitSpecificationFor: AtomicPrimitive;
17}
18
19#[verifier::external_type_specification]
20pub struct ExOrdering(Ordering);
21
22macro_rules! atomic_specs_common {
23    ($at:ty, $ty:ty) => {
24        verus!{
25
26        pub assume_specification [ <$at>::new ](v: $ty) -> $at;
27
28        pub assume_specification [ <$at>::compare_exchange ](
29            atomic: &$at,
30            current: $ty,
31            new: $ty,
32            success: Ordering,
33            failure: Ordering,
34        ) -> Result<$ty, $ty>;
35
36        pub assume_specification [ <$at>::compare_exchange_weak ](
37            atomic: &$at,
38            current: $ty,
39            new: $ty,
40            success: Ordering,
41            failure: Ordering,
42        ) -> Result<$ty, $ty>;
43
44        pub assume_specification [ <$at>::fetch_and ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
45
46        pub assume_specification [ <$at>::fetch_nand ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
47
48        pub assume_specification [ <$at>::fetch_or ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
49
50        pub assume_specification [ <$at>::fetch_xor ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
51
52        pub assume_specification [ <$at>::load ](atomic: &$at, order: Ordering) -> $ty;
53
54        pub assume_specification [ <$at>::store ](atomic: &$at, val: $ty, order: Ordering);
55
56        pub assume_specification [ <$at>::swap ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
57
58        }
59    };
60}
61
62macro_rules! atomic_specs_int_specific {
63    ($at:ty, $ty:ty) => {
64        verus!{
65
66        pub assume_specification [ <$at>::fetch_add ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
67
68        pub assume_specification [ <$at>::fetch_sub ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
69
70        pub assume_specification [ <$at>::fetch_min ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
71
72        pub assume_specification [ <$at>::fetch_max ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
73
74        }
75    };
76}
77
78macro_rules! atomic_specs_int {
79    ($at:ty, $ty:ty) => {
80        atomic_specs_common!($at, $ty);
81        atomic_specs_int_specific!($at, $ty);
82    };
83}
84
85macro_rules! atomic_specs_bool {
86    ($at:ty, $ty:ty) => {
87        atomic_specs_common!($at, $ty);
88    };
89}
90
91atomic_specs_int!(AtomicU8, u8);
92atomic_specs_int!(AtomicU16, u16);
93atomic_specs_int!(AtomicU32, u32);
94#[cfg(target_has_atomic = "64")]
95atomic_specs_int!(AtomicU64, u64);
96atomic_specs_int!(AtomicUsize, usize);
97
98atomic_specs_int!(AtomicI8, i8);
99atomic_specs_int!(AtomicI16, i16);
100atomic_specs_int!(AtomicI32, i32);
101#[cfg(target_has_atomic = "64")]
102atomic_specs_int!(AtomicI64, i64);
103atomic_specs_int!(AtomicIsize, isize);
104
105atomic_specs_bool!(AtomicBool, bool);
vstd/std_specs/atomic.rs

vstd/std_specs/
atomic.rs
