ice: unimplemented boxed_fn_once #2874
Description
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