Difference in size of generators between rustc (with panic=unwind!) and Kani

[fzaiser]

Update: the discrepancy is in fact due to Kani assuming panic=abort, but the Rust compiler assuming panic=unwind by default.

In #1378 (comment), it was observed that Kani sometimes reports a different size of a generator than the LLVM backend of rustc. Interestingly, the WASM backend seems to disagree with LLVM as well (see rust-lang/rust#62807).

The example code is the following:

#![feature(generators, generator_trait)]

use std::ops::Generator;

const FOO_SIZE: usize = 1024;
struct Foo([u8; FOO_SIZE]);

impl Drop for Foo {
    fn drop(&mut self) {}
}

fn noop() {}

fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
    static || {
        let first = Foo([0; FOO_SIZE]);
        noop();
        let _second = first;
        yield;
        // _second dropped here
    }
}

fn main() {
    // This fails for Kani: it thinks the size is 1025, and so does the WASM backend.
    assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop()));
}

[celinval]

@fzaiser I was taking a look at this issue, and I bumped into the following rust issue: rust-lang/rust#59123. It seems that the panic strategy can impact the generator size.

If I run the example you pasted above with the following command:

rustc +nightly-2022-08-16-x86_64-unknown-linux-gnu size.rs -C panic=abort && ./size

The assertion fails because the size is now 1025:

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `1026`,
 right: `1025`', size.rs:26:5
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[giltho]

Why would you write that specific test though? Isn't it actually a good thing that Kani differs from LLVM? The size of a generator is a property the developer should never rely on

[fzaiser]

@giltho Kani is supposed to be bit-precise model checker, so we should get the sizes right. It's not something the user should rely on, but internally, Kani should compute the right sizes for offsets etc.

[giltho]

@fzaiser

so we should get the sizes right

I agree, but what is the "right" size? If WASM and LLVM disagree, why would LLVM be "right" and WASM be "wrong"?

[giltho]

The test has been disabled for WASM, I don't think it's a bad thing to disable it for Kani too

[fzaiser]

@giltho It looks like the actual difference is not LLVM vs WASM but "panic=unwind" vs "panic=abort". So we may have to update the tests. I'll update the title when I know for sure what the reason is.