ICE: unable to find field 0 for type StructTag (never_type)

[matthiaskrgr]

I tried this code:

#![feature(never_type)]
#[derive(Copy, Clone)]
pub enum E {
    A(!),
}
pub union U {
    u: (),
    e: E,
}


#[kani::proof]
fn main() {
    let E::A(ref _a) = unsafe { &(&U { u: () }).e };
}

using the following command line invocation:

cargo kani 

with Kani version: 0.56.0

I expected to see this happen: explanation

Instead, this happened: explanation

Kani Rust Verifier 0.56.0 (cargo plugin)
   Compiling kani v0.1.0 (/tmp/kani)
thread 'rustc' panicked at /__w/kani/kani/cprover_bindings/src/goto_program/expr.rs:740:13:
internal error: entered unreachable code: unable to find field 0 for type StructTag("tag-_305974959086658262508942713228466380997")
stack backtrace:
error: internal compiler error: Kani unexpectedly panicked at panicked at /__w/kani/kani/cprover_bindings/src/goto_program/expr.rs:740:13:
                                internal error: entered unreachable code: unable to find field 0 for type StructTag("tag-_305974959086658262508942713228466380997").

   0:     0x7763d9b1105a - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::ha689401f443fba58
   1:     0x7763da203426 - core::fmt::write::h09af537ef9d31c38
   2:     0x7763db3d8851 - std::io::Write::write_fmt::he95fb0c4685d97a6
   3:     0x7763d9b10eb2 - std::sys::backtrace::BacktraceLock::print::h7a83d27b793c4347
   4:     0x7763d9b133d1 - std::panicking::default_hook::{{closure}}::h954d5693366e5d11
   5:     0x7763d9b13204 - std::panicking::default_hook::hcd4d1d9e834fb485
   6:     0x5cf9b5491025 - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::he03cf627f70b6494
   7:     0x5cf9b5491533 - kani_compiler::session::JSON_PANIC_HOOK::{{closure}}::{{closure}}::h0cc63ddea8fb6636
   8:     0x5cf9b54788ea - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hb57347180f304fe9
   9:     0x7763d9b13ae8 - std::panicking::rust_panic_with_hook::hed093b35b993a1c7
  10:     0x7763d9b138ba - std::panicking::begin_panic_handler::{{closure}}::hd39c03c25db5675d
  11:     0x7763d9b11509 - std::sys::backtrace::__rust_end_short_backtrace::h6d39914f0d7b34fe
  12:     0x7763d9b1357c - rust_begin_unwind
  13:     0x7763d68bdcc0 - core::panicking::panic_fmt::ha518594d9318f161
  14:     0x5cf9b537e969 - cprover_bindings::goto_program::expr::Expr::member::h7b8c60b881438cc3
  15:     0x5cf9b52890e1 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection::h62be44933e802843
  16:     0x5cf9b528c5bd - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_stable::ha69dff746f75b336
  17:     0x5cf9b528b63f - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_ref_stable::he708169671f0b166
  18:     0x5cf9b5291cd8 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_stable::hde3d113caf472bf4
  19:     0x5cf9b529df39 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::hc9f0803f88240fd7
  20:     0x5cf9b52b4c40 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::ha504701bf9fca083
  21:     0x5cf9b53e90cf - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::hfba6fa9809da6115
  22:     0x5cf9b53a5f07 - rustc_smir::rustc_internal::run::he6782047d4590d05
  23:     0x5cf9b53eb558 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::ha6a0f43a9dd96aec
  24:     0x7763db22e770 - <rustc_interface[9081e2b11a975511]::queries::Linker>::codegen_and_build_linker
  25:     0x7763daf49f8b - rustc_interface[9081e2b11a975511]::interface::run_compiler::<core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>, rustc_driver_impl[24270441c709375b]::run_compiler::{closure#0}>::{closure#1}
  26:     0x7763dafeb8d0 - std[30db60597c87498f]::sys::backtrace::__rust_begin_short_backtrace::<rustc_interface[9081e2b11a975511]::util::run_in_thread_with_globals<rustc_interface[9081e2b11a975511]::util::run_in_thread_pool_with_globals<rustc_interface[9081e2b11a975511]::interface::run_compiler<core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>, rustc_driver_impl[24270441c709375b]::run_compiler::{closure#0}>::{closure#1}, core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>>::{closure#0}, core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>>
  27:     0x7763dafebf3a - <<std[30db60597c87498f]::thread::Builder>::spawn_unchecked_<rustc_interface[9081e2b11a975511]::util::run_in_thread_with_globals<rustc_interface[9081e2b11a975511]::util::run_in_thread_pool_with_globals<rustc_interface[9081e2b11a975511]::interface::run_compiler<core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>, rustc_driver_impl[24270441c709375b]::run_compiler::{closure#0}>::{closure#1}, core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>>::{closure#0}, core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2ef2d91bd42ab161]::result::Result<(), rustc_span[6b75f413cb27e6ac]::ErrorGuaranteed>>::{closure#1} as core[2ef2d91bd42ab161]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  28:     0x7763dafec32b - std::sys::pal::unix::thread::Thread::new::thread_start::h44e9704e75fad799
  29:     0x7763d54a339d - <unknown>
  30:     0x7763d552849c - <unknown>
  31:                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
_RNvCszMSQ9zntzn_4kani4main
[Kani] current codegen location: Loc { file: "src/main.rs", function: None, start_line: 13, start_col: Some(1), end_line: 13, end_col: Some(10), pragmas: [] }
error: could not compile `kani` (bin "kani")

Caused by:
  process didn't exit successfully: `/home/matthias/.cargo/bin/sccache /home/matthias/.kani/kani-0.56.0/bin/kani-compiler --crate-name kani --edition=2021 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=319 --crate-type bin --emit=dep-info,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs)' --check-cfg 'cfg(feature, values())' -C metadata=dc18e5818b59b867 -C extra-filename=-dc18e5818b59b867 --out-dir /tmp/kani/target/kani/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=/tmp/kani/target/kani/x86_64-unknown-linux-gnu/debug/incremental -L dependency=/tmp/kani/target/kani/x86_64-unknown-linux-gnu/debug/deps -L dependency=/tmp/kani/target/kani/debug/deps -Cllvm-args=--reachability=harnesses -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /home/matthias/.kani/kani-0.56.0 -L /home/matthias/.kani/kani-0.56.0/lib --extern kani --extern 'noprelude:std=/home/matthias/.kani/kani-0.56.0/lib/libstd.rlib' -Ctarget-cpu=native -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers '--check-cfg=cfg(kani)' --kani-compiler '-Cllvm-args=--check-version=0.56.0 --log-level=warn --assertion-reach-checks'` (exit status: 101)
error: Failed to compile `kani` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at /__w/kani/kani/cprover_bindings/src/goto_program/expr.rs:740:13:
                                internal error: entered unreachable code: unable to find field 0 for type StructTag("tag-_305974959086658262508942713228466380997").