Skip to content

Invariant-parameterize Ptr #715

Closed
@jswrenn

Description

@jswrenn

In #406, we introduced the Ptr type to describe pointers that lie somewhere between the invariants of NonNull<T> and &T. This type has both reduced the labor required to track invariants in our documentation, and revealed further opportunities for improvement. Namely: do actually do many things with a Ptr, you must do so through unsafe methods that have further unencapsulated requirements.

I propose that we extend Ptr to handle these conditional invariants, by encoding them as const generic parameters; e.g.:

/// A raw pointer with more restrictions.
///
/// `Ptr<T>` is similar to `NonNull<T>`, but it is more restrictive in the
/// following ways:
/// - It must derive from a valid allocation
/// - It must reference a byte range which is contained inside the
///   allocation from which it derives
///   - As a consequence, the byte range it references must have a size
///     which does not overflow `isize`
/// - `ptr` conforms to the aliasing invariant of `ASSUME_ALIASING`
/// - If `ASSUME_ALIGNMENT`, it must satisfy `T`'s alignment requirement
/// - If `ASSUME_VALIDITY`, it must satisfy `T`'s bit validity requirement
///
/// Thanks to these restrictions, it is easier to prove the soundness of
/// some operations using `Ptr`s.
///
/// `Ptr<'a, T>` is [covariant] in `'a` and `T`.
///
/// [covariant]: https://doc.rust-lang.org/reference/subtyping.html
pub struct Ptr<
    'a,
    T,
    const ASSUME_ALIASING: invariant::Aliasing,
    const ASSUME_ALIGNMENT: bool,
    const ASSUME_VALIDITY: bool,
> where
    T: 'a + ?Sized,
{
    /// INVARIANTS:
    /// 0. `ptr` is derived from some valid Rust allocation, `A`
    /// 1. `ptr` has the same provenance as `A`
    /// 2. `ptr` addresses a byte range which is entirely contained in `A`
    /// 3. `ptr` addresses a byte range whose length fits in an `isize`
    /// 4. `ptr` addresses a byte range which does not wrap around the address
    ///     space
    /// 5. `A` is guaranteed to live for at least `'a`
    /// 6. `T: 'a`
    /// 7. `ptr` conforms to the aliasing invariant of `ASSUME_ALIASING`
    /// 8. If `ASSUME_ALIGNMENT`, `ptr` is validly-aligned for `T`
    /// 9. If `ASSUME_VALIDITY`, `ptr` is validly-initialized for `T`
    ptr: NonNull<T>,
    _lifetime: PhantomData<&'a ()>,
}

// TODO: Replace this module with enums, once it becomes possible to do so.
// Use a unique integer for each invariant kind.
pub mod invariant {
    pub type Aliasing = u8;

    /// No invariants.
    pub const None: Aliasing = 0;
    
    /// The pointer adheres to the aliasing rules of a `&T`.
    pub const Shared: Aliasing = 1;
    
    /// The pointer adheres to the aliasing rules of a `&mut T`. 
    pub const Unique: Aliasing = 2;
}

We would then provide methods for asserting invariants; e.g.:

/// Assumes that `Ptr` adheres to the aliasing requirements of a `&T` reference.
///
/// # Safety
///
/// The caller promises that `Ptr` adheres to the aliasing requirements of a
/// `&T` reference.
impl<
        'a,
        T,
        const ASSUME_ALIASING: invariant::Aliasing,
        const ASSUME_ALIGNMENT: bool,
        const ASSUME_VALIDITY: bool,
    > Ptr<'a, T, ASSUME_ALIASING, ASSUME_ALIGNMENT, ASSUME_VALIDITY>
where
    T: 'a + ?Sized,
{
    pub unsafe fn assume_unique(
        self,
    ) -> Ptr<'a, T, {invariant::Unique}, ASSUME_ALIGNMENT, ASSUME_VALIDITY> {
        // SAFETY: The caller has promised that `Ptr` adheres to the aliasing
        // requirements of a `&T` reference.
        unsafe { Ptr::new(self.ptr) }
    }
}

...forgetting invariants; e.g.:

impl<
        'a,
        T,
        const ASSUME_ALIASING: invariant::Aliasing,
        const ASSUME_ALIGNMENT: bool,
        const ASSUME_VALIDITY: bool,
    > Ptr<'a, T, ASSUME_ALIASING, ASSUME_ALIGNMENT, ASSUME_VALIDITY>
where
    T: 'a + ?Sized,
{
    /// Forgets that `Ptr` has a validity invariant.
    pub fn forget_valid(self) -> Ptr<'a, T, ASSUME_ALIASING, ASSUME_ALIGNMENT, false> {
        // SAFETY: The invariants of `Ptr` when `ASSUME_VALIDITY = false` are a
        // strict subset of the obligations when `ASSUME_VALIDITY = true`.
        unsafe { Ptr::new(self.ptr) }
    }
}

...and safe methods conditioned on those invariants:

impl<'a, T> Ptr<'a, T, { invariant::Shared }, true, true>
where
    T: 'a + ?Sized,
{
    pub fn as_ref(self) -> &'a T {
        // SAFETY:
        // By invariant on `Ptr`:
        // 0. `ptr` is derived from some valid Rust allocation, `A`
        // 1. `ptr` has the same provenance as `A`
        // 2. `ptr` addresses a byte range which is entirely contained in `A`
        // 3. `ptr` addresses a byte range whose length fits in an `isize`
        // 4. `ptr` addresses a byte range which does not wrap around the address
        //     space
        // 5. `A` is guaranteed to live for at least `'a`
        // 6. `T: 'a`
        // 7. `ptr` conforms to the aliasing invariant of a shared reference,
        //    because `ASSUME_ALIASING = invariant::Shared`
        // 8. `ptr` is validly-aligned for `T` because `ASSUME_ALIGNMENT = true`
        // 9. `ptr` is validly-initialized for `T` because `ASSUME_VALIDITY = true`
        unsafe { self.ptr.as_ref() }
    }
}

Why should we do this?

Doing this will help us maintain and document the safety invariants on Ptr and its methods. The above proposal has enough fidelity that we will be able to remove caller-enforced safety conditions on TryFromBytes::is_bit_valid to type invariants on a Ptr<'_, Self, ASSUME_ALIASING = {invariants::Shared}, ASSUME_ALIGNMENT = false, ASSUME_VALIDITY = false> and make is_bit_valid safe.

Unresolved Questions

How should we name things? Does ASSUME_VALIDITY have enough fidelity? How should we express maybe-invalid-but-has-unsafecells-in-the-right-places?

Prototype

https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=f4e7f9df5377bda62ab7e17c0287128a

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions