creusot_std/std/sync/
arc.rs

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

creusot_std/std/sync/
arc.rs
