From 02dc876d9d7939be682c2397949b21fa367ec8f2 Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Sat, 7 Sep 2024 14:43:05 -0700 Subject: [PATCH] Write some safety proofs (#1615) Adds some informal proofs as accepted risks per #1358 Makes progress on #896 --- src/impls.rs | 24 ++++++++++++---------- src/pointer/ptr.rs | 31 +++++++++++++++++++++++++++- src/util.rs | 51 ++++++++++++++++++++++++++++++++++------------ 3 files changed, 81 insertions(+), 25 deletions(-) diff --git a/src/impls.rs b/src/impls.rs index 5e5349503d..3f05994594 100644 --- a/src/impls.rs +++ b/src/impls.rs @@ -307,8 +307,8 @@ safety_comment! { /// `NonZeroU16` is guaranteed to have the same layout and bit validity as /// `u16` with the exception that `0` is not a valid instance. /// - /// [2] TODO(#896): Write a safety proof for this before the next stable - /// release. + /// [2] `NonZeroXxx` self-evidently does not contain `UnsafeCell`s. This is + /// not a proof, but we are accepting this as a known risk per #1358. unsafe_impl!(NonZeroU8: TryFromBytes; |n: MaybeAligned| NonZeroU8::new(n.read_unaligned()).is_some()); unsafe_impl!(NonZeroI8: TryFromBytes; |n: MaybeAligned| NonZeroI8::new(n.read_unaligned()).is_some()); unsafe_impl!(NonZeroU16: TryFromBytes; |n: MaybeAligned| NonZeroU16::new(n.read_unaligned()).is_some()); @@ -360,12 +360,10 @@ safety_comment! { safety_comment! { /// SAFETY: /// While it's not fully documented, the consensus is that `Box` does not - /// contain any `UnsafeCell`s for `T: Sized` [1]. + /// contain any `UnsafeCell`s for `T: Sized` [1]. This is not a complete + /// proof, but we are accepting this as a known risk per #1358. /// /// [1] https://github.com/rust-lang/unsafe-code-guidelines/issues/492 - /// - /// TODO(#896): Write a more complete safety proof before the next stable - /// release. #[cfg(feature = "alloc")] unsafe_impl!( #[cfg_attr(doc_cfg, doc(cfg(feature = "alloc")))] @@ -435,7 +433,9 @@ safety_comment! { safety_comment! { /// SAFETY: - /// TODO(#896): Write this safety proof before the next stable release. + /// `fn()` and `extern "C" fn()` self-evidently do not contain + /// `UnsafeCell`s. This is not a proof, but we are accepting this as a known + /// risk per #1358. unsafe_impl_for_power_set!(A, B, C, D, E, F, G, H, I, J, K, L -> M => Immutable for opt_fn!(...)); unsafe_impl_for_power_set!(A, B, C, D, E, F, G, H, I, J, K, L -> M => Immutable for opt_extern_c_fn!(...)); } @@ -488,8 +488,10 @@ mod atomics { /// cannot be greater than its size [3], the only possible value for /// the alignment is 1. Thus, it is sound to implement `Unaligned`. /// - /// [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943): - /// Cite docs once they've landed. + /// [1] Per (for example) https://doc.rust-lang.org/1.81.0/std/sync/atomic/struct.AtomicU8.html: + /// + /// This type has the same size, alignment, and bit validity as + /// the underlying integer type /// /// [2] Per https://doc.rust-lang.org/reference/type-layout.html#size-and-alignment: /// @@ -830,8 +832,8 @@ safety_comment! { safety_comment! { /// SAFETY: - /// - /// TODO(#896): Write this safety proof before the next stable release. + /// `NonNull` self-evidently does not contain `UnsafeCell`s. This is not + /// a proof, but we are accepting this as a known risk per #1358. unsafe_impl!(T: ?Sized => Immutable for NonNull); } diff --git a/src/pointer/ptr.rs b/src/pointer/ptr.rs index de70aa7832..5c12ad7224 100644 --- a/src/pointer/ptr.rs +++ b/src/pointer/ptr.rs @@ -1411,7 +1411,36 @@ mod _project { // `ptr` is non-null. let ptr = unsafe { NonNull::new_unchecked(ptr) }; - // SAFETY: TODO(#896) + // SAFETY: + // + // Lemma 0: `ptr` addresses a subset of the bytes addressed by + // `self`, and has the same provenance. + // Proof: The caller guarantees that `start <= end <= self.len()`. + // Thus, `base` is in-bounds of `self`, and `base + (end - + // start)` is also in-bounds of self. Finally, `ptr` is + // constructed using provenance-preserving operations. + // + // 0. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is + // not zero sized, then `ptr` is derived from some valid Rust + // allocation, `A`. + // 1. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is + // not zero sized, then `ptr` has valid provenance for `A`. + // 2. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is + // not zero sized, then `ptr` addresses a byte range which is + // entirely contained in `A`. + // 3. Per Lemma 0 and by invariant on `self`, `ptr` addresses a byte + // range whose length fits in an `isize`. + // 4. Per Lemma 0 and by invariant on `self`, `ptr` addresses a byte + // range which does not wrap around the address space. + // 5. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is + // not zero sized, then `A` is guaranteed to live for at least + // `'a`. + // 6. Per Lemma 0 and by invariant on `self`, `ptr` conforms to the + // aliasing invariant of [`I::Aliasing`](invariant::Aliasing). + // 7. Per Lemma 0 and by invariant on `self`, `ptr` conforms to the + // alignment invariant of [`I::Alignment`](invariant::Alignment). + // 8. Per Lemma 0 and by invariant on `self`, `ptr` conforms to the + // validity invariant of [`I::Validity`](invariant::Validity). unsafe { Ptr::new(ptr) } } diff --git a/src/util.rs b/src/util.rs index e2b4fbe436..1557f4e5df 100644 --- a/src/util.rs +++ b/src/util.rs @@ -103,7 +103,10 @@ impl ValidityVariance for Invariant { // - Per [1], `MaybeUninit` has the same size as `T`. // - See inline comments for other safety justifications. // -// [1] TODO(#896): Write a safety proof before the next stable release. +// [1] Per https://doc.rust-lang.org/1.81.0/std/mem/union.MaybeUninit.html#layout-1: +// +// `MaybeUninit` is guaranteed to have the same size, alignment, and ABI as +// `T` unsafe impl TransparentWrapper for MaybeUninit { type Inner = T; @@ -145,14 +148,22 @@ unsafe impl TransparentWrapper for MaybeUninit { // - Per [1], `ManuallyDrop` has the same size as `T`. // - See inline comments for other safety justifications. // -// [1] TODO(#896): Write a safety proof before the next stable release. +// [1] Per https://doc.rust-lang.org/1.81.0/std/mem/struct.ManuallyDrop.html: +// +// `ManuallyDrop` is guaranteed to have the same layout and bit validity as +// `T` unsafe impl TransparentWrapper for ManuallyDrop { type Inner = T; // SAFETY: Per [1], `ManuallyDrop` has `UnsafeCell`s covering the same // byte ranges as `Inner = T`. // - // [1] TODO(#896): Write a safety proof before the next stable release. + // [1] Per https://doc.rust-lang.org/1.81.0/std/mem/struct.ManuallyDrop.html: + // + // `ManuallyDrop` is guaranteed to have the same layout and bit + // validity as `T`, and is subject to the same layout optimizations as + // `T`. As a consequence, it has no effect on the assumptions that the + // compiler makes about its contents. type UnsafeCellVariance = Covariant; // SAFETY: Per [1], `ManuallyDrop` has the same layout as `T`, and thus // has the same alignment as `T`. @@ -190,14 +201,22 @@ unsafe impl TransparentWrapper for ManuallyDrop // - Per [1], `Wrapping` has the same size as `T`. // - See inline comments for other safety justifications. // -// [1] TODO(#896): Write a safety proof before the next stable release. +// [1] Per https://doc.rust-lang.org/1.81.0/std/num/struct.Wrapping.html#layout-1: +// +// `Wrapping` is guaranteed to have the same layout and ABI as `T`. unsafe impl TransparentWrapper for Wrapping { type Inner = T; - // SAFETY: Per [1], `Wrapping` has `UnsafeCell`s covering the same byte - // ranges as `Inner = T`. + // SAFETY: Per [1], `Wrapping` has the same layout as `T`. Since its + // single field (of type `T`) is public, it would be a breaking change to + // add or remove fields. Thus, we know that `Wrapping` contains a `T` (as + // opposed to just having the same size and alignment as `T`) with no pre- + // or post-padding. Thus, `Wrapping` must have `UnsafeCell`s covering the + // same byte ranges as `Inner = T`. // - // [1] TODO(#896): Write a safety proof before the next stable release. + // [1] Per https://doc.rust-lang.org/1.81.0/std/num/struct.Wrapping.html#layout-1: + // + // `Wrapping` is guaranteed to have the same layout and ABI as `T`. type UnsafeCellVariance = Covariant; // SAFETY: Per [1], `Wrapping` has the same layout as `T`, and thus has // the same alignment as `T`. @@ -354,8 +373,10 @@ macro_rules! unsafe_impl_transparent_wrapper_for_atomic { // native counterpart, respectively. Per [1], `$atomic` and `$native` // have the same size. // - // [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943): - // Cite docs once they've landed. + // [1] Per (for example) https://doc.rust-lang.org/1.81.0/std/sync/atomic/struct.AtomicU64.html: + // + // This type has the same size and bit validity as the underlying + // integer type $(#[$attr])* unsafe impl<$tyvar, I: crate::invariant::Invariants> crate::util::TransparentWrapper for $atomic { unsafe_impl_transparent_wrapper_for_atomic!(@inner $atomic [$native]); @@ -385,8 +406,10 @@ macro_rules! unsafe_impl_transparent_wrapper_for_atomic { // set `type Inner = UnsafeCell<$native>`. Thus, `Self` and // `Self::Inner` have `UnsafeCell`s covering the same byte ranges. // - // [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943): - // Cite docs once they've landed. + // [1] Per (for example) https://doc.rust-lang.org/1.81.0/std/sync/atomic/struct.AtomicU64.html: + // + // This type has the same size and bit validity as the underlying + // integer type type UnsafeCellVariance = crate::util::Covariant; // SAFETY: No safety justification is required for an invariant @@ -398,8 +421,10 @@ macro_rules! unsafe_impl_transparent_wrapper_for_atomic { // `$native` are an atomic type and its native counterpart, // respectively. // - // [1] TODO(#896), TODO(https://github.com/rust-lang/rust/pull/121943): - // Cite docs once they've landed. + // [1] Per (for example) https://doc.rust-lang.org/1.81.0/std/sync/atomic/struct.AtomicU64.html: + // + // This type has the same size and bit validity as the underlying + // integer type type ValidityVariance = crate::util::Covariant; fn cast_into_inner(ptr: *mut $atomic) -> *mut UnsafeCell<$native> {