Skip to content

Redesign Ptr invariants to enforce both upper and lower bounds #1866

Open
@joshlf

Description

Currently, the invariants enforced by Ptr are used strictly as lower bounds. We require code to prove soundness in order to increase the strictness of an invariant, for example to go from any alignment to Aligned:

zerocopy/src/pointer/ptr.rs

Lines 779 to 781 in 1b037c8

pub(crate) unsafe fn assume_alignment<A: Alignment>(
self,
) -> Ptr<'a, T, (I::Aliasing, A, I::Validity)> {

...but we permit the opposite direction without restriction:

pub fn forget_aligned(self) -> Ptr<'a, T, (I::Aliasing, Any, I::Validity)> {

While it's not clear that our API currently permits any unsoundness, this general philosophy that some APIs are okay which are probably actually unsound.

Consider, for example, adding two seemingly innocuous methods to Ptr:

  • forget_valid modifies the validity invariant on an existing Ptr to be Any
  • as_maybe_uninit turns a Ptr<T> into a Ptr<MaybeUninit<T>, (..., ..., Valid)> (since MaybeUninit has no validity requirements)

Taken together, these can be used to produce UB:

zerocopy/src/pointer/ptr.rs

Lines 946 to 974 in a3d4387

use core::mem::MaybeUninit;
impl<'a, T, I: Invariants> Ptr<'a, T, I> {
/// Forgets that `self`'s referent is a bit-valid `T`.
fn forget_valid(self) -> Ptr<'a, T, (I::Aliasing, I::Alignment, Any)> {
// SAFETY: `Any` is less restrictive than any validity invariant.
unsafe { self.assume_invariants() }
}
fn as_maybe_uninit(self) -> Ptr<'a, MaybeUninit<T>, (I::Aliasing, I::Alignment, Valid)> {
// SAFETY: `MaybeUninit<T>` has the same size and `UnsafeCell`s as
// `T`. This is a provenance-preserving cast.
let ptr = unsafe { self.cast_unsized(|ptr| ptr.cast::<MaybeUninit<T>>()) };
// SAFETY: `MaybeUninit<T>` has the same alignment as `T`.
let ptr = unsafe { ptr.assume_alignment::<I::Alignment>() };
// SAFETY: `MaybeUninit<T>` has no validity requirements.
unsafe { ptr.assume_valid() }
}
}
let mut b = true;
let ptr = Ptr::from_mut(&mut b);
let ptr = ptr.forget_valid();
let ptr = ptr.as_maybe_uninit();
let mu = ptr.as_mut();
*mu = crate::transmute!(2u8);
assert_eq!(b, true);

Indeed, Miri detects this UB:

test pointer::ptr::test_forget_valid ... error: Undefined Behavior: constructing invalid value: encountered 0x02, but expected a boolean
   --> src/pointer/ptr.rs:974:5
    |
974 |     assert_eq!(b, true);
    |     ^^^^^^^^^^^^^^^^^^^ constructing invalid value: encountered 0x02, but expected a boolean
    |
    = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
    = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
    = note: BACKTRACE on thread `pointer::ptr::test_forget_valid`:
    = note: inside `pointer::ptr::test_forget_valid` at ~/.rustup/toolchains/nightly-2024-10-09-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/macros/mod.rs:46:22: 46:31
note: inside closure
   --> src/pointer/ptr.rs:945:23
    |
944 | #[test]
    | ------- in this procedural macro expansion
945 | fn test_forget_valid() {
    |                       ^
    = note: this error originates in the macro `assert_eq` which comes from the expansion of the attribute macro `test` (in Nightly builds, run with -Z macro-backtrace for more info)

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to 1 previous error; 1 warning emitted

error: test failed, to rerun pass `--lib`

This implies that we need to fundamentally rethink what invariants mean in Ptr. In particular:

  • We need to think of invariants as providing both lower and upper bounds on behavior
  • We need to think of producing a lower invariant as potentially being problematic if it permits subsequent code to do things using that lower invariant that might violate invariants assumed by predecessors of the current Ptr (as as_maybe_uninit does in this example)

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions