Skip to content

Commit

Permalink
[pointer] Document validity safety invariant
Browse files Browse the repository at this point in the history
Document the semantics of `Ptr` validity invariants on the `Validity`
trait.

Makes progress on #2226, #1866

gherrit-pr-id: Ie66db9044be1dc310a6b7280a73652a357878376
  • Loading branch information
joshlf committed Mar 3, 2025
1 parent 07cdb8b commit daf3a21
Show file tree
Hide file tree
Showing 6 changed files with 232 additions and 143 deletions.
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

0 comments on commit daf3a21

Please sign in to comment.