ICE: entered unreachable code: Only expected constant index for arrays and slices: also found it for: *mut [isize]

[matthiaskrgr]

I tried this code:

// run-pass

#![allow(unused_variables)]

#[kani::proof]
pub fn main() {
    let x = &[1, 2, 3, 4, 5];
    let x: &[isize] = &[1, 2, 3, 4, 5];
    if !x.is_empty() {
        let el = match x {
            &[1, ref tail @ ..] => &tail[0],
            _ => unreachable!()
        };
        println!("{}", *el);
    }
}

using the following command line invocation:

`RUSTFLAGS="-Zmir-opt-level=2" kani vec-matching-legal-tail-element-borrow.rs`

with Kani version: 0.34.0

I expected to see this happen: explanation

Instead, this happened: explanation

Kani Rust Verifier 0.34.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:741:18:
internal error: entered unreachable code: Only expected constant index for arrays and slices: also found it for:
	*mut [isize]
stack backtrace:
   0:     0x7f4bc6b6319c - std::backtrace_rs::backtrace::libunwind::trace::haf256adafafbe58d
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f4bc6b6319c - std::backtrace_rs::backtrace::trace_unsynchronized::hfe1951132ff691c0
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f4bc6b6319c - std::sys_common::backtrace::_print_fmt::h9a0fe52434930c36
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7f4bc6b6319c - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h24adccbf3e1ada83
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f4bc6bc989c - core::fmt::rt::Argument::fmt::h18ba555e398addfe
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/fmt/rt.rs:138:9
   5:     0x7f4bc6bc989c - core::fmt::write::hbf3ee2d80be74759
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/fmt/mod.rs:1094:21
   6:     0x7f4bc6b5590e - std::io::Write::write_fmt::hfc2b3251522ff943
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/io/mod.rs:1714:15
   7:     0x7f4bc6b62f85 - std::sys_common::backtrace::_print::hfdc8ddb5f3ddee36
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7f4bc6b62f85 - std::sys_common::backtrace::print::h316f264b298c7a30
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7f4bc6b660da - std::panicking::panic_hook_with_disk_dump::{{closure}}::h136bbb963feeea4a
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:278:22
  10:     0x7f4bc6b65d73 - std::panicking::panic_hook_with_disk_dump::hd91a018a982a84f7
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:312:9
  11:     0x55a48c14771d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::hbdcd1e2153d1f24b
  12:     0x55a48c145e63 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hc68eaec26ff64861
  13:     0x7f4bc6b66980 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hd99b1fe24ccd07b5
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2021:9
  14:     0x7f4bc6b66980 - std::panicking::rust_panic_with_hook::h1593161995c9c003
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:733:13
  15:     0x7f4bc6b66707 - std::panicking::begin_panic_handler::{{closure}}::h6b4a934e37237346
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:621:13
  16:     0x7f4bc6b636d6 - std::sys_common::backtrace::__rust_end_short_backtrace::h365e31c6291fdffa
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7f4bc6b66452 - rust_begin_unwind
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:617:5
  18:     0x7f4bc6bc5c53 - core::panicking::panic_fmt::hbd2564497e278309
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/panicking.rs:67:14
  19:     0x55a48c0e909b - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection::h8ef94609a9faa773
  20:     0x55a48c0ea182 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::hca2771dc57ddaeac
  21:     0x55a48c0e96eb - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_ref::hf82258f676decb3a
  22:     0x55a48c0ec328 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h2d1feaaf678662c2
  23:     0x55a48c0f9f93 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::hbe3635206b55fa31
  24:     0x55a48c0b2860 - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::had8f57135e8154af
  25:     0x55a48c10f87b - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::he08100d10d5a8739
  26:     0x55a48c1dbf7e - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h1c7461510b84019a
  27:     0x55a48c1e09e5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h72f45c460ba9f3e3
  28:     0x7f4bc9094dc2 - <rustc_session[83a530cc07544870]::session::Session>::time::<alloc[b2a4fa84f81d55c8]::boxed::Box<dyn core[8e2a8f22f3da315]::any::Any>, rustc_interface[b10bd5cb1b971de9]::passes::start_codegen::{closure#0}>
  29:     0x7f4bc909490b - rustc_interface[b10bd5cb1b971de9]::passes::start_codegen
  30:     0x7f4bc908ef1a - <rustc_middle[32728bc096d751c7]::ty::context::GlobalCtxt>::enter::<<rustc_interface[b10bd5cb1b971de9]::queries::Queries>::ongoing_codegen::{closure#0}, core[8e2a8f22f3da315]::result::Result<alloc[b2a4fa84f81d55c8]::boxed::Box<dyn core[8e2a8f22f3da315]::any::Any>, rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
  31:     0x7f4bc908df53 - <rustc_interface[b10bd5cb1b971de9]::interface::Compiler>::enter::<rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}::{closure#2}, core[8e2a8f22f3da315]::result::Result<core[8e2a8f22f3da315]::option::Option<rustc_interface[b10bd5cb1b971de9]::queries::Linker>, rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
  32:     0x7f4bc9086fc8 - std[b7e5a9c79ea9fbed]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[b10bd5cb1b971de9]::util::run_in_thread_pool_with_globals<rustc_interface[b10bd5cb1b971de9]::interface::run_compiler<core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>, rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}>::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
  33:     0x7f4bc908674e - <<std[b7e5a9c79ea9fbed]::thread::Builder>::spawn_unchecked_<rustc_interface[b10bd5cb1b971de9]::util::run_in_thread_pool_with_globals<rustc_interface[b10bd5cb1b971de9]::interface::run_compiler<core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>, rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}>::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#1} as core[8e2a8f22f3da315]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  34:     0x7f4bc6b71125 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hb18992c0c074fb04
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2007:9
  35:     0x7f4bc6b71125 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::ha4998f5f9033c44e
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2007:9
  36:     0x7f4bc6b71125 - std::sys::unix::thread::Thread::new::thread_start::h3370231efa79af31
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys/unix/thread.rs:108:17
  37:     0x7f4bc668c9eb - <unknown>
  38:     0x7f4bc6710ebc - <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/kani/vec-matching-legal-tail-element-borrow.rs", function: None, start_line: 6, start_col: Some(1), end_line: 6, end_col: Some(14) }
error: /home/matthias/.kani/kani-0.34.0/bin/kani-compiler exited with status exit status: 101

[matthiaskrgr]

This is fixed with kani 0.40
Oops, nevermind, forgot the rustflags :(