offset safety check is overly restrictive for ZSTs

[carolynzech]

I tried this code:

#[kani::proof]
fn main() {
    let mut x = ();
    let ptr: *mut () = &mut x as *mut ();
    let count: usize = (isize::MAX as usize) + 1;
    let res = unsafe { ptr.add(count) };
}

using the following command line invocation:

cargo kani

with Kani version: 0.59

I expected to see this happen: verification succeeds because for ZSTs, the offset can overflow isize.

Instead, this happened: Kani failed with this safety check:

kani/library/kani_core/src/models.rs

Line 165 in 006e5da

kani::safety_check(false, "Offset value overflows isize");

[carolynzech]

Note that in Miri, this snippet runs without errors. If I change the pointee type to a non-ZST, I get:

error: Undefined Behavior: overflowing pointer arithmetic: the total offset in bytes does not fit in an `isize`
 --> src/main.rs:5:24
  |
5 |     let res = unsafe { ptr.add(count) };
  |                        ^^^^^^^^^^^^^^ overflowing pointer arithmetic: the total offset in bytes does not fit in an `isize`
  |
  = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
  = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
  = note: BACKTRACE:
  = note: inside `main` at src/main.rs:5:24: 5:38

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace