1313//! Invariants are encoded as ([`Aliasing`], [`Alignment`], [`Validity`])
1414//! triples implementing the [`Invariants`] trait.
1515
16+ use super :: * ;
17+
1618/// The invariants of a [`Ptr`][super::Ptr].
1719pub trait Invariants : Sealed {
1820 type Aliasing : Aliasing ;
@@ -88,7 +90,14 @@ pub trait Validity: Sealed {
8890///
8991/// Given `A: Reference`, callers may assume that either `A = Shared` or `A =
9092/// Exclusive`.
91- pub trait Reference : Aliasing + Sealed { }
93+ pub trait Reference : Aliasing + Sealed {
94+ fn with < ' a , T , I , S , E , O > ( ptr : Ptr < ' a , T , I > , shared : S , exclusive : E ) -> O
95+ where
96+ T : ' a + ?Sized ,
97+ I : Invariants < Aliasing = Self > ,
98+ S : FnOnce ( Ptr < ' a , T , I :: WithAliasing < Shared > > ) -> O ,
99+ E : FnOnce ( Ptr < ' a , T , I :: WithAliasing < Exclusive > > ) -> O ;
100+ }
92101
93102/// No requirement - any invariant is allowed.
94103pub enum Any { }
@@ -129,7 +138,18 @@ impl Aliasing for Shared {
129138 type Variance < ' a , T : ' a + ?Sized > = & ' a T ;
130139 type MappedTo < M : AliasingMapping > = M :: FromShared ;
131140}
132- impl Reference for Shared { }
141+ impl Reference for Shared {
142+ #[ inline( always) ]
143+ fn with < ' a , T , I , S , E , O > ( ptr : Ptr < ' a , T , I > , shared : S , _exclusive : E ) -> O
144+ where
145+ T : ' a + ?Sized ,
146+ I : Invariants < Aliasing = Shared > ,
147+ S : FnOnce ( Ptr < ' a , T , I :: WithAliasing < Shared > > ) -> O ,
148+ E : FnOnce ( Ptr < ' a , T , I :: WithAliasing < Exclusive > > ) -> O ,
149+ {
150+ shared ( ptr. unify_invariants ( ) )
151+ }
152+ }
133153
134154/// The `Ptr<'a, T>` adheres to the aliasing rules of a `&'a mut T`.
135155///
@@ -142,10 +162,21 @@ impl Aliasing for Exclusive {
142162 type Variance < ' a , T : ' a + ?Sized > = & ' a mut T ;
143163 type MappedTo < M : AliasingMapping > = M :: FromExclusive ;
144164}
145- impl Reference for Exclusive { }
165+ impl Reference for Exclusive {
166+ #[ inline( always) ]
167+ fn with < ' a , T , I , S , E , O > ( ptr : Ptr < ' a , T , I > , _shared : S , exclusive : E ) -> O
168+ where
169+ T : ' a + ?Sized ,
170+ I : Invariants < Aliasing = Exclusive > ,
171+ S : FnOnce ( Ptr < ' a , T , I :: WithAliasing < Shared > > ) -> O ,
172+ E : FnOnce ( Ptr < ' a , T , I :: WithAliasing < Exclusive > > ) -> O ,
173+ {
174+ exclusive ( ptr. unify_invariants ( ) )
175+ }
176+ }
146177
147- /// The referent is aligned: for `Ptr<T>`, the referent's address is a
148- /// multiple of the `T`'s alignment.
178+ /// The referent is aligned: for `Ptr<T>`, the referent's address is a multiple
179+ /// of the `T`'s alignment.
149180pub enum Aligned { }
150181impl Alignment for Aligned {
151182 type MappedTo < M : AlignmentMapping > = M :: FromAligned ;
@@ -182,8 +213,8 @@ impl Validity for AsInitialized {
182213 type MappedTo < M : ValidityMapping > = M :: FromAsInitialized ;
183214}
184215
185- /// The byte ranges in the referent are fully initialized. In other words, if
186- /// the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`.
216+ /// The byte ranges in the referent are fully initialized. In other words,
217+ /// if the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`.
187218pub enum Initialized { }
188219impl Validity for Initialized {
189220 type MappedTo < M : ValidityMapping > = M :: FromInitialized ;
@@ -296,6 +327,32 @@ pub use mapping::*;
296327mod mapping {
297328 use super :: * ;
298329
330+ pub trait Mapping {
331+ type Aliasing : AliasingMapping ;
332+ type Alignment : AlignmentMapping ;
333+ type Validity : ValidityMapping ;
334+ }
335+
336+ // TODO: How to make this less error prone? Right now, e.g.,
337+ // `(Preserved, Any, Preserved)` and `(Any, Preserved, Preserved)` both
338+ // implement `Mapping`, and it's not clear from the definition which
339+ // order the invariants come in.
340+ //
341+ // First attempt was to do `Mapping for ((Aliasing, A), (Alignment, AA),
342+ // (Validity, V))`, but not all of `Aliasing`, `Alignment`, and
343+ // `Validity` are object safe.
344+ impl < A : AliasingMapping , AA : AlignmentMapping , V : ValidityMapping > Mapping for ( A , AA , V ) {
345+ type Aliasing = A ;
346+ type Alignment = AA ;
347+ type Validity = V ;
348+ }
349+
350+ impl Mapping for Preserved {
351+ type Aliasing = Preserved ;
352+ type Alignment = Preserved ;
353+ type Validity = Preserved ;
354+ }
355+
299356 pub trait AliasingMapping {
300357 type FromAny : Aliasing ;
301358 type FromShared : Aliasing ;
@@ -314,6 +371,16 @@ mod mapping {
314371 type FromValid : Validity ;
315372 }
316373
374+ // TODO: Better name?
375+ pub enum Preserved { }
376+
377+ #[ allow( type_alias_bounds) ]
378+ pub type Mapped < I : Invariants , M : Mapping > = (
379+ MappedAliasing < I :: Aliasing , M :: Aliasing > ,
380+ MappedAlignment < I :: Alignment , M :: Alignment > ,
381+ MappedValidity < I :: Validity , M :: Validity > ,
382+ ) ;
383+
317384 #[ allow( type_alias_bounds) ]
318385 pub type MappedAliasing < I : Aliasing , M : AliasingMapping > = I :: MappedTo < M > ;
319386
@@ -331,13 +398,42 @@ mod mapping {
331398 type FromExclusive = FromExclusive ;
332399 }
333400
401+ pub enum UnsafeCellMismatch { }
402+
403+ impl AliasingMapping for UnsafeCellMismatch {
404+ type FromAny = Any ;
405+ type FromShared = Any ;
406+ type FromExclusive = Exclusive ;
407+ }
408+
409+ impl AliasingMapping for Preserved {
410+ type FromAny = Any ;
411+ type FromShared = Shared ;
412+ type FromExclusive = Exclusive ;
413+ }
414+
334415 impl < FromAny : Alignment , FromAligned : Alignment > AlignmentMapping
335- for ( ( Any , FromAny ) , ( Shared , FromAligned ) )
416+ for ( ( Any , FromAny ) , ( Aligned , FromAligned ) )
336417 {
337418 type FromAny = FromAny ;
338419 type FromAligned = FromAligned ;
339420 }
340421
422+ impl AlignmentMapping for Any {
423+ type FromAny = Any ;
424+ type FromAligned = Any ;
425+ }
426+
427+ impl AlignmentMapping for Preserved {
428+ type FromAny = Any ;
429+ type FromAligned = Aligned ;
430+ }
431+
432+ impl AlignmentMapping for Aligned {
433+ type FromAny = Aligned ;
434+ type FromAligned = Aligned ;
435+ }
436+
341437 impl <
342438 FromAny : Validity ,
343439 FromAsInitialized : Validity ,
@@ -363,4 +459,39 @@ mod mapping {
363459 type FromInitialized = FromInitialized ;
364460 type FromValid = Any ;
365461 }
462+
463+ impl ValidityMapping for Any {
464+ type FromAny = Any ;
465+ type FromAsInitialized = Any ;
466+ type FromInitialized = Any ;
467+ type FromValid = Any ;
468+ }
469+
470+ impl ValidityMapping for Preserved {
471+ type FromAny = Any ;
472+ type FromAsInitialized = AsInitialized ;
473+ type FromInitialized = Initialized ;
474+ type FromValid = Valid ;
475+ }
476+
477+ impl ValidityMapping for AsInitialized {
478+ type FromAny = AsInitialized ;
479+ type FromAsInitialized = AsInitialized ;
480+ type FromInitialized = AsInitialized ;
481+ type FromValid = AsInitialized ;
482+ }
483+
484+ impl ValidityMapping for Initialized {
485+ type FromAny = Initialized ;
486+ type FromAsInitialized = Initialized ;
487+ type FromInitialized = Initialized ;
488+ type FromValid = Initialized ;
489+ }
490+
491+ impl ValidityMapping for Valid {
492+ type FromAny = Valid ;
493+ type FromAsInitialized = Valid ;
494+ type FromInitialized = Valid ;
495+ type FromValid = Valid ;
496+ }
366497}
0 commit comments