Skip to content

Commit 31cfbd7

Browse files
joshlfjoshlf
authored
[ptr] Simplify PtrInner's invariants (#2450)
gherrit-pr-id: I855bc98cf1674d02e3750e2fc55810be79795796
1 parent 7abd7be commit 31cfbd7

File tree

2 files changed

+112
-152
lines changed

2 files changed

+112
-152
lines changed

‎src/pointer/inner.rs‎

Lines changed: 92 additions & 114 deletions
Original file line numberDiff line numberDiff line change
@@ -31,17 +31,32 @@ mod _def {
3131
{
3232
/// # Invariants
3333
///
34-
/// 0. If `ptr`'s referent is not zero sized, then `ptr` is derived from
35-
/// some valid Rust allocation, `A`.
36-
/// 1. If `ptr`'s referent is not zero sized, then `ptr` has valid
37-
/// provenance for `A`.
38-
/// 2. If `ptr`'s referent is not zero sized, then `ptr` addresses a
39-
/// byte range which is entirely contained in `A`.
40-
/// 3. `ptr` addresses a byte range whose length fits in an `isize`.
41-
/// 4. `ptr` addresses a byte range which does not wrap around the
42-
/// address space.
43-
/// 5. If `ptr`'s referent is not zero sized,`A` is guaranteed to live
34+
/// 0. If `ptr`'s referent is not zero sized, then `ptr` has valid
35+
/// provenance for its referent, which is entirely contained in some
36+
/// Rust allocation, `A`.
37+
/// 1. If `ptr`'s referent is not zero sized, `A` is guaranteed to live
4438
/// for at least `'a`.
39+
///
40+
/// # Postconditions
41+
///
42+
/// By virtue of these invariants, code may assume the following, which
43+
/// are logical implications of the invariants:
44+
/// - `ptr`'s referent is not larger than `isize::MAX` bytes \[1\]
45+
/// - `ptr`'s referent does not wrap around the address space \[1\]
46+
///
47+
/// \[1\] Per <https://doc.rust-lang.org/1.85.0/std/ptr/index.html#allocated-object>:
48+
///
49+
/// For any allocated object with `base` address, `size`, and a set of
50+
/// `addresses`, the following are guaranteed:
51+
/// ...
52+
/// - `size <= isize::MAX`
53+
///
54+
/// As a consequence of these guarantees, given any address `a` within
55+
/// the set of addresses of an allocated object:
56+
/// ...
57+
/// - It is guaranteed that, given `o = a - base` (i.e., the offset of
58+
/// `a` within the allocated object), `base + o` will not wrap around
59+
/// the address space (in other words, will not overflow `usize`)
4560
ptr: NonNull<T>,
4661
// SAFETY: `&'a UnsafeCell<T>` is covariant in `'a` and invariant in `T`
4762
// [1]. We use this construction rather than the equivalent `&mut T`,
@@ -67,17 +82,11 @@ mod _def {
6782
///
6883
/// The caller promises that:
6984
///
70-
/// 0. If `ptr`'s referent is not zero sized, then `ptr` is derived from
71-
/// some valid Rust allocation, `A`.
72-
/// 1. If `ptr`'s referent is not zero sized, then `ptr` has valid
73-
/// provenance for `A`.
74-
/// 2. If `ptr`'s referent is not zero sized, then `ptr` addresses a
75-
/// byte range which is entirely contained in `A`.
76-
/// 3. `ptr` addresses a byte range whose length fits in an `isize`.
77-
/// 4. `ptr` addresses a byte range which does not wrap around the
78-
/// address space.
79-
/// 5. If `ptr`'s referent is not zero sized, then `A` is guaranteed to
80-
/// live for at least `'a`.
85+
/// 0. If `ptr`'s referent is not zero sized, then `ptr` has valid
86+
/// provenance for its referent, which is entirely contained in some
87+
/// Rust allocation, `A`.
88+
/// 1. If `ptr`'s referent is not zero sized, `A` is guaranteed to live
89+
/// for at least `'a`.
8190
pub(crate) const unsafe fn new(ptr: NonNull<T>) -> PtrInner<'a, T> {
8291
// SAFETY: The caller has promised to satisfy all safety invariants
8392
// of `PtrInner`.
@@ -102,18 +111,23 @@ impl<'a, T: ?Sized> PtrInner<'a, T> {
102111
let ptr = NonNull::from(ptr);
103112
// SAFETY:
104113
// 0. If `ptr`'s referent is not zero sized, then `ptr`, by invariant on
105-
// `&'a T`, is derived from some valid Rust allocation, `A`.
106-
// 1. If `ptr`'s referent is not zero sized, then `ptr`, by invariant on
107-
// `&'a T`, has valid provenance for `A`.
108-
// 2. If `ptr`'s referent is not zero sized, then `ptr`, by invariant on
109-
// `&'a T`, addresses a byte range which is entirely contained in
110-
// `A`.
111-
// 3. `ptr`, by invariant on `&'a T`, addresses a byte range whose
112-
// length fits in an `isize`.
113-
// 4. `ptr`, by invariant on `&'a T`, addresses a byte range which does
114-
// not wrap around the address space.
115-
// 5. If `ptr`'s referent is not zero sized, then `A`, by invariant on
114+
// `&'a T` [1], has valid provenance for its referent, which is
115+
// entirely contained in some Rust allocation, `A`.
116+
// 1. If `ptr`'s referent is not zero sized, then `A`, by invariant on
116117
// `&'a T`, is guaranteed to live for at least `'a`.
118+
//
119+
// [1] Per https://doc.rust-lang.org/1.85.0/std/primitive.reference.html#safety:
120+
//
121+
// For all types, `T: ?Sized`, and for all `t: &T` or `t: &mut T`,
122+
// when such values cross an API boundary, the following invariants
123+
// must generally be upheld:
124+
// ...
125+
// - if `size_of_val(t) > 0`, then `t` is dereferenceable for
126+
// `size_of_val(t)` many bytes
127+
//
128+
// If `t` points at address `a`, being “dereferenceable” for N bytes
129+
// means that the memory range `[a, a + N)` is all contained within a
130+
// single allocated object.
117131
unsafe { Self::new(ptr) }
118132
}
119133

@@ -123,18 +137,23 @@ impl<'a, T: ?Sized> PtrInner<'a, T> {
123137
let ptr = NonNull::from(ptr);
124138
// SAFETY:
125139
// 0. If `ptr`'s referent is not zero sized, then `ptr`, by invariant on
126-
// `&'a mut T`, is derived from some valid Rust allocation, `A`.
127-
// 1. If `ptr`'s referent is not zero sized, then `ptr`, by invariant on
128-
// `&'a mut T`, has valid provenance for `A`.
129-
// 2. If `ptr`'s referent is not zero sized, then `ptr`, by invariant on
130-
// `&'a mut T`, addresses a byte range which is entirely contained in
131-
// `A`.
132-
// 3. `ptr`, by invariant on `&'a mut T`, addresses a byte range whose
133-
// length fits in an `isize`.
134-
// 4. `ptr`, by invariant on `&'a mut T`, addresses a byte range which
135-
// does not wrap around the address space.
136-
// 5. If `ptr`'s referent is not zero sized, then `A`, by invariant on
140+
// `&'a mut T` [1], has valid provenance for its referent, which is
141+
// entirely contained in some Rust allocation, `A`.
142+
// 1. If `ptr`'s referent is not zero sized, then `A`, by invariant on
137143
// `&'a mut T`, is guaranteed to live for at least `'a`.
144+
//
145+
// [1] Per https://doc.rust-lang.org/1.85.0/std/primitive.reference.html#safety:
146+
//
147+
// For all types, `T: ?Sized`, and for all `t: &T` or `t: &mut T`,
148+
// when such values cross an API boundary, the following invariants
149+
// must generally be upheld:
150+
// ...
151+
// - if `size_of_val(t) > 0`, then `t` is dereferenceable for
152+
// `size_of_val(t)` many bytes
153+
//
154+
// If `t` points at address `a`, being “dereferenceable” for N bytes
155+
// means that the memory range `[a, a + N)` is all contained within a
156+
// single allocated object.
138157
unsafe { Self::new(ptr) }
139158
}
140159
}
@@ -168,34 +187,24 @@ impl<'a, T> PtrInner<'a, [T]> {
168187

169188
let ptr = core::ptr::slice_from_raw_parts_mut(base, len);
170189

171-
// SAFETY: By invariant, `self`'s address is non-null and its range does
172-
// not wrap around the address space. Since, by the preceding lemma,
173-
// `ptr` addresses a range within that addressed by `self`, `ptr` is
174-
// non-null.
190+
// SAFETY: By invariant, `self`'s referent is either a ZST or lives
191+
// entirely in an allocation. `ptr` points inside of or one byte past
192+
// the end of that referent. Thus, in either case, `ptr` is non-null.
175193
let ptr = unsafe { NonNull::new_unchecked(ptr) };
176194

177195
// SAFETY:
178196
//
179197
// Lemma 0: `ptr` addresses a subset of the bytes addressed by `self`,
180198
// and has the same provenance. Proof: The caller guarantees
181-
// that `start <= end <= self.len()`. Thus, `base` is in-bounds of
182-
// `self`, and `base + (end - start)` is also in-bounds of self.
183-
// Finally, `ptr` is constructed using provenance-preserving
184-
// operations.
199+
// that `start <= end <= self.len()`. Thus, `base` is in-bounds
200+
// of `self`, and `base + (end - start)` is also in-bounds of
201+
// self. Finally, `ptr` is constructed using
202+
// provenance-preserving operations.
185203
//
186204
// 0. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is not
187-
// zero sized, then `ptr` is derived from some valid Rust allocation,
188-
// `A`.
205+
// zero sized, then `ptr` has valid provenance for its referent,
206+
// which is entirely contained in some Rust allocation, `A`.
189207
// 1. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is not
190-
// zero sized, then `ptr` has valid provenance for `A`.
191-
// 2. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is not
192-
// zero sized, then `ptr` addresses a byte range which is entirely
193-
// contained in `A`.
194-
// 3. Per Lemma 0 and by invariant on `self`, `ptr` addresses a byte
195-
// range whose length fits in an `isize`.
196-
// 4. Per Lemma 0 and by invariant on `self`, `ptr` addresses a byte
197-
// range which does not wrap around the address space.
198-
// 5. Per Lemma 0 and by invariant on `self`, if `ptr`'s referent is not
199208
// zero sized, then `A` is guaranteed to live for at least `'a`.
200209
unsafe { PtrInner::new(ptr) }
201210
}
@@ -267,30 +276,23 @@ impl<'a, T> PtrInner<'a, [T]> {
267276
// provenance, cite those docs.
268277
let elem = unsafe { base.add(i) };
269278

270-
// SAFETY:
271-
// - `elem` must not be null. `base` is constructed from a
272-
// `NonNull` pointer, and the addition that produces `elem` must
273-
// not overflow or wrap around, so `elem >= base > 0`.
279+
// SAFETY: `elem` must not be null. `base` is constructed from a
280+
// `NonNull` pointer, and the addition that produces `elem` must not
281+
// overflow or wrap around, so `elem >= base > 0`.
274282
//
275283
// TODO(#429): Once `NonNull::new_unchecked` documents that it
276284
// preserves provenance, cite those docs.
277285
let elem = unsafe { NonNull::new_unchecked(elem) };
278286

279287
// SAFETY: The safety invariants of `Ptr::new` (see definition) are
280288
// satisfied:
281-
// 0. If `elem`'s referent is not zero sized, then `elem` is derived
282-
// from a valid Rust allocation, because `self` is derived from a
283-
// valid Rust allocation, by invariant on `Ptr`.
284-
// 1. If `elem`'s referent is not zero sized, then `elem` has valid
285-
// provenance for `self`, because it derived from `self` using a
286-
// series of provenance-preserving operations.
287-
// 2. If `elem`'s referent is not zero sized, then `elem` is
288-
// entirely contained in the allocation of `self` (see above).
289-
// 3. `elem` addresses a byte range whose length fits in an `isize`
290-
// (see above).
291-
// 4. `elem` addresses a byte range which does not wrap around the
292-
// address space (see above).
293-
// 5. If `elem`'s referent is not zero sized, then the allocation of
289+
// 0. If `elem`'s referent is not zero sized, then `elem` has valid
290+
// provenance for its referent, because it derived from `self`
291+
// using a series of provenance-preserving operations, and
292+
// because `self` has valid provenance for its referent. By the
293+
// same argument, `elem`'s referent is entirely contained within
294+
// the same allocated object as `self`'s referent.
295+
// 1. If `elem`'s referent is not zero sized, then the allocation of
294296
// `elem` is guaranteed to live for at least `'a`, because `elem`
295297
// is entirely contained in `self`, which lives for at least `'a`
296298
// by invariant on `Ptr`.
@@ -346,25 +348,11 @@ impl<'a, T, const N: usize> PtrInner<'a, [T; N]> {
346348
// same allocation as `self`, if any.
347349
//
348350
// 0. By the above lemma, if `slice`'s referent is not zero sized, then
349-
// `slice` is derived from the same allocation as `self`, which, by
350-
// invariant on `Ptr`, is valid.
351+
// `slice` has the same referent as `self`. By invariant on `self`,
352+
// this referent is entirely contained within some allocation, `A`.
353+
// Because `slice` was constructed using provenance-preserving
354+
// operations, it has provenance for its entire referent.
351355
// 1. By the above lemma, if `slice`'s referent is not zero sized, then
352-
// , `slice` has valid provenance for `A`, since it is derived from
353-
// the pointer `self`, which, by invariant on `Ptr`, has valid
354-
// provenance for `A`.
355-
// 2. By the above lemma, if `slice`'s referent is not zero sized, then
356-
// `slice` addresses a byte range which is entirely contained in `A`,
357-
// because it references exactly the same byte range as `self`,
358-
// which, by invariant on `Ptr`, is entirely contained in `A`.
359-
// 3. By the above lemma, `slice` addresses a byte range whose length
360-
// fits in an `isize`, since it addresses exactly the same byte range
361-
// as `self`, which, by invariant on `Ptr`, has a length that fits in
362-
// an `isize`.
363-
// 4. By the above lemma, `slice` addresses a byte range which does not
364-
// wrap around the address space, since it addresses exactly the same
365-
// byte range as `self`, which, by invariant on `Ptr`, does not wrap
366-
// around the address space.
367-
// 5. By the above lemma, if `slice`'s referent is not zero sized, then
368356
// `A` is guaranteed to live for at least `'a`, because it is derived
369357
// from the same allocation as `self`, which, by invariant on `Ptr`,
370358
// lives for at least `'a`.
@@ -464,26 +452,16 @@ impl<'a> PtrInner<'a, [u8]> {
464452

465453
// SAFETY:
466454
// 0. By invariant, if `target`'s referent is not zero sized, then
467-
// `target` is derived from some valid Rust allocation, `A`. By
468-
// contract on `cast`, `ptr` is derived from `self`, and thus from
469-
// the same valid Rust allocation, `A`.
470-
// 1. By invariant, if `target`'s referent is not zero sized, then
471455
// `target` has provenance valid for some Rust allocation, `A`.
472456
// Because `ptr` is derived from `target` via provenance-preserving
473-
// operations, `ptr` will also have provenance valid for `A`.
474-
// - `validate_cast_and_convert_metadata` promises that the object
457+
// operations, `ptr` will also have provenance valid for its entire
458+
// referent.
459+
// 1. `validate_cast_and_convert_metadata` promises that the object
475460
// described by `elems` and `split_at` lives at a byte range which is
476-
// a subset of the input byte range. Thus:
477-
// 2. Since, by invariant, if `target`'s referent is not zero sized,
478-
// then `target` addresses a byte range which is entirely
479-
// contained in `A`, so does `ptr`.
480-
// 3. Since, by invariant, `target` addresses a byte range whose
481-
// length fits in an `isize`, so does `ptr`.
482-
// 4. Since, by invariant, `target` addresses a byte range which does
483-
// not wrap around the address space, so does `ptr`.
484-
// 5. Since, by invariant, if `target`'s referent is not zero sized,
485-
// then `target` refers to an allocation which is guaranteed to
486-
// live for at least `'a`, so does `ptr`.
461+
// a subset of the input byte range. Thus, by invariant, if
462+
// `target`'s referent is not zero sized, then `target` refers to an
463+
// allocation which is guaranteed to live for at least `'a`, and thus
464+
// so does `ptr`.
487465
Ok((unsafe { PtrInner::new(ptr) }, remainder))
488466
}
489467
}

0 commit comments

Comments
 (0)