Kani 0.27 unexpectedly panicked during compilation

[ytakano]

I tried this code:

https://github.com/ytakano/kani_compile_error_simple_channel/blob/master/src/unbounded.rs

runner.rs in this repository is equivalent to manual_spawn.rs of Kani.

use alloc::{collections::VecDeque, sync::Arc};
use core::task::Waker;
use std::sync::Mutex;

/// Channel.
struct Channel<T> {
    queue: VecDeque<T>,
    waker_receiver: Option<Waker>,
    terminated: bool,
}

/// Sender of a channel.
pub struct Sender<T> {
    chan: Arc<Mutex<Channel<T>>>,
}

impl<T> Clone for Sender<T> {
    fn clone(&self) -> Self {
        Self {
            chan: self.chan.clone(),
        }
    }
}

impl<T> Sender<T> {
    pub async fn send(&self, data: T) -> Result<(), &'static str> {
        let mut chan = self.chan.lock().unwrap();

        if chan.terminated {
            return Err("Connection closed");
        }

        chan.queue.push_back(data);

        Ok(())
    }

    pub fn is_terminated(&self) -> bool {
        let chan = self.chan.lock().unwrap();
        chan.terminated
    }
}

impl<T> Drop for Sender<T> {
    fn drop(&mut self) {
        let mut chan = self.chan.lock().unwrap();
        chan.terminated = true;
        if let Some(waker) = chan.waker_receiver.take() {
            waker.wake();
        }
    }
}

pub fn new_sender<T>() -> Sender<T> {
    let chan = Channel {
        queue: Default::default(),
        waker_receiver: None,
        terminated: false,
    };

    let chan = Arc::new(Mutex::new(chan));
    Sender { chan }
}

unsafe impl<T> Send for Sender<T> {}

#[cfg(kani)]
mod tests {
    use super::*;
    use crate::runner;

    #[kani::proof]
    #[kani::unwind(10)]
    fn check() {
        runner::spawnable_block_on(
            async {
                let num: usize = kani::any();
                kani::assume(num <= 5);

                let tx = new_sender();

                let task1 = async move {
                    for i in 0..num {
                        tx.send(i).await.unwrap();
                    }
                };

                let join1 = runner::spawn(task1);

                join1.await;
            },
            runner::RoundRobin::default(),
        );
    }
}

using the following command line invocation:

$ RUST_BACKTRACE=1 cargo kani
   Compiling kani_async v0.1.0 (/home/ytakano/kani_async)
warning: field `waker_receiver` is never read
 --> src/unbounded.rs:8:5
  |
6 | struct Channel<T> {
  |        ------- field in this struct
7 |     queue: VecDeque<T>,
8 |     waker_receiver: Option<Waker>,
  |     ^^^^^^^^^^^^^^
  |
  = note: `#[warn(dead_code)]` on by default

thread 'rustc' panicked at 'Error in struct_expr; value type does not match field type.
        StructTag("tag-_7931425818576372193::DirectFields")
        [Field { name: "generator_field_1", typ: CInteger(SizeT) }, Field { name: "generator_field_0", typ: Pointer { typ: StructTag("tag-_2670222561860564476") } }, Field { name: "case", typ: Unsignedbv { width: 8 } }]
        [Expr { value: Symbol { identifier: "_RNvMs_NtCs4eKqxUCtJjz_10kani_async9unboundedINtB4_6SenderjE4sendB6_::1::var_1::self" }, typ: Pointer { typ: StructTag("tag-_2670222561860564476") }, location: None, size_of_annotation: None }, Expr { value: Symbol { identifier: "_RNvMs_NtCs4eKqxUCtJjz_10kani_async9unboundedINtB4_6SenderjE4sendB6_::1::var_2::data" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }, Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]', cprover_bindings/src/goto_program/expr.rs:809:9
stack backtrace:
error: internal compiler error: Kani unexpectedly panicked at panicked at 'Error in struct_expr; value type does not match field type.
                                    StructTag("tag-_7931425818576372193::DirectFields")
                                    [Field { name: "generator_field_1", typ: CInteger(SizeT) }, Field { name: "generator_field_0", typ: Pointer { typ: StructTag("tag-_2670222561860564476") } }, Field { name: "case", typ: Unsignedbv { width: 8 } }]
                                    [Expr { value: Symbol { identifier: "_RNvMs_NtCs4eKqxUCtJjz_10kani_async9unboundedINtB4_6SenderjE4sendB6_::1::var_1::self" }, typ: Pointer { typ: StructTag("tag-_2670222561860564476") }, location: None, size_of_annotation: None }, Expr { value: Symbol { identifier: "_RNvMs_NtCs4eKqxUCtJjz_10kani_async9unboundedINtB4_6SenderjE4sendB6_::1::var_2::data" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }, Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]', cprover_bindings/src/goto_program/expr.rs:809:9.

   0: rust_begin_unwind
             at /rustc/9aa5c24b7d763fb98d998819571128ff2eb8a3ca/library/std/src/panicking.rs:575:5
   1: core::panicking::panic_fmt
             at /rustc/9aa5c24b7d763fb98d998819571128ff2eb8a3ca/library/core/src/panicking.rs:64:14
   2: cprover_bindings::goto_program::expr::Expr::struct_expr_from_values
   3: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue
   4: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
   5: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
   6: std::thread::local::LocalKey<T>::with
   7: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
   8: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
   9: rustc_interface::passes::start_codegen
  10: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorGuaranteed>>
  11: <rustc_interface::queries::Queries>::ongoing_codegen
  12: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
  13: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  14: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Kani unexpectedly panicked during compilation.
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: unbounded::Sender::<usize>::send
_RNvMs_NtCs4eKqxUCtJjz_10kani_async9unboundedINtB4_6SenderjE4sendB6_
[Kani] current codegen location: Loc { file: "/home/ytakano/kani_async/src/unbounded.rs", function: None, start_line: 26, start_col: Some(5), end_line: 26, end_col: Some(66) }
error: could not compile `kani_async`; 2 warnings emitted
error: Failed to compile `kani_async` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at 'Error in struct_expr; value type does not match field type.
                                    StructTag("tag-_7931425818576372193::DirectFields")
                                    [Field { name: "generator_field_1", typ: CInteger(SizeT) }, Field { name: "generator_field_0", typ: Pointer { typ: StructTag("tag-_2670222561860564476") } }, Field { name: "case", typ: Unsignedbv { width: 8 } }]
                                    [Expr { value: Symbol { identifier: "_RNvMs_NtCs4eKqxUCtJjz_10kani_async9unboundedINtB4_6SenderjE4sendB6_::1::var_1::self" }, typ: Pointer { typ: StructTag("tag-_2670222561860564476") }, location: None, size_of_annotation: None }, Expr { value: Symbol { identifier: "_RNvMs_NtCs4eKqxUCtJjz_10kani_async9unboundedINtB4_6SenderjE4sendB6_::1::var_2::data" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }, Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]', cprover_bindings/src/goto_program/expr.rs:809:9.

with Kani version:

$ rustc --version
rustc 1.71.0-nightly (c4190f2d3 2023-05-07)
$ cargo kani --version
cargo-kani 0.27.0

[zhassan-aws]

Thanks @ytakano for the bug report. It seems there is a mismatch in the order of the struct fields that is causing the panic. We will look into it.

[zhassan-aws]

This is a minimal stand-alone reproducer:

use core::{future::Future, pin::Pin};

type BoxFuture = Pin<Box<dyn Future<Output = ()> + Sync + 'static>>;

pub struct Scheduler {
    task: Option<BoxFuture>,
}

impl Scheduler {
    /// Adds a future to the scheduler's task list, returning a JoinHandle
    pub fn spawn<F: Future<Output = ()> + Sync + 'static>(&mut self, fut: F) {
        self.task = Some(Box::pin(fut));
    }
}

/// Polls the given future and the tasks it may spawn until all of them complete
///
/// Contrary to block_on, this allows `spawn`ing other futures
pub fn spawnable_block_on<F: Future<Output = ()> + Sync + 'static>(scheduler: &mut Scheduler, fut: F) {
    scheduler.spawn(fut);
}
/// Sender of a channel.
pub struct Sender {}

impl Sender {
    pub async fn send(&self) {}
}

#[kani::proof]
fn check() {
    let mut scheduler = Scheduler { task: None };
    spawnable_block_on(&mut scheduler, async {
        let num: usize = 1;
        let tx = Sender {};

        let _task1 = async move {
            for _i in 0..num {
                tx.send().await;
            }
        };
    });
}

Running that with RUSTFLAGS="--edition 2018" kani unbounded.rs produces the same crash.