ICE: place: Unexpected type mismatch in projection:

[matthiaskrgr]

I tried this code:

#![allow(unused)]

use std::{
    cell::{Cell, RefCell},
    future::Future,
    marker::Unpin,
    panic,
    pin::Pin,
    ptr,
    rc::Rc,
    task::{Context, Poll, RawWaker, RawWakerVTable, Waker},
};

struct InjectedFailure;

struct Defer<T> {
    ready: bool,
    value: Option<T>,
}

impl<T: Unpin> Future for Defer<T> {
    type Output = T;
    fn poll(mut self: Pin<&mut Self>, cx: &mut Context) -> Poll<Self::Output> {
        if self.ready {
            Poll::Ready(self.value.take().unwrap())
        } else {
            self.ready = true;
            Poll::Pending
        }
    }
}

struct Allocator {
    data: RefCell<Vec<bool>>,
    failing_op: usize,
    cur_ops: Cell<usize>,
}

impl panic::UnwindSafe for Allocator {}
impl panic::RefUnwindSafe for Allocator {}

impl Drop for Allocator {
    fn drop(&mut self) {
        let data = self.data.borrow();
        if data.iter().any(|d| *d) {
            panic!("missing free: {:?}", data);
        }
    }
}

impl Allocator {
    fn new(failing_op: usize) -> Self {
        Allocator { failing_op, cur_ops: Cell::new(0), data: RefCell::new(vec![]) }
    }
    fn alloc(&self) -> impl Future<Output = Ptr<'_>> + '_ {
        self.fallible_operation();

        let mut data = self.data.borrow_mut();

        let addr = data.len();
        data.push(true);
        Defer { ready: false, value: Some(Ptr(addr, self)) }
    }
    fn fallible_operation(&self) {
        self.cur_ops.set(self.cur_ops.get() + 1);

        if self.cur_ops.get() == self.failing_op {
            panic::panic_any(InjectedFailure);
        }
    }
}

struct Ptr<'a>(usize, &'a Allocator);
impl<'a> Drop for Ptr<'a> {
    fn drop(&mut self) {
        match self.1.data.borrow_mut()[self.0] {
            false => panic!("double free at index {:?}", self.0),
            ref mut d => *d = false,
        }

        self.1.fallible_operation();
    }
}

async fn dynamic_init(a: Rc<Allocator>, c: bool) {
    let _x;
    if c {
        _x = Some(a.alloc().await);
    }
}


fn run_test<F, G>(cx: &mut Context<'_>, ref f: F)
where
    F: Fn(Rc<Allocator>) -> G,
    G: Future<Output = ()>,
{
    for polls in 0.. {
        // Run without any panics to find which operations happen after the
        // penultimate `poll`.
        let first_alloc = Rc::new(Allocator::new(usize::MAX));
        let mut fut = Box::pin(f(first_alloc.clone()));
        let mut ops_before_last_poll = 0;
        let mut completed = false;
        for _ in 0..polls {
            ops_before_last_poll = first_alloc.cur_ops.get();
            if let Poll::Ready(()) = fut.as_mut().poll(cx) {
                completed = true;
            }
        }
        drop(fut);

        // Start at `ops_before_last_poll` so that we will always be able to
        // `poll` the expected number of times.
        for failing_op in ops_before_last_poll..first_alloc.cur_ops.get() {
            let alloc = Rc::new(Allocator::new(failing_op + 1));
            let f = &f;
            let cx = &mut *cx;
            let result = panic::catch_unwind(panic::AssertUnwindSafe(move || {
                let mut fut = Box::pin(f(alloc));
                for _ in 0..polls {
                    let _ = fut.as_mut().poll(cx);
                }
                drop(fut);
            }));
            match result {
                Ok(..) => panic!("test executed more ops on first call"),
                Err(e) => {
                    if e.downcast_ref::<InjectedFailure>().is_none() {
                        panic::resume_unwind(e);
                    }
                }
            }
        }

        if completed {
            break;
        }
    }
}

fn clone_waker(data: *const ()) -> RawWaker {
    RawWaker::new(data, &RawWakerVTable::new(clone_waker, drop, drop, drop))
}

#[kani::proof]
fn main() {
    let waker = unsafe { Waker::from_raw(clone_waker(ptr::null())) };
    let context = &mut Context::from_waker(&waker);

    run_test(context, |a| dynamic_init(a, false));
    
}

using the following command line invocation:

RUSTFLAGS="--edition=2021" kani a.rs

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

 WARN kani_compiler::codegen_cprover_gotoc::codegen::place Unexpected type mismatch in projection:
Expr { value: Index { array: Expr { value: Symbol { identifier: "_ZN116_$LT$core..core_simd..vector..Simd$LT$T$C$_$GT$$u20$as$u20$core..convert..From$LT$$u5b$T$u3b$$u20$LANES$u5d$$GT$$GT$4from17h8017b470b1c73338E::1::var_0" }, typ: Vector { typ: Unsignedbv { width: 8 }, size: 1 }, location: None }, index: Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None } }, typ: Unsignedbv { width: 8 }, location: None }
Expr type
Unsignedbv { width: 8 }
Type from MIR
StructTag("tag-[_13358953601680865708; 1]")
thread '<unnamed>' panicked at 'Panic requires a string message', kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs:203:9
stack backtrace:
   0:     0x7fc6c25667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fc6c25667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fc6c25667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7fc6c25667da - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9271b09f3576b7e0
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fc6c25c92ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7fc6c2556c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7fc6c25665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7fc6c25665a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7fc6c25692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7fc6c256902b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x55f484faeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x55f484f04f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7fc6c2569b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7fc6c2569b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x7fc6c2569862 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:577:13
  15:     0x7fc6c2566c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
  16:     0x7fc6c25695b2 - rust_begin_unwind
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
  17:     0x7fc6c25c5cd3 - core::panicking::panic_fmt::hbacb72817da3b060
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
  18:     0x55f484e7ce56 - kani_compiler::codegen_cprover_gotoc::codegen::assert::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_panic::h019eec7366d1a630
  19:     0x55f484fc9040 - <kani_compiler::codegen_cprover_gotoc::overrides::hooks::Panic as kani_compiler::codegen_cprover_gotoc::overrides::hooks::GotocHook>::handle::h415cefb04e744048
  20:     0x55f484edc424 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::hba20b41c6ebc6f6b
  21:     0x55f484e7f15d - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
  22:     0x55f484f0abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
  23:     0x55f484f964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  24:     0x7fc6c4a86fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  25:     0x7fc6c4a86ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  26:     0x7fc6c4a847a6 - <rustc_interface[aec886e93b1add3f]::passes::QueryContext>::enter::<<rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  27:     0x7fc6c4a81a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  28:     0x7fc6c4a80f67 - <rustc_interface[aec886e93b1add3f]::interface::Compiler>::enter::<rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}::{closure#2}, core[6d94cc961ac87456]::result::Result<core[6d94cc961ac87456]::option::Option<rustc_interface[aec886e93b1add3f]::queries::Linker>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  29:     0x7fc6c4a7bf88 - rustc_span[ae2df7aa7c6c667b]::with_source_map::<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  30:     0x7fc6c4a7ba75 - <scoped_tls[db87656d258d017b]::ScopedKey<rustc_span[ae2df7aa7c6c667b]::SessionGlobals>>::set::<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  31:     0x7fc6c4a7b062 - std[acd1f573e90225f]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  32:     0x7fc6c50ec49e - <<std[acd1f573e90225f]::thread::Builder>::spawn_unchecked_<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#1} as core[6d94cc961ac87456]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  33:     0x7fc6c65da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  34:     0x7fc6c65da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  35:     0x7fc6c65da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  36:     0x7fc6c221dbb5 - <unknown>
  37:     0x7fc6c229fd90 - <unknown>
  38:                0x0 - <unknown>

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: std::panic::panic_any::<InjectedFailure>
_RINvNtCskhzp34QgdsD_3std5panic9panic_anyNtCsbvss9KOnXkz_1a15InjectedFailureEBE_
[Kani] current codegen location: Loc { file: "/home/runner/.rustup/toolchains/nightly-2022-12-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panic.rs", function: None, start_line: 60, start_col: Some(1), end_line: 60, end_col: Some(55) }
error: /home/matthias/.kani/kani-0.22.0/bin/kani-compiler exited with status exit status: 101

[zhassan-aws]

Thanks for the bug report @matthiaskrgr.

Here is a minimal reproducer:

struct Foo;

#[kani::proof]
fn main() {
    std::panic::panic_any(Foo)
}

thread '<unnamed>' panicked at 'Panic requires a string message', kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs:203:9
note: run with `RUST_BACKTRACE=1` environment variable to display a 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: std::panic::panic_any::<Foo>
_RINvNtCsbkGKF7C7D4B_3std5panic9panic_anyNtCs9Af4eIVbVvg_11empty_panic3FooEBE_
[Kani] current codegen location: Loc { file: "/home/ubuntu/.rustup/toolchains/nightly-2022-12-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panic.rs", function: None, start_line: 60, start_col: Some(1), end_line: 60, end_col: Some(55) }

[matthiaskrgr]

with 0.40 , the original sample only panics with Panic requires a string message now, and no more "type mismatch in projection"

reduced sample also shows no change