ICE: unimplemented on 2021 closure

[matthiaskrgr]

I tried this code:

#![deny(rust_2021_incompatible_closure_captures)]

#[kani::proof]
fn main() {
    struct Foo(u32);
    impl Drop for Foo {
        fn drop(&mut self) {
            println!("dropped {}", self.0);
        }
    }

    let f1 = Foo(0x600D);


    let c1 = move || {
        let _ = &f1;
    };
    drop(c1);
}
//~^ NOTE in Rust 2018, `f0` is dropped here along with the closure, but in Rust 2021 `f0` is not part of the closure

using the following command line invocation:

 RUST_BACKTRACE=full RUSTFLAGS="--edition=2021 -Zmir-opt-level=2" kani kani.rs

with Kani version: 0.35.0

I expected to see this happen: explanation

Instead, this happened: explanation

Kani Rust Verifier 0.35.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:428:18:
not implemented
stack backtrace:
   0:     0x7fa595f6329c - std::backtrace_rs::backtrace::libunwind::trace::h28e11dce06475f43
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fa595f6329c - std::backtrace_rs::backtrace::trace_unsynchronized::h21f22a3bfa3fb013
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fa595f6329c - std::sys_common::backtrace::_print_fmt::hafc6985e93f76ae0
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7fa595f6329c - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h36c63275fbd3f0f8
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fa595fc93ec - core::fmt::rt::Argument::fmt::h9b33518f8511caca
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/fmt/rt.rs:138:9
   5:     0x7fa595fc93ec - core::fmt::write::h67226f5192a09eca
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/fmt/mod.rs:1094:21
   6:     0x7fa595f55d2e - std::io::Write::write_fmt::h744b3076c6ca0e52
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/io/mod.rs:1714:15
   7:     0x7fa595f63084 - std::sys_common::backtrace::_print::h4bcc2e79e4348aa6
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7fa595f63084 - std::sys_common::backtrace::print::h74142c12abe5e25d
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7fa595f6617a - std::panicking::panic_hook_with_disk_dump::{{closure}}::h7d3e65abd6cf3378
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:278:22
  10:     0x7fa595f65e67 - std::panicking::panic_hook_with_disk_dump::h5bbd6ac133545f46
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:312:9
  11:     0x55fca893f2dd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h5067a4a6926df452
  12:     0x55fca893e463 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hbc7dbed47af55a6e
  13:     0x7fa595f66a20 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hbc8f8f631658dcc9
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2021:9
  14:     0x7fa595f66a20 - std::panicking::rust_panic_with_hook::h7b16b439ec100c23
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:733:13
  15:     0x7fa595f66761 - std::panicking::begin_panic_handler::{{closure}}::hd03f21e4b251a35c
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:619:13
  16:     0x7fa595f637c6 - std::sys_common::backtrace::__rust_end_short_backtrace::he8aad725f5dd71ab
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7fa595f664f2 - rust_begin_unwind
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:617:5
  18:     0x7fa595fc57f3 - core::panicking::panic_fmt::h37323eb5862b87ad
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/panicking.rs:67:14
  19:     0x7fa595fc5883 - core::panicking::panic::ha74a0707102dff8d
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/panicking.rs:117:5
  20:     0x55fca88dfcd0 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_scalar::h866d7c01955cc5f4
  21:     0x55fca88dd538 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::h2c59c4b345bfb21b
  22:     0x55fca899e72f - core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut::h6f9cf1d4f5574ff0
  23:     0x55fca8926785 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h59425a7a355828fa
  24:     0x55fca88fba75 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall_args::h0e50b2fdee2adc26
  25:     0x55fca88f8b65 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::h061f66ae0a57f0f2
  26:     0x55fca88b4135 - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::h59b22828e30bde2e
  27:     0x55fca890cb1b - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hc4985c898bede1f1
  28:     0x55fca89ceaae - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h71130359840cd186
  29:     0x55fca89d35a5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h25888e407b1b3e70
  30:     0x7fa59840d3c2 - <rustc_session[a6bdf9a4b51671a9]::session::Session>::time::<alloc[10a91b7ea9db36b6]::boxed::Box<dyn core[3ec4812ddef0ef93]::any::Any>, rustc_interface[39ac7ec62dd85acc]::passes::start_codegen::{closure#0}>
  31:     0x7fa59840cf1b - rustc_interface[39ac7ec62dd85acc]::passes::start_codegen
  32:     0x7fa598407bba - <rustc_middle[9074e8ddcc94940f]::ty::context::GlobalCtxt>::enter::<<rustc_interface[39ac7ec62dd85acc]::queries::Queries>::ongoing_codegen::{closure#0}, core[3ec4812ddef0ef93]::result::Result<alloc[10a91b7ea9db36b6]::boxed::Box<dyn core[3ec4812ddef0ef93]::any::Any>, rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>
  33:     0x7fa598407066 - <rustc_interface[39ac7ec62dd85acc]::interface::Compiler>::enter::<rustc_driver_impl[e8f28f10c524a0ae]::run_compiler::{closure#1}::{closure#2}, core[3ec4812ddef0ef93]::result::Result<core[3ec4812ddef0ef93]::option::Option<rustc_interface[39ac7ec62dd85acc]::queries::Linker>, rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>
  34:     0x7fa598404338 - std[98f21c237d3a11b9]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[39ac7ec62dd85acc]::util::run_in_thread_pool_with_globals<rustc_interface[39ac7ec62dd85acc]::interface::run_compiler<core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>, rustc_driver_impl[e8f28f10c524a0ae]::run_compiler::{closure#1}>::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>
  35:     0x7fa598403ac5 - <<std[98f21c237d3a11b9]::thread::Builder>::spawn_unchecked_<rustc_interface[39ac7ec62dd85acc]::util::run_in_thread_pool_with_globals<rustc_interface[39ac7ec62dd85acc]::interface::run_compiler<core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>, rustc_driver_impl[e8f28f10c524a0ae]::run_compiler::{closure#1}>::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>::{closure#1} as core[3ec4812ddef0ef93]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  36:     0x7fa595f71225 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h5d092cb8decc581e
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2007:9
  37:     0x7fa595f71225 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h88f1cce7655d0913
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2007:9
  38:     0x7fa595f71225 - std::sys::unix::thread::Thread::new::thread_start::h775d92d70f807a4c
                               at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys/unix/thread.rs:108:17
  39:     0x7fa595a8c9eb - <unknown>
  40:     0x7fa595b10dfc - <unknown>
  41:                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/im/kani.rs", function: None, start_line: 4, start_col: Some(1), end_line: 4, end_col: Some(10) }
error: /home/matthias/.kani/kani-0.35.0/bin/kani-compiler exited with status exit status: 101

[zhassan-aws]

This following program is sufficient to produce a crash:

#[kani::proof]
fn main() {
    struct Foo(u32);
    let f1 = Foo(0x600);
}

when run as follows:

$ RUSTFLAGS="-Zmir-opt-level=2" kani iss2725.rs 
Kani Rust Verifier 0.35.0 (standalone)
warning: unused variable: `f1`
 --> iss2725.rs:4:9
  |
4 |     let f1 = Foo(0x600);
  |         ^^ help: if this is intentional, prefix it with an underscore: `_f1`
  |
  = note: `#[warn(unused_variables)]` on by default

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs:54:17:
Unhandled VarDebugInfoContents::Composite
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: main
main
[Kani] current codegen location: Loc { file: "/home/ubuntu/examples/iss2725.rs", function: None, start_line: 2, start_col: Some(1), end_line: 2, end_col: Some(10) }
warning: 1 warning emitted

error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101

This crash is different from the original one though (requires handling VarDebugInfoContents::Composite here).

[matthiaskrgr]

triage: still crashing with 0.40