Skip to content

Commit 099ad08

Browse files
AlexLB99AlexLB99
authored
align_to and align_to_mut contract and harnesses (#405)
Towards solving #19 This PR adds harnesses and contracts for align_to() and align_to_mut(). For the contract for align_to_mut(), we're using a wrapper and writing a contract for that instead, due to model-checking/kani#3764. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 34236a6 commit 099ad08

File tree

1 file changed

+156
-0
lines changed

1 file changed

+156
-0
lines changed

‎library/core/src/slice/mod.rs

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,12 @@
66
77
#![stable(feature = "rust1", since = "1.0.0")]
88

9+
use safety::{ensures, requires};
10+
911
use crate::cmp::Ordering::{self, Equal, Greater, Less};
1012
use crate::intrinsics::{exact_div, unchecked_sub};
13+
#[cfg(kani)]
14+
use crate::kani;
1115
use crate::mem::{self, MaybeUninit, SizedTypeProperties};
1216
use crate::num::NonZero;
1317
use crate::ops::{OneSidedRange, OneSidedRangeBound, Range, RangeBounds, RangeInclusive};
@@ -4123,6 +4127,39 @@ impl<T> [T] {
41234127
/// ```
41244128
#[stable(feature = "slice_align_to", since = "1.30.0")]
41254129
#[must_use]
4130+
//Checks if the part that will be transmuted from type T to U is valid for type U
4131+
//reuses most function logic up to use of from_raw_parts,
4132+
//where the potentially unsafe transmute occurs
4133+
#[requires(
4134+
U::IS_ZST || T::IS_ZST || {
4135+
let ptr = self.as_ptr();
4136+
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
4137+
offset > self.len() || {
4138+
let (_, rest) = self.split_at(offset);
4139+
let (us_len, _) = rest.align_to_offsets::<U>();
4140+
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len);
4141+
crate::ub_checks::can_dereference(middle)
4142+
}
4143+
}
4144+
)]
4145+
//The following clause guarantees that middle is of maximum size within self
4146+
//If U or T are ZSTs, then middle has size zero, so we adapt the check in that case
4147+
#[ensures(|(prefix, _, suffix): &(&[T], &[U], &[T])|
4148+
((U::IS_ZST || T::IS_ZST) && prefix.len() == self.len()) || (
4149+
(prefix.len() * size_of::<T>() < align_of::<U>()) &&
4150+
(suffix.len() * size_of::<T>() < size_of::<U>())
4151+
)
4152+
)]
4153+
//Either align_to just returns self in the prefix, or the 3 returned slices
4154+
//should be sequential, contiguous, and have same total length as self
4155+
#[ensures(|(prefix, middle, suffix): &(&[T], &[U], &[T])|
4156+
prefix.as_ptr() == self.as_ptr() &&
4157+
(prefix.len() == self.len() || (
4158+
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
4159+
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
4160+
((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) )
4161+
)
4162+
)]
41264163
pub unsafe fn align_to<U>(&self) -> (&[T], &[U], &[T]) {
41274164
// Note that most of this function will be constant-evaluated,
41284165
if U::IS_ZST || T::IS_ZST {
@@ -4188,6 +4225,39 @@ impl<T> [T] {
41884225
/// ```
41894226
#[stable(feature = "slice_align_to", since = "1.30.0")]
41904227
#[must_use]
4228+
//Checks if the part that will be transmuted from type T to U is valid for type U
4229+
//reuses most function logic up to use of from_raw_parts,
4230+
//where the potentially unsafe transmute occurs
4231+
#[requires(
4232+
U::IS_ZST || T::IS_ZST || {
4233+
let ptr = self.as_ptr();
4234+
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
4235+
offset > self.len() || {
4236+
let (_, rest) = self.split_at(offset);
4237+
let (us_len, _) = rest.align_to_offsets::<U>();
4238+
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len);
4239+
crate::ub_checks::can_dereference(middle)
4240+
}
4241+
}
4242+
)]
4243+
//The following clause guarantees that middle is of maximum size within self
4244+
//If U or T are ZSTs, then middle has size zero, so we adapt the check in that case
4245+
#[ensures(|(prefix, _, suffix): &(&mut [T], &mut [U], &mut [T])|
4246+
((U::IS_ZST || T::IS_ZST) && prefix.len() == old(self.len())) || (
4247+
(prefix.len() * size_of::<T>() < align_of::<U>()) &&
4248+
(suffix.len() * size_of::<T>() < size_of::<U>())
4249+
)
4250+
)]
4251+
//Either align_to just returns self in the prefix, or the 3 returned slices
4252+
//should be sequential, contiguous, and have same total length as self
4253+
#[ensures(|(prefix, middle, suffix): &(&mut [T], &mut [U], &mut [T])|
4254+
prefix.as_ptr() == old(self.as_ptr()) &&
4255+
(prefix.len() == old(self.len()) || (
4256+
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
4257+
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
4258+
((suffix.as_ptr()).add(suffix.len()) == old((self.as_ptr()).add(self.len())))
4259+
))
4260+
)]
41914261
pub unsafe fn align_to_mut<U>(&mut self) -> (&mut [T], &mut [U], &mut [T]) {
41924262
// Note that most of this function will be constant-evaluated,
41934263
if U::IS_ZST || T::IS_ZST {
@@ -5410,3 +5480,89 @@ unsafe impl GetDisjointMutIndex for range::RangeInclusive<usize> {
54105480
RangeInclusive::from(*self).is_overlapping(&RangeInclusive::from(*other))
54115481
}
54125482
}
5483+
5484+
#[cfg(kani)]
5485+
#[unstable(feature = "kani", issue = "none")]
5486+
mod verify {
5487+
use super::*;
5488+
5489+
//generates proof_of_contract harness for align_to given the T (src) and U (dst) types
5490+
macro_rules! proof_of_contract_for_align_to {
5491+
($harness:ident, $src:ty, $dst:ty) => {
5492+
#[kani::proof_for_contract(<[$src]>::align_to)]
5493+
fn $harness() {
5494+
const ARR_SIZE: usize = 100;
5495+
let src_arr: [$src; ARR_SIZE] = kani::any();
5496+
let src_slice = kani::slice::any_slice_of_array(&src_arr);
5497+
let dst_slice = unsafe { src_slice.align_to::<$dst>() };
5498+
}
5499+
};
5500+
}
5501+
5502+
//generates harnesses for align_to where T is a given src type and U is one of the main primitives
5503+
macro_rules! gen_align_to_harnesses {
5504+
($mod_name:ident, $src_type:ty) => {
5505+
mod $mod_name {
5506+
use super::*;
5507+
5508+
proof_of_contract_for_align_to!(align_to_u8, $src_type, u8);
5509+
proof_of_contract_for_align_to!(align_to_u16, $src_type, u16);
5510+
proof_of_contract_for_align_to!(align_to_u32, $src_type, u32);
5511+
proof_of_contract_for_align_to!(align_to_u64, $src_type, u64);
5512+
proof_of_contract_for_align_to!(align_to_u128, $src_type, u128);
5513+
proof_of_contract_for_align_to!(align_to_bool, $src_type, bool);
5514+
proof_of_contract_for_align_to!(align_to_char, $src_type, char);
5515+
proof_of_contract_for_align_to!(align_to_unit, $src_type, ());
5516+
}
5517+
};
5518+
}
5519+
5520+
gen_align_to_harnesses!(align_to_from_u8, u8);
5521+
gen_align_to_harnesses!(align_to_from_u16, u16);
5522+
gen_align_to_harnesses!(align_to_from_u32, u32);
5523+
gen_align_to_harnesses!(align_to_from_u64, u64);
5524+
gen_align_to_harnesses!(align_to_from_u128, u128);
5525+
gen_align_to_harnesses!(align_to_from_bool, bool);
5526+
gen_align_to_harnesses!(align_to_from_char, char);
5527+
gen_align_to_harnesses!(align_to_from_unit, ());
5528+
5529+
//generates proof_of_contract harness for align_to_mut given the T (src) and U (dst) types
5530+
macro_rules! proof_of_contract_for_align_to_mut {
5531+
($harness:ident, $src:ty, $dst:ty) => {
5532+
#[kani::proof_for_contract(<[$src]>::align_to_mut)]
5533+
fn $harness() {
5534+
const ARR_SIZE: usize = 100;
5535+
let mut src_arr: [$src; ARR_SIZE] = kani::any();
5536+
let src_slice = kani::slice::any_slice_of_array_mut(&mut src_arr);
5537+
let dst_slice = unsafe { src_slice.align_to_mut::<$dst>() };
5538+
}
5539+
};
5540+
}
5541+
5542+
//generates harnesses between a given src type and all the main primitives
5543+
macro_rules! gen_align_to_mut_harnesses {
5544+
($mod_name:ident, $src_type:ty) => {
5545+
mod $mod_name {
5546+
use super::*;
5547+
5548+
proof_of_contract_for_align_to_mut!(align_to_mut_u8, $src_type, u8);
5549+
proof_of_contract_for_align_to_mut!(align_to_mut_u16, $src_type, u16);
5550+
proof_of_contract_for_align_to_mut!(align_to_mut_u32, $src_type, u32);
5551+
proof_of_contract_for_align_to_mut!(align_to_mut_u64, $src_type, u64);
5552+
proof_of_contract_for_align_to_mut!(align_to_mut_u128, $src_type, u128);
5553+
proof_of_contract_for_align_to_mut!(align_to_mut_bool, $src_type, bool);
5554+
proof_of_contract_for_align_to_mut!(align_to_mut_char, $src_type, char);
5555+
proof_of_contract_for_align_to_mut!(align_to_mut_unit, $src_type, ());
5556+
}
5557+
};
5558+
}
5559+
5560+
gen_align_to_mut_harnesses!(align_to_mut_from_u8, u8);
5561+
gen_align_to_mut_harnesses!(align_to_mut_from_u16, u16);
5562+
gen_align_to_mut_harnesses!(align_to_mut_from_u32, u32);
5563+
gen_align_to_mut_harnesses!(align_to_mut_from_u64, u64);
5564+
gen_align_to_mut_harnesses!(align_to_mut_from_u128, u128);
5565+
gen_align_to_mut_harnesses!(align_to_mut_from_bool, bool);
5566+
gen_align_to_mut_harnesses!(align_to_mut_from_char, char);
5567+
gen_align_to_mut_harnesses!(align_to_mut_from_unit, ());
5568+
}

0 commit comments

Comments
 (0)