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

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

align_to and align_to_mut contract and harnesses #405

Changes from all commits
Commits
Show all changes
3 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
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
166 changes: 166 additions & 0 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 @@ -4006,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())) )
)
)]
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see in the ensures clauses the condition that the middle part is correctly aligned.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, this is something I was wondering about -- my impression was that because it's UB to create a misaligned reference, it would be redundant to have a check for the middle part being aligned (since if it isn't, there would already be UB by the time the ensures clause is checked, meaning the check would either return true or something potentially invalid due to previous UB). But of course it's possible that Kani might have some way to circumvent this problem that I'm not familiar with (otherwise the only way I can think of would be to write this check as an assert inside the body of align_to, right before where there could potentially be UB). Would be happy to hear your thoughts on this whenever you have a chance!

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 @@ -4114,6 +4151,48 @@ impl<T> [T] {
}
}

//We need the following wrapper because it is not currently possible to write
//contracts for functions that return mut refs to input arguments
//see https://github.com/model-checking/kani/issues/3764
//----------------------------
//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): &(*const [T], *const [U], *const [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): &(*const [T], *const [U], *const [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())) )
)
)]
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see in the ensures clauses the condition that the middle part is correctly aligned.

unsafe fn align_to_mut_wrapper<U>(&mut self) -> (*const [T], *const [U], *const [T]) {
let (prefix_mut, mid_mut, suffix_mut) = self.align_to_mut::<U>();
(prefix_mut as *const [T], mid_mut as *const [U], suffix_mut as *const [T])
}

/// Splits a slice into a prefix, a middle of aligned SIMD types, and a suffix.
///
/// This is a safe wrapper around [`slice::align_to`], so inherits the same
Expand Down Expand Up @@ -5291,3 +5370,90 @@ 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
//this uses the contract for align_to_mut_wrapper (see comment there for why)
macro_rules! proof_of_contract_for_align_to_mut {
($harness:ident, $src:ty, $dst:ty) => {
#[kani::proof_for_contract(<[$src]>::align_to_mut_wrapper)]
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_wrapper::<$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