Generate arbitrary `Vec` with symbolic length

[zhuyutian57]

I write a simple proof for Vec::append as follows. But it fails to check the post-condition.

use std::alloc::*;

#[kani::proof]
fn main() {
    // Create a valid `Vec`
    let cap = kani::any::<usize>();
    kani::assume(cap <= isize::MAX as usize);
    let mut _vec_1 = Vec::with_capacity(cap);
    let length_1 = kani::any::<usize>();
    kani::assume(length_1 <= cap);
    unsafe {
        _vec_1.set_len(length_1);
    }

    // Initialize `_vec_1[i]` with 
    let i = kani::any::<usize>();
    let value_i = kani::any::<bool>();
    kani::assume(length_1 > 1 && i < length_1);
    _vec_1[i] = value_i;

    // `_vec_2` is a `Vec` with only one non-deterministic value.
    let n = 1;
    let value_j = kani::any::<bool>();
    let mut _vec_2 = vec![value_j; n];

    // Assume that the growth do not overflow.
    kani::assume(cap <= isize::MAX as usize / 2);
    kani::assume(length_1 + n <= isize::MAX as usize);
    // Append
    _vec_1.append(&mut _vec_2);
    
    assert!(_vec_1.len() == length_1 + n);
    assert!(_vec_2.is_empty());
    // Failed Checks: assertion failed: _vec_1[i] == value_i
    //  File: "<builtin-library-memcpy>", line 46, in memcpy
    assert!(_vec_1[i] == value_i);
    // Unreachable.
    assert!(_vec_1[length_1] == value_j);
}

The results are:

...
SUMMARY:
 ** 1 of 89 failed (5 unreachable)
Failed Checks: assertion failed: _vec_1[i] == value_i
 File: "<builtin-library-memcpy>", line 46, in memcpy

VERIFICATION:- FAILED
Verification Time: 6.751468s

Manual Harness Summary:
Verification failed for - main
Complete - 0 successfully verified harnesses, 1 failure, 1 total.

Is there a bug in Kani or CBMC? Or, something is wrong in the above code.

[zhassan-aws]

Hi @zhuyutian57. Thanks for filing this issue. The above program has undefined behavior in the _vec_1.set_len(length_1) line; the safety conditions for set_len state that the elements at old_len..new_len must be initialized which is not the case here. So, this could be the cause for the failure we're seeing.

[zhuyutian57]

Thanks. The failure occurs in the function contract of std::ptr::slice_from_raw_parts when we index Vec.

[zhuyutian57]

Is there any API to assume a memory region with non-deterministic size is initialized?

[zhassan-aws]

Can you explain what you're trying to do? Would kani::vec::any_vec help?

kani/library/kani/src/vec.rs

Line 6 in 12ef829

pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>

[zhuyutian57]

The above API required a constant MAX_LENGTH. Can we do that with a valid symbolic MAX_LENGTH.

I try to allocate a memory region and initialize the allocated memory with kani::any.

For example, we can initialize the memory region with a loop.

let size = kani::any();
let align = align_of::<i32>();
kani::assume(size % align == 0 && size <= isize::MAX as usize);
let layout = unsafe { Layout::from_size_align_unchecked(size, align) };
let ptr = unsafe { alloce(layout) as *mut i32 };
// Initialization
for i in 0..(size / align) {
    unsafe ( *ptr.add(i) = kani::any(); )
}

Can the initialization loop be replaced by some assumption? For example,

// kani::mem::is_initialized is a private predicate
kani::assume(kani::mem::is_initialized(ptr, size / align))

[zhassan-aws]

The above API required a constant MAX_LENGTH. Can we do that with a valid symbolic MAX_LENGTH.

With any_vec, the actual length of the Vec is symbolic (anywhere in the range 0 to MAX_LENGTH).

I try to allocate a memory region and initialize the allocated memory with kani::any.

For example, we can initialize the memory region with a loop.

You can do that through creating an array and then turning it into a Vec, e.g.:

    const N: usize = 100;
    let arr: [bool; N] = kani::any();
    let len = kani::any_where(|x| *x <= N);
    let v: Vec<bool> = arr[..len].into();
    assert!(v.len() <= N);

Can the initialization loop be replaced by some assumption? For example,

Unfortunately, this is not possible.