Skip to content

Commit 7955ba1

Browse files
committed
Generalize split_at_unchecked
Makes progress towards #1290.
1 parent 04cafb2 commit 7955ba1

File tree

5 files changed

+463
-97
lines changed

5 files changed

+463
-97
lines changed

src/lib.rs

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -381,6 +381,7 @@ use crate::pointer::invariant::{self, BecauseExclusive};
381381
extern crate alloc;
382382
#[cfg(any(feature = "alloc", test))]
383383
use alloc::{boxed::Box, vec::Vec};
384+
use util::MetadataOf;
384385

385386
#[cfg(any(feature = "alloc", test, kani))]
386387
use core::alloc::Layout;
@@ -1021,6 +1022,163 @@ safety_comment! {
10211022
unsafe_impl_known_layout!(T: ?Sized + KnownLayout => #[repr(T::MaybeUninit)] MaybeUninit<T>);
10221023
}
10231024

1025+
/// DSTs that can be split in two.
1026+
///
1027+
/// # Safety
1028+
///
1029+
/// The trailing slice is well-aligned for its element type.
1030+
pub unsafe trait SplitAt: KnownLayout<PointerMetadata = usize> {
1031+
/// The element type of the trailing slice.
1032+
type Elem;
1033+
1034+
/// Splits `T` in two.
1035+
///
1036+
/// # Safety
1037+
///
1038+
/// The caller promises that:
1039+
/// 0. `l_len.get()` is not greater than the length of `self`'s trailing
1040+
/// slice.
1041+
/// 1. if `I::Aliasing` is [`Exclusive`], then `l_len.padding_needed_for()
1042+
/// == 0`.
1043+
#[doc(hidden)]
1044+
#[allow(private_interfaces)]
1045+
unsafe fn ptr_split_at_unchecked<'a, I, R>(
1046+
ptr: Ptr<'a, Self, I>,
1047+
l_len: MetadataOf<Self>,
1048+
) -> (Ptr<'a, Self, I>, Ptr<'a, [Self::Elem], I>)
1049+
where
1050+
I: invariant::Invariants,
1051+
Self: pointer::Read<I::Aliasing, R>,
1052+
{
1053+
let inner = ptr.as_inner();
1054+
1055+
// SAFETY: The caller promises that `l_len.get()` is not greater than
1056+
// the length of `self`'s trailing slice.
1057+
let (left, right) = unsafe { inner.split_at_unchecked(l_len) };
1058+
1059+
// Lemma 0: `left` and `right` conform to the aliasing invariant
1060+
// `I::Aliasing`. Proof: If `I::Aliasing` is `Exclusive`, the caller
1061+
// promises that `l_len.padding_needed_for() == 0`. Consequently,
1062+
// there is no trailing padding after `left`'s final element that would
1063+
// overlap into `right`. If `I::Aliasing` is shared, then overlap
1064+
// between their referents is permissible.
1065+
1066+
// SAFETY:
1067+
// 0. `left` conforms to the aliasing invariant of `I::Aliasing, by
1068+
// Lemma 0.
1069+
// 1. `left` conforms to the alignment invariant of `I::Alignment,
1070+
// because the referents of `left` and `Self` have the same address
1071+
// and type (and, thus, alignment requirement).
1072+
// 2. `left` conforms to the validity invariant of `I::Validity``,
1073+
// because TODO.
1074+
let left = unsafe { Ptr::from_inner(left) };
1075+
1076+
// SAFETY:
1077+
// 0. `right` conforms to the aliasing invariant of `I::Aliasing, by
1078+
// Lemma 0.
1079+
// 1. `right` conforms to the alignment invariant of `I::Alignment,
1080+
// because TODO. (this is a tricky one)
1081+
// 2. `right` conforms to the validity invariant of `I::Validity``,
1082+
// because TODO. (this is a tricky one).
1083+
let right = unsafe { Ptr::from_inner(right) };
1084+
1085+
(left, right)
1086+
}
1087+
1088+
/// Unsafely splits `self` in two.
1089+
///
1090+
/// # Safety
1091+
///
1092+
/// The caller promises that `l_len` is not greater than the length of
1093+
/// `self`'s trailing slice.
1094+
unsafe fn split_at_unchecked(&self, l_len: usize) -> (&Self, &[Self::Elem])
1095+
where
1096+
Self: Immutable,
1097+
{
1098+
// SAFETY: `&self` is an instance of `&Self` for which the caller has
1099+
// promised that `l_len` is not greater than the length of `self`'s
1100+
// trailing slice.
1101+
let l_len = unsafe { MetadataOf::new_unchecked(l_len) };
1102+
let ptr = Ptr::from_ref(self);
1103+
// SAFETY:
1104+
// 0. The caller promises that `l_len` is not greater than the length of
1105+
// `self`'s trailing slice.
1106+
// 1. `ptr`'s aliasing is `Shared`
1107+
// 2. By contract on `SplitAt`, the trailing slice is well aligned for
1108+
// its element type.
1109+
let (left, right) = unsafe { Self::ptr_split_at_unchecked(ptr, l_len) };
1110+
(left.as_ref(), right.as_ref())
1111+
}
1112+
1113+
/// Attempts to split `self` into two.
1114+
///
1115+
/// Returns `None` if `l_len` is greater than the length of `self`'s
1116+
/// trailing slice.
1117+
fn split_at(&self, l_len: usize) -> Option<(&Self, &[Self::Elem])>
1118+
where
1119+
Self: Immutable,
1120+
{
1121+
if l_len <= Ptr::from_ref(self).len() {
1122+
// SAFETY: We have checked that `l_len` is not greater than the
1123+
// length of `self`'s trailing slice.
1124+
Some(unsafe { self.split_at_unchecked(l_len) })
1125+
} else {
1126+
None
1127+
}
1128+
}
1129+
1130+
/// Unsafely splits `self` in two.
1131+
///
1132+
/// # Safety
1133+
///
1134+
/// The caller promises that:
1135+
/// 0. `l_len` is not greater than the length of `self`'s trailing slice.
1136+
/// 1. The trailing padding bytes of the left portion will not overlap the
1137+
/// right portion. For some dynamically sized types, the padding that
1138+
/// appears after the trailing slice field [is a dynamic function of the
1139+
/// trailing slice length](KnownLayout#slice-dst-layout). Thus for some
1140+
/// types this condition is dependent on the value of `l_len`.
1141+
unsafe fn split_at_mut_unchecked(&mut self, l_len: usize) -> (&mut Self, &mut [Self::Elem]) {
1142+
// SAFETY: `&mut self` is an instance of `&mut Self` for which the
1143+
// caller has promised that `l_len` is not greater than the length of
1144+
// `self`'s trailing slice.
1145+
let l_len = unsafe { MetadataOf::new_unchecked(l_len) };
1146+
let ptr = Ptr::from_mut(self);
1147+
// SAFETY:
1148+
// 0. The caller promises that `l_len` is not greater than the length of
1149+
// `self`'s trailing slice.
1150+
// 1. `ptr`'s aliasing is `Exclusive`; the caller promises that
1151+
// `l_len.padding_needed_for() == 0`.
1152+
// 2. By contract on `SplitAt`, the trailing slice is well aligned for
1153+
// its element type.
1154+
let (left, right) = unsafe { Self::ptr_split_at_unchecked(ptr, l_len) };
1155+
(left.as_mut(), right.as_mut())
1156+
}
1157+
1158+
/// Attempts to split `self` into two.
1159+
///
1160+
/// Returns `None` if `l_len` is greater than the length of `self`'s
1161+
/// trailing slice, or if the given `l_len` would result in [the trailing
1162+
/// padding](KnownLayout#slice-dst-layout) of the left portion overlapping
1163+
/// the right portion.
1164+
fn split_at_mut(&mut self, l_len: usize) -> Option<(&mut Self, &mut [Self::Elem])> {
1165+
match MetadataOf::new(self, l_len) {
1166+
Some(l_len) if l_len.padding_needed_for() == 0 => {
1167+
// SAFETY: We have ensured both that:
1168+
// 0. `l_len <= self.len()`
1169+
// 1. `l_len.padding_needed_for() == 0
1170+
Some(unsafe { self.split_at_mut_unchecked(l_len.get()) })
1171+
}
1172+
_ => None,
1173+
}
1174+
}
1175+
}
1176+
1177+
// SAFETY: TODO
1178+
unsafe impl<T> SplitAt for [T] {
1179+
type Elem = T;
1180+
}
1181+
10241182
/// Analyzes whether a type is [`FromZeros`].
10251183
///
10261184
/// This derive analyzes, at compile time, whether the annotated type satisfies

0 commit comments

Comments
 (0)