-
Notifications
You must be signed in to change notification settings - Fork 138
Description
This design obsoletes or incorporates the following pre-existing issues:
- Obsoletes Extend
Ptrto store unboxed values #1875 - Obsoletes Overhaul
Ptr's validity invariant modeling #1866 - Incorporates Generic transmutability #1359 with the exception that invariant types will now live on the new
Valuetype instead of onPtr
Co-authored with @jswrenn
Overview
- Add a new
Valuetype which tracks a value's alignment and validity - Remove the alignment and validity invariants from
Ptr - Replace
Ptr<T>withPtr<Value<T>>as appropriate - Support generic transmutation as described in Generic transmutability #1359
Background
Recent issues such as #1866, #1889, and #2226 have demonstrated that our existing conception of invariants in Ptr is flawed. In particular, we have historically conceived of invariants as being monotonically increasing in strictness (e.g., Valid is a subset of AsInitialized). We've recently realized that this is incomplete: sometimes invariants also impose a upper- as well as a lower-bound on behavior. See #1866 for a detailed discussion of how this can lead to unsoundness.
Mental model
We've come to the following mental model that provides a unified explanation for all of these issues.
A naive understanding of Ptr invariants suggests that they simply encode knowledge. For example, a ptr: Ptr<T, Valid> encodes the knowledge that ptr's referent is a bit-valid T. However, reborrowing complicates this story.
Consider, as outlined in #1866, t: Ptr<T>. Naively, I should be able to convert this to mu: Ptr<MaybeUninit<T>, Valid> regardless of t's validity invariant; after all, all byte sequences are valid instances of MaybeUninit<T>. However, if we rephrase this in terms of references, that's clearly invalid! Going from &mut T to &mut MaybeUninit<T> is unsound, as the latter reference can be used to write arbitrary bytes to a memory location which is referenced as a &mut T.
This highlights that we need to not only consider the current type (i.e., the T in Ptr<T>), but also the types of all references/Ptrs from which the current Ptr is reborrowed (its "ancestors", to coin a phrase). If we do this, then we can reconceptualize the invariant as not only providing knowledge about the current value of the Ptr's referent, but also a constraint about what values are permitted to be written to the referent. In particular, all values written to the referent must be valid for all ancestor references/Ptrs.
Note that this only affects validity, but not aliasing or alignment. Aliasing is a compile-time property, and so it cannot change at runtime. Alignment is a property of a particular Ptr (and not of its ancestors) and so it really is just a matter of knowledge, not a constraint (in other words, "forgetting" that a Ptr is aligned can never cause problems).
Thus, we can reconceptualize the validity invariant in the following way:
- A
Ptr<T, Validity>has typeTand validityValidity - A pair of type and validity,
(T, Validity), defines a set of valid values,V. For example,(bool, Valid)defines the set{0x00, 0x01}, and(bool, AsInitialized)defines the set{0x00, ..., 0x255}. Note that changing the type and changing the validity can both affectV. - Code is permitted to assume that only values in
Vwill be present in the referent - Code must promise to only write values in
Vto the referent - Code may only change
Vin a way that doesn't violate the preceding two requirements. As mentioned above, this implicates both invariant changes and type transmutations.
In this conception, a pair of type and validity has more degrees of freedom than we actually need. We can change both the type and the validity, but at the end of the day, all we care about is the set of valid values.* In fact, "set of valid values" is really what a type is. This suggests that we just need a type-level representation of... types? Yes!
* Except that type implicates pointer metadata, but that's orthogonal to the present discussion.
In particular, we need the ability for Ptr<T> to encode the invariants that we currently encode separately (alignment and validity). In theory, we could do this using "memory gadgets" like Unalign, MaybeUninit, and a hypothetical future MaybeValid (TODO: Reference issue number). However, we've found that these can have expressivity issues regarding Sized-ness, and nesting gets especially weird (e.g., how do support transmuting Unalign<T> to Unalign<MaybeUninit<T>>?).
Instead, this issue proposes a generic Value type which is the generalization of Unalign, MaybeUninit, and MaybeValid. We still encode alignment and validity in type-level parameters as we do today, but we move these from Ptr to Value, leaving Ptr with only an aliasing invariant.
Design
- Need type-level representation of alignment so that we can write
impl TransmuteFromPtr<Src>: TransmuteFrom<Src> where Src::Alignment: Gt<Dst::Alignment> {}- Requires us to drop support for
repr(Rust)types
- Requires us to drop support for