creusot_std/std/
sync.rs

1use crate::prelude::*;
2use std::sync::Arc;
3
4#[cfg(creusot)]
5use crate::std::ptr::PointerExt as _;
6
7#[cfg(creusot)]
8use core::ops::Deref;
9
10#[cfg(feature = "nightly")]
11use core::alloc::Allocator;
12
13pub mod atomic_relacq;
14#[cfg(feature = "sc-drf")]
15pub mod atomic_sc;
16
17/// Extension trait for [`Arc`].
18pub trait ArcExt {
19    /// The `T` in `Arc<T>`
20    type Pointee: ?Sized;
21
22    /// Get the underlying raw pointer, in logic.
23    ///
24    /// Used to specify [`Arc::as_ptr`].
25    #[logic]
26    fn as_ptr_logic(self) -> *const Self::Pointee;
27}
28#[cfg(feature = "nightly")]
29impl<T: ?Sized, A: Allocator> ArcExt for Arc<T, A> {
30    type Pointee = T;
31    #[logic(opaque)]
32    fn as_ptr_logic(self) -> *const T {
33        dead
34    }
35}
36
37#[cfg(feature = "nightly")]
38impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Arc<T, A> {
39    type DeepModelTy = T::DeepModelTy;
40    #[logic(open, inline)]
41    fn deep_model(self) -> Self::DeepModelTy {
42        pearlite! { *self.view().deep_model() }
43    }
44}
45
46#[cfg(feature = "nightly")]
47impl<T: ?Sized, A: Allocator> View for Arc<T, A> {
48    type ViewTy = Box<T>;
49    #[logic(opaque)]
50    fn view(self) -> Self::ViewTy {
51        dead
52    }
53}
54
55extern_spec! {
56    impl<T> Arc<T> {
57        #[check(ghost)]
58        #[ensures(*result@ == value)]
59        fn new(value: T) -> Self;
60    }
61
62    impl<T, A: Allocator> Arc<T, A> {
63        #[check(ghost)]
64        #[ensures(result == this.as_ptr_logic())]
65        #[ensures(!result.is_null_logic())]
66        fn as_ptr(this: &Arc<T, A>) -> *const T;
67
68        #[check(terminates)] // Not ghost, as this would allow deducing that there is a finite number of possible `Arc`s.
69        #[ensures(result == (this.as_ptr_logic().deep_model() == other.as_ptr_logic().deep_model()))]
70        #[ensures(result ==> this@ == other@)]
71        fn ptr_eq(this: &Arc<T, A>, other: &Arc<T, A>) -> bool;
72    }
73
74    impl<T, A: Allocator> AsRef<T> for Arc<T, A> {
75        #[check(ghost)]
76        #[ensures(*result == *(*self)@)]
77        fn as_ref(&self) -> &T;
78    }
79
80    impl<T: ?Sized, A: Allocator + Clone> Clone for Arc<T, A> {
81        #[check(ghost)]
82        #[ensures(result == *self)]
83        fn clone(&self) -> Arc<T, A>;
84    }
85
86    impl<T: ?Sized, A: Allocator> Deref for Arc<T, A> {
87        #[check(ghost)]
88        #[ensures(*result == *(*self)@)]
89        fn deref(&self) -> &T { self.as_ref() }
90    }
91}
92
93/// Dummy impls that don't use the unstable trait Allocator
94#[cfg(not(feature = "nightly"))]
95impl<T: DeepModel> DeepModel for Arc<T> {
96    type DeepModelTy = T::DeepModelTy;
97}
98
99#[cfg(not(feature = "nightly"))]
100impl<T> View for Arc<T> {
101    type ViewTy = T;
102}
creusot_std/std/sync.rs

creusot_std/std/
sync.rs
