Assertion failure in check_vtable_size

[tedinski]

Reproduction steps:

$ cargo new exr-test
     Created binary (application) `exr-test` package
$ cd exr-test/
$ cargo add exr
    Updating crates.io index
      Adding exr v1.5.0 to dependencies.
$ cargo kani
[..SNIP..]
thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `40`,
 right: `33`', kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:883:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
If you are seeing this message, please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: <meta::header::LayerAttributes as std::fmt::Debug>::fmt
_RNvXs2_NtNtCs6ehrxsMMmGu_3exr4meta6headerNtB5_15LayerAttributesNtNtCs2ybv9YpAGK_4core3fmt5Debug3fmt
[Kani] current codegen location: Loc { file: "/home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/exr-1.5.0/src/meta/header.rs", function: None, start_line: 1150, start_col: Some(5), end_line: 1150, end_col: Some(79) }
error: could not compile `exr`
Error: cargo exited with status exit status: 101

That "current codegen location" is here:

impl std::fmt::Debug for LayerAttributes {
    fn fmt(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

[tedinski]

This also occurs in tokio-postgres

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `920`,
 right: `1831`', kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:883:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
If you are seeing this message, please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: prepare::prepare_rec
_RNvNtCsbtOfR33BsoT_14tokio_postgres7prepare11prepare_rec
[Kani] current codegen location: Loc { file: "/home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/tokio-postgres-0.7.7/src/prepare.rs", function: None, start_line: 106, start_col: Some(1), end_line: 110, end_col: Some(73) }

And in threadpool

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `4400`,
 right: `4106`', kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:883:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
If you are seeing this message, please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: threadpool::ThreadPool::execute::<[closure@exr::block::writer::ParallelBlocksCompressor<exr::block::writer::OnProgressChunkWriter<exr::block::writer::ChunkWriter<&mut &mut std::io::BufWriter<std::fs::File>>, fn(f64)>>::add_block_to_compression_queue::{closure#0}]>
_RINvMs3_CsfmIsuIbxhid_10threadpoolNtB6_10ThreadPool7executeNCNvMs3_NtNtCs7iMfnwNXZd0_3exr5block6writerINtB13_24ParallelBlocksCompressorINtB13_21OnProgressChunkWriterINtB13_11ChunkWriterQQINtNtNtNtCslqDs7LX7IdZ_3std2io8buffered9bufwriter9BufWriterNtNtB38_2fs4FileEEFdEuEE30add_block_to_compression_queue0ECskB3hp221BIC_5image
[Kani] current codegen location: Loc { file: "/home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/threadpool-1.8.1/src/lib.rs", function: None, start_line: 427, start_col: Some(5), end_line: 429, end_col: Some(38) }

[fzaiser]

Example without dependencies (~130 lines) that I hit while working on #1504:

use std::{
    sync::{
        atomic::{AtomicI64, Ordering},
        Arc,
    },
    future::Future,
    pin::Pin,
    task::{Context, RawWaker, RawWakerVTable, Waker},
};

const NOOP_RAW_WAKER: RawWaker = {
    #[inline]
    unsafe fn clone_waker(_: *const ()) -> RawWaker {
        NOOP_RAW_WAKER
    }

    #[inline]
    unsafe fn noop(_: *const ()) {}

    RawWaker::new(
        std::ptr::null(),
        &RawWakerVTable::new(clone_waker, noop, noop, noop),
    )
};

type BoxFuture = Pin<Box<dyn Future<Output = ()>>>;

static mut GLOBAL_EXECUTOR: SpawnOnceScheduler = SpawnOnceScheduler::new();

struct SpawnOnceScheduler
{
    spawner: Option<BoxFuture>,
    spawnee: Option<BoxFuture>,
}

impl SpawnOnceScheduler
{
    pub const fn new() -> Self {
        Self {
            spawner: None,
            spawnee: None,
        }
    }

    pub fn spawn(&mut self, fut: impl Future<Output = ()> + 'static) {
        let _ = std::mem::replace(&mut self.spawnee, Some(Box::pin(fut)));
    }

    pub fn run(&mut self) {
        let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
        let cx = &mut Context::from_waker(&waker);
        let mut index = 0;
        while self.spawner.is_some() || self.spawnee.is_some() {
            index = (index + 1) % 2;
            if index == 0 {
                Self::poll_task(&mut self.spawner, cx)
            } else {
                Self::poll_task(&mut self.spawnee, cx)
            }
        }
    }

    fn poll_task(task: &mut Option<BoxFuture>, cx: &mut Context) {
        if let Some(fut) = task.as_mut() {
            match fut.as_mut().poll(cx) {
                std::task::Poll::Ready(_) => {
                    let _ = std::mem::replace(task, None);
                }
                std::task::Poll::Pending => (),
            }
        }
    }

    pub fn block_on(
        self: &'static mut Self,
        fut: impl Future<Output = ()> + 'static,
    ) {
        let _ = std::mem::replace(&mut self.spawner, Some(Box::pin(fut)));
        self.run();
    }
}

pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) {
    unsafe { GLOBAL_EXECUTOR.spawn(fut) }
}

pub fn spawnable_block_on(
    fut: impl Future<Output = ()> + 'static,
) {
    unsafe { GLOBAL_EXECUTOR.block_on(fut) }
}

struct YieldNow {
    yielded: bool,
}

impl Future for YieldNow {
    type Output = ();

    fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
        if self.yielded {
            cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
            std::task::Poll::Ready(())
        } else {
            self.yielded = true;
            std::task::Poll::Pending
        }
    }
}
pub fn yield_now() -> impl Future<Output = ()> {
    YieldNow { yielded: false }
}

#[cfg_attr(kani, kani::proof)]
#[cfg_attr(kani, kani::unwind(4))]
fn nondeterministic_schedule() {
    let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc
    let x2 = x.clone();
    spawnable_block_on(
        async move {
            yield_now().await;
            x2.fetch_add(1, Ordering::Relaxed);
        },
    );
    assert_eq!(x.load(Ordering::Relaxed), 2);
}

Run it like this: RUSTFLAGS="--edition 2021" kani test.rs

Result:

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `16`,
 right: `17`', kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:883:9

[celinval]

I believe this issue has similar root cause as #1395. The failure is triggered while trying to create a vtable for a generator wrapper:

let _7: std::pin::Pin<std::boxed::Box<dyn std::future::Future<Output = ()>>>
let _8: std::pin::Pin<std::boxed::Box<std::future::from_generator::GenFuture<[static generator@size.rs:123:20: 126:10]>>>
...
_7 = move _8 as std::pin::Pin<std::boxed::Box<dyn std::future::Future<Output = ()>>> (Pointer(Unsize))

I.e.: This code is converting std::future::from_generator::GenFuture<[static [generator@size.rs](mailto:generator@size.rs):123:20: 126:10]> into dyn std::future::Future<Output = ()>.

We fail because the size of std::future::from_generator::GenFuture<[static [generator@size.rs](mailto:generator@size.rs):123:20: 126:10]> computed using layout_of differs from getting the size of the type we have generated.