diff --git a/library/core/src/slice/sort/shared/smallsort.rs b/library/core/src/slice/sort/shared/smallsort.rs index fd7011c757e1a..357eb412e0de9 100644 --- a/library/core/src/slice/sort/shared/smallsort.rs +++ b/library/core/src/slice/sort/shared/smallsort.rs @@ -73,7 +73,7 @@ impl 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)) @@ -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) }; @@ -638,13 +638,15 @@ unsafe fn insert_tail 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. @@ -665,7 +667,8 @@ unsafe fn insert_tail 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)) @@ -695,7 +698,7 @@ pub fn insertion_sort_shift_left 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(), @@ -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)`, @@ -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!( + ::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; 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!( + ::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; 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!( + ::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!( + ::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!( + ::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!( + ::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); + } }