Skip to content

align_to and align_to_mut contract and harnesses #405

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jul 24, 2025
Merged

align_to and align_to_mut contract and harnesses #405

Changes from 6 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
106a110
align_to and align_to_mut contracts
AlexLB99 Jul 2, 2025
c2a64d8
Merge branch 'model-checking:main' into check_align_to
AlexLB99 Jul 2, 2025
9e62272
updated/added comments to slice/mod.rs
AlexLB99 Jul 2, 2025
31a8d89
Merge branch 'model-checking:main' into check_align_to
AlexLB99 Jul 22, 2025
fc2a863
moved align_to_mut_wrapper contract to align_to_mut
AlexLB99 Jul 22, 2025
68dd9ba
formatting
AlexLB99 Jul 22, 2025
ed67c16
Merge branch 'model-checking:main' into check_align_to
AlexLB99 Jul 23, 2025
7e8d09c
fixed mismerge
AlexLB99 Jul 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
253 changes: 162 additions & 91 deletions library/core/src/slice/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,12 @@

#![stable(feature = "rust1", since = "1.0.0")]

use safety::{ensures, requires};

use crate::cmp::Ordering::{self, Equal, Greater, Less};
use crate::intrinsics::{exact_div, unchecked_sub};
#[cfg(kani)]
use crate::kani;
use crate::mem::{self, MaybeUninit, SizedTypeProperties};
use crate::num::NonZero;
use crate::ops::{OneSidedRange, OneSidedRangeBound, Range, RangeBounds, RangeInclusive};
Expand Down Expand Up @@ -1316,7 +1320,7 @@ impl<T> [T] {
assert_unsafe_precondition!(
check_language_ub,
"slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
(n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n),
(n: usize = N, len: usize = self.len()) => n != 0 && len % n == 0,
);
// SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length
let new_len = unsafe { exact_div(self.len(), N) };
Expand Down Expand Up @@ -1512,7 +1516,7 @@ impl<T> [T] {
assert_unsafe_precondition!(
check_language_ub,
"slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
(n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n)
(n: usize = N, len: usize = self.len()) => n != 0 && len % n == 0
);
// SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length
let new_len = unsafe { exact_div(self.len(), N) };
Expand Down Expand Up @@ -2764,89 +2768,6 @@ impl<T> [T] {
None
}

/// Returns a subslice with the optional prefix removed.
///
/// If the slice starts with `prefix`, returns the subslice after the prefix. If `prefix`
/// is empty or the slice does not start with `prefix`, simply returns the original slice.
/// If `prefix` is equal to the original slice, returns an empty slice.
///
/// # Examples
///
/// ```
/// #![feature(trim_prefix_suffix)]
///
/// let v = &[10, 40, 30];
///
/// // Prefix present - removes it
/// assert_eq!(v.trim_prefix(&[10]), &[40, 30][..]);
/// assert_eq!(v.trim_prefix(&[10, 40]), &[30][..]);
/// assert_eq!(v.trim_prefix(&[10, 40, 30]), &[][..]);
///
/// // Prefix absent - returns original slice
/// assert_eq!(v.trim_prefix(&[50]), &[10, 40, 30][..]);
/// assert_eq!(v.trim_prefix(&[10, 50]), &[10, 40, 30][..]);
///
/// let prefix : &str = "he";
/// assert_eq!(b"hello".trim_prefix(prefix.as_bytes()), b"llo".as_ref());
/// ```
#[must_use = "returns the subslice without modifying the original"]
#[unstable(feature = "trim_prefix_suffix", issue = "142312")]
pub fn trim_prefix<P: SlicePattern<Item = T> + ?Sized>(&self, prefix: &P) -> &[T]
where
T: PartialEq,
{
// This function will need rewriting if and when SlicePattern becomes more sophisticated.
let prefix = prefix.as_slice();
let n = prefix.len();
if n <= self.len() {
let (head, tail) = self.split_at(n);
if head == prefix {
return tail;
}
}
self
}

/// Returns a subslice with the optional suffix removed.
///
/// If the slice ends with `suffix`, returns the subslice before the suffix. If `suffix`
/// is empty or the slice does not end with `suffix`, simply returns the original slice.
/// If `suffix` is equal to the original slice, returns an empty slice.
///
/// # Examples
///
/// ```
/// #![feature(trim_prefix_suffix)]
///
/// let v = &[10, 40, 30];
///
/// // Suffix present - removes it
/// assert_eq!(v.trim_suffix(&[30]), &[10, 40][..]);
/// assert_eq!(v.trim_suffix(&[40, 30]), &[10][..]);
/// assert_eq!(v.trim_suffix(&[10, 40, 30]), &[][..]);
///
/// // Suffix absent - returns original slice
/// assert_eq!(v.trim_suffix(&[50]), &[10, 40, 30][..]);
/// assert_eq!(v.trim_suffix(&[50, 30]), &[10, 40, 30][..]);
/// ```
#[must_use = "returns the subslice without modifying the original"]
#[unstable(feature = "trim_prefix_suffix", issue = "142312")]
pub fn trim_suffix<P: SlicePattern<Item = T> + ?Sized>(&self, suffix: &P) -> &[T]
where
T: PartialEq,
{
// This function will need rewriting if and when SlicePattern becomes more sophisticated.
let suffix = suffix.as_slice();
let (len, n) = (self.len(), suffix.len());
if n <= len {
let (head, tail) = self.split_at(len - n);
if tail == suffix {
return head;
}
}
self
}

/// Binary searches this slice for a given element.
/// If the slice is not sorted, the returned result is unspecified and
/// meaningless.
Expand Down Expand Up @@ -4089,6 +4010,39 @@ impl<T> [T] {
/// ```
#[stable(feature = "slice_align_to", since = "1.30.0")]
#[must_use]
//Checks if the part that will be transmuted from type T to U is valid for type U
//reuses most function logic up to use of from_raw_parts,
//where the potentially unsafe transmute occurs
#[requires(
U::IS_ZST || T::IS_ZST || {
let ptr = self.as_ptr();
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
offset > self.len() || {
let (_, rest) = self.split_at(offset);
let (us_len, _) = rest.align_to_offsets::<U>();
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len);
crate::ub_checks::can_dereference(middle)
}
}
)]
//The following clause guarantees that middle is of maximum size within self
//If U or T are ZSTs, then middle has size zero, so we adapt the check in that case
#[ensures(|(prefix, _, suffix): &(&[T], &[U], &[T])|
((U::IS_ZST || T::IS_ZST) && prefix.len() == self.len()) || (
(prefix.len() * size_of::<T>() < align_of::<U>()) &&
(suffix.len() * size_of::<T>() < size_of::<U>())
)
)]
//Either align_to just returns self in the prefix, or the 3 returned slices
//should be sequential, contiguous, and have same total length as self
#[ensures(|(prefix, middle, suffix): &(&[T], &[U], &[T])|
prefix.as_ptr() == self.as_ptr() &&
(prefix.len() == self.len() || (
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) )
)
)]
pub unsafe fn align_to<U>(&self) -> (&[T], &[U], &[T]) {
// Note that most of this function will be constant-evaluated,
if U::IS_ZST || T::IS_ZST {
Expand Down Expand Up @@ -4154,6 +4108,39 @@ impl<T> [T] {
/// ```
#[stable(feature = "slice_align_to", since = "1.30.0")]
#[must_use]
//Checks if the part that will be transmuted from type T to U is valid for type U
//reuses most function logic up to use of from_raw_parts,
//where the potentially unsafe transmute occurs
#[requires(
U::IS_ZST || T::IS_ZST || {
let ptr = self.as_ptr();
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
offset > self.len() || {
let (_, rest) = self.split_at(offset);
let (us_len, _) = rest.align_to_offsets::<U>();
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len);
crate::ub_checks::can_dereference(middle)
}
}
)]
//The following clause guarantees that middle is of maximum size within self
//If U or T are ZSTs, then middle has size zero, so we adapt the check in that case
#[ensures(|(prefix, _, suffix): &(&mut [T], &mut [U], &mut [T])|
((U::IS_ZST || T::IS_ZST) && prefix.len() == old(self.len())) || (
(prefix.len() * size_of::<T>() < align_of::<U>()) &&
(suffix.len() * size_of::<T>() < size_of::<U>())
)
)]
//Either align_to just returns self in the prefix, or the 3 returned slices
//should be sequential, contiguous, and have same total length as self
#[ensures(|(prefix, middle, suffix): &(&mut [T], &mut [U], &mut [T])|
prefix.as_ptr() == old(self.as_ptr()) &&
(prefix.len() == old(self.len()) || (
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
((suffix.as_ptr()).add(suffix.len()) == old((self.as_ptr()).add(self.len())))
))
)]
pub unsafe fn align_to_mut<U>(&mut self) -> (&mut [T], &mut [U], &mut [T]) {
// Note that most of this function will be constant-evaluated,
if U::IS_ZST || T::IS_ZST {
Expand Down Expand Up @@ -4866,7 +4853,7 @@ impl<T> [T] {

let byte_offset = elem_start.wrapping_sub(self_start);

if !byte_offset.is_multiple_of(size_of::<T>()) {
if byte_offset % size_of::<T>() != 0 {
return None;
}

Expand Down Expand Up @@ -4920,7 +4907,7 @@ impl<T> [T] {

let byte_start = subslice_start.wrapping_sub(self_start);

if !byte_start.is_multiple_of(size_of::<T>()) {
if byte_start % size_of::<T>() != 0 {
return None;
}

Expand Down Expand Up @@ -5158,17 +5145,15 @@ where
}

#[stable(feature = "rust1", since = "1.0.0")]
#[rustc_const_unstable(feature = "const_default", issue = "67792")]
impl<T> const Default for &[T] {
impl<T> Default for &[T] {
/// Creates an empty slice.
fn default() -> Self {
&[]
}
}

#[stable(feature = "mut_slice_default", since = "1.5.0")]
#[rustc_const_unstable(feature = "const_default", issue = "67792")]
impl<T> const Default for &mut [T] {
impl<T> Default for &mut [T] {
/// Creates a mutable empty slice.
fn default() -> Self {
&mut []
Expand Down Expand Up @@ -5376,3 +5361,89 @@ unsafe impl GetDisjointMutIndex for range::RangeInclusive<usize> {
RangeInclusive::from(*self).is_overlapping(&RangeInclusive::from(*other))
}
}

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;

//generates proof_of_contract harness for align_to given the T (src) and U (dst) types
macro_rules! proof_of_contract_for_align_to {
($harness:ident, $src:ty, $dst:ty) => {
#[kani::proof_for_contract(<[$src]>::align_to)]
fn $harness() {
const ARR_SIZE: usize = 100;
let src_arr: [$src; ARR_SIZE] = kani::any();
let src_slice = kani::slice::any_slice_of_array(&src_arr);
let dst_slice = unsafe { src_slice.align_to::<$dst>() };
}
};
}

//generates harnesses for align_to where T is a given src type and U is one of the main primitives
macro_rules! gen_align_to_harnesses {
($mod_name:ident, $src_type:ty) => {
mod $mod_name {
use super::*;

proof_of_contract_for_align_to!(align_to_u8, $src_type, u8);
proof_of_contract_for_align_to!(align_to_u16, $src_type, u16);
proof_of_contract_for_align_to!(align_to_u32, $src_type, u32);
proof_of_contract_for_align_to!(align_to_u64, $src_type, u64);
proof_of_contract_for_align_to!(align_to_u128, $src_type, u128);
proof_of_contract_for_align_to!(align_to_bool, $src_type, bool);
proof_of_contract_for_align_to!(align_to_char, $src_type, char);
proof_of_contract_for_align_to!(align_to_unit, $src_type, ());
}
};
}

gen_align_to_harnesses!(align_to_from_u8, u8);
gen_align_to_harnesses!(align_to_from_u16, u16);
gen_align_to_harnesses!(align_to_from_u32, u32);
gen_align_to_harnesses!(align_to_from_u64, u64);
gen_align_to_harnesses!(align_to_from_u128, u128);
gen_align_to_harnesses!(align_to_from_bool, bool);
gen_align_to_harnesses!(align_to_from_char, char);
gen_align_to_harnesses!(align_to_from_unit, ());

//generates proof_of_contract harness for align_to_mut given the T (src) and U (dst) types
macro_rules! proof_of_contract_for_align_to_mut {
($harness:ident, $src:ty, $dst:ty) => {
#[kani::proof_for_contract(<[$src]>::align_to_mut)]
fn $harness() {
const ARR_SIZE: usize = 100;
let mut src_arr: [$src; ARR_SIZE] = kani::any();
let src_slice = kani::slice::any_slice_of_array_mut(&mut src_arr);
let dst_slice = unsafe { src_slice.align_to_mut::<$dst>() };
}
};
}

//generates harnesses between a given src type and all the main primitives
macro_rules! gen_align_to_mut_harnesses {
($mod_name:ident, $src_type:ty) => {
mod $mod_name {
use super::*;

proof_of_contract_for_align_to_mut!(align_to_mut_u8, $src_type, u8);
proof_of_contract_for_align_to_mut!(align_to_mut_u16, $src_type, u16);
proof_of_contract_for_align_to_mut!(align_to_mut_u32, $src_type, u32);
proof_of_contract_for_align_to_mut!(align_to_mut_u64, $src_type, u64);
proof_of_contract_for_align_to_mut!(align_to_mut_u128, $src_type, u128);
proof_of_contract_for_align_to_mut!(align_to_mut_bool, $src_type, bool);
proof_of_contract_for_align_to_mut!(align_to_mut_char, $src_type, char);
proof_of_contract_for_align_to_mut!(align_to_mut_unit, $src_type, ());
}
};
}

gen_align_to_mut_harnesses!(align_to_mut_from_u8, u8);
gen_align_to_mut_harnesses!(align_to_mut_from_u16, u16);
gen_align_to_mut_harnesses!(align_to_mut_from_u32, u32);
gen_align_to_mut_harnesses!(align_to_mut_from_u64, u64);
gen_align_to_mut_harnesses!(align_to_mut_from_u128, u128);
gen_align_to_mut_harnesses!(align_to_mut_from_bool, bool);
gen_align_to_mut_harnesses!(align_to_mut_from_char, char);
gen_align_to_mut_harnesses!(align_to_mut_from_unit, ());
}
Loading