Kani failed to detect unaligned access to N-ZST pointers

[giltho]

CBMC doesn't model pointer alignments, see #1168 .
This leads to unsoundness in the kani proofs - although keep in mind that these are really corner cases.

Rust expects pointers to N-aligned ZSTs to have an alignment of N.
Creating a misaligned reference, or dereferencing a misaligned pointer is undefined behaviour. That is also the case with pointers to ZSTs, even though dereferencing a pointer to a ZST is no-op.

For example, this code is invalid Rust, and triggers undefined behaviour:

use std::ptr::NonNull;

#[derive(Clone, Copy)]
#[repr(align(32))]
struct Zst32;

#[kani::proof]
pub fn main() {
    unsafe {
        let u: NonNull<Zst32> = NonNull::new_unchecked(8 as *mut Zst32);
        let v = *(u.as_ptr());
    }
}

You can try running it with MIRI in the playground, it is properly caught: the alignment check should fail. However, Kani does not catch it.

---

Similarly, Rust guarantees that creating references to ZSTs will yield properly-aligned pointers.
For example, the following code is a test that is guaranteed to always pass

#[repr(align(32))]
struct Zst32;

#[kani::proof]
pub fn main() {
    let u: Zst32 = Zst32;
    let v = &u;

    assert_eq!((v as *const Zst32 as usize) % 32, 0, "pointers to a 32-ZST should be 32 aligned")
}

But, this test should not pass:

#[repr(align(32))]
struct Zst32;

#[kani::proof]
pub fn main() {
    let u: Zst32 = Zst32;
    let v = &u;

    assert_eq!((v as *const Zst32 as usize) % 4096, 0, "pointers to a 32-ZST should be 4096 aligned - that is incorrect")
}

You can try running it in the playground, with miri or not; it is a bit non-deterministic, but there is a very strong chance that it fails.
In kani, it passes. I've tried a few things, and it seems that pointers will behave as if they were aligned on any power of 2 in CBMC.

[celinval]

@tautschnig did your change to ZST fixed this?

[tautschnig]

Yes, this was indeed fixed in #3134, as the following test (extension of the original example) confirms:

#[repr(align(32))]
struct Zst32;

#[kani::proof]
pub fn main() {
    let u: Zst32 = Zst32;
    let v = &u;

    assert_eq!((v as *const Zst32 as usize) % 32, 0, "pointers to a 32-ZST should be 32 aligned");
    assert_eq!((v as *const Zst32 as usize) % 64, 0, "pointers to a 32-ZST should be 64 aligned - that is incorrect");
    assert_eq!((v as *const Zst32 as usize) % 4096, 0, "pointers to a 32-ZST should be 4096 aligned - that is incorrect")
}

The first assertion passes, the second and the third one fail as they should.