ICE: resolution failed during building vtable representation

[matthiaskrgr]

I tried this code:

use std::future::Future;

pub trait Service {
    type Response;
    type Future: Future<Output = Self::Response>;
}

pub trait ThriftService: Service<Future = Box<dyn Future<Output = i32>>, Response = i32> {
    fn foo(&self) {}
}

#[kani::proof]
fn main() {
    let x: &dyn ThriftService = todo!();
}

using the following command line invocation:

kani file.rs

with Kani version: 0.46.0

I expected to see this happen: explanation

Instead, this happened: explanation

Kani Rust Verifier 0.46.0 (standalone)
warning: unused variable: `x`
  --> 102933-2.rs:14:9
   |
14 |     let x: &dyn ThriftService = todo!();
   |         ^ help: if this is intentional, prefix it with an underscore: `_x`
   |
   = note: `#[warn(unused_variables)]` on by default

thread 'rustc' panicked at compiler/rustc_trait_selection/src/traits/vtable.rs:297:22:
resolution failed during building vtable representation
stack backtrace:
   0:     0x7f89e238be86 - std::backtrace_rs::backtrace::libunwind::trace::haa62de98ce20d13c
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x7f89e238be86 - std::backtrace_rs::backtrace::trace_unsynchronized::h4bc7f582e9f49dbd
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f89e238be86 - std::sys_common::backtrace::_print_fmt::h07d78988ae6e922d
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:68:5
   3:     0x7f89e238be86 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::he72c24e459b4aee4
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f89e23de740 - core::fmt::rt::Argument::fmt::h9ff3b213e1468f5f
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/fmt/rt.rs:142:9
   5:     0x7f89e23de740 - core::fmt::write::h0ab1f59280077a18
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/fmt/mod.rs:1120:17
   6:     0x7f89e237f7bf - std::io::Write::write_fmt::h2f48f6201433d434
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/io/mod.rs:1810:15
   7:     0x7f89e238bc64 - std::sys_common::backtrace::_print::h710dac96d5446d07
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7f89e238bc64 - std::sys_common::backtrace::print::h22982b9f2c94c190
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7f89e238e9f7 - std::panicking::default_hook::{{closure}}::h19052586580466eb
  10:     0x7f89e238e759 - std::panicking::default_hook::h9f3f4c25f2a49543
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:292:9
  11:     0x555a2258b29d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62bee1eb7956b9f6
  12:     0x555a2258aaa3 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h252d31e703366824
  13:     0x7f89e238f146 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h0ebb0eb5cf5e84f1
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2030:9
  14:     0x7f89e238f146 - std::panicking::rust_panic_with_hook::hb83cfb3ac729d1b2
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:785:13
  15:     0x7f89e238ee92 - std::panicking::begin_panic_handler::{{closure}}::hf6588d71adde3329
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:659:13
  16:     0x7f89e238c386 - std::sys_common::backtrace::__rust_end_short_backtrace::hfa69dd6720275711
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:171:18
  17:     0x7f89e238ebe4 - rust_begin_unwind
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:647:5
  18:     0x7f89e23dae45 - core::panicking::panic_fmt::h3d775185360585e3
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:72:14
  19:     0x7f89e23dabf3 - core::panicking::panic_display::h2fa64a4c53bd8264
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:196:5
  20:     0x7f89e23dabf3 - core::panicking::panic_str::h6489743b3479b590
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:171:5
  21:     0x7f89e23dabf3 - core::option::expect_failed::hf1a3cf552f2a183e
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/option.rs:1988:5
  22:     0x7f89e68ad0d5 - rustc_trait_selection[dbb56e670474f001]::traits::vtable::vtable_entries::{closure#0}
  23:     0x7f89e68ad9ff - rustc_trait_selection[dbb56e670474f001]::traits::vtable::vtable_entries
  24:     0x7f89e68ad528 - rustc_query_impl[3212609eeba22f38]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[3212609eeba22f38]::query_impl::vtable_entries::dynamic_query::{closure#2}::{closure#0}, rustc_middle[ea9ac6a1ebc6c470]::query::erase::Erased<[u8; 16usize]>>
  25:     0x7f89e68ad4e7 - <rustc_query_impl[3212609eeba22f38]::query_impl::vtable_entries::dynamic_query::{closure#2} as core[2f78b8535a2e64fa]::ops::function::FnOnce<(rustc_middle[ea9ac6a1ebc6c470]::ty::context::TyCtxt, rustc_middle[ea9ac6a1ebc6c470]::ty::sty::Binder<rustc_middle[ea9ac6a1ebc6c470]::ty::sty::TraitRef>)>>::call_once
  26:     0x7f89e7145ee8 - rustc_query_system[a07abdd064d033d]::query::plumbing::try_execute_query::<rustc_query_impl[3212609eeba22f38]::DynamicConfig<rustc_query_system[a07abdd064d033d]::query::caches::DefaultCache<rustc_middle[ea9ac6a1ebc6c470]::ty::sty::Binder<rustc_middle[ea9ac6a1ebc6c470]::ty::sty::TraitRef>, rustc_middle[ea9ac6a1ebc6c470]::query::erase::Erased<[u8; 16usize]>>, false, false, false>, rustc_query_impl[3212609eeba22f38]::plumbing::QueryCtxt, false>
  27:     0x7f89e7145bb5 - rustc_query_impl[3212609eeba22f38]::query_impl::vtable_entries::get_query_non_incr::__rust_end_short_backtrace
  28:     0x555a224ceaac - rustc_middle::query::plumbing::query_get_at::h47a173c70f0167ca
  29:     0x555a2252e2b4 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty_ref::h3d135cacf211876b
  30:     0x555a2252a47e - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty::hb550fd5603eeed6c
  31:     0x555a225363e5 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h70ea6b1d619c790d
  32:     0x555a225f9e9a - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h179e069baadeebc1
  33:     0x555a225b1430 - scoped_tls::ScopedKey<T>::set::h462dbe7b3063cb5c
  34:     0x555a225e91a4 - rustc_smir::rustc_internal::init::hdab7351afa62793a
  35:     0x555a225b4054 - stable_mir::compiler_interface::run::hdc01671daf50c78a
  36:     0x555a225fd62e - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd5728f8a33105c7d
  37:     0x7f89e6e6aff0 - rustc_interface[79a3a7c6d29fbb15]::passes::start_codegen
  38:     0x7f89e6e6a75c - <rustc_interface[79a3a7c6d29fbb15]::queries::Queries>::codegen_and_build_linker
  39:     0x7f89e717a44a - rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler::<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}
  40:     0x7f89e73e5986 - std[da4468a6436061de]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_with_globals<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_pool_with_globals<rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>
  41:     0x7f89e73e57b3 - <<std[da4468a6436061de]::thread::Builder>::spawn_unchecked_<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_with_globals<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_pool_with_globals<rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#1} as core[2f78b8535a2e64fa]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  42:     0x7f89e2398735 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hda2c57e98ef914e1
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2016:9
  43:     0x7f89e2398735 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h4c1ca1ffb3984aed
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2016:9
  44:     0x7f89e2398735 - std::sys::pal::unix::thread::Thread::new::thread_start::h6dfa281031503fa8
                               at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys/pal/unix/thread.rs:108:17
  45:     0x7f89e203c9eb - <unknown>
  46:     0x7f89e20c07cc - <unknown>
  47:                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: main
main
[Kani] current codegen location: Loc { file: "102933-2.rs", function: None, start_line: 13, start_col: Some(1), end_line: 13, end_col: Some(10) }
warning: 1 warning emitted

error: /home/matthias/.kani/kani-0.46.0/bin/kani-compiler exited with status exit status: 101