ICE: place: Unexpected type mismatch in projection:

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

@matthiaskrgr

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) }

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

Triaged against main (de756c9): still reproduces, and #4813, #2684, #2497 and #2253 are all the same root cause — assert_sig_matches! for the catch_unwind intrinsic (kani-compiler/src/intrinsics.rs:243) still expects ... => RigidTy::Int(IntTy::I32), but the intrinsic now returns bool:

// library/core/src/intrinsics/mod.rs
pub unsafe fn catch_unwind<Data: ptr::Thin>(
    _try_fn: unsafe fn(*mut Data),
    _data: *mut Data,
    _catch_fn: unsafe fn(*mut Data, *mut u8),
) -> bool;

So any program that reaches catch_unwind (thread::spawn(..).join(), BufReader, the async-waker reproducers here) takes the compiler down instead of getting the intended Unimplemented/#267 message. Fixing the expected return type in that one assertion should close all four. It also blocks autoharness --std over the standard library, which hits it while compiling proc_macro.

On main 1640445da the minimal panic_any(Foo) reproducer fails verification normally on the panic, and the original program compiles and verifies in a bounded run (--default-unwind 2 --no-unwinding-checks), so this crash is gone and the issue can be closed.

Fixed by e47388f (#4819). On main: panic_any repro 2253-1 fails verification normally, catch_unwind variant 2253-3 verifies, no crash.

Navigation Menu

Repository navigation

ICE: place: Unexpected type mismatch in projection: #2253

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

ICE: place: Unexpected type mismatch in projection: #2253

Description

Activity

zhassan-aws commented on Mar 2, 2023

matthiaskrgr commented on Nov 12, 2023

feliperodri commented on Sep 25, 2026

srivatsansamraj commented on Oct 5, 2026

feliperodri commented on Nov 5, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions