creusot_std/std/
rc.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::std::ptr::PointerExt as _;
4#[cfg(creusot)]
5use std::ops::Deref;
6use std::rc::Rc;
7#[cfg(feature = "nightly")]
8use std::{alloc::Allocator, boxed::Box};
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.view().deep_model() }
37    }
38}
39
40#[cfg(feature = "nightly")]
41impl<T: ?Sized, A: Allocator> View for Rc<T, A> {
42    type ViewTy = Box<T>;
43    #[logic(opaque)]
44    fn view(self) -> Self::ViewTy {
45        dead
46    }
47}
48
49extern_spec! {
50    #[trusted(positive(T))]
51    type Rc<T>;
52
53    impl<T> Rc<T> {
54        /// Note: if you want to have a `Rc` in ghost code, please use
55        /// [`crate::ghost::GhostShared`].
56        #[check(terminates)] // Not ghost, to avoid exhausting all possible `Rc`
57                             // addresses. This could be observed by `ptr_eq`.
58        #[ensures(*result@ == value)]
59        fn new(value: T) -> Self;
60    }
61
62    impl<T, A: Allocator> Rc<T, A> {
63        #[check(ghost)]
64        #[ensures(result == this.as_ptr_logic())]
65        #[ensures(!result.is_null_logic())]
66        fn as_ptr(this: &Rc<T, A>) -> *const T;
67
68        #[check(ghost)]
69        #[ensures(result == (this.as_ptr_logic().addr_logic() == other.as_ptr_logic().addr_logic()))]
70        #[ensures(result ==> this == other)]
71        fn ptr_eq(this: &Rc<T, A>, other: &Rc<T, A>) -> bool;
72    }
73
74
75    impl<T, A: Allocator> AsRef<T> for Rc<T, A> {
76        #[check(ghost)]
77        #[ensures(*result == *(*self)@)]
78        fn as_ref(&self) -> &T;
79    }
80
81    impl<T: ?Sized, A: Allocator + Clone> Clone for Rc<T, A> {
82        #[check(terminates)] // Not ghost: see `Rc::new`
83        #[ensures(result == *self)]
84        fn clone(&self) -> Rc<T, A>;
85    }
86
87    impl<T: ?Sized, A: Allocator> Deref for Rc<T, A> {
88        #[check(ghost)]
89        #[ensures(*result == *(*self)@)]
90        fn deref(&self) -> &T { self.as_ref() }
91    }
92}
93
94/// Dummy impls that don't use the unstable trait Allocator
95#[cfg(not(feature = "nightly"))]
96impl<T: DeepModel> DeepModel for Rc<T> {
97    type DeepModelTy = T::DeepModelTy;
98}
99
100#[cfg(not(feature = "nightly"))]
101impl<T> View for Rc<T> {
102    type ViewTy = T;
103}
creusot_std/std/rc.rs

creusot_std/std/
rc.rs
