Kani - Generate an array with a constraint on elements

[Yenyun035]

In the harness for from_bytes_until_nul from the CStr challenge, we are trying to construct a CStr from an u8 array. One check we have for from_bytes_until_nul is to provide an u8 array with only the last byte being a null byte. We want Kani to generate an input array where all bytes except the last are non-null bytes. We tried kani::any_where but we're not sure how to specify the constraint at the element level, or is it not possible to do that? Maybe there is a better way?

Our current approach:

#[kani::proof]
#[kani::unwind(32)]
fn check_from_bytes_until_nul_single_nul_byte_end() {
    const ARR_LEN: usize = 32;
    // ensure that the string does not have intermediate null bytes
    // TODO: there might be a better way
    let mut string: [u8; ARR_LEN] = kani::any_where(|x: &[u8; ARR_LEN]| !x[..ARR_LEN-1].contains(&0));
    // ensure that the string is properly null-terminated
    string[ARR_LEN - 1] = 0;

    let c_str = CStr::from_bytes_until_nul(&string).unwrap();
    assert!(c_str.is_safe());
}

Appreciate any guidance. @celinval @zhassan-aws

[zhassan-aws]

Hi @Yenyun035. Can you clarify the reason why you want to ensure none of the bytes except the last is null?

Wouldn't from_bytes_until_nul just stop at the first null and ignore everything after?

[Yenyun035]

We explicitly wrote three harnesses:

• Check 1: A random byte in a u8 array is guaranteed to be a null byte
• Check 2: Only the last byte of a u8 array is a null byte
• Check 3: The first byte of a u8 array is a null byte.

And this question refers to the second case. Or, is Check 2 self-contained in Check 1? In that case, this question won't matter. But if we have a harness that checks if panic happens when from_bytes_until_nul is invoked on an array that has no null bytes, we might want to generate such an array (e.g. with kani::any_where).

Reference: PR#180

[zhassan-aws]

And this question refers to the second case. Or, is Check 2 self-contained in Check 1?

Yes, it seems to me that harnesses 1 and 2 should be merged.

But if we have a harness that checks if panic happens when from_bytes_until_nul is invoked on an array that has no null bytes, we might want to generate such an array (e.g. with kani::any_where).

It might be more efficient to generate an array and assume the value is non-zero in a loop, e.g.:

    let mut string: [u8; ARR_LEN] = kani::any();
    for i in 0..ARR_LEN {
        kani::assume(string[i] != 0);
    }

[celinval]

@Yenyun035, I posted a comment in your PR. I would recommend that you don't add such restriction to the input. I would recommend that you merge the harnesses, and provide an input slice with arbitrary bytes. This should cover cases where there's only one 0 byte at the end, as well as cases with no 0 byte, or 0 bytes in other locations.

The from_bytes_until_nul is a safe function, and from its spec it should return a valid Result no matter what. Since we also want to check that any CStr that might've been returned is safe, you can check if the result is Ok(cstr), and, in that case, assert that the string is safe.

BTW, for generating the slice, you could use any_slice_of_array. I.e.:

let buffer : [u8; MAX_SIZE] = kani::any();
let slice = kani::slice::any_slice_of_array(&buffer);