creusot_std/std/
rc.rs

1#[cfg(creusot)]
2use crate::std::ptr::PointerExt as _;
3use crate::{logic::ops::DerefLogic, prelude::*};
4#[cfg(feature = "nightly")]
5use std::alloc::Allocator;
6#[cfg(creusot)]
7use std::ops::Deref;
8use std::rc::Rc;
9
10/// Extension trait for [`Rc`].
11pub trait RcExt {
12    /// The `T` in `Rc<T>`
13    type Pointee: ?Sized;
14
15    /// Get the underlying raw pointer, in logic.
16    ///
17    /// Used to specify [`Rc::as_ptr`].
18    #[logic]
19    fn as_ptr_logic(self) -> *const Self::Pointee;
20}
21
22#[cfg(feature = "nightly")]
23impl<T: ?Sized, A: Allocator> RcExt for Rc<T, A> {
24    type Pointee = T;
25    #[logic(opaque)]
26    fn as_ptr_logic(self) -> *const T {
27        dead
28    }
29}
30
31#[cfg(feature = "nightly")]
32impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Rc<T, A> {
33    type DeepModelTy = T::DeepModelTy;
34    #[logic(open, inline)]
35    fn deep_model(self) -> Self::DeepModelTy {
36        pearlite! { (*self).deep_model() }
37    }
38}
39
40#[cfg(feature = "nightly")]
41impl<T: ?Sized, A: Allocator> DerefLogic for Rc<T, A> {
42    #[logic(opaque)]
43    fn deref_logic(&self) -> &T {
44        dead
45    }
46}
47
48extern_spec! {
49    #[trusted(positive(T))]
50    type Rc<T>;
51
52    impl<T> Rc<T> {
53        /// Note: if you want to have a `Rc` in ghost code, please use
54        /// [`crate::ghost::GhostShared`].
55        #[check(terminates)] // Not ghost, to avoid exhausting all possible `Rc`
56                             // addresses. This could be observed by `ptr_eq`.
57        #[ensures(*result == value)]
58        fn new(value: T) -> Self;
59    }
60
61    impl<T, A: Allocator> Rc<T, A> {
62        #[check(ghost)]
63        #[ensures(result == this.as_ptr_logic())]
64        #[ensures(!result.is_null_logic())]
65        fn as_ptr(this: &Rc<T, A>) -> *const T;
66
67        #[check(ghost)]
68        #[ensures(result == (this.as_ptr_logic().addr_logic() == other.as_ptr_logic().addr_logic()))]
69        #[ensures(result ==> this == other)]
70        fn ptr_eq(this: &Rc<T, A>, other: &Rc<T, A>) -> bool;
71    }
72
73
74    impl<T, A: Allocator> AsRef<T> for Rc<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 Rc<T, A> {
81        #[check(terminates)] // Not ghost: see `Rc::new`
82        #[ensures(result == *self)]
83        fn clone(&self) -> Rc<T, A>;
84    }
85
86    impl<T: ?Sized, A: Allocator> Deref for Rc<T, A> {
87        #[check(ghost)]
88        #[logic_alias(self.deref_logic())]
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 + ?Sized> DeepModel for Rc<T> {
96    type DeepModelTy = T::DeepModelTy;
97}
98
99#[cfg(not(feature = "nightly"))]
100impl<T: ?Sized> DerefLogic for Rc<T> {}
creusot_std/std/rc.rs

creusot_std/std/
rc.rs
