Pointer Generator for different pointee types

[stogaru]

@feliperodri I’ve been experimenting with the new PointerGenerator API and have a couple of examples I’d like to discuss.

I have a proof using a specific type, (f64, bool), like this:

#[kani::proof_for_contract(<*mut (f64, bool)>::offset)]
pub fn check_tuple_normal() {
    let mut test_val: (f64, bool) = kani::any::<(f64, bool)>();
    let test_ptr: *mut (f64, bool) = &mut test_val;
    let count: isize = kani::any();
    unsafe {
        test_ptr.offset(count);
    }
}

And using the pointer generator for the same type:

#[kani::proof_for_contract(<*mut (f64, bool)>::offset)]
pub fn check_tuple_pg() {
    let mut generator = PointerGenerator::<16>::new();
    let ArbitraryPointer { ptr: ptr1, .. } = generator.any_in_bounds::<(f64, bool)>();
    let count: isize = kani::any();
    unsafe {
        ptr1.offset(count);
    }
}

Is there any significant difference between using a specific type in the proof (like in check_tuple_normal) versus using the pointer generator (as in check_tuple_pg)? Additionally, do you have a preference for one approach over the other in your proofs?

[celinval]

The main advantage of the pointer generator is that it will cover more scenarios, such as unaligned and uninitialized pointers, which is preferred.