Redesign Ptr
invariants to enforce both upper and lower bounds #1866
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
:
Lines 779 to 781 in 1b037c8
...but we permit the opposite direction without restriction:
Line 936 in 1b037c8
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 existingPtr
to beAny
as_maybe_uninit
turns aPtr<T>
into aPtr<MaybeUninit<T>, (..., ..., Valid)>
(sinceMaybeUninit
has no validity requirements)
Taken together, these can be used to produce UB:
Lines 946 to 974 in a3d4387
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
(asas_maybe_uninit
does in this example)