Improve performance and language support of memory initialization checks

[artemagvanian]

This is a follow-up PR for #3264, a part of the larger work towards #3300.

This PR introduces:

• Use of demonic non-determinism (prophecy variables) to improve memory initialization checks performance;
  • Instead of keeping track of memory initialization of each possibly uninitialized byte pointed to by some pointer, one is chosen non-deterministically;
• Tests for proper memory initialization checks injection for compiler intrinsics;
• Separate functions for checking memory initialization of slice chunks.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[artemagvanian]

Seems like Release Bundle / BuildBundle-Linux (pull_request) is failing because of actions/checkout#1809

[celinval]

I think it would be much simpler if you

[zhassan-aws]

Nice!

What happens if there are two accesses to distinct uninitialized memory in a row? Will the first violation block the reporting of the second?

[artemagvanian]

What happens if there are two accesses to distinct uninitialized memory in a row? Will the first violation block the reporting of the second?

Good question: I tested this simple case and all of the violations were reported.

use std::ptr::addr_of;

#[repr(C)]
struct S(u32, u8);

/// Checks that Kani catches an attempt to access padding of a struct using raw pointers.
#[kani::proof]
fn check_uninit_padding() {
    let s = S(0, 0);
    let ptr: *const u8 = addr_of!(s) as *const u8;
    let padding = unsafe { *(ptr.add(5)) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
    let padding_next = unsafe { *(ptr.add(6)) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
    inner_fn(ptr);
}

fn inner_fn(ptr: *const u8) {
    let padding_inner = unsafe { *(ptr.add(7)) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB.
}

[zhassan-aws]

Good question: I tested this simple case and all of the violations were reported.

Cool, thanks for checking.

[zhassan-aws]

Thanks!