ICE: failed to get layout for, too big for arch

[matthiaskrgr]

I tried this code:

struct S<T> { x: [T; !0] }

pub fn f() -> usize {
    std::mem::size_of::<S<u8>>()
}

#[kani::proof]
fn main() {
    let x = f();
}

using the following command line invocation:

kani file.rs

with Kani version: kani 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

warning: unused variable: `x`
  --> 94961.rs:10:9
   |
10 |     let x = f();
   |         ^ help: if this is intentional, prefix it with an underscore: `_x`
   |
   = note: `#[warn(unused_variables)]` on by default

warning: field `x` is never read
 --> 94961.rs:2:15
  |
2 | struct S<T> { x: [T; !0] }
  |        -      ^
  |        |
  |        field in this struct
  |
  = note: `#[warn(dead_code)]` on by default

error: internal compiler error: kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:371:9: failed to get layout for `S<u8>`: values of the type `[u8; 18446744073709551615]` are too big for the current architecture

thread '<unnamed>' panicked at 'Box<dyn Any>', /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/compiler/rustc_errors/src/lib.rs:973:33
stack backtrace:
   0:     0x7f4bbe3667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f4bbe3667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f4bbe3667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7f4bbe3667da - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9271b09f3576b7e0
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f4bbe3c92ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7f4bbe356c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7f4bbe3665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7f4bbe3665a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7f4bbe3692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7f4bbe36902b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x558cf2baeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x558cf2b04f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7f4bbe369b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7f4bbe369b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x558cf2ba4f23 - std::panicking::begin_panic::{{closure}}::h429784b5bf999dc7
  15:     0x558cf2ba49a6 - std::sys_common::backtrace::__rust_end_short_backtrace::h9e612c1a00372269
  16:     0x558cf2a62656 - std::panicking::begin_panic::hf05c55b450963c46
  17:     0x558cf2b30f96 - std::panic::panic_any::hdda34431bdc38203
  18:     0x558cf2b2d87b - rustc_errors::HandlerInner::span_bug::h236ce07c1ef8f346
  19:     0x558cf2b2e240 - rustc_errors::Handler::span_bug::h4d51fe6d3766be6b
  20:     0x558cf2b877bb - rustc_middle::ty::context::tls::with_context_opt::h1360d9493b07c7d5
  21:     0x558cf2b87819 - rustc_middle::util::bug::opt_span_bug_fmt::hb0db4e7386f184f6
  22:     0x558cf2a63b77 - rustc_middle::util::bug::span_bug_fmt::h424192caf45f6812
  23:     0x558cf2aef3e5 - <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx as rustc_middle::ty::layout::LayoutOfHelpers>::handle_layout_err::h73e3fcce28cb6269
  24:     0x558cf2a75df7 - rustc_middle::ty::layout::LayoutOf::spanned_layout_of::{{closure}}::h42c66e2ed93375d5
  25:     0x558cf2a75d52 - rustc_middle::ty::layout::LayoutOf::spanned_layout_of::ha06bf1008b9988e1
  26:     0x558cf2aca735 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h57a2cf71297ecf62
  27:     0x558cf2ad8080 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h4c6e1c8bf226a338
  28:     0x558cf2a7ef10 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
  29:     0x558cf2b0abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
  30:     0x558cf2b964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  31:     0x7f4bc0886fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  32:     0x7f4bc0886ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  33:     0x7f4bc08847a6 - <rustc_interface[aec886e93b1add3f]::passes::QueryContext>::enter::<<rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  34:     0x7f4bc0881a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  35:     0x7f4bc0880f67 - <rustc_interface[aec886e93b1add3f]::interface::Compiler>::enter::<rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}::{closure#2}, core[6d94cc961ac87456]::result::Result<core[6d94cc961ac87456]::option::Option<rustc_interface[aec886e93b1add3f]::queries::Linker>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  36:     0x7f4bc087bf88 - rustc_span[ae2df7aa7c6c667b]::with_source_map::<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  37:     0x7f4bc087ba75 - <scoped_tls[db87656d258d017b]::ScopedKey<rustc_span[ae2df7aa7c6c667b]::SessionGlobals>>::set::<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  38:     0x7f4bc087b062 - std[acd1f573e90225f]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  39:     0x7f4bc0eec49e - <<std[acd1f573e90225f]::thread::Builder>::spawn_unchecked_<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#1} as core[6d94cc961ac87456]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  40:     0x7f4bc23da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  41:     0x7f4bc23da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  42:     0x7f4bc23da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  43:     0x7f4bbdfe6bb5 - <unknown>
  44:     0x7f4bbe068d90 - <unknown>
  45:                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: std::mem::size_of::<S<u8>>
_RINvNtCshQhm45nWocF_4core3mem7size_ofINtCsfo5SW6dqY4U_5_949611ShEEBC_
[Kani] current codegen location: Loc { file: "/home/runner/.rustup/toolchains/nightly-2022-12-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", function: None, start_line: 308, start_col: Some(1), end_line: 308, end_col: Some(35) }
error: aborting due to previous error; 2 warnings emitted

error: /home/matthias/.kani/kani-0.22.0/bin/kani-compiler exited with status exit status: 101

[zhassan-aws]

Thanks for the bug report. We should exit gracefully with an error like rustc does on this program:

$ rustc test.rs 
warning: unused variable: `x`
 --> test.rs:9:9
  |
9 |     let x = f();
  |         ^ help: if this is intentional, prefix it with an underscore: `_x`
  |
  = note: `#[warn(unused_variables)]` on by default

warning: field `x` is never read
 --> test.rs:1:15
  |
1 | struct S<T> { x: [T; !0] }
  |        -      ^
  |        |
  |        field in this struct
  |
  = note: `#[warn(dead_code)]` on by default

error: values of the type `[u8; 18446744073709551615]` are too big for the current architecture

error: aborting due to previous error; 2 warnings emitted

[matthiaskrgr]

Triage kani 0.40: still crashing

Kani Rust Verifier 0.40.0 (standalone)
warning: unused variable: `x`
 --> a.rs:9:9
  |
9 |     let x = f();
  |         ^ help: if this is intentional, prefix it with an underscore: `_x`
  |
  = note: `#[warn(unused_variables)]` on by default

warning: field `x` is never read
 --> a.rs:1:15
  |
1 | struct S<T> { x: [T; !0] }
  |        -      ^
  |        |
  |        field in this struct
  |
  = note: `#[warn(dead_code)]` on by default

error: internal compiler error: kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:340:9: failed to get layout for `S<u8>`: values of the type `[u8; usize::MAX]` are too big for the current architecture

thread 'rustc' panicked at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/compiler/rustc_errors/src/lib.rs:1000:33:
Box<dyn Any>
note: run with `RUST_BACKTRACE=1` environment variable to display a 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_function: std::mem::size_of::<S<u8>>
_RINvNtCs5k6HhVuWWKi_4core3mem7size_ofINtCsaxqAW6SeOYc_1a1ShEEBC_
[Kani] current codegen location: Loc { file: "/github/home/.rustup/toolchains/nightly-2023-10-31-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", function: None, start_line: 312, start_col: Some(1), end_line: 312, end_col: Some(35) }
error: aborting due to previous error; 2 warnings emitted

error: /home/matthias/.kani/kani-0.40.0/bin/kani-compiler exited with status exit status: 101