ICE: entered unreachable code: Only expected constant index for arrays and slices: also found it for: *mut [isize] #2682
Description
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