ICE: assertion failure: Expected constant allocation for ..., but got a mutable instead #2730
Description
I tried this code:
static mut FOO: Foo = Foo {
field: &mut [42] as *mut [i32] as *mut i32,
};
struct Foo {
field: *mut i32,
}
unsafe impl Sync for Foo {}
#[kani::proof]
fn main() {
assert_eq!(unsafe { *FOO.field = 69; *FOO.field }, 69);
}using the following command line invocation:
RUSTFLAGS="-Zmir-opt-level=2" RUST_BACKTRACE=full RUSTC_WRAPPER="" cargo kani
with Kani version: 0.35.0
I expected to see this happen: explanation
Instead, this happened: explanation
Kani Rust Verifier 0.35.0 (cargo plugin)
Compiling kani v0.1.0 (/tmp/kani)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:548:9:
assertion `left == right` failed: Expected constant allocation for `Some("kani.d1f1d340b3a1dad::kani::alloc4")`, but got a mutable instead
left: Mut
right: Not
error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:548:9:
assertion `left == right` failed: Expected constant allocation for `Some("kani.d1f1d340b3a1dad::kani::alloc4")`, but got a mutable instead
left: Mut
right: Not.
stack backtrace:
0: 0x7f4811b6329c - std::backtrace_rs::backtrace::libunwind::trace::h28e11dce06475f43
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
1: 0x7f4811b6329c - std::backtrace_rs::backtrace::trace_unsynchronized::h21f22a3bfa3fb013
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
2: 0x7f4811b6329c - std::sys_common::backtrace::_print_fmt::hafc6985e93f76ae0
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:67:5
3: 0x7f4811b6329c - <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: 0x7f4811bc93ec - core::fmt::rt::Argument::fmt::h9b33518f8511caca
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/fmt/rt.rs:138:9
5: 0x7f4811bc93ec - core::fmt::write::h67226f5192a09eca
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/fmt/mod.rs:1094:21
6: 0x7f4811b55d2e - std::io::Write::write_fmt::h744b3076c6ca0e52
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/io/mod.rs:1714:15
7: 0x7f4811b63084 - std::sys_common::backtrace::_print::h4bcc2e79e4348aa6
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:47:5
8: 0x7f4811b63084 - std::sys_common::backtrace::print::h74142c12abe5e25d
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:34:9
9: 0x7f4811b6617a - std::panicking::panic_hook_with_disk_dump::{{closure}}::h7d3e65abd6cf3378
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:278:22
10: 0x7f4811b65e67 - std::panicking::panic_hook_with_disk_dump::h5bbd6ac133545f46
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:312:9
11: 0x55711b33f2dd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h5067a4a6926df452
12: 0x55711b33f5cd - kani_compiler::session::JSON_PANIC_HOOK::{{closure}}::{{closure}}::h449e03c79d4f70ea
13: 0x55711b33e463 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hbc7dbed47af55a6e
14: 0x7f4811b66a20 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hbc8f8f631658dcc9
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2021:9
15: 0x7f4811b66a20 - std::panicking::rust_panic_with_hook::h7b16b439ec100c23
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:733:13
16: 0x7f4811b667a7 - std::panicking::begin_panic_handler::{{closure}}::hd03f21e4b251a35c
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:621:13
17: 0x7f4811b637c6 - std::sys_common::backtrace::__rust_end_short_backtrace::he8aad725f5dd71ab
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:170:18
18: 0x7f4811b664f2 - rust_begin_unwind
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:617:5
19: 0x7f4811bc57f3 - core::panicking::panic_fmt::h37323eb5862b87ad
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/panicking.rs:67:14
20: 0x7f4811bc5d15 - core::panicking::assert_failed_inner::h203d73c9cdc85fdd
21: 0x55711b29ecff - core::panicking::assert_failed::h0dcfd4d42a3f4717
22: 0x55711b2e15f9 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_const_allocation::hfaf842eacfa5715e
23: 0x55711b2e0415 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_alloc_pointer::hc11591ed759f1d32
24: 0x55711b2e2a40 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_allocation_data::hd4d00d7c36cc76bd
25: 0x55711b2e198b - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_alloc_in_memory::h0613f33a5f8d3759
26: 0x55711b30ba04 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hb78fbbf93858f04a
27: 0x55711b3ceb75 - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h71130359840cd186
28: 0x55711b3d35a5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h25888e407b1b3e70
29: 0x7f481400d3c2 - <rustc_session[a6bdf9a4b51671a9]::session::Session>::time::<alloc[10a91b7ea9db36b6]::boxed::Box<dyn core[3ec4812ddef0ef93]::any::Any>, rustc_interface[39ac7ec62dd85acc]::passes::start_codegen::{closure#0}>
30: 0x7f481400cf1b - rustc_interface[39ac7ec62dd85acc]::passes::start_codegen
31: 0x7f4814007bba - <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>>
32: 0x7f4814007066 - <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>>
33: 0x7f4814004338 - 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>>
34: 0x7f4814003ac5 - <<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}
35: 0x7f4811b71225 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h5d092cb8decc581e
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2007:9
36: 0x7f4811b71225 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h88f1cce7655d0913
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2007:9
37: 0x7f4811b71225 - std::sys::unix::thread::Thread::new::thread_start::h775d92d70f807a4c
at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys/unix/thread.rs:108:17
38: 0x7f481168c9eb - <unknown>
39: 0x7f4811710dfc - <unknown>
40: 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_static: DefId(0:3 ~ kani[0d1f]::FOO)
[Kani] current codegen location: Loc { file: "/tmp/kani/src/main.rs", function: None, start_line: 1, start_col: Some(1), end_line: 1, end_col: Some(20) }
error: could not compile `kani` (bin "kani")
error: Failed to compile `kani` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:548:9:
assertion `left == right` failed: Expected constant allocation for `Some("kani.d1f1d340b3a1dad::kani::alloc4")`, but got a mutable instead
left: Mut
right: Not.