Skip to content

Commit fc2a863

Browse files
committed
moved align_to_mut_wrapper contract to align_to_mut
1 parent 31a8d89 commit fc2a863

File tree

1 file changed

+41
-136
lines changed

1 file changed

+41
-136
lines changed

library/core/src/slice/mod.rs

Lines changed: 41 additions & 136 deletions
Original file line numberDiff line numberDiff line change
@@ -1320,7 +1320,7 @@ impl<T> [T] {
13201320
assert_unsafe_precondition!(
13211321
check_language_ub,
13221322
"slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
1323-
(n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n),
1323+
(n: usize = N, len: usize = self.len()) => n != 0 && len % n == 0,
13241324
);
13251325
// SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length
13261326
let new_len = unsafe { exact_div(self.len(), N) };
@@ -1516,7 +1516,7 @@ impl<T> [T] {
15161516
assert_unsafe_precondition!(
15171517
check_language_ub,
15181518
"slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
1519-
(n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n)
1519+
(n: usize = N, len: usize = self.len()) => n != 0 && len % n == 0
15201520
);
15211521
// SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length
15221522
let new_len = unsafe { exact_div(self.len(), N) };
@@ -2768,89 +2768,6 @@ impl<T> [T] {
27682768
None
27692769
}
27702770

2771-
/// Returns a subslice with the optional prefix removed.
2772-
///
2773-
/// If the slice starts with `prefix`, returns the subslice after the prefix. If `prefix`
2774-
/// is empty or the slice does not start with `prefix`, simply returns the original slice.
2775-
/// If `prefix` is equal to the original slice, returns an empty slice.
2776-
///
2777-
/// # Examples
2778-
///
2779-
/// ```
2780-
/// #![feature(trim_prefix_suffix)]
2781-
///
2782-
/// let v = &[10, 40, 30];
2783-
///
2784-
/// // Prefix present - removes it
2785-
/// assert_eq!(v.trim_prefix(&[10]), &[40, 30][..]);
2786-
/// assert_eq!(v.trim_prefix(&[10, 40]), &[30][..]);
2787-
/// assert_eq!(v.trim_prefix(&[10, 40, 30]), &[][..]);
2788-
///
2789-
/// // Prefix absent - returns original slice
2790-
/// assert_eq!(v.trim_prefix(&[50]), &[10, 40, 30][..]);
2791-
/// assert_eq!(v.trim_prefix(&[10, 50]), &[10, 40, 30][..]);
2792-
///
2793-
/// let prefix : &str = "he";
2794-
/// assert_eq!(b"hello".trim_prefix(prefix.as_bytes()), b"llo".as_ref());
2795-
/// ```
2796-
#[must_use = "returns the subslice without modifying the original"]
2797-
#[unstable(feature = "trim_prefix_suffix", issue = "142312")]
2798-
pub fn trim_prefix<P: SlicePattern<Item = T> + ?Sized>(&self, prefix: &P) -> &[T]
2799-
where
2800-
T: PartialEq,
2801-
{
2802-
// This function will need rewriting if and when SlicePattern becomes more sophisticated.
2803-
let prefix = prefix.as_slice();
2804-
let n = prefix.len();
2805-
if n <= self.len() {
2806-
let (head, tail) = self.split_at(n);
2807-
if head == prefix {
2808-
return tail;
2809-
}
2810-
}
2811-
self
2812-
}
2813-
2814-
/// Returns a subslice with the optional suffix removed.
2815-
///
2816-
/// If the slice ends with `suffix`, returns the subslice before the suffix. If `suffix`
2817-
/// is empty or the slice does not end with `suffix`, simply returns the original slice.
2818-
/// If `suffix` is equal to the original slice, returns an empty slice.
2819-
///
2820-
/// # Examples
2821-
///
2822-
/// ```
2823-
/// #![feature(trim_prefix_suffix)]
2824-
///
2825-
/// let v = &[10, 40, 30];
2826-
///
2827-
/// // Suffix present - removes it
2828-
/// assert_eq!(v.trim_suffix(&[30]), &[10, 40][..]);
2829-
/// assert_eq!(v.trim_suffix(&[40, 30]), &[10][..]);
2830-
/// assert_eq!(v.trim_suffix(&[10, 40, 30]), &[][..]);
2831-
///
2832-
/// // Suffix absent - returns original slice
2833-
/// assert_eq!(v.trim_suffix(&[50]), &[10, 40, 30][..]);
2834-
/// assert_eq!(v.trim_suffix(&[50, 30]), &[10, 40, 30][..]);
2835-
/// ```
2836-
#[must_use = "returns the subslice without modifying the original"]
2837-
#[unstable(feature = "trim_prefix_suffix", issue = "142312")]
2838-
pub fn trim_suffix<P: SlicePattern<Item = T> + ?Sized>(&self, suffix: &P) -> &[T]
2839-
where
2840-
T: PartialEq,
2841-
{
2842-
// This function will need rewriting if and when SlicePattern becomes more sophisticated.
2843-
let suffix = suffix.as_slice();
2844-
let (len, n) = (self.len(), suffix.len());
2845-
if n <= len {
2846-
let (head, tail) = self.split_at(len - n);
2847-
if tail == suffix {
2848-
return head;
2849-
}
2850-
}
2851-
self
2852-
}
2853-
28542771
/// Binary searches this slice for a given element.
28552772
/// If the slice is not sorted, the returned result is unspecified and
28562773
/// meaningless.
@@ -4191,6 +4108,39 @@ impl<T> [T] {
41914108
/// ```
41924109
#[stable(feature = "slice_align_to", since = "1.30.0")]
41934110
#[must_use]
4111+
//Checks if the part that will be transmuted from type T to U is valid for type U
4112+
//reuses most function logic up to use of from_raw_parts,
4113+
//where the potentially unsafe transmute occurs
4114+
#[requires(
4115+
U::IS_ZST || T::IS_ZST || {
4116+
let ptr = self.as_ptr();
4117+
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
4118+
offset > self.len() || {
4119+
let (_, rest) = self.split_at(offset);
4120+
let (us_len, _) = rest.align_to_offsets::<U>();
4121+
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len);
4122+
crate::ub_checks::can_dereference(middle)
4123+
}
4124+
}
4125+
)]
4126+
//The following clause guarantees that middle is of maximum size within self
4127+
//If U or T are ZSTs, then middle has size zero, so we adapt the check in that case
4128+
#[ensures(|(prefix, _, suffix): &(&mut [T], &mut [U], &mut [T])|
4129+
((U::IS_ZST || T::IS_ZST) && prefix.len() == old(self.len())) || (
4130+
(prefix.len() * size_of::<T>() < align_of::<U>()) &&
4131+
(suffix.len() * size_of::<T>() < size_of::<U>())
4132+
)
4133+
)]
4134+
//Either align_to just returns self in the prefix, or the 3 returned slices
4135+
//should be sequential, contiguous, and have same total length as self
4136+
#[ensures(|(prefix, middle, suffix): &(&mut [T], &mut [U], &mut [T])|
4137+
prefix.as_ptr() == old(self.as_ptr()) &&
4138+
(prefix.len() == old(self.len()) || (
4139+
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
4140+
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
4141+
((suffix.as_ptr()).add(suffix.len()) == old((self.as_ptr()).add(self.len())))
4142+
))
4143+
)]
41944144
pub unsafe fn align_to_mut<U>(&mut self) -> (&mut [T], &mut [U], &mut [T]) {
41954145
// Note that most of this function will be constant-evaluated,
41964146
if U::IS_ZST || T::IS_ZST {
@@ -4234,48 +4184,6 @@ impl<T> [T] {
42344184
}
42354185
}
42364186

4237-
//We need the following wrapper because it is not currently possible to write
4238-
//contracts for functions that return mut refs to input arguments
4239-
//see https://github.com/model-checking/kani/issues/3764
4240-
//----------------------------
4241-
//Checks if the part that will be transmuted from type T to U is valid for type U
4242-
//reuses most function logic up to use of from_raw_parts,
4243-
//where the potentially unsafe transmute occurs
4244-
#[requires(
4245-
U::IS_ZST || T::IS_ZST || {
4246-
let ptr = self.as_ptr();
4247-
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
4248-
offset > self.len() || {
4249-
let (_, rest) = self.split_at(offset);
4250-
let (us_len, _) = rest.align_to_offsets::<U>();
4251-
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len);
4252-
crate::ub_checks::can_dereference(middle)
4253-
}
4254-
}
4255-
)]
4256-
//The following clause guarantees that middle is of maximum size within self
4257-
//If U or T are ZSTs, then middle has size zero, so we adapt the check in that case
4258-
#[ensures(|(prefix, _, suffix): &(*const [T], *const [U], *const [T])|
4259-
((U::IS_ZST || T::IS_ZST) && prefix.len() == self.len()) || (
4260-
(prefix.len() * size_of::<T>() < align_of::<U>()) &&
4261-
(suffix.len() * size_of::<T>() < size_of::<U>())
4262-
)
4263-
)]
4264-
//Either align_to just returns self in the prefix, or the 3 returned slices
4265-
//should be sequential, contiguous, and have same total length as self
4266-
#[ensures(|(prefix, middle, suffix): &(*const [T], *const [U], *const [T])|
4267-
prefix.as_ptr() == self.as_ptr() &&
4268-
(prefix.len() == self.len() || (
4269-
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
4270-
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
4271-
((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) )
4272-
)
4273-
)]
4274-
unsafe fn align_to_mut_wrapper<U>(&mut self) -> (*const [T], *const [U], *const [T]) {
4275-
let (prefix_mut, mid_mut, suffix_mut) = self.align_to_mut::<U>();
4276-
(prefix_mut as *const [T], mid_mut as *const [U], suffix_mut as *const [T])
4277-
}
4278-
42794187
/// Splits a slice into a prefix, a middle of aligned SIMD types, and a suffix.
42804188
///
42814189
/// This is a safe wrapper around [`slice::align_to`], so inherits the same
@@ -4945,7 +4853,7 @@ impl<T> [T] {
49454853

49464854
let byte_offset = elem_start.wrapping_sub(self_start);
49474855

4948-
if !byte_offset.is_multiple_of(size_of::<T>()) {
4856+
if byte_offset % size_of::<T>() != 0 {
49494857
return None;
49504858
}
49514859

@@ -4999,7 +4907,7 @@ impl<T> [T] {
49994907

50004908
let byte_start = subslice_start.wrapping_sub(self_start);
50014909

5002-
if !byte_start.is_multiple_of(size_of::<T>()) {
4910+
if byte_start % size_of::<T>() != 0 {
50034911
return None;
50044912
}
50054913

@@ -5237,17 +5145,15 @@ where
52375145
}
52385146

52395147
#[stable(feature = "rust1", since = "1.0.0")]
5240-
#[rustc_const_unstable(feature = "const_default", issue = "67792")]
5241-
impl<T> const Default for &[T] {
5148+
impl<T> Default for &[T] {
52425149
/// Creates an empty slice.
52435150
fn default() -> Self {
52445151
&[]
52455152
}
52465153
}
52475154

52485155
#[stable(feature = "mut_slice_default", since = "1.5.0")]
5249-
#[rustc_const_unstable(feature = "const_default", issue = "67792")]
5250-
impl<T> const Default for &mut [T] {
5156+
impl<T> Default for &mut [T] {
52515157
/// Creates a mutable empty slice.
52525158
fn default() -> Self {
52535159
&mut []
@@ -5502,15 +5408,14 @@ mod verify {
55025408
gen_align_to_harnesses!(align_to_from_unit, ());
55035409

55045410
//generates proof_of_contract harness for align_to_mut given the T (src) and U (dst) types
5505-
//this uses the contract for align_to_mut_wrapper (see comment there for why)
55065411
macro_rules! proof_of_contract_for_align_to_mut {
55075412
($harness:ident, $src:ty, $dst:ty) => {
5508-
#[kani::proof_for_contract(<[$src]>::align_to_mut_wrapper)]
5413+
#[kani::proof_for_contract(<[$src]>::align_to_mut)]
55095414
fn $harness() {
55105415
const ARR_SIZE: usize = 100;
55115416
let mut src_arr: [$src; ARR_SIZE] = kani::any();
55125417
let src_slice = kani::slice::any_slice_of_array_mut(&mut src_arr);
5513-
let dst_slice = unsafe { src_slice.align_to_mut_wrapper::<$dst>() };
5418+
let dst_slice = unsafe { src_slice.align_to_mut::<$dst>() };
55145419
}
55155420
};
55165421
}

0 commit comments

Comments
 (0)