Skip to content

[pointer] Document validity safety invariant #2403

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 6, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 14 additions & 59 deletions src/impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,19 +101,11 @@ safety_comment! {
/// - Given `t: *mut bool` and `let r = *mut u8`, `r` refers to an object
/// of the same size as that referred to by `t`. This is true because
/// `bool` and `u8` have the same size (1 byte) [1]. Neither `r` nor `t`
/// contain `UnsafeCell`s because neither `bool` nor `u8` do [4].
/// - Since the closure takes a `&u8` argument, given a `Maybe<'a,
/// bool>` which satisfies the preconditions of
/// `TryFromBytes::<bool>::is_bit_valid`, it must be guaranteed that the
/// memory referenced by that `MaybeValid` always contains a valid `u8`.
/// Since `bool`'s single byte is always initialized, `is_bit_valid`'s
/// precondition requires that the same is true of its argument. Since
/// `u8`'s only bit validity invariant is that its single byte must be
/// initialized, this memory is guaranteed to contain a valid `u8`.
/// contain `UnsafeCell`s because neither `bool` nor `u8` do [3].
/// - The impl must only return `true` for its argument if the original
/// `Maybe<bool>` refers to a valid `bool`. We only return true if
/// the `u8` value is 0 or 1, and both of these are valid values for
/// `bool`. [3]
/// `Maybe<bool>` refers to a valid `bool`. We only return true if the
/// `u8` value is 0 or 1, and both of these are valid values for `bool`.
/// [2]
///
/// [1] Per https://doc.rust-lang.org/1.81.0/reference/type-layout.html#primitive-data-layout:
///
Expand All @@ -124,16 +116,12 @@ safety_comment! {
/// | `bool` | 1 |
/// | `u8`/`i8` | 1 |
///
/// [2] Per https://doc.rust-lang.org/1.81.0/reference/type-layout.html#size-and-alignment:
///
/// The size of a value is always a multiple of its alignment.
///
/// [3] Per https://doc.rust-lang.org/1.81.0/reference/types/boolean.html:
/// [2] Per https://doc.rust-lang.org/1.81.0/reference/types/boolean.html:
///
/// The value false has the bit pattern 0x00 and the value true has the
/// bit pattern 0x01.
///
/// [4] TODO(#429): Justify this claim.
/// [3] TODO(#429): Justify this claim.
unsafe_impl!(bool: TryFromBytes; |byte: MaybeAligned<u8>| *byte.unaligned_as_ref() < 2);
}
safety_comment! {
Expand All @@ -155,20 +143,10 @@ safety_comment! {
/// - Given `t: *mut char` and `let r = *mut u32`, `r` refers to an object
/// of the same size as that referred to by `t`. This is true because
/// `char` and `u32` have the same size [1]. Neither `r` nor `t` contain
/// `UnsafeCell`s because neither `char` nor `u32` do [4].
/// - Since the closure takes a `&u32` argument, given a `Maybe<'a,
/// char>` which satisfies the preconditions of
/// `TryFromBytes::<char>::is_bit_valid`, it must be guaranteed that the
/// memory referenced by that `MaybeValid` always contains a valid
/// `u32`. Since `char`'s bytes are always initialized [2],
/// `is_bit_valid`'s precondition requires that the same is true of its
/// argument. Since `u32`'s only bit validity invariant is that its
/// bytes must be initialized, this memory is guaranteed to contain a
/// valid `u32`.
/// `UnsafeCell`s because neither `char` nor `u32` do [3].
/// - The impl must only return `true` for its argument if the original
/// `Maybe<char>` refers to a valid `char`. `char::from_u32`
/// guarantees that it returns `None` if its input is not a valid
/// `char`. [3]
/// `Maybe<char>` refers to a valid `char`. `char::from_u32` guarantees
/// that it returns `None` if its input is not a valid `char`. [2]
///
/// [1] Per https://doc.rust-lang.org/nightly/reference/types/textual.html#layout-and-bit-validity:
///
Expand All @@ -177,14 +155,10 @@ safety_comment! {
///
/// [2] Per https://doc.rust-lang.org/core/primitive.char.html#method.from_u32:
///
/// Every byte of a `char` is guaranteed to be initialized.
///
/// [3] Per https://doc.rust-lang.org/core/primitive.char.html#method.from_u32:
///
/// `from_u32()` will return `None` if the input is not a valid value for
/// a `char`.
///
/// [4] TODO(#429): Justify this claim.
/// [3] TODO(#429): Justify this claim.
unsafe_impl!(char: TryFromBytes; |candidate: MaybeAligned<u32>| {
let candidate = candidate.read_unaligned::<BecauseImmutable>();
char::from_u32(candidate).is_some()
Expand Down Expand Up @@ -215,19 +189,9 @@ safety_comment! {
/// `str` and `[u8]` have the same representation. [1] Neither `t` nor
/// `r` contain `UnsafeCell`s because `[u8]` doesn't, and both `t` and
/// `r` have that representation.
/// - Since the closure takes a `&[u8]` argument, given a `Maybe<'a,
/// str>` which satisfies the preconditions of
/// `TryFromBytes::<str>::is_bit_valid`, it must be guaranteed that the
/// memory referenced by that `MaybeValid` always contains a valid
/// `[u8]`. Since `str`'s bytes are always initialized [1],
/// `is_bit_valid`'s precondition requires that the same is true of its
/// argument. Since `[u8]`'s only bit validity invariant is that its
/// bytes must be initialized, this memory is guaranteed to contain a
/// valid `[u8]`.
/// - The impl must only return `true` for its argument if the original
/// `Maybe<str>` refers to a valid `str`. `str::from_utf8`
/// guarantees that it returns `Err` if its input is not a valid `str`.
/// [2]
/// `Maybe<str>` refers to a valid `str`. `str::from_utf8` guarantees
/// that it returns `Err` if its input is not a valid `str`. [2]
///
/// [1] Per https://doc.rust-lang.org/1.81.0/reference/types/textual.html:
///
Expand Down Expand Up @@ -296,18 +260,9 @@ safety_comment! {
/// because `NonZeroXxx` and `xxx` have the same size. [1] Neither `r`
/// nor `t` refer to any `UnsafeCell`s because neither `NonZeroXxx` [2]
/// nor `xxx` do.
/// - Since the closure takes a `&xxx` argument, given a `Maybe<'a,
/// NonZeroXxx>` which satisfies the preconditions of
/// `TryFromBytes::<NonZeroXxx>::is_bit_valid`, it must be guaranteed
/// that the memory referenced by that `MabyeValid` always contains a
/// valid `xxx`. Since `NonZeroXxx`'s bytes are always initialized [1],
/// `is_bit_valid`'s precondition requires that the same is true of its
/// argument. Since `xxx`'s only bit validity invariant is that its
/// bytes must be initialized, this memory is guaranteed to contain a
/// valid `xxx`.
/// - The impl must only return `true` for its argument if the original
/// `Maybe<NonZeroXxx>` refers to a valid `NonZeroXxx`. The only
/// `xxx` which is not also a valid `NonZeroXxx` is 0. [1]
/// `Maybe<NonZeroXxx>` refers to a valid `NonZeroXxx`. The only `xxx`
/// which is not also a valid `NonZeroXxx` is 0. [1]
///
/// [1] Per https://doc.rust-lang.org/1.81.0/core/num/type.NonZeroU16.html:
///
Expand Down
14 changes: 12 additions & 2 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2845,7 +2845,12 @@ unsafe fn try_read_from<S, T: TryFromBytes>(
let c_ptr = Ptr::from_mut(&mut candidate);
let c_ptr = c_ptr.transparent_wrapper_into_inner();
// SAFETY: `c_ptr` has no uninitialized sub-ranges because it derived from
// `candidate`, which the caller promises is entirely initialized.
// `candidate`, which the caller promises is entirely initialized. Since
// `candidate` is a `MaybeUninit`, it has no validity requirements, and so
// no values written to `c_ptr` can violate its validity. Since `c_ptr` has
// `Exclusive` aliasing, no mutations may happen except via `c_ptr` so long
// as it is live, so we don't need to worry about the fact that `c_ptr` may
// have more restricted validity than `candidate`.
let c_ptr = unsafe { c_ptr.assume_validity::<invariant::Initialized>() };

// This call may panic. If that happens, it doesn't cause any soundness
Expand Down Expand Up @@ -4603,7 +4608,12 @@ pub unsafe trait FromBytes: FromZeros {

let ptr = Ptr::from_mut(&mut buf);
// SAFETY: After `buf.zero()`, `buf` consists entirely of initialized,
// zeroed bytes.
// zeroed bytes. Since `MaybeUninit` has no validity requirements, `ptr`
// cannot be used to write values which will violate `buf`'s bit
// validity. Since `ptr` has `Exclusive` aliasing, nothing other than
// `ptr` may be used to mutate `ptr`'s referent, and so its bit validity
// cannot be violated even though `buf` may have more permissive bit
// validity than `ptr`.
let ptr = unsafe { ptr.assume_validity::<invariant::Initialized>() };
let ptr = ptr.as_bytes::<BecauseExclusive>();
src.read_exact(ptr.as_mut())?;
Expand Down
70 changes: 62 additions & 8 deletions src/pointer/invariant.rs
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,48 @@ pub trait Aliasing: Sealed {
pub trait Alignment: Sealed {}

/// The validity invariant of a [`Ptr`][super::Ptr].
pub trait Validity: Sealed {}
///
/// # Safety
///
/// In this section, we will use `Ptr<T, V>` as a shorthand for `Ptr<T, I:
/// Invariants<Validity = V>>` for brevity.
///
/// Each `V: Validity` defines a set of bit values which may appear in the
/// referent of a `Ptr<T, V>`, denoted `S(T, V)`. Each `V: Validity`, in its
/// documentation, provides a definition of `S(T, V)` which must be valid for
/// all `T: ?Sized`. Any `V: Validity` must guarantee that this set is only a
/// function of the *bit validity* of the referent type, `T`, and not of any
/// other property of `T`. As a consequence, given `V: Validity`, `T`, and `U`
/// where `T` and `U` have the same bit validity, `S(V, T) = S(V, U)`.
///
/// It is guaranteed that the referent of any `ptr: Ptr<T, V>` is a member of
/// `S(T, V)`. Unsafe code must ensure that this guarantee will be upheld for
/// any existing `Ptr`s or any `Ptr`s that that code creates.
///
/// An important implication of this guarantee is that it restricts what
/// transmutes are sound, where "transmute" is used in this context to refer to
/// changing the referent type or validity invariant of a `Ptr`, as either
/// change may change the set of bit values permitted to appear in the referent.
/// In particular, the following are necessary (but not sufficient) conditions
/// in order for a transmute from `src: Ptr<T, V>` to `dst: Ptr<U, W>` to be
/// sound:
/// - If `S(T, V) = S(U, W)`, then no restrictions apply; otherwise,
/// - If `dst` permits mutation of its referent (e.g. via `Exclusive` aliasing
/// or interior mutation under `Shared` aliasing), then it must hold that
/// `S(T, V) ⊇ S(U, W)` - in other words, the transmute must not expand the
/// set of allowed referent bit patterns. A violation of this requirement
/// would permit using `dst` to write `x` where `x ∈ S(U, W)` but `x ∉ S(T,
/// V)`, which would violate the guarantee that `src`'s referent may only
/// contain values in `S(T, V)`.
/// - If the referent may be mutated without going through `dst` while `dst` is
/// live (e.g. via interior mutation on a `Shared`-aliased `Ptr` or `&`
/// reference), then it must hold that `S(T, V) ⊆ S(U, W)` - in other words,
/// the transmute must not shrink the set of allowed referent bit patterns. A
/// violation of this requirement would permit using `src` or another
/// mechanism (e.g. a `&` reference used to derive `src`) to write `x` where
/// `x ∈ S(T, V)` but `x ∉ S(U, W)`, which would violate the guarantee that
/// `dst`'s referent may only contain values in `S(U, W)`.
pub unsafe trait Validity: Sealed {}

/// An [`Aliasing`] invariant which is either [`Shared`] or [`Exclusive`].
///
Expand Down Expand Up @@ -90,9 +131,14 @@ impl Alignment for Aligned {}
/// Any bit pattern is allowed in the `Ptr`'s referent, including uninitialized
/// bytes.
pub enum Uninit {}
impl Validity for Uninit {}

/// The byte ranges initialized in `T` are also initialized in the referent.
// SAFETY: `Uninit`'s validity is well-defined for all `T: ?Sized`, and is not a
// function of any property of `T` other than its bit validity (in fact, it's
// not even a property of `T`'s bit validity, but this is more than we are
// required to uphold).
unsafe impl Validity for Uninit {}

/// The byte ranges initialized in `T` are also initialized in the referent of a
/// `Ptr<T>`.
///
/// Formally: uninitialized bytes may only be present in `Ptr<T>`'s referent
/// where they are guaranteed to be present in `T`. This is a dynamic property:
Expand All @@ -119,16 +165,24 @@ impl Validity for Uninit {}
/// enum type, in which case the same rules apply depending on the state of
/// its discriminant, and so on recursively).
pub enum AsInitialized {}
impl Validity for AsInitialized {}
// SAFETY: `AsInitialized`'s validity is well-defined for all `T: ?Sized`, and
// is not a function of any property of `T` other than its bit validity.
unsafe impl Validity for AsInitialized {}

/// The byte ranges in the referent are fully initialized. In other words, if
/// the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`.
pub enum Initialized {}
impl Validity for Initialized {}
// SAFETY: `Initialized`'s validity is well-defined for all `T: ?Sized`, and is
// not a function of any property of `T` other than its bit validity (in fact,
// it's not even a property of `T`'s bit validity, but this is more than we are
// required to uphold).
unsafe impl Validity for Initialized {}

/// The referent is bit-valid for `T`.
/// The referent of a `Ptr<T>` is bit-valid for `T`.
pub enum Valid {}
impl Validity for Valid {}
// SAFETY: `Valid`'s validity is well-defined for all `T: ?Sized`, and is not a
// function of any property of `T` other than its bit validity.
unsafe impl Validity for Valid {}

/// # Safety
///
Expand Down
2 changes: 1 addition & 1 deletion src/pointer/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ where
T: Copy,
T: invariant::Read<Aliasing, R>,
{
// SAFETY: By invariant on `MaybeAligned`, `raw` contains
// SAFETY: By invariant on `MaybeAligned`, `self` contains
// validly-initialized data for `T`. By `T: Read<Aliasing>`, we are
// permitted to perform a read of `self`'s referent.
unsafe { self.as_inner().read_unaligned() }
Expand Down
Loading
Loading