Skip to content

Commit

Permalink
Write some safety proofs (#1615)
Browse files Browse the repository at this point in the history 
Adds some informal proofs as accepted risks per #1358

Makes progress on #896
  • Loading branch information
@joshlf
joshlf committed Sep 7, 2024
1 parent d66705a commit 02dc876
Show file tree
Hide file tree
Showing 3 changed files with 81 additions and 25 deletions.
24 changes: 13 additions & 11 deletions src/impls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<u8>| NonZeroU8::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroI8: TryFromBytes; |n: MaybeAligned<i8>| NonZeroI8::new(n.read_unaligned()).is_some());
unsafe_impl!(NonZeroU16: TryFromBytes; |n: MaybeAligned<u16>| NonZeroU16::new(n.read_unaligned()).is_some());
Expand Down Expand Up @@ -360,12 +360,10 @@ safety_comment! {
safety_comment! {
/// SAFETY:
/// While it's not fully documented, the consensus is that `Box<T>` 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")))]
Expand Down Expand Up @@ -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!(...));
}
Expand Down Expand Up @@ -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:
///
Expand Down Expand Up @@ -830,8 +832,8 @@ safety_comment! {

safety_comment! {
/// SAFETY:
///
/// TODO(#896): Write this safety proof before the next stable release.
/// `NonNull<T>` 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<T>);
}

Expand Down
31 changes: 30 additions & 1 deletion src/pointer/ptr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) }
}

Expand Down
51 changes: 38 additions & 13 deletions src/util.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,10 @@ impl<I: invariant::Validity> ValidityVariance<I> for Invariant {
// - Per [1], `MaybeUninit<T>` 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<T>` is guaranteed to have the same size, alignment, and ABI as
// `T`
unsafe impl<T, I: Invariants> TransparentWrapper<I> for MaybeUninit<T> {
type Inner = T;

Expand Down Expand Up @@ -145,14 +148,22 @@ unsafe impl<T, I: Invariants> TransparentWrapper<I> for MaybeUninit<T> {
// - Per [1], `ManuallyDrop<T>` 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<T>` is guaranteed to have the same layout and bit validity as
// `T`
unsafe impl<T: ?Sized, I: Invariants> TransparentWrapper<I> for ManuallyDrop<T> {
type Inner = T;

// SAFETY: Per [1], `ManuallyDrop<T>` 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<T>` 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<T>` has the same layout as `T`, and thus
// has the same alignment as `T`.
Expand Down Expand Up @@ -190,14 +201,22 @@ unsafe impl<T: ?Sized, I: Invariants> TransparentWrapper<I> for ManuallyDrop<T>
// - Per [1], `Wrapping<T>` 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<T>` is guaranteed to have the same layout and ABI as `T`.
unsafe impl<T, I: Invariants> TransparentWrapper<I> for Wrapping<T> {
type Inner = T;

// SAFETY: Per [1], `Wrapping<T>` has `UnsafeCell`s covering the same byte
// ranges as `Inner = T`.
// SAFETY: Per [1], `Wrapping<T>` 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<T>` contains a `T` (as
// opposed to just having the same size and alignment as `T`) with no pre-
// or post-padding. Thus, `Wrapping<T>` 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<T>` is guaranteed to have the same layout and ABI as `T`.
type UnsafeCellVariance = Covariant;
// SAFETY: Per [1], `Wrapping<T>` has the same layout as `T`, and thus has
// the same alignment as `T`.
Expand Down Expand Up @@ -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<I> for $atomic {
unsafe_impl_transparent_wrapper_for_atomic!(@inner $atomic [$native]);
Expand Down Expand Up @@ -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
Expand All @@ -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> {
Expand Down

0 comments on commit 02dc876

Please sign in to comment.