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

creusot_std/std/
sync.rs
