Skip to content

Commit

Permalink
WIP(will be squashed)
Browse files Browse the repository at this point in the history
  • Loading branch information
@ShoyuVanilla
ShoyuVanilla committed Dec 29, 2024
1 parent cee4294 commit 483ba1a
Showing 1 changed file with 143 additions and 16 deletions.
159 changes: 143 additions & 16 deletions library/core/src/slice/sort/shared/smallsort.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ impl<T: FreezeMarker> StableSmallSortTypeImpl for T {
// - kani contract attribute macros doesnt't work with `default fn`
// - we cannot specify the trait member function with `proof_for_contract`
#[cfg(kani)]
#[kani::modifies(v)]
#[kani::modifies(v, scratch)]
#[ensures(|_| {
let mut is_less = is_less.clone();
v.is_sorted_by(|a, b| !is_less(b, a))
Expand Down Expand Up @@ -605,7 +605,7 @@ where
///
/// # Safety
/// begin < tail and p must be valid and initialized for all begin <= p <= tail.
#[cfg_attr(kani, kani::modifies(begin, tail))]
#[cfg_attr(kani, kani::modifies(begin, tail))] // FIXME: This should contain all ptrs [begin, tail]
#[requires(begin.addr() < tail.addr() && {
let len = tail.addr() - begin.addr();
let is_less: &mut F = unsafe { mem::transmute(&is_less) };
Expand Down Expand Up @@ -638,13 +638,15 @@ unsafe fn insert_tail<T, F: FnMut(&T, &T) -> bool>(begin: *mut T, tail: *mut T,
let tmp = ManuallyDrop::new(tail.read());
let mut gap_guard = CopyOnDrop { src: &*tmp, dst: tail, len: 1 };

#[safety::loop_invariant(
sift.addr() >= begin.addr() && sift.addr() < tail.addr()
)]
// FIXME: This was `loop` but kani's loop contract doesn't support `loop`.
// Once it is supported, replace `while true` with the original `loop`
#[allow(while_true)]
while true {
loop {
// FIXME: This should be loop contract but sadly, making this into
// loop invariant takes too much time in verification and causes OOM
#[cfg(kani)]
kani::assert(
sift.addr() >= begin.addr() && sift.addr() < tail.addr(),
"loop invariants",
);

// SAFETY: we move sift into the gap (which is valid), and point the
// gap guard destination at sift, ensuring that if a panic occurs the
// gap is once again filled.
Expand All @@ -665,7 +667,8 @@ unsafe fn insert_tail<T, F: FnMut(&T, &T) -> bool>(begin: *mut T, tail: *mut T,
}

/// Sort `v` assuming `v[..offset]` is already sorted.
#[cfg_attr(kani, kani::modifies(v))]
// FIXME: Disabled this due to [model-checking/kani#3682]
// #[cfg_attr(kani, kani::modifies(v))]
#[requires(offset != 0 && offset <= v.len() && {
let is_less: &mut F = unsafe { mem::transmute(&is_less) };
v[..offset].is_sorted_by(|a, b| !is_less(b, a))
Expand Down Expand Up @@ -695,7 +698,7 @@ pub fn insertion_sort_shift_left<T, F: FnMut(&T, &T) -> bool>(
let mut tail = v_base.add(offset);
while tail != v_end {
// FIXME: This should be loop contract but sadly, making this into
// loop invariant causes OOM
// loop invariant takes too much time in verification and causes OOM
#[cfg(kani)]
kani::assert(
tail.addr() > v_base.addr() && tail.addr() <= v_end.addr(),
Expand Down Expand Up @@ -1034,17 +1037,26 @@ mod verify {
);
}

// FIXME: Ideally, this should be `proof_for_contract(insertion_sort_shift_left)`,
// but there is no way to set `kani::modifies` for arbitrary number of pointers
// in [begin, tail]
#[kani::proof_for_contract(insert_tail)]
#[kani::unwind(17)]
pub fn check_insert_tail() {
let mut array: [u8; INSERTION_SORT_MAX_LEN] = kani::any();
let tail = kani::any_where(|x: &usize| *x < INSERTION_SORT_MAX_LEN);
let mut is_less = |x: &u8, y: &u8| x < y;
let tail = kani::any_where(|x: &usize| *x > 0 && *x < INSERTION_SORT_MAX_LEN);
let mut array = kani::any_where(|x: &[u8; INSERTION_SORT_MAX_LEN]| {
x[..tail].is_sorted_by(|a, b| !is_less(b, a))
});
unsafe {
let begin = array.as_mut_ptr();
let tail = begin.add(tail);
insert_tail(begin, tail, &mut is_less);
}
kani::assert(
array[..=tail].is_sorted_by(|a, b| !is_less(b, a)),
"slice is not sorted",
);
}

// FIXME: Ideally, this should be `proof_for_contract(insertion_sort_shift_left)`,
Expand Down Expand Up @@ -1120,13 +1132,128 @@ mod verify {
}

#[kani::proof_for_contract(_stable_small_sort_type_impl_small_sort)]
#[kani::stub_verified(insertion_sort_shift_left)]
#[kani::stub_verified(insert_tail)]
#[kani::unwind(16)]
pub fn check_stable_small_sort_type_impl_small_sort() {
let mut array: [u8; SMALL_SORT_FALLBACK_THRESHOLD] = kani::any();
let len = kani::any_where(|x: &usize| *x <= SMALL_SORT_FALLBACK_THRESHOLD);
assert_eq!(
<u8 as StableSmallSortTypeImpl>::small_sort_threshold(),
SMALL_SORT_GENERAL_THRESHOLD,
);

let mut array: [u8; SMALL_SORT_GENERAL_THRESHOLD] = kani::any();
let len = kani::any_where(|x: &usize| *x <= SMALL_SORT_GENERAL_THRESHOLD);
let mut scratch: [MaybeUninit<u8>; SMALL_SORT_GENERAL_SCRATCH_LEN]
= [const { MaybeUninit::uninit() }; SMALL_SORT_GENERAL_SCRATCH_LEN];
let mut is_less = |x: &u8, y: &u8| x < y;
_stable_small_sort_type_impl_small_sort(&mut array[..len], &mut scratch, &mut is_less);
}

struct NonFreeze(u8);

impl !crate::marker::Freeze for NonFreeze {}

impl kani::Arbitrary for NonFreeze {
fn any() -> NonFreeze {
NonFreeze(kani::any())
}
}

#[kani::proof_for_contract(_stable_small_sort_type_impl_small_sort)]
#[kani::stub_verified(insertion_sort_shift_left)]
#[kani::unwind(16)]
pub fn check_stable_small_sort_type_impl_small_sort_nonfreeze() {
assert_eq!(
<NonFreeze as StableSmallSortTypeImpl>::small_sort_threshold(),
SMALL_SORT_FALLBACK_THRESHOLD,
);

let mut array: [NonFreeze; SMALL_SORT_FALLBACK_THRESHOLD] = kani::any();
let len = kani::any_where(|x: &usize| *x <= SMALL_SORT_FALLBACK_THRESHOLD);
let mut scratch: [MaybeUninit<NonFreeze>; SMALL_SORT_GENERAL_SCRATCH_LEN]
= [const { MaybeUninit::uninit() }; SMALL_SORT_GENERAL_SCRATCH_LEN];
let mut is_less = |x: &NonFreeze, y: &NonFreeze| x.0 < y.0;
_stable_small_sort_type_impl_small_sort(&mut array[..len], &mut scratch, &mut is_less);
}

// Freeze version is same with `_unstable_small_sort_freeze_type_impl_small_sort`
#[kani::proof_for_contract(_unstable_small_sort_type_impl_small_sort)]
#[kani::stub_verified(insertion_sort_shift_left)]
#[kani::unwind(16)]
pub fn check_unstable_small_sort_type_impl_small_sort_nonfreeze() {
assert_eq!(
<NonFreeze as UnstableSmallSortTypeImpl>::small_sort_threshold(),
SMALL_SORT_FALLBACK_THRESHOLD,
);

let mut array: [NonFreeze; SMALL_SORT_FALLBACK_THRESHOLD] = kani::any();
let len = kani::any_where(|x: &usize| *x <= SMALL_SORT_FALLBACK_THRESHOLD);
let mut is_less = |x: &NonFreeze, y: &NonFreeze| x.0 < y.0;
_unstable_small_sort_type_impl_small_sort(&mut array[..len], &mut is_less);
}

// This calls `small_sort_network` internally
#[kani::proof_for_contract(_unstable_small_sort_freeze_type_impl_small_sort)]
#[kani::stub_verified(insertion_sort_shift_left)]
#[kani::unwind(17)]
pub fn check_unstable_small_sort_freeze_type_impl_small_sort_network() {
assert_eq!(
<u8 as UnstableSmallSortFreezeTypeImpl>::small_sort_threshold(),
SMALL_SORT_NETWORK_THRESHOLD,
);

let mut array: [u8; SMALL_SORT_NETWORK_THRESHOLD] = kani::any();
let len = kani::any_where(|x: &usize| *x <= SMALL_SORT_NETWORK_THRESHOLD);
let mut is_less = |x: &u8, y: &u8| x < y;
_unstable_small_sort_freeze_type_impl_small_sort(&mut array[..len], &mut is_less);
}

// This calls `small_sort_general` internally
#[kani::proof_for_contract(_unstable_small_sort_freeze_type_impl_small_sort)]
#[kani::stub_verified(insert_tail)]
#[kani::unwind(16)]
pub fn check_unstable_small_sort_freeze_type_impl_small_sort_general() {
#[derive(Clone, Copy)]
struct Bigger(u8, MaybeUninit<[u8; 8]>);

impl kani::Arbitrary for Bigger {
fn any() -> Bigger {
Bigger(kani::any(), MaybeUninit::uninit())
}
}

assert_eq!(
<Bigger as UnstableSmallSortFreezeTypeImpl>::small_sort_threshold(),
SMALL_SORT_GENERAL_THRESHOLD,
);

let mut array: [Bigger; SMALL_SORT_GENERAL_THRESHOLD] = kani::any();
let len = kani::any_where(|x: &usize| *x <= SMALL_SORT_GENERAL_THRESHOLD);
let mut is_less = |x: &Bigger, y: &Bigger| x.0 < y.0;
_unstable_small_sort_freeze_type_impl_small_sort(&mut array[..len], &mut is_less);
}

// This calls `small_sort_fallback` internally
#[kani::proof_for_contract(_unstable_small_sort_freeze_type_impl_small_sort)]
#[kani::stub_verified(insertion_sort_shift_left)]
#[kani::unwind(16)]
pub fn check_unstable_small_sort_freeze_type_impl_small_sort_fallback() {
#[derive(Clone, Copy)]
struct Biggest(u8, MaybeUninit<[u8; 86]>);

impl kani::Arbitrary for Biggest {
fn any() -> Biggest {
Biggest(kani::any(), MaybeUninit::uninit())
}
}

assert_eq!(
<Biggest as UnstableSmallSortFreezeTypeImpl>::small_sort_threshold(),
SMALL_SORT_FALLBACK_THRESHOLD,
);

let mut array: [Biggest; SMALL_SORT_FALLBACK_THRESHOLD] = kani::any();
let len = kani::any_where(|x: &usize| *x <= SMALL_SORT_FALLBACK_THRESHOLD);
let mut is_less = |x: &Biggest, y: &Biggest| x.0 < y.0;
_unstable_small_sort_freeze_type_impl_small_sort(&mut array[..len], &mut is_less);
}
}

0 comments on commit 483ba1a

Please sign in to comment.