ice: unimplemented boxed_fn_once

[matthiaskrgr]

I tried this code:

fn boxed_fn_once(f: Box<dyn FnOnce() -> i32>) -> i32 {
    f()
}

#[kani::proof]
fn main() {
    assert_eq!(
        boxed_fn_once(Box::new({
            let x = 13;
            move || x
        })),
        13,
    );
}

using the following command line invocation:

RUSTFLAGS="-Zmir-opt-level=2" kani closures.rs

with Kani version: 0.40

I expected to see this happen: explanation

Instead, this happened: explanation

Kani Rust Verifier 0.40.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:427:18:
not implemented
stack backtrace:
   0:     0x7faae01d5cfc - std::backtrace_rs::backtrace::libunwind::trace::h974857262e179b17
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x7faae01d5cfc - std::backtrace_rs::backtrace::trace_unsynchronized::h6adce2053c056ac9
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7faae01d5cfc - std::sys_common::backtrace::_print_fmt::hcf2018a5ad956761
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7faae01d5cfc - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h3d39e48ce4d7e36f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7faae0237f50 - core::fmt::rt::Argument::fmt::hef0ae15422a7f61d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/rt.rs:142:9
   5:     0x7faae0237f50 - core::fmt::write::hf465a4ba34489409
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/mod.rs:1117:17
   6:     0x7faae01c9c1f - std::io::Write::write_fmt::hf34ad5986fa99e89
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/io/mod.rs:1763:15
   7:     0x7faae01d5ae4 - std::sys_common::backtrace::_print::h5aa7f1d99916c125
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7faae01d5ae4 - std::sys_common::backtrace::print::h036d85b5c81889eb
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7faae01d8777 - std::panicking::default_hook::{{closure}}::h9b311bcc8d2b2a40
  10:     0x7faae01d84df - std::panicking::default_hook::hd7a03fd029ce4ee2
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:292:9
  11:     0x561461c07c0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h270fbeb056d900dc
  12:     0x561461c07703 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h410a2f5534eafaf7
  13:     0x7faae01d8eb8 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h079168172b9ee18d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2021:9
  14:     0x7faae01d8eb8 - std::panicking::rust_panic_with_hook::h9ec5267af19ebd61
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:783:13
  15:     0x7faae01d8bd9 - std::panicking::begin_panic_handler::{{closure}}::hded4ae2a191a7bae
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:649:13
  16:     0x7faae01d61c6 - std::sys_common::backtrace::__rust_end_short_backtrace::h3b03f6ccd27da73f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7faae01d8972 - rust_begin_unwind
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:645:5
  18:     0x7faae0234675 - core::panicking::panic_fmt::h290f6f1be63b094c
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:72:14
  19:     0x7faae0234713 - core::panicking::panic::hac1e457063a02956
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:127:5
  20:     0x561461af04e3 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_scalar::h46f1eed74bf69bd0
  21:     0x561461aeda77 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::h4e38dfde4e70e9b4
  22:     0x561461bef717 - core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut::h9a417065f39331cd
  23:     0x561461b43135 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h79ec947e06b1cd22
  24:     0x561461b15925 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall_args::hc248c62471a71149
  25:     0x561461b13281 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::h3967cbd0413177f5
  26:     0x561461ac3a9b - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::h892262db0bd2a271
  27:     0x561461b270ec - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hc439f7b37aa26293
  28:     0x561461b5b10a - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::hc367daaf74d3c1cb
  29:     0x561461b5fcf5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h2ef5769ca04f3bc4
  30:     0x7faadf180fd9 - rustc_interface[90d65b0f51490bf6]::passes::start_codegen
  31:     0x7faadf180a96 - <rustc_interface[90d65b0f51490bf6]::queries::Queries>::ongoing_codegen
  32:     0x7faadf143693 - std[d7fc13cc5242579e]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>
  33:     0x7faadf142909 - <<std[d7fc13cc5242579e]::thread::Builder>::spawn_unchecked_<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#1} as core[53bdee0566a68c19]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  34:     0x7faae01e3c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he310d06a8f297797
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  35:     0x7faae01e3c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h69350f715ad37c20
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  36:     0x7faae01e3c85 - std::sys::unix::thread::Thread::new::thread_start::h7310dea1d780d6a0
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys/unix/thread.rs:108:17
  37:     0x7faada5639eb - <unknown>
  38:     0x7faada5e77cc - <unknown>
  39:                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: "/tmp/icemaker/closures.rs", function: None, start_line: 6, start_col: Some(1), end_line: 6, end_col: Some(10) }
error: /home/matthias/.kani/kani-0.40.0/bin/kani-compiler exited with status exit status: 101