Skip to content

Commit ab94cc1

Browse files
AlexLB99AlexLB99
committed
fixed formatting
1 parent 8afe8f6 commit ab94cc1

File tree

1 file changed

+54
-119
lines changed

1 file changed

+54
-119
lines changed

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

Lines changed: 54 additions & 119 deletions
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,19 @@
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};
1418
use crate::panic::const_panic;
1519
use crate::simd::{self, Simd};
1620
use crate::ub_checks::assert_unsafe_precondition;
17-
use crate::{fmt, hint, ptr, range, slice, ub_checks};
18-
19-
use safety::{ensures, requires};
20-
#[cfg(kani)]
21-
use crate::kani;
21+
use crate::{fmt, hint, ptr, range, slice};
2222

2323
#[unstable(
2424
feature = "slice_internals",
@@ -5346,46 +5346,14 @@ mod verify {
53465346
mod $mod_name {
53475347
use super::*;
53485348

5349-
proof_of_contract_for_align_to!(
5350-
align_to_u8,
5351-
$src_type,
5352-
u8
5353-
);
5354-
proof_of_contract_for_align_to!(
5355-
align_to_u16,
5356-
$src_type,
5357-
u16
5358-
);
5359-
proof_of_contract_for_align_to!(
5360-
align_to_u32,
5361-
$src_type,
5362-
u32
5363-
);
5364-
proof_of_contract_for_align_to!(
5365-
align_to_u64,
5366-
$src_type,
5367-
u64
5368-
);
5369-
proof_of_contract_for_align_to!(
5370-
align_to_u128,
5371-
$src_type,
5372-
u128
5373-
);
5374-
proof_of_contract_for_align_to!(
5375-
align_to_bool,
5376-
$src_type,
5377-
bool
5378-
);
5379-
proof_of_contract_for_align_to!(
5380-
align_to_char,
5381-
$src_type,
5382-
char
5383-
);
5384-
proof_of_contract_for_align_to!(
5385-
align_to_unit,
5386-
$src_type,
5387-
()
5388-
);
5349+
proof_of_contract_for_align_to!(align_to_u8, $src_type, u8);
5350+
proof_of_contract_for_align_to!(align_to_u16, $src_type, u16);
5351+
proof_of_contract_for_align_to!(align_to_u32, $src_type, u32);
5352+
proof_of_contract_for_align_to!(align_to_u64, $src_type, u64);
5353+
proof_of_contract_for_align_to!(align_to_u128, $src_type, u128);
5354+
proof_of_contract_for_align_to!(align_to_bool, $src_type, bool);
5355+
proof_of_contract_for_align_to!(align_to_char, $src_type, char);
5356+
proof_of_contract_for_align_to!(align_to_unit, $src_type, ());
53895357
}
53905358
};
53915359
}
@@ -5405,40 +5373,39 @@ mod verify {
54055373

54065374
//We write this as an impl so that we can refer to "self"
54075375
impl<T> wrap_align_to_mut<T> for [T] {
5408-
//We need the following wrapper because it is not currently possible to write
5409-
//contracts for functions that return mut refs to input arguments
5410-
//see https://github.com/model-checking/kani/issues/3764
5411-
//----------------------------
5412-
//Checks if the part that will be transmuted from type T to U is valid for type U
5413-
//reuses most function logic up to use of from_raw_parts,
5414-
//where the potentially unsafe transmute occurs
5415-
#[requires(
5416-
U::IS_ZST || T::IS_ZST || {
5417-
let ptr = self.as_ptr();
5418-
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
5419-
offset > self.len() || {
5420-
let (_, rest) = self.split_at(offset);
5421-
let (us_len, _) = rest.align_to_offsets::<U>();
5422-
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len
5423-
);
5424-
ub_checks::can_dereference(middle)
5425-
}
5426-
}
5427-
)]
5428-
//The following two ensures clauses guarantee that middle is of maximum size within self
5429-
#[ensures(|(prefix, _, _): &(*const [T], *const [U], *const [T])| prefix.len() * size_of::<T>() < align_of::<U>())]
5430-
#[ensures(|(_, _, suffix): &(*const [T], *const [U], *const [T])| suffix.len() * size_of::<T>() < size_of::<U>())]
5431-
//Either align_to just returns self in the prefix, or the 3 returned slices
5432-
//should be sequential, contiguous, and have same total length as self
5433-
#[ensures(|(prefix, middle, suffix): &(*const [T], *const [U], *const [T])|
5434-
prefix.as_ptr() == self.as_ptr() &&
5435-
(prefix.len() == self.len() || (
5436-
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
5437-
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
5438-
((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) )
5439-
)
5440-
)]
5441-
unsafe fn align_to_mut_wrapper<U>(&mut self) -> (*const [T], *const [U], *const [T]) {
5376+
//We need the following wrapper because it is not currently possible to write
5377+
//contracts for functions that return mut refs to input arguments
5378+
//see https://github.com/model-checking/kani/issues/3764
5379+
//----------------------------
5380+
//Checks if the part that will be transmuted from type T to U is valid for type U
5381+
//reuses most function logic up to use of from_raw_parts,
5382+
//where the potentially unsafe transmute occurs
5383+
#[requires(
5384+
U::IS_ZST || T::IS_ZST || {
5385+
let ptr = self.as_ptr();
5386+
let offset = crate::ptr::align_offset(ptr, align_of::<U>());
5387+
offset > self.len() || {
5388+
let (_, rest) = self.split_at(offset);
5389+
let (us_len, _) = rest.align_to_offsets::<U>();
5390+
let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len);
5391+
ub_checks::can_dereference(middle)
5392+
}
5393+
}
5394+
)]
5395+
//The following two ensures clauses guarantee that middle is of maximum size within self
5396+
#[ensures(|(prefix, _, _): &(*const [T], *const [U], *const [T])| prefix.len() * size_of::<T>() < align_of::<U>())]
5397+
#[ensures(|(_, _, suffix): &(*const [T], *const [U], *const [T])| suffix.len() * size_of::<T>() < size_of::<U>())]
5398+
//Either align_to just returns self in the prefix, or the 3 returned slices
5399+
//should be sequential, contiguous, and have same total length as self
5400+
#[ensures(|(prefix, middle, suffix): &(*const [T], *const [U], *const [T])|
5401+
prefix.as_ptr() == self.as_ptr() &&
5402+
(prefix.len() == self.len() || (
5403+
((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
5404+
((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
5405+
((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) )
5406+
)
5407+
)]
5408+
unsafe fn align_to_mut_wrapper<U>(&mut self) -> (*const [T], *const [U], *const [T]) {
54425409
let (prefix_mut, mid_mut, suffix_mut) = self.align_to_mut::<U>();
54435410
(prefix_mut as *const [T], mid_mut as *const [U], suffix_mut as *const [T])
54445411
}
@@ -5461,46 +5428,14 @@ mod verify {
54615428
mod $mod_name {
54625429
use super::*;
54635430

5464-
proof_of_contract_for_align_to_mut!(
5465-
align_to_mut_u8,
5466-
$src_type,
5467-
u8
5468-
);
5469-
proof_of_contract_for_align_to_mut!(
5470-
align_to_mut_u16,
5471-
$src_type,
5472-
u16
5473-
);
5474-
proof_of_contract_for_align_to_mut!(
5475-
align_to_mut_u32,
5476-
$src_type,
5477-
u32
5478-
);
5479-
proof_of_contract_for_align_to_mut!(
5480-
align_to_mut_u64,
5481-
$src_type,
5482-
u64
5483-
);
5484-
proof_of_contract_for_align_to_mut!(
5485-
align_to_mut_u128,
5486-
$src_type,
5487-
u128
5488-
);
5489-
proof_of_contract_for_align_to_mut!(
5490-
align_to_mut_bool,
5491-
$src_type,
5492-
bool
5493-
);
5494-
proof_of_contract_for_align_to_mut!(
5495-
align_to_mut_char,
5496-
$src_type,
5497-
char
5498-
);
5499-
proof_of_contract_for_align_to_mut!(
5500-
align_to_mut_unit,
5501-
$src_type,
5502-
()
5503-
);
5431+
proof_of_contract_for_align_to_mut!(align_to_mut_u8, $src_type, u8);
5432+
proof_of_contract_for_align_to_mut!(align_to_mut_u16, $src_type, u16);
5433+
proof_of_contract_for_align_to_mut!(align_to_mut_u32, $src_type, u32);
5434+
proof_of_contract_for_align_to_mut!(align_to_mut_u64, $src_type, u64);
5435+
proof_of_contract_for_align_to_mut!(align_to_mut_u128, $src_type, u128);
5436+
proof_of_contract_for_align_to_mut!(align_to_mut_bool, $src_type, bool);
5437+
proof_of_contract_for_align_to_mut!(align_to_mut_char, $src_type, char);
5438+
proof_of_contract_for_align_to_mut!(align_to_mut_unit, $src_type, ());
55045439
}
55055440
};
55065441
}

0 commit comments

Comments
 (0)