diff --git a/src/next_array.rs b/src/next_array.rs index e9747e52c..59dec6b0e 100644 --- a/src/next_array.rs +++ b/src/next_array.rs @@ -17,7 +17,7 @@ struct ArrayBuilder { impl ArrayBuilder { /// Initializes a new, empty `ArrayBuilder`. pub fn new() -> Self { - // SAFETY: the validity invariant trivially hold for a zero-length array. + // SAFETY: The safety invariant of `arr` trivially holds for `len = 0`. Self { arr: [(); N].map(|_| MaybeUninit::uninit()), len: 0, @@ -28,26 +28,48 @@ impl ArrayBuilder { /// /// # Panics /// - /// This panics if `self.len() >= N`. + /// This panics if `self.len >= N` or if `self.len == usize::MAX`. pub fn push(&mut self, value: T) { - // SAFETY: we maintain the invariant here that arr[..len] is valid. - // Indexing with self.len also ensures self.len < N, and thus <= N after - // the increment. + // PANICS: This will panic if `self.len >= N`. + // SAFETY: The safety invariant of `self.arr` applies to elements at + // indices `0..self.len` — not to the element at `self.len`. Writing to + // the element at index `self.len` therefore does not violate the safety + // invariant of `self.arr`. Even if this line panics, we have not + // created any intermediate invalid state. self.arr[self.len] = MaybeUninit::new(value); - self.len += 1; + // PANICS: This will panic if `self.len == usize::MAX`. + // SAFETY: By invariant on `self.arr`, all elements at indicies + // `0..self.len` are valid. Due to the above write, the element at + // `self.len` is now also valid. Consequently, all elements at indicies + // `0..(self.len + 1)` are valid, and `self.len` can be safely + // incremented without violating `self.arr`'s invariant. It is fine if + // this increment panics, as we have not created any intermediate + // invalid state. + self.len = match self.len.checked_add(1) { + Some(sum) => sum, + None => panic!("`self.len == usize::MAX`; cannot increment `len`"), + }; } - /// Consumes the elements in the `ArrayBuilder` and returns them as an array `[T; N]`. + /// Consumes the elements in the `ArrayBuilder` and returns them as an array + /// `[T; N]`. /// /// If `self.len() < N`, this returns `None`. pub fn take(&mut self) -> Option<[T; N]> { if self.len == N { - // Take the array, resetting our length back to zero. + // SAFETY: Decreasing the value of `self.len` cannot violate the + // safety invariant on `self.arr`. self.len = 0; + + // SAFETY: Since `self.len` is 0, `self.arr` may safely contain + // uninitialized elements. let arr = mem::replace(&mut self.arr, [(); N].map(|_| MaybeUninit::uninit())); - // SAFETY: we had len == N, so all elements in arr are valid. - Some(unsafe { arr.map(|v| v.assume_init()) }) + Some(arr.map(|v| { + // SAFETY: We know that all elements of `arr` are valid because + // we checked that `len == N`. + unsafe { v.assume_init() } + })) } else { None } @@ -56,14 +78,54 @@ impl ArrayBuilder { impl Drop for ArrayBuilder { fn drop(&mut self) { + // Select the valid elements of `self.arr`. + // + // LEMMA 1: The elements of `valid` reference the valid elements of + // `self.arr`. + // + // PROOF: `slice::split_at_mut(mid)` produces a pair of slices, the + // first of which contains the elements at the indices `0..mid`. By + // invariant on `self.arr`, the elements of `self.arr` at indicies + // `0..self.len` are valid. Assuming that `slice::split_at_mut` is + // correctly implemented, the slice `valid` will only reference the + // valid elements of `self.arr`. + let (valid, _) = self.arr.split_at_mut(self.len); + + // Cast `valid` from `&[MaybeUninit]` to `&[T]` + // + // `align_to_mut` guarantees that the length of the casted slice will be + // as long as possible within the constraints of the source and + // destination element types' alignments and size. Since + // `MaybeUninit` and `T` have identical sizes [1], all elements will + // be casted and the prefix and suffix components of the return value + // will be empty. + // + // SAFETY: It is sound to cast a `MaybeUninit` that contains a valid + // `T` to a `T`. A `MaybeUninit` is guaranteed to have the same same + // size, alignment, and ABI as `T` [1], and by LEMMA 1, `valid` consists + // only of `MaybeUninit` in the initialized state. + // + // [1]: https://doc.rust-lang.org/std/mem/union.MaybeUninit.html#layout-1 + let (_, valid, _): (_, &mut [T], _) = unsafe { valid.align_to_mut::() }; + + // Run the destructors of `valid`'s elements. + // + // SAFETY: + // - `valid`, a `&mut [T]`, is valid for both reads and writes by + // invariant on `&mut [T]` + // - `valid`, a `&mut [T]`, is properly aligned, by invariant on `&mut + // [T]` + // - `valid`, a `&mut [T]`, is non-null, by invariant on `&mut [T]` + // - `valid` is valid for dropping, because it is data owned by the + // `ArrayBuilder` and we place no additional drop-related invariants + // on it + // - `valid`, a &mut [T], is the only way to access the parts of `valid` + // because it is an exclusive reference, and it is consumed by + // `drop_in_place`. + // - The referent of `valid`, which may not be `Copy` is not re-used + // after the invocation of `ptr::drop_in_place`. unsafe { - // SAFETY: arr[..len] is valid, so must be dropped. First we create - // a pointer to this valid slice, then drop that slice in-place. - // The cast from *mut MaybeUninit to *mut T is always sound by - // the layout guarantees of MaybeUninit. - let ptr_to_first: *mut MaybeUninit = self.arr.as_mut_ptr(); - let ptr_to_slice = ptr::slice_from_raw_parts_mut(ptr_to_first.cast::(), self.len); - ptr::drop_in_place(ptr_to_slice); + ptr::drop_in_place(valid); } } }