ice: Expected '&[T]' to point to a single buffer #3021
Description
I tried this code:
// run-pass
// This does not reflect a stable guarantee (we guarantee very little for equality of pointers
// around `const`), but it would be good to understand what is happening if these assertions ever
// fail.
use std::ptr::NonNull;
use std::slice::from_raw_parts;
const PTR_U16: *const u16 = NonNull::dangling().as_ptr();
const CONST_U16_REF: &[u16] = unsafe { from_raw_parts(PTR_U16, 0) };
#[kani::proof]
fn main() {
let ptr_u16 = unsafe { from_raw_parts(PTR_U16, 0) }.as_ptr();
assert_eq!(ptr_u16, CONST_U16_REF.as_ptr());
}using the following command line invocation:
kani file.rs
with Kani version: 0.46.0
I expected to see this happen: explanation
Instead, this happened: explanation
Kani Rust Verifier 0.46.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:275:21:
assertion `left == right` failed: Expected `&[T]` to point to a single buffer
left: 0
right: 1
stack backtrace:
0: 0x7f46cc98be86 - std::backtrace_rs::backtrace::libunwind::trace::haa62de98ce20d13c
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
1: 0x7f46cc98be86 - std::backtrace_rs::backtrace::trace_unsynchronized::h4bc7f582e9f49dbd
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
2: 0x7f46cc98be86 - std::sys_common::backtrace::_print_fmt::h07d78988ae6e922d
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:68:5
3: 0x7f46cc98be86 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::he72c24e459b4aee4
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:44:22
4: 0x7f46cc9de740 - core::fmt::rt::Argument::fmt::h9ff3b213e1468f5f
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/fmt/rt.rs:142:9
5: 0x7f46cc9de740 - core::fmt::write::h0ab1f59280077a18
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/fmt/mod.rs:1120:17
6: 0x7f46cc97f7bf - std::io::Write::write_fmt::h2f48f6201433d434
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/io/mod.rs:1810:15
7: 0x7f46cc98bc64 - std::sys_common::backtrace::_print::h710dac96d5446d07
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:47:5
8: 0x7f46cc98bc64 - std::sys_common::backtrace::print::h22982b9f2c94c190
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:34:9
9: 0x7f46cc98e9f7 - std::panicking::default_hook::{{closure}}::h19052586580466eb
10: 0x7f46cc98e759 - std::panicking::default_hook::h9f3f4c25f2a49543
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:292:9
11: 0x56077078b29d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62bee1eb7956b9f6
12: 0x56077078aaa3 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h252d31e703366824
13: 0x7f46cc98f146 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h0ebb0eb5cf5e84f1
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2030:9
14: 0x7f46cc98f146 - std::panicking::rust_panic_with_hook::hb83cfb3ac729d1b2
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:785:13
15: 0x7f46cc98ee92 - std::panicking::begin_panic_handler::{{closure}}::hf6588d71adde3329
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:659:13
16: 0x7f46cc98c386 - std::sys_common::backtrace::__rust_end_short_backtrace::hfa69dd6720275711
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:171:18
17: 0x7f46cc98ebe4 - rust_begin_unwind
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:647:5
18: 0x7f46cc9dae45 - core::panicking::panic_fmt::h3d775185360585e3
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:72:14
19: 0x7f46cc9db4bf - core::panicking::assert_failed_inner::h0e5c67b40620ee84
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:337:23
20: 0x5607706c157f - core::panicking::assert_failed::hc10042bb9abc23bf
21: 0x5607707034a9 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_const_ptr::h8e34f4e7d832cc8a
22: 0x5607707015ee - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::try_codegen_constant::hf98efd98acfac45a
23: 0x560770700d86 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_allocation::h4cdc94a8511effd6
24: 0x5607707006aa - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand_stable::h669d4e8bb4fb2d55
25: 0x560770711abb - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_stable::h03604d81673e65d8
26: 0x56077071ec34 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h9ef1fd17419243a3
27: 0x560770736b18 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h70ea6b1d619c790d
28: 0x5607707f9e9a - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h179e069baadeebc1
29: 0x5607707b1430 - scoped_tls::ScopedKey<T>::set::h462dbe7b3063cb5c
30: 0x5607707e91a4 - rustc_smir::rustc_internal::init::hdab7351afa62793a
31: 0x5607707b4054 - stable_mir::compiler_interface::run::hdc01671daf50c78a
32: 0x5607707fd62e - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd5728f8a33105c7d
33: 0x7f46d146aff0 - rustc_interface[79a3a7c6d29fbb15]::passes::start_codegen
34: 0x7f46d146a75c - <rustc_interface[79a3a7c6d29fbb15]::queries::Queries>::codegen_and_build_linker
35: 0x7f46d177a44a - rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler::<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}
36: 0x7f46d19e5986 - std[da4468a6436061de]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_with_globals<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_pool_with_globals<rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>
37: 0x7f46d19e57b3 - <<std[da4468a6436061de]::thread::Builder>::spawn_unchecked_<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_with_globals<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_pool_with_globals<rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#1} as core[2f78b8535a2e64fa]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
38: 0x7f46cc998735 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hda2c57e98ef914e1
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2016:9
39: 0x7f46cc998735 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h4c1ca1ffb3984aed
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2016:9
40: 0x7f46cc998735 - std::sys::pal::unix::thread::Thread::new::thread_start::h6dfa281031503fa8
at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys/pal/unix/thread.rs:108:17
41: 0x7f46cc6729eb - <unknown>
42: 0x7f46cc6f67cc - <unknown>
43: 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: "issue-105536-const-val-roundtrip-ptr-eq.rs", function: None, start_line: 14, start_col: Some(1), end_line: 14, end_col: Some(10) }
error: /home/matthias/.kani/kani-0.46.0/bin/kani-compiler exited with status exit status: 101