diff --git a/src/lib.rs b/src/lib.rs index 16f6fccdc5..38069281c3 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -243,6 +243,7 @@ mod macros; pub mod byteorder; #[doc(hidden)] pub mod macro_util; +mod proof_utils; mod util; // TODO(#252): If we make this pub, come up with a better name. mod wrappers; @@ -2501,47 +2502,24 @@ safety_comment! { } safety_comment! { /// SAFETY: - /// `Wrapping` is guaranteed by its docs [1] to have the same layout and - /// bit validity as `T`. Also, `Wrapping` is `#[repr(transparent)]`, and - /// has a single field, which is `pub`. Per the reference [2], this means - /// that the `#[repr(transparent)]` attribute is "considered part of the - /// public ABI". - /// - /// - `TryFromBytes`: The safety requirements for `unsafe_impl!` with an - /// `is_bit_valid` closure: - /// - Given `t: *mut Wrapping` and `let r = *mut T`, `r` refers to an - /// object of the same size as that referred to by `t`. This is true - /// because `Wrapping` and `T` have the same layout - /// - The alignment of `Wrapping` is equal to the alignment of `T`. - /// - The impl must only return `true` for its argument if the original - /// `Ptr>` refers to a valid `Wrapping`. Since - /// `Wrapping` has the same bit validity as `T`, and since our impl - /// just calls `T::is_bit_valid`, our impl returns `true` exactly when - /// its argument contains a valid `Wrapping`. - /// - `FromBytes`: Since `Wrapping` has the same bit validity as `T`, if - /// `T: FromBytes`, then all initialized byte sequences are valid - /// instances of `Wrapping`. Similarly, if `T: FromBytes`, then - /// `Wrapping` doesn't contain any `UnsafeCell`s. Thus, `impl FromBytes - /// for Wrapping where T: FromBytes` is a sound impl. - /// - `AsBytes`: Since `Wrapping` has the same bit validity as `T`, if - /// `T: AsBytes`, then all valid instances of `Wrapping` have all of - /// their bytes initialized. Similarly, if `T: AsBytes`, then - /// `Wrapping` doesn't contain any `UnsafeCell`s. Thus, `impl AsBytes - /// for Wrapping where T: AsBytes` is a valid impl. - /// - `Unaligned`: Since `Wrapping` has the same layout as `T`, - /// `Wrapping` has alignment 1 exactly when `T` does. - /// - /// [1] Per https://doc.rust-lang.org/core/num/struct.NonZeroU16.html: - /// - /// `NonZeroU16` is guaranteed to have the same layout and bit validity as - /// `u16` with the exception that `0` is not a valid instance. - /// - /// TODO(#429): Add quotes from documentation. - /// - /// [1] TODO(https://doc.rust-lang.org/nightly/core/num/struct.Wrapping.html#layout-1): - /// Reference this documentation once it's available on stable. - /// - /// [2] https://doc.rust-lang.org/nomicon/other-reprs.html#reprtransparent + /// `Wrapping` is `#[repr(transparent)]` and has a single `T` field, + /// which is `pub`. [1] Per axiom-repr-transparent-layout-validity, we may + /// take this to imply that `Wrapping: transparent-layout-validity(T)`. + /// This is bolstered by [2]. + /// - `TryFromBytes`: Since the closure takes `Ptr`, `Wrapping: + /// transparent-layout-validity(T)` satisfies `unsafe_impl!`'s safety + /// preconditions. + /// - `FromZeroes`, `FromBytes`, `AsBytes`, `Unaligned`: Per + /// lemma-repr-transparent-zerocopy-traits, since `Wrapping: + /// transparent-layout-validity(T)`, if `T` satisfies the safety + /// preconditions of `FromZeroes`, `FromBytes`, `AsBytes`, or `Unaligned`, + /// then `Wrapping` does too (respectively). + /// + /// [1] https://doc.rust-lang.org/core/num/struct.Wrapping.html + /// + /// [2] Per https://doc.rust-lang.org/nightly/core/num/struct.Wrapping.html: + /// + /// `Wrapping` is guaranteed to have the same layout and ABI as `T`. unsafe_impl!(T: TryFromBytes => TryFromBytes for Wrapping; |candidate: Ptr| { // SAFETY: // - Since `T` and `Wrapping` have the same layout and bit validity @@ -2589,31 +2567,19 @@ safety_comment! { } safety_comment! { /// SAFETY: - /// `ManuallyDrop` has the same layout and bit validity as `T` [1], and - /// accessing the inner value is safe (meaning that it's unsound to leave - /// the inner value uninitialized while exposing the `ManuallyDrop` to safe - /// code). - /// - `FromZeroes`, `FromBytes`: Since it has the same layout as `T`, any - /// valid `T` is a valid `ManuallyDrop`. If `T: FromZeroes`, a sequence - /// of zero bytes is a valid `T`, and thus a valid `ManuallyDrop`. If - /// `T: FromBytes`, any sequence of bytes is a valid `T`, and thus a valid - /// `ManuallyDrop`. - /// - `AsBytes`: Since it has the same layout as `T`, and since it's unsound - /// to let safe code access a `ManuallyDrop` whose inner value is - /// uninitialized, safe code can only ever access a `ManuallyDrop` whose - /// contents are a valid `T`. Since `T: AsBytes`, this means that safe - /// code can only ever access a `ManuallyDrop` with all initialized bytes. - /// - `Unaligned`: `ManuallyDrop` has the same layout (and thus alignment) - /// as `T`, and `T: Unaligned` guarantees that that alignment is 1. - /// - /// `ManuallyDrop` is guaranteed to have the same layout and bit - /// validity as `T` + /// `ManuallyDrop` has the same layout and bit validity as `T` [1]. Per + /// axiom-transparent-layout-validity, we may use this to assume that + /// `ManuallyDrop: transparent-layout-validity(T)`. Per + /// lemma-repr-transparent-zerocopy-traits, if `T` satisfies the safety + /// preconditions of `FromZeroes`, `FromBytes`, `AsBytes`, or `Unaligned`, + /// then `ManuallyDrop` does too (respectively). /// /// [1] Per https://doc.rust-lang.org/nightly/core/mem/struct.ManuallyDrop.html: /// - /// TODO(#429): - /// - Add quotes from docs. - /// - Once [1] (added in + /// `ManuallyDrop` is guaranteed to have the same layout and bit + /// validity as `T`. + /// + /// TODO(#429): Once [1] (added in /// https://github.com/rust-lang/rust/pull/115522) is available on stable, /// quote the stable docs instead of the nightly docs. unsafe_impl!(T: ?Sized + FromZeroes => FromZeroes for ManuallyDrop); diff --git a/src/macros.rs b/src/macros.rs index 2da78af7df..dcc6a6dd28 100644 --- a/src/macros.rs +++ b/src/macros.rs @@ -44,18 +44,22 @@ macro_rules! safety_comment { /// be the case that any initialized sequence of bytes constitutes a valid /// instance of `$ty`. /// - If an `is_bit_valid` impl is provided, then: -/// - Regardless of whether the provided closure takes a `Ptr<$repr>` or -/// `&$repr` argument, it must be the case that, given `t: *mut $ty` and -/// `let r = t as *mut $repr`, `r` refers to an object of equal or lesser -/// size than the object referred to by `t`. -/// - If the provided closure takes a `&$repr` argument, then given a `Ptr<'a, -/// $ty>` which satisfies the preconditions of +/// - If `$ty: !transparent-layout-validity($repr)`, all of the following must +/// hold: +/// - Given `t: *mut $ty` and `let r = t as *mut $repr`, `r` refers to an +/// object of equal or lesser size than the object referred to by `t`. +/// - The alignment of `$repr` is less than or equal to the alignment of +/// `$ty`. +/// - If the provided closure takes a `&$repr` argument, then given a +/// `Ptr<'a, $ty>` which satisfies the preconditions of /// `TryFromBytes::<$ty>::is_bit_valid`, it must be guaranteed that the /// memory referenced by that `Ptr` always contains a valid `$repr`. -/// - The alignment of `$repr` is less than or equal to the alignment of -/// `$ty`. -/// - The impl of `is_bit_valid` must only return `true` for its argument -/// `Ptr<$repr>` if the original `Ptr<$ty>` refers to a valid `$ty`. +/// - At least one of the following must hold: +/// - The impl of `is_bit_valid` must only return `true` for its argument +/// `Ptr<$repr>` if the original `Ptr<$ty>` refers to a valid `$ty`. +/// - `$ty: transparent-layout-validity($repr)`, the provided closure takes +/// a `Ptr<'a, $repr>`, and the body of the closure is equal to +/// `TryFromBytes::<$repr>::is_bit_valid`. macro_rules! unsafe_impl { // Implement `$trait` for `$ty` with no bounds. ($(#[$attr:meta])* $ty:ty: $trait:ident $(; |$candidate:ident: &$repr:ty| $is_bit_valid:expr)?) => { @@ -133,15 +137,20 @@ macro_rules! unsafe_impl { }; (@method TryFromBytes ; |$candidate:ident: &$repr:ty| $is_bit_valid:expr) => { + // SAFETY: The caller has promised that this implementation is correct. #[inline] unsafe fn is_bit_valid(candidate: Ptr<'_, Self>) -> bool { // SAFETY: // - The argument to `cast_unsized` is `|p| p as *mut _` as required // by that method's safety precondition. - // - The caller has promised that the cast results in an object of - // equal or lesser size. - // - The caller has promised that `$repr`'s alignment is less than - // or equal to `Self`'s alignment. + // - Either the caller has promised that the cast results in an + // object of equal or lesser size, or `$ty: + // transparent-layout-validity($repr)`, which guarantees that the + // cast results in an object of equal size. + // - Either the caller has promised that `$repr`'s alignment is less + // than or equal to `Self`'s alignment, or `$ty: + // transparent-layout-validity($repr)`, which guarantees that + // `$repr` and `$ty` have the same alignment. #[allow(clippy::as_conversions)] let candidate = unsafe { candidate.cast_unsized::<$repr, _>(|p| p as *mut _) }; // SAFETY: @@ -160,15 +169,26 @@ macro_rules! unsafe_impl { } }; (@method TryFromBytes ; |$candidate:ident: Ptr<$repr:ty>| $is_bit_valid:expr) => { + // SAFETY: At least one of the following holds: + // - The caller has promised that this implementation is correct. + // - `$ty: transparent-layout-validity($repr)` and the body is equal to + // `TryFromBytes::<$repr>::is_bit_valid`. In this case, the bit + // validity of `$ty` and `$repr` are equivalent, and so + // `TryFromBytes::<$repr>::is_bit_valid` is a valid implementation of + // `TryFromBytes::<$ty>::is_bit_valid`. #[inline] unsafe fn is_bit_valid(candidate: Ptr<'_, Self>) -> bool { // SAFETY: // - The argument to `cast_unsized` is `|p| p as *mut _` as required // by that method's safety precondition. - // - The caller has promised that the cast results in an object of - // equal or lesser size. - // - The caller has promised that `$repr`'s alignment is less than - // or equal to `Self`'s alignment. + // - Either the caller has promised that the cast results in an + // object of equal or lesser size, or `$ty: + // transparent-layout-validity($repr)`, which guarantees that the + // cast results in an object of equal size. + // - Either the caller has promised that `$repr`'s alignment is less + // than or equal to `Self`'s alignment, or `$ty: + // transparent-layout-validity($repr)`, which guarantees that + // `$repr` and `$ty` have the same alignment. #[allow(clippy::as_conversions)] let $candidate = unsafe { candidate.cast_unsized::<$repr, _>(|p| p as *mut _) }; $is_bit_valid diff --git a/src/proof_utils.rs b/src/proof_utils.rs new file mode 100644 index 0000000000..157a558bcf --- /dev/null +++ b/src/proof_utils.rs @@ -0,0 +1,117 @@ +// Copyright 2023 The Fuchsia Authors +// +// Licensed under a BSD-style license , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! This module exists to hold this doc comment, which provides lemmas which can +//! be used in soundness proofs. +//! +//! # Definitions +//! +//! ## transparent-layout-validity +//! +//! A type, `T`, has the property `transparent-layout-validity(U)` if the +//! following all hold: +//! - `T` and `U` have the same alignment +//! - For all `t: *const T`, `let u = t as *const U` is valid and +//! `size_of_val_raw(t) == size_of_val_raw(u)`. +//! - For all `u: *const U`, `let t = *const T` is valid and `size_of_val_raw(u) +//! == size_of_val_raw(t)`. +//! - For all `(t, u): (*const T, *const U)` where `size_of_val_raw(t) == +//! size_of_val_raw(u)`: +//! - `t` and `u` refer to `UnsafeCell`s at the same byte ranges. +//! - If `*t` contains a valid `T`, that implies that `*u` contains a valid +//! `U`. +//! - If `*u` contains a valid `U`, that implies that `*t` contains a valid +//! `T`. +//! +//! # Axioms +//! +//! These are statements which are not technically logically bulletproof, but +//! capture the way that language is used in practice in the Rust Reference and +//! standard library documentation. +//! +//! ## axiom-transparent-layout-validity +//! +//! Given types `T` and `U`, the phrase "`T` is guaranteed to have the same +//! layout and bit validity as `U`" is taken to imply that `T` has the property +//! `transparent-layout-validity(U)`. +//! +//! The term "layout" is used in Rust documentation to refer to a type's size +//! and alignment and the sizes, alignments, and byte offsets of each of the +//! type's fields. In practice, phrases like the above are only ever used in +//! contexts where the following additional properties also hold: +//! - `T` and `U` have the same vtable kinds. `T`'s and `U`'s pointer metadata +//! is such that raw pointer casts preserve size and field placement. +//! - `T` and `U` have `UnsafeCell`s at the same byte ranges. +//! +//! ## axiom-repr-transparent-layout-validity +//! +//! Given types `T` and `U`, if `T` is a `#[repr(transparent)]` struct with a +//! `pub` field of type `U`, and `T` does not contain any other fields, then +//! `T` has the property `transparent-layout-validity(U)`. +//! +//! Per the [Rust Reference][repr-transparent]: +//! +//! > \[`repr(transparent)`\] is only considered part of the public ABI of a +//! > type if either its single field is `pub`, or if its layout is documented +//! > in prose. +//! +//! [repr-transparent]: https://doc.rust-lang.org/nomicon/other-reprs.html#reprtransparent +//! +//! # Lemmas +//! +//! ## lemma-repr-transparent-zerocopy-traits +//! +//! - Lemma: Given types `T` and `U` where `T` is +//! `transparent-layout-validity(U)`, for each `Trait` in `FromZeroes`, +//! `FromBytes`, `AsBytes`, and `Unaligned`, if `U` satisfies the safety +//! preconditions of `Trait`, then `T` does as well. +//! - Proof: +//! - `FromZeroes`, `FromBytes`, and `AsBytes` all require that a type not +//! contain any `UnsafeCell`s. `T: transparent-layout-validity(U)` +//! guarantees that, for all pairs of `t: *const T` and `u: *const U` of +//! equal size, `t` and `u` refer to `UnsafeCell`s at the same byte ranges. +//! If `U: FromZeroes`, `U: FromBytes`, or `U: AsBytes`, no instance of `U` +//! contains `UnsafeCell`s at any byte ranges. Thus, no instance of `T` +//! contains `UnsafeCell`s at any byte ranges. +//! - `U: FromZeroes` additionally requires that, given `u: *const U`, it is +//! sound to initialize `*u` to contain all zero bytes. Since, for all `t: +//! *const T` and `u: *const U` of equal size, `*t` and `*u` have equal bit +//! validity, then it must also be the case that, given `t: *const T`, it is +//! sound to initialize `*t` to contain all zero bytes. +//! - `U: FromBytes` additionally requires that, given `u: *const U`, it is +//! sound to initialize `*u` to contain any sequence of `u8`s. Since, for +//! all `t: *const T` and `u: *const U` of equal size, `*t` and `*u` have +//! equal bit validity, then it must also be the case that, given `t: *const +//! T`, it is sound to initialize `*t` to contain any sequence of `u8`s. +//! - `U: AsBytes` additionally requires that, given `u: &U`, it is sound to +//! treat `t` as an immutable `[u8]` of length `size_of_val(u)`. This is +//! equivalent to saying that no instance of `U` can contain bytes which are +//! invalid for `u8`. Since, for all `t: *const T` and `u: *const U` of +//! equal size, `*t` and `*u` have equal bit validity, then it must also be +//! the case that no instance of `T` can contain bytes which are invalid for +//! `u8`. +//! - `U: Unaligned` requires that `U`'s alignment is 1. `T: +//! transparent-layout-validity(U)` guarantees that `T`'s alignment is equal +//! to `U`'s, and is thus also 1. +//! +//! ## lemma-transparent-layout-validity-is-bit-valid +//! +//! - Lemma: Given `T` and `U` where `T` is `transparent-layout-validity(U)`, +//! given `t: Ptr<'a, T>` which satisfies the safety preconditions of +//! `TryFromBytes::::is_bit_valid`, and given `u: Ptr<'a, U>` which +//! addresses the same range as `t`, `u` satisfies the safety preconditions of +//! `TryFromBytes::::is_bit_valid`. +//! - Proof: TODO +//! +//! WARNING: This might not actually be sound! In particular, `T: +//! transparent-layout-validity(U)` doesn't guarantee that, given an enum +//! discriminant with a particular value, the subset of values of `T` which are +//! valid for that discriminant is the same as the subset of values of `U` which +//! are valid for that discriminant. As a result, it may be possible to pass a +//! `Ptr` which has uninitialized bytes which are not problematic for `T` but +//! which are problematic for `U`.