Struct PointerGenerator

pub struct PointerGenerator<const BYTES: usize> { /* private fields */ }

Pointer generator that can be used to generate arbitrary pointers.

This generator allows users to build pointers with different safety properties. This is different than creating a pointer that can have any address, since it will never point to a previously allocated object. See this section for more details.

The generator contains an internal buffer of a constant generic size, BYTES, that it uses to generate InBounds and OutOfBounds pointers. In those cases, the generated pointers will have the same provenance as the generator, and the same lifetime. The address of an InBounds pointer will represent all possible addresses in the range of the generator’s buffer address.

For other allocation statuses, the generator will create a pointer that satisfies the given condition. The pointer address will not represent all possible addresses that satisfies the given allocation status.

For example:

    let mut generator = PointerGenerator::<10>::new();
    let arbitrary = generator.any_alloc_status::<char>();
    kani::assume(arbitrary.status == AllocationStatus::InBounds);
    // Pointer may be unaligned, but it should be in-bounds, so it is safe to write to
    unsafe { arbitrary.ptr.write_unaligned(kani::any()) }

The generator is parameterized by the number of bytes of its internal buffer. See pointer_generator function if you would like to create a generator that fits a minimum number of objects of a given type. Example:

    // These generators have the same capacity of 6 bytes.
    let generator1 = PointerGenerator::<6>::new();
    let generator2 = pointer_generator::<i16, 3>();

Buffer size

The internal buffer is used to generate pointers, and its size determines the maximum number of pointers it can generate without overlapping. Larger values will impact the maximum distance between generated pointers.

We recommend that you pick a size that is at least big enough to cover the cases where all pointers produced are non-overlapping. The buffer size in bytes must be big enough to fit distinct objects for each call of generate pointer. For example, generating two *mut u8 and one *mut u32 requires a buffer of at least 6 bytes.

This guarantees that your harness covers cases where all generated pointers point to allocated positions that do not overlap. For example:

    let mut generator = PointerGenerator::<6>::new();
    let ptr1: *mut u8 = generator.any_in_bounds().ptr;
    let ptr2: *mut u8 = generator.any_in_bounds().ptr;
    let ptr3: *mut u32 = generator.any_in_bounds().ptr;
    // This cover is satisfied.
    cover!((ptr1 as usize) >= (ptr2 as usize) + size_of::<u8>()
           && (ptr2 as usize) >= (ptr3 as usize) + size_of::<u32>());
    // As well as having overlapping pointers.
    cover!((ptr1 as usize) == (ptr3 as usize));

The first cover will be satisfied, since there exists at least one path where the generator produces inbounds pointers that do not overlap. Such as this scenario:

+--------+--------+--------+--------+--------+--------+
| Byte 0 | Byte 1 | Byte 2 | Byte 3 | Byte 4 | Byte 5 |
+--------+--------+--------+--------+--------+--------+
<--------------- ptr3 --------------><--ptr2-><--ptr1->

I.e., the generator buffer is large enough to fit all 3 objects without overlapping.

In contrast, if we had used a size of 1 element, all calls to any_in_bounds() would return elements that overlap, and the first cover would no longer be satisfied.

Note that the generator requires a minimum number of 1 byte, otherwise the InBounds case would never be covered. Compilation will fail if you try to create a generator of size 0.

Additionally, the verification will fail if you try to generate a pointer for a type with size greater than the buffer size.

Use larger buffer size if you want to cover scenarios where the distance between the generated pointers matters.

The only caveats of using very large numbers are:

1. The value cannot exceed the solver maximum object size (currently 2^48 by default), neither Rust’s maximum object size (isize::MAX).
2. Larger sizes could impact performance as they can lead to an exponential increase in the number of possibilities of pointer placement within the buffer.

Pointer provenance

The pointer returned in the InBounds and OutOfBounds case will have the same provenance as the generator.

Use the same generator if you want to handle cases where 2 or more pointers may overlap. E.g.:

    let mut generator = pointer_generator::<char, 5>();
    let ptr1 = generator.any_in_bounds::<char>().ptr;
    let ptr2 = generator.any_in_bounds::<char>().ptr;
    // This cover is satisfied.
    cover!(ptr1 == ptr2)

If you want to cover cases where two or more pointers may not have the same provenance, you will need to instantiate multiple generators. You can also apply non-determinism to cover cases where the pointers may or may not have the same provenance. E.g.:

    let mut generator1 = pointer_generator::<char, 5>();
    let mut generator2 = pointer_generator::<char, 5>();
    let ptr1: *const char = generator1.any_in_bounds().ptr;
    let ptr2: *const char = if kani::any() {
        // Pointers will have same provenance and may overlap.
        generator1.any_in_bounds().ptr
    } else {
        // Pointers will have different provenance and will not overlap.
        generator2.any_in_bounds().ptr
    };
    // Invoke the function under verification
    unsafe { my_target(ptr1, ptr2) };

Pointer Generator vs Pointer with any address

Creating a pointer using the generator is different than generating a pointer with any address.

I.e.:

    // This pointer represents any address, and it may point to anything in memory,
    // allocated or not.
    let ptr1 = kani::any::<usize>() as *const u8;

    // This pointer address will either point to unallocated memory, to a dead object
    // or to allocated memory within the generator address space.
    let mut generator = PointerGenerator::<5>::new();
    let ptr2: *const u8 = generator.any_alloc_status().ptr;

Kani cannot reason about a pointer allocation status (except for asserting its validity). Thus, the generator was introduced to help writing harnesses that need to impose constraints to the arbitrary pointer allocation status. It also allow us to restrict the pointer provenance, excluding for example the address of variables that are not available in the current context. As a limitation, it will not cover the entire address space that a pointer can take.

If your harness does not need to reason about pointer allocation, for example, verifying pointer wrapping arithmetic, using a pointer with any address will allow you to cover all possible scenarios.

Implementations

impl<const BYTES: usize> PointerGenerator<BYTES>

pub fn new() -> Self

Create a new PointerGenerator.

pub fn any_alloc_status<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T>

where T: Arbitrary,

Creates a raw pointer with non-deterministic properties.

The pointer returned is either dangling or has the same provenance of the generator.

pub fn any_in_bounds<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T>

where T: Arbitrary,

Creates a in-bounds raw pointer with non-deterministic properties.

The pointer points to an allocated location with the same provenance of the generator. The pointer may be unaligned, and the pointee may be uninitialized.

    let mut generator = PointerGenerator::<6>::new();
    let ptr1: *mut u8 = generator.any_in_bounds().ptr;
    let ptr2: *mut u8 = generator.any_in_bounds().ptr;
    // SAFETY: Both pointers have the same provenance.
    let distance = unsafe { ptr1.offset_from(ptr2) };
    assert!(distance > -5 && distance < 5)

Trait Implementations

impl<const BYTES: usize> Debug for PointerGenerator<BYTES>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.