1*c3739801SMiguel Ojeda // Copyright 2024 The Fuchsia Authors 2*c3739801SMiguel Ojeda // 3*c3739801SMiguel Ojeda // Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0 4*c3739801SMiguel Ojeda // <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT 5*c3739801SMiguel Ojeda // license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option. 6*c3739801SMiguel Ojeda // This file may not be copied, modified, or distributed except according to 7*c3739801SMiguel Ojeda // those terms. 8*c3739801SMiguel Ojeda 9*c3739801SMiguel Ojeda #![allow(missing_copy_implementations, missing_debug_implementations, missing_docs)] 10*c3739801SMiguel Ojeda 11*c3739801SMiguel Ojeda //! The parameterized invariants of a [`Ptr`][super::Ptr]. 12*c3739801SMiguel Ojeda //! 13*c3739801SMiguel Ojeda //! Invariants are encoded as ([`Aliasing`], [`Alignment`], [`Validity`]) 14*c3739801SMiguel Ojeda //! triples implementing the [`Invariants`] trait. 15*c3739801SMiguel Ojeda 16*c3739801SMiguel Ojeda /// The invariants of a [`Ptr`][super::Ptr]. 17*c3739801SMiguel Ojeda pub trait Invariants: Sealed { 18*c3739801SMiguel Ojeda type Aliasing: Aliasing; 19*c3739801SMiguel Ojeda type Alignment: Alignment; 20*c3739801SMiguel Ojeda type Validity: Validity; 21*c3739801SMiguel Ojeda } 22*c3739801SMiguel Ojeda 23*c3739801SMiguel Ojeda impl<A: Aliasing, AA: Alignment, V: Validity> Invariants for (A, AA, V) { 24*c3739801SMiguel Ojeda type Aliasing = A; 25*c3739801SMiguel Ojeda type Alignment = AA; 26*c3739801SMiguel Ojeda type Validity = V; 27*c3739801SMiguel Ojeda } 28*c3739801SMiguel Ojeda 29*c3739801SMiguel Ojeda /// The aliasing invariant of a [`Ptr`][super::Ptr]. 30*c3739801SMiguel Ojeda /// 31*c3739801SMiguel Ojeda /// All aliasing invariants must permit reading from the bytes of a pointer's 32*c3739801SMiguel Ojeda /// referent which are not covered by [`UnsafeCell`]s. 33*c3739801SMiguel Ojeda /// 34*c3739801SMiguel Ojeda /// [`UnsafeCell`]: core::cell::UnsafeCell 35*c3739801SMiguel Ojeda pub trait Aliasing: Sealed { 36*c3739801SMiguel Ojeda /// Is `Self` [`Exclusive`]? 37*c3739801SMiguel Ojeda #[doc(hidden)] 38*c3739801SMiguel Ojeda const IS_EXCLUSIVE: bool; 39*c3739801SMiguel Ojeda } 40*c3739801SMiguel Ojeda 41*c3739801SMiguel Ojeda /// The alignment invariant of a [`Ptr`][super::Ptr]. 42*c3739801SMiguel Ojeda pub trait Alignment: Sealed { 43*c3739801SMiguel Ojeda #[doc(hidden)] 44*c3739801SMiguel Ojeda #[must_use] 45*c3739801SMiguel Ojeda fn read<T, I, R>(ptr: crate::Ptr<'_, T, I>) -> T 46*c3739801SMiguel Ojeda where 47*c3739801SMiguel Ojeda T: Copy + Read<I::Aliasing, R>, 48*c3739801SMiguel Ojeda I: Invariants<Alignment = Self, Validity = Valid>, 49*c3739801SMiguel Ojeda I::Aliasing: Reference; 50*c3739801SMiguel Ojeda } 51*c3739801SMiguel Ojeda 52*c3739801SMiguel Ojeda /// The validity invariant of a [`Ptr`][super::Ptr]. 53*c3739801SMiguel Ojeda /// 54*c3739801SMiguel Ojeda /// # Safety 55*c3739801SMiguel Ojeda /// 56*c3739801SMiguel Ojeda /// In this section, we will use `Ptr<T, V>` as a shorthand for `Ptr<T, I: 57*c3739801SMiguel Ojeda /// Invariants<Validity = V>>` for brevity. 58*c3739801SMiguel Ojeda /// 59*c3739801SMiguel Ojeda /// Each `V: Validity` defines a set of bit values which may appear in the 60*c3739801SMiguel Ojeda /// referent of a `Ptr<T, V>`, denoted `S(T, V)`. Each `V: Validity`, in its 61*c3739801SMiguel Ojeda /// documentation, provides a definition of `S(T, V)` which must be valid for 62*c3739801SMiguel Ojeda /// all `T: ?Sized`. Any `V: Validity` must guarantee that this set is only a 63*c3739801SMiguel Ojeda /// function of the *bit validity* of the referent type, `T`, and not of any 64*c3739801SMiguel Ojeda /// other property of `T`. As a consequence, given `V: Validity`, `T`, and `U` 65*c3739801SMiguel Ojeda /// where `T` and `U` have the same bit validity, `S(V, T) = S(V, U)`. 66*c3739801SMiguel Ojeda /// 67*c3739801SMiguel Ojeda /// It is guaranteed that the referent of any `ptr: Ptr<T, V>` is a member of 68*c3739801SMiguel Ojeda /// `S(T, V)`. Unsafe code must ensure that this guarantee will be upheld for 69*c3739801SMiguel Ojeda /// any existing `Ptr`s or any `Ptr`s that that code creates. 70*c3739801SMiguel Ojeda /// 71*c3739801SMiguel Ojeda /// An important implication of this guarantee is that it restricts what 72*c3739801SMiguel Ojeda /// transmutes are sound, where "transmute" is used in this context to refer to 73*c3739801SMiguel Ojeda /// changing the referent type or validity invariant of a `Ptr`, as either 74*c3739801SMiguel Ojeda /// change may change the set of bit values permitted to appear in the referent. 75*c3739801SMiguel Ojeda /// In particular, the following are necessary (but not sufficient) conditions 76*c3739801SMiguel Ojeda /// in order for a transmute from `src: Ptr<T, V>` to `dst: Ptr<U, W>` to be 77*c3739801SMiguel Ojeda /// sound: 78*c3739801SMiguel Ojeda /// - If `S(T, V) = S(U, W)`, then no restrictions apply; otherwise, 79*c3739801SMiguel Ojeda /// - If `dst` permits mutation of its referent (e.g. via `Exclusive` aliasing 80*c3739801SMiguel Ojeda /// or interior mutation under `Shared` aliasing), then it must hold that 81*c3739801SMiguel Ojeda /// `S(T, V) ⊇ S(U, W)` - in other words, the transmute must not expand the 82*c3739801SMiguel Ojeda /// set of allowed referent bit patterns. A violation of this requirement 83*c3739801SMiguel Ojeda /// would permit using `dst` to write `x` where `x ∈ S(U, W)` but `x ∉ S(T, 84*c3739801SMiguel Ojeda /// V)`, which would violate the guarantee that `src`'s referent may only 85*c3739801SMiguel Ojeda /// contain values in `S(T, V)`. 86*c3739801SMiguel Ojeda /// - If the referent may be mutated without going through `dst` while `dst` is 87*c3739801SMiguel Ojeda /// live (e.g. via interior mutation on a `Shared`-aliased `Ptr` or `&` 88*c3739801SMiguel Ojeda /// reference), then it must hold that `S(T, V) ⊆ S(U, W)` - in other words, 89*c3739801SMiguel Ojeda /// the transmute must not shrink the set of allowed referent bit patterns. A 90*c3739801SMiguel Ojeda /// violation of this requirement would permit using `src` or another 91*c3739801SMiguel Ojeda /// mechanism (e.g. a `&` reference used to derive `src`) to write `x` where 92*c3739801SMiguel Ojeda /// `x ∈ S(T, V)` but `x ∉ S(U, W)`, which would violate the guarantee that 93*c3739801SMiguel Ojeda /// `dst`'s referent may only contain values in `S(U, W)`. 94*c3739801SMiguel Ojeda pub unsafe trait Validity: Sealed { 95*c3739801SMiguel Ojeda const KIND: ValidityKind; 96*c3739801SMiguel Ojeda } 97*c3739801SMiguel Ojeda 98*c3739801SMiguel Ojeda pub enum ValidityKind { 99*c3739801SMiguel Ojeda Uninit, 100*c3739801SMiguel Ojeda AsInitialized, 101*c3739801SMiguel Ojeda Initialized, 102*c3739801SMiguel Ojeda Valid, 103*c3739801SMiguel Ojeda } 104*c3739801SMiguel Ojeda 105*c3739801SMiguel Ojeda /// An [`Aliasing`] invariant which is either [`Shared`] or [`Exclusive`]. 106*c3739801SMiguel Ojeda /// 107*c3739801SMiguel Ojeda /// # Safety 108*c3739801SMiguel Ojeda /// 109*c3739801SMiguel Ojeda /// Given `A: Reference`, callers may assume that either `A = Shared` or `A = 110*c3739801SMiguel Ojeda /// Exclusive`. 111*c3739801SMiguel Ojeda pub trait Reference: Aliasing + Sealed {} 112*c3739801SMiguel Ojeda 113*c3739801SMiguel Ojeda /// The `Ptr<'a, T>` adheres to the aliasing rules of a `&'a T`. 114*c3739801SMiguel Ojeda /// 115*c3739801SMiguel Ojeda /// The referent of a shared-aliased `Ptr` may be concurrently referenced by any 116*c3739801SMiguel Ojeda /// number of shared-aliased `Ptr` or `&T` references, or by any number of 117*c3739801SMiguel Ojeda /// `Ptr<U>` or `&U` references as permitted by `T`'s library safety invariants, 118*c3739801SMiguel Ojeda /// and may not be concurrently referenced by any exclusively-aliased `Ptr`s or 119*c3739801SMiguel Ojeda /// `&mut` references. The referent must not be mutated, except via 120*c3739801SMiguel Ojeda /// [`UnsafeCell`]s, and only when permitted by `T`'s library safety invariants. 121*c3739801SMiguel Ojeda /// 122*c3739801SMiguel Ojeda /// [`UnsafeCell`]: core::cell::UnsafeCell 123*c3739801SMiguel Ojeda pub enum Shared {} 124*c3739801SMiguel Ojeda impl Aliasing for Shared { 125*c3739801SMiguel Ojeda const IS_EXCLUSIVE: bool = false; 126*c3739801SMiguel Ojeda } 127*c3739801SMiguel Ojeda impl Reference for Shared {} 128*c3739801SMiguel Ojeda 129*c3739801SMiguel Ojeda /// The `Ptr<'a, T>` adheres to the aliasing rules of a `&'a mut T`. 130*c3739801SMiguel Ojeda /// 131*c3739801SMiguel Ojeda /// The referent of an exclusively-aliased `Ptr` may not be concurrently 132*c3739801SMiguel Ojeda /// referenced by any other `Ptr`s or references, and may not be accessed (read 133*c3739801SMiguel Ojeda /// or written) other than via this `Ptr`. 134*c3739801SMiguel Ojeda pub enum Exclusive {} 135*c3739801SMiguel Ojeda impl Aliasing for Exclusive { 136*c3739801SMiguel Ojeda const IS_EXCLUSIVE: bool = true; 137*c3739801SMiguel Ojeda } 138*c3739801SMiguel Ojeda impl Reference for Exclusive {} 139*c3739801SMiguel Ojeda 140*c3739801SMiguel Ojeda /// It is unknown whether the pointer is aligned. 141*c3739801SMiguel Ojeda pub enum Unaligned {} 142*c3739801SMiguel Ojeda 143*c3739801SMiguel Ojeda impl Alignment for Unaligned { 144*c3739801SMiguel Ojeda #[inline(always)] 145*c3739801SMiguel Ojeda fn read<T, I, R>(ptr: crate::Ptr<'_, T, I>) -> T 146*c3739801SMiguel Ojeda where 147*c3739801SMiguel Ojeda T: Copy + Read<I::Aliasing, R>, 148*c3739801SMiguel Ojeda I: Invariants<Alignment = Self, Validity = Valid>, 149*c3739801SMiguel Ojeda I::Aliasing: Reference, 150*c3739801SMiguel Ojeda { 151*c3739801SMiguel Ojeda (*ptr.into_unalign().as_ref()).into_inner() 152*c3739801SMiguel Ojeda } 153*c3739801SMiguel Ojeda } 154*c3739801SMiguel Ojeda 155*c3739801SMiguel Ojeda /// The referent is aligned: for `Ptr<T>`, the referent's address is a multiple 156*c3739801SMiguel Ojeda /// of the `T`'s alignment. 157*c3739801SMiguel Ojeda pub enum Aligned {} 158*c3739801SMiguel Ojeda impl Alignment for Aligned { 159*c3739801SMiguel Ojeda #[inline(always)] 160*c3739801SMiguel Ojeda fn read<T, I, R>(ptr: crate::Ptr<'_, T, I>) -> T 161*c3739801SMiguel Ojeda where 162*c3739801SMiguel Ojeda T: Copy + Read<I::Aliasing, R>, 163*c3739801SMiguel Ojeda I: Invariants<Alignment = Self, Validity = Valid>, 164*c3739801SMiguel Ojeda I::Aliasing: Reference, 165*c3739801SMiguel Ojeda { 166*c3739801SMiguel Ojeda *ptr.as_ref() 167*c3739801SMiguel Ojeda } 168*c3739801SMiguel Ojeda } 169*c3739801SMiguel Ojeda 170*c3739801SMiguel Ojeda /// Any bit pattern is allowed in the `Ptr`'s referent, including uninitialized 171*c3739801SMiguel Ojeda /// bytes. 172*c3739801SMiguel Ojeda pub enum Uninit {} 173*c3739801SMiguel Ojeda // SAFETY: `Uninit`'s validity is well-defined for all `T: ?Sized`, and is not a 174*c3739801SMiguel Ojeda // function of any property of `T` other than its bit validity (in fact, it's 175*c3739801SMiguel Ojeda // not even a property of `T`'s bit validity, but this is more than we are 176*c3739801SMiguel Ojeda // required to uphold). 177*c3739801SMiguel Ojeda unsafe impl Validity for Uninit { 178*c3739801SMiguel Ojeda const KIND: ValidityKind = ValidityKind::Uninit; 179*c3739801SMiguel Ojeda } 180*c3739801SMiguel Ojeda 181*c3739801SMiguel Ojeda /// The byte ranges initialized in `T` are also initialized in the referent of a 182*c3739801SMiguel Ojeda /// `Ptr<T>`. 183*c3739801SMiguel Ojeda /// 184*c3739801SMiguel Ojeda /// Formally: uninitialized bytes may only be present in `Ptr<T>`'s referent 185*c3739801SMiguel Ojeda /// where they are guaranteed to be present in `T`. This is a dynamic property: 186*c3739801SMiguel Ojeda /// if, at a particular byte offset, a valid enum discriminant is set, the 187*c3739801SMiguel Ojeda /// subsequent bytes may only have uninitialized bytes as specified by the 188*c3739801SMiguel Ojeda /// corresponding enum. 189*c3739801SMiguel Ojeda /// 190*c3739801SMiguel Ojeda /// Formally, given `len = size_of_val_raw(ptr)`, at every byte offset, `b`, in 191*c3739801SMiguel Ojeda /// the range `[0, len)`: 192*c3739801SMiguel Ojeda /// - If, in any instance `t: T` of length `len`, the byte at offset `b` in `t` 193*c3739801SMiguel Ojeda /// is initialized, then the byte at offset `b` within `*ptr` must be 194*c3739801SMiguel Ojeda /// initialized. 195*c3739801SMiguel Ojeda /// - Let `c` be the contents of the byte range `[0, b)` in `*ptr`. Let `S` be 196*c3739801SMiguel Ojeda /// the subset of valid instances of `T` of length `len` which contain `c` in 197*c3739801SMiguel Ojeda /// the offset range `[0, b)`. If, in any instance of `t: T` in `S`, the byte 198*c3739801SMiguel Ojeda /// at offset `b` in `t` is initialized, then the byte at offset `b` in `*ptr` 199*c3739801SMiguel Ojeda /// must be initialized. 200*c3739801SMiguel Ojeda /// 201*c3739801SMiguel Ojeda /// Pragmatically, this means that if `*ptr` is guaranteed to contain an enum 202*c3739801SMiguel Ojeda /// type at a particular offset, and the enum discriminant stored in `*ptr` 203*c3739801SMiguel Ojeda /// corresponds to a valid variant of that enum type, then it is guaranteed 204*c3739801SMiguel Ojeda /// that the appropriate bytes of `*ptr` are initialized as defined by that 205*c3739801SMiguel Ojeda /// variant's bit validity (although note that the variant may contain another 206*c3739801SMiguel Ojeda /// enum type, in which case the same rules apply depending on the state of 207*c3739801SMiguel Ojeda /// its discriminant, and so on recursively). 208*c3739801SMiguel Ojeda pub enum AsInitialized {} 209*c3739801SMiguel Ojeda // SAFETY: `AsInitialized`'s validity is well-defined for all `T: ?Sized`, and 210*c3739801SMiguel Ojeda // is not a function of any property of `T` other than its bit validity. 211*c3739801SMiguel Ojeda unsafe impl Validity for AsInitialized { 212*c3739801SMiguel Ojeda const KIND: ValidityKind = ValidityKind::AsInitialized; 213*c3739801SMiguel Ojeda } 214*c3739801SMiguel Ojeda 215*c3739801SMiguel Ojeda /// The byte ranges in the referent are fully initialized. In other words, if 216*c3739801SMiguel Ojeda /// the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`. 217*c3739801SMiguel Ojeda pub enum Initialized {} 218*c3739801SMiguel Ojeda // SAFETY: `Initialized`'s validity is well-defined for all `T: ?Sized`, and is 219*c3739801SMiguel Ojeda // not a function of any property of `T` other than its bit validity (in fact, 220*c3739801SMiguel Ojeda // it's not even a property of `T`'s bit validity, but this is more than we are 221*c3739801SMiguel Ojeda // required to uphold). 222*c3739801SMiguel Ojeda unsafe impl Validity for Initialized { 223*c3739801SMiguel Ojeda const KIND: ValidityKind = ValidityKind::Initialized; 224*c3739801SMiguel Ojeda } 225*c3739801SMiguel Ojeda 226*c3739801SMiguel Ojeda /// The referent of a `Ptr<T>` is valid for `T`, upholding bit validity and any 227*c3739801SMiguel Ojeda /// library safety invariants. 228*c3739801SMiguel Ojeda pub enum Valid {} 229*c3739801SMiguel Ojeda // SAFETY: `Valid`'s validity is well-defined for all `T: ?Sized`, and is not a 230*c3739801SMiguel Ojeda // function of any property of `T` other than its bit validity. 231*c3739801SMiguel Ojeda unsafe impl Validity for Valid { 232*c3739801SMiguel Ojeda const KIND: ValidityKind = ValidityKind::Valid; 233*c3739801SMiguel Ojeda } 234*c3739801SMiguel Ojeda 235*c3739801SMiguel Ojeda /// # Safety 236*c3739801SMiguel Ojeda /// 237*c3739801SMiguel Ojeda /// `DT: CastableFrom<ST, SV, DV>` is sound if `SV = DV = Uninit` or `SV = DV = 238*c3739801SMiguel Ojeda /// Initialized`. 239*c3739801SMiguel Ojeda pub unsafe trait CastableFrom<ST: ?Sized, SV, DV> {} 240*c3739801SMiguel Ojeda 241*c3739801SMiguel Ojeda // SAFETY: `SV = DV = Uninit`. 242*c3739801SMiguel Ojeda unsafe impl<ST: ?Sized, DT: ?Sized> CastableFrom<ST, Uninit, Uninit> for DT {} 243*c3739801SMiguel Ojeda // SAFETY: `SV = DV = Initialized`. 244*c3739801SMiguel Ojeda unsafe impl<ST: ?Sized, DT: ?Sized> CastableFrom<ST, Initialized, Initialized> for DT {} 245*c3739801SMiguel Ojeda 246*c3739801SMiguel Ojeda /// [`Ptr`](crate::Ptr) referents that permit unsynchronized read operations. 247*c3739801SMiguel Ojeda /// 248*c3739801SMiguel Ojeda /// `T: Read<A, R>` implies that a pointer to `T` with aliasing `A` permits 249*c3739801SMiguel Ojeda /// unsynchronized read operations. This can be because `A` is [`Exclusive`] or 250*c3739801SMiguel Ojeda /// because `T` does not permit interior mutation. 251*c3739801SMiguel Ojeda /// 252*c3739801SMiguel Ojeda /// # Safety 253*c3739801SMiguel Ojeda /// 254*c3739801SMiguel Ojeda /// `T: Read<A, R>` if either of the following conditions holds: 255*c3739801SMiguel Ojeda /// - `A` is [`Exclusive`] 256*c3739801SMiguel Ojeda /// - `T` implements [`Immutable`](crate::Immutable) 257*c3739801SMiguel Ojeda /// 258*c3739801SMiguel Ojeda /// As a consequence, if `T: Read<A, R>`, then any `Ptr<T, (A, ...)>` is 259*c3739801SMiguel Ojeda /// permitted to perform unsynchronized reads from its referent. 260*c3739801SMiguel Ojeda pub trait Read<A: Aliasing, R> {} 261*c3739801SMiguel Ojeda 262*c3739801SMiguel Ojeda impl<A: Aliasing, T: ?Sized + crate::Immutable> Read<A, BecauseImmutable> for T {} 263*c3739801SMiguel Ojeda impl<T: ?Sized> Read<Exclusive, BecauseExclusive> for T {} 264*c3739801SMiguel Ojeda 265*c3739801SMiguel Ojeda /// Unsynchronized reads are permitted because only one live [`Ptr`](crate::Ptr) 266*c3739801SMiguel Ojeda /// or reference may exist to the referent bytes at a time. 267*c3739801SMiguel Ojeda #[derive(Copy, Clone, Debug)] 268*c3739801SMiguel Ojeda pub enum BecauseExclusive {} 269*c3739801SMiguel Ojeda 270*c3739801SMiguel Ojeda /// Unsynchronized reads are permitted because no live [`Ptr`](crate::Ptr)s or 271*c3739801SMiguel Ojeda /// references permit interior mutation. 272*c3739801SMiguel Ojeda #[derive(Copy, Clone, Debug)] 273*c3739801SMiguel Ojeda pub enum BecauseImmutable {} 274*c3739801SMiguel Ojeda 275*c3739801SMiguel Ojeda use sealed::Sealed; 276*c3739801SMiguel Ojeda mod sealed { 277*c3739801SMiguel Ojeda use super::*; 278*c3739801SMiguel Ojeda 279*c3739801SMiguel Ojeda pub trait Sealed {} 280*c3739801SMiguel Ojeda 281*c3739801SMiguel Ojeda impl Sealed for Shared {} 282*c3739801SMiguel Ojeda impl Sealed for Exclusive {} 283*c3739801SMiguel Ojeda 284*c3739801SMiguel Ojeda impl Sealed for Unaligned {} 285*c3739801SMiguel Ojeda impl Sealed for Aligned {} 286*c3739801SMiguel Ojeda 287*c3739801SMiguel Ojeda impl Sealed for Uninit {} 288*c3739801SMiguel Ojeda impl Sealed for AsInitialized {} 289*c3739801SMiguel Ojeda impl Sealed for Initialized {} 290*c3739801SMiguel Ojeda impl Sealed for Valid {} 291*c3739801SMiguel Ojeda 292*c3739801SMiguel Ojeda impl<A: Sealed, AA: Sealed, V: Sealed> Sealed for (A, AA, V) {} 293*c3739801SMiguel Ojeda 294*c3739801SMiguel Ojeda impl Sealed for BecauseImmutable {} 295*c3739801SMiguel Ojeda impl Sealed for BecauseExclusive {} 296*c3739801SMiguel Ojeda } 297