Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
joshlf opened this issue Oct 10, 2024 · 0 comments
Open

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

joshlf opened this issue Oct 10, 2024 · 0 comments

Comments

@joshlf
Copy link
Member

joshlf commented Oct 10, 2024

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)
joshlf added a commit that referenced this issue Oct 12, 2024
Previously, we supported the `AtLeast` bound, which was used to describe
a subset relationship in which `I: AtLeast<J>` implied that `I` as at
least as restrictive as `J`. However, as described in #1866, this
incorrectly models invariants as monotonic. In reality, invariants both
provide guarantees but also *require* guarantees.

This commit takes a step in the direction of resolving #1866 by removing
`AtLeast`. Uses of `AtLeast<Shared>` are replaced by a new `Reference`
trait, which is implemented for `Shared` and `Exclusive`. This serves
two purposes: First, it makes it explicit what this bound means.
Previously, `AtLeast<Shared>` had an ambiguous meaning, while
`Reference` means precisely that an invariant is either `Shared` or
`Exclusive` and nothing else. Second, it paves the way for #1183, in
which we may add new aliasing invariants which convey ownership. In that
case, it will be important for existing methods to add `Reference`
bounds when those methods would not be sound in the face of ownership
semantics.

We also inline the items in the `invariant` module, which were
previously generated by macro. The addition of the `Reference` trait did
not play nicely with that macro, and we will likely need to go further
from the macro in order to fix #1839 – this fix will likely require
making aliasing invariants meaningfully different than other invariants,
for example by adding an associated type.

Makes progress on #1866
joshlf added a commit that referenced this issue Oct 12, 2024
Previously, we supported the `AtLeast` bound, which was used to describe
a subset relationship in which `I: AtLeast<J>` implied that `I` as at
least as restrictive as `J`. However, as described in #1866, this
incorrectly models invariants as monotonic. In reality, invariants both
provide guarantees but also *require* guarantees.

This commit takes a step in the direction of resolving #1866 by removing
`AtLeast`. Uses of `AtLeast<Shared>` are replaced by a new `Reference`
trait, which is implemented for `Shared` and `Exclusive`. This serves
two purposes: First, it makes it explicit what this bound means.
Previously, `AtLeast<Shared>` had an ambiguous meaning, while
`Reference` means precisely that an invariant is either `Shared` or
`Exclusive` and nothing else. Second, it paves the way for #1183, in
which we may add new aliasing invariants which convey ownership. In that
case, it will be important for existing methods to add `Reference`
bounds when those methods would not be sound in the face of ownership
semantics.

We also inline the items in the `invariant` module, which were
previously generated by macro. The addition of the `Reference` trait did
not play nicely with that macro, and we will likely need to go further
from the macro in order to fix #1839 – this fix will likely require
making aliasing invariants meaningfully different than other invariants,
for example by adding an associated type.

Makes progress on #1866
joshlf added a commit that referenced this issue Oct 12, 2024
Previously, we supported the `AtLeast` bound, which was used to describe
a subset relationship in which `I: AtLeast<J>` implied that `I` as at
least as restrictive as `J`. However, as described in #1866, this
incorrectly models invariants as monotonic. In reality, invariants both
provide guarantees but also *require* guarantees.

This commit takes a step in the direction of resolving #1866 by removing
`AtLeast`. Uses of `AtLeast<Shared>` are replaced by a new `Reference`
trait, which is implemented for `Shared` and `Exclusive`. This serves
two purposes: First, it makes it explicit what this bound means.
Previously, `AtLeast<Shared>` had an ambiguous meaning, while
`Reference` means precisely that an invariant is either `Shared` or
`Exclusive` and nothing else. Second, it paves the way for #1183, in
which we may add new aliasing invariants which convey ownership. In that
case, it will be important for existing methods to add `Reference`
bounds when those methods would not be sound in the face of ownership
semantics.

We also inline the items in the `invariant` module, which were
previously generated by macro. The addition of the `Reference` trait did
not play nicely with that macro, and we will likely need to go further
from the macro in order to fix #1839 – this fix will likely require
making aliasing invariants meaningfully different than other invariants,
for example by adding an associated type.

Makes progress on #1866
joshlf added a commit that referenced this issue Oct 14, 2024
Previously, we supported the `AtLeast` bound, which was used to describe
a subset relationship in which `I: AtLeast<J>` implied that `I` as at
least as restrictive as `J`. However, as described in #1866, this
incorrectly models invariants as monotonic. In reality, invariants both
provide guarantees but also *require* guarantees.

This commit takes a step in the direction of resolving #1866 by removing
`AtLeast`. Uses of `AtLeast<Shared>` are replaced by a new `Reference`
trait, which is implemented for `Shared` and `Exclusive`. This serves
two purposes: First, it makes it explicit what this bound means.
Previously, `AtLeast<Shared>` had an ambiguous meaning, while
`Reference` means precisely that an invariant is either `Shared` or
`Exclusive` and nothing else. Second, it paves the way for #1183, in
which we may add new aliasing invariants which convey ownership. In that
case, it will be important for existing methods to add `Reference`
bounds when those methods would not be sound in the face of ownership
semantics.

We also inline the items in the `invariant` module, which were
previously generated by macro. The addition of the `Reference` trait did
not play nicely with that macro, and we will likely need to go further
from the macro in order to fix #1839 – this fix will likely require
making aliasing invariants meaningfully different than other invariants,
for example by adding an associated type.

Makes progress on #1866
github-merge-queue bot pushed a commit that referenced this issue Oct 14, 2024
Previously, we supported the `AtLeast` bound, which was used to describe
a subset relationship in which `I: AtLeast<J>` implied that `I` as at
least as restrictive as `J`. However, as described in #1866, this
incorrectly models invariants as monotonic. In reality, invariants both
provide guarantees but also *require* guarantees.

This commit takes a step in the direction of resolving #1866 by removing
`AtLeast`. Uses of `AtLeast<Shared>` are replaced by a new `Reference`
trait, which is implemented for `Shared` and `Exclusive`. This serves
two purposes: First, it makes it explicit what this bound means.
Previously, `AtLeast<Shared>` had an ambiguous meaning, while
`Reference` means precisely that an invariant is either `Shared` or
`Exclusive` and nothing else. Second, it paves the way for #1183, in
which we may add new aliasing invariants which convey ownership. In that
case, it will be important for existing methods to add `Reference`
bounds when those methods would not be sound in the face of ownership
semantics.

We also inline the items in the `invariant` module, which were
previously generated by macro. The addition of the `Reference` trait did
not play nicely with that macro, and we will likely need to go further
from the macro in order to fix #1839 – this fix will likely require
making aliasing invariants meaningfully different than other invariants,
for example by adding an associated type.

Makes progress on #1866
joshlf added a commit that referenced this issue Oct 14, 2024
Previously, we supported the `AtLeast` bound, which was used to describe
a subset relationship in which `I: AtLeast<J>` implied that `I` as at
least as restrictive as `J`. However, as described in #1866, this
incorrectly models invariants as monotonic. In reality, invariants both
provide guarantees but also *require* guarantees.

This commit takes a step in the direction of resolving #1866 by removing
`AtLeast`. Uses of `AtLeast<Shared>` are replaced by a new `Reference`
trait, which is implemented for `Shared` and `Exclusive`. This serves
two purposes: First, it makes it explicit what this bound means.
Previously, `AtLeast<Shared>` had an ambiguous meaning, while
`Reference` means precisely that an invariant is either `Shared` or
`Exclusive` and nothing else. Second, it paves the way for #1183, in
which we may add new aliasing invariants which convey ownership. In that
case, it will be important for existing methods to add `Reference`
bounds when those methods would not be sound in the face of ownership
semantics.

We also inline the items in the `invariant` module, which were
previously generated by macro. The addition of the `Reference` trait did
not play nicely with that macro, and we will likely need to go further
from the macro in order to fix #1839 – this fix will likely require
making aliasing invariants meaningfully different than other invariants,
for example by adding an associated type.

Makes progress on #1866
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant