Static `union` values can panic kani

[teskje]

Kani compilation can panic on static union type declarations.

I ran this code:

#![allow(dead_code)]

static FOO: Data = Data { a: [0; 3] };

union Data {
    a: [u8; 3],
    b: u16,
}

#[kani::proof]
fn main() {
    let _x = &FOO;
}

using the following command line invocation:

kani test.rs

with Kani version:

main (commit: 0b68df0)

I expected to see this happen: Kani does not crash.

Instead, this happened: Kani crashes:

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:958:9:
assertion `left == right` failed
  left: 32
 right: 24
stack backtrace:
   0: __rustc::rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::assert_failed_inner
   3: core::panicking::assert_failed
   4: cprover_bindings::goto_program::expr::Expr::transmute_to
   5: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_alloc_in_memory
   6: kani_compiler::codegen_cprover_gotoc::codegen::static_var::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_static
   7: std::thread::local::LocalKey<T>::with
   8: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
   9: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
  10: rustc_smir::rustc_internal::init
  11: scoped_tls::ScopedKey<T>::set
  12: rustc_smir::rustc_internal::run
  13: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
  14: <rustc_interface::queries::Linker>::codegen_and_build_linker
  15: rustc_interface::passes::create_and_enter_global_ctxt::<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>
  16: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

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: FOO
[Kani] current codegen location: Loc { file: "test.rs", function: None, start_line: 3, start_col: Some(1), end_line: 3, end_col: Some(17), pragmas: [] }

[teskje]

One likely way to encounter this panic in practice is by having a static std::sync::LazyLock, which is how we stumbled over this.

[carolynzech]

Thanks for filing an issue @teskje. I've reproduced this on my end; we'll look into it and get back to you.

[carolynzech]

Hi @teskje-- #4112 fixed this issue. You can wait until the next release of Kani (in ~3 weeks) or build from source if you'd like to use it sooner. Let us know if you have any more issues!