Slice comparison/loop unwinding causing extensive kani runtime

[QinyuanWu]

I found that when I try to compare slice values after calling NonNull::slice_from_raw_parts, kani runtime increases drastically if

• array length is long(e.g. 10 vs 100000)
• creating a slice from an array with length of kani::any()

    // pub const fn slice_from_raw_parts(data: NonNull<T>, len: usize) -> Self
    #[kani::proof_for_contract(NonNull::slice_from_raw_parts)]
    pub fn non_null_check_slice_from_raw_parts() {
        const arr_len: usize = 10;
        // Create a non-deterministic array
        let mut arr: [i8; arr_len] = kani::any();
        // Get a raw NonNull pointer to the start of the slice
        let arr_raw_ptr = NonNull::new(arr.as_mut_ptr()).unwrap();  
        // Create NonNull slice from the start pointer and ends at random slice_len
        let slice_len: usize = kani::any(); // if set to 3 kani finishes in 1.3s
        kani::assume(slice_len <= arr_len);
        let nonnull_slice = NonNull::<[i8]>::slice_from_raw_parts(arr_raw_ptr, slice_len);
        // Ensure slice content is preserved, runtime at this step is proportional to arr_len
        unsafe {
            kani::assert( &arr[..slice_len] == nonnull_slice.as_ref(), "slice content must preserve" );
        }
    }

Contract:

    //TODO: The entire memory range of this slice must be contained within a single allocated object(same_allocation?)
    #[requires(data.pointer.is_aligned() 
        && len as isize * core::mem::size_of::<T>() as isize <= isize::MAX
        && (len as isize).checked_mul(core::mem::size_of::<T>() as isize).is_some()
        && (data.pointer as isize).checked_add(len as isize * core::mem::size_of::<T>() as isize).is_some())] // adding len * core::mem::size_of::<T>() to data must not “wrap around” the address space
    #[ensures(|result| !result.pointer.is_null())] //TODO: &data[..len] == result.as_ref() preserve content
    pub const fn slice_from_raw_parts(data: NonNull<T>, len: usize) -> Self {
        // SAFETY: `data` is a `NonNull` pointer which is necessarily non-null
        unsafe { Self::new_unchecked(super::slice_from_raw_parts_mut(data.as_ptr(), len)) }
    }

For example, when I set let slice_len: usize = kani::any();, kani keeps trying to do

aborting path on assume(false) at file /Users/owo/Desktop/verify-rust-std/library/core/src/option.rs line 606 column 5 function option::Option::<isize>::is_some thread 0
aborting path on assume(false) at file /Users/owo/Desktop/verify-rust-std/library/core/src/slice/index.rs line 64 column 5 function slice::index::slice_end_index_len_fail_rt thread 0
aborting path on assume(false) at file /Users/owo/Desktop/verify-rust-std/library/core/src/slice/index.rs line 57 column 5 function slice::index::slice_end_index_len_fail thread 0
aborting path on assume(false) at file /Users/owo/Desktop/verify-rust-std/library/core/src/slice/index.rs line 467 column 13 function <ops::range::Range<usize> as slice::index::SliceIndex<[i8]>>::index thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
...
Unwinding loop memcmp.0 iteration 21162 file <builtin-library-memcmp> line 25 function memcmp thread 0
...(has not terminated after 20+ minutes)

But if I set let slice_len: usize = 3;, the harness and contract is verified much quicker and the loop iteration stops at 3:

aborting path on assume(false) at file /Users/owo/Desktop/verify-rust-std/library/core/src/option.rs line 606 column 5 function option::Option::<isize>::is_some thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
...
SUMMARY:
 ** 0 of 247 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 1.3063408s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

I wonder why there is such a drastic difference, especially considering the original array length is only 10. Thank you! @zhassan-aws

[zhassan-aws]

Hi @QinyuanWu. When the array length is constrained via an assumption, i.e.

        let slice_len: usize = kani::any(); // if set to 3 kani finishes in 1.3s
        kani::assume(slice_len <= arr_len);

CBMC is unable to determine if the unwinding is sufficient during symbolic execution, hence it keeps unwinding. In this case, an unwind attribute must be specified, e.g.

    #[kani::proof_for_contract(NonNull::slice_from_raw_parts)]
    #[kani::unwind(11)]
    pub fn non_null_check_slice_from_raw_parts() {

Specifying an unwind value should resolve the issue.