Skip to content

ICE: Can't apply .member operation to ... #2256

New issue
New issue
Closed
Bug
#5006
Closed
ICE: Can't apply .member operation to ...#2256
Bug
#5006
Labels
[C] BugThis is a bug. Something isn't working.[F] CrashKani crashed
Milestone
Autoharness

Description

@matthiaskrgr
matthiaskrgr
opened on Mar 2, 2023

I tried this code:

#![feature(extern_types)]

use std::ptr::addr_of;

extern "C" {
    type Opaque;
}

unsafe impl Sync for Opaque {}

#[repr(C)]
pub struct List<T> {
    len: usize,
    data: [T; 0],
    tail: Opaque,
}

#[repr(C)]
pub struct ListImpl<T, const N: usize> {
    len: usize,
    data: [T; N],
}

impl<T> List<T> {
    const fn as_slice(&self) -> &[T] {
        unsafe {
            let ptr = addr_of!(self.tail) as *const T;
            std::slice::from_raw_parts(ptr, self.len)
        }
    }
}

impl<T, const N: usize> ListImpl<T, N> {
    const fn as_list(&self) -> &List<T> {
        unsafe { std::mem::transmute(self) }
    }
}

pub static A: ListImpl<u128, 3> = ListImpl {
    len: 3,
    data: [5, 6, 7],
};
pub static A_REF: &'static List<u128> = A.as_list();


#[kani::proof]
fn main() {
    assert_eq!(A_REF.as_slice(), &[5, 6, 7]);
}

using the following command line invocation:

kani file.rs

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

thread '<unnamed>' panicked at 'Can't apply .member operation to
	Expr { value: Symbol { identifier: "_RNvMs_Csbvss9KOnXkz_1aINtB4_4ListoE8as_sliceB4_::1::var_1::self" }, typ: Pointer { typ: StructTag("tag-_14785732211509494010") }, location: None }
	data', /home/runner/work/kani/kani/cprover_bindings/src/goto_program/expr.rs:653:9
stack backtrace:
   0:     0x7f32fa5667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f32fa5667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f32fa5667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7f32fa5667da - <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:     0x7f32fa5c92ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7f32fa556c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7f32fa5665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7f32fa5665a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7f32fa5692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7f32fa56902b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x5614bcbaeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x5614bcb04f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7f32fa569b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7f32fa569b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x7f32fa5698a9 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:579:13
  15:     0x7f32fa566c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
  16:     0x7f32fa5695b2 - rust_begin_unwind
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
  17:     0x7f32fa5c5cd3 - core::panicking::panic_fmt::hbacb72817da3b060
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
  18:     0x5614bcb22c15 - cprover_bindings::goto_program::expr::Expr::member::h45935a5f8bc82b3d
  19:     0x5614bcac5dfe - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection::hdcf315eeaf354832
  20:     0x5614bcac8519 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::h38d104924b36ba37
  21:     0x5614bcac7568 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_ref::h4b77c777dff90545
  22:     0x5614bcac8fbb - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h57a2cf71297ecf62
  23:     0x5614bcad8080 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h4c6e1c8bf226a338
  24:     0x5614bca7ef10 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
  25:     0x5614bcb0abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
  26:     0x5614bcb964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  27:     0x7f32fca86fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  28:     0x7f32fca86ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  29:     0x7f32fca847a6 - <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>>
  30:     0x7f32fca81a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  31:     0x7f32fca80f67 - <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>>
  32:     0x7f32fca7bf88 - 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}>
  33:     0x7f32fca7ba75 - <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>>
  34:     0x7f32fca7b062 - 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>>
  35:     0x7f32fd0ec49e - <<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}
  36:     0x7f32fe5da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  37:     0x7f32fe5da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  38:     0x7f32fe5da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  39:     0x7f32fa305bb5 - <unknown>
  40:     0x7f32fa387d90 - <unknown>
  41:                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: List::<u128>::as_slice
_RNvMs_Csbvss9KOnXkz_1aINtB4_4ListoE8as_sliceB4_
[Kani] current codegen location: Loc { file: "/home/matthias/vcs/github/icemaker/kani/a.rs", function: None, start_line: 25, start_col: Some(5), end_line: 25, end_col: Some(37) }
error: /home/matthias/.kani/kani-0.22.0/bin/kani-compiler exited with status exit status: 101

Activity

  1. matthiaskrgr
    added
    [C] BugThis is a bug. Something isn't working.
    on Mar 2, 2023
  2. zhassan-aws
    added
    [F] CrashKani crashed
    on Mar 2, 2023

  3. matthiaskrgr commented on Nov 12, 2023

    @matthiaskrgr
    matthiaskrgr
    on Nov 12, 2023
    ContributorAuthor

    Still crashing with 0.40

  4. celinval
    self-assigned this
    on Nov 15, 2024

  5. celinval commented on Nov 15, 2024

    @celinval
    celinval
    on Nov 15, 2024
    Contributor

    Need to add this test and validate that #3644 fixes this issue

  6. carolynzech commented on Dec 2, 2024

    @carolynzech
    carolynzech
    on Dec 2, 2024
    Contributor

    #3644 does not fix this issue--I ran on the most recent of Kani and got (abbreviated for brevity):

    cmzech@80a9971b5e20 playground % RUST_BACKTRACE=1 cargo kani
Kani Rust Verifier 0.56.0 (cargo plugin)
   Compiling playground v0.1.0 (/Users/cmzech/playground)
error: internal compiler error: Kani unexpectedly panicked at panicked at /Users/cmzech/kani/cprover_bindings/src/goto_program/expr.rs:733:9:
                                Can't apply .member operation to
                                    Expr { value: Symbol { identifier: "_RNvMs_CsfJ1dmgQudhL_10playgroundINtB4_4ListoE8as_sliceB4_::1::var_1::self" }, typ: Pointer { typ: StructTag("tag-_52126446309227075690537447433486615545") }, location: None, size_of_annotation: None }
                                    data.

thread 'rustc' panicked at /Users/cmzech/kani/cprover_bindings/src/goto_program/expr.rs:733:9:
Can't apply .member operation to
        Expr { value: Symbol { identifier: "_RNvMs_CsfJ1dmgQudhL_10playgroundINtB4_4ListoE8as_sliceB4_::1::var_1::self" }, typ: Pointer { typ: StructTag("tag-_52126446309227075690537447433486615545") }, location: None, size_of_annotation: None }
        data
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: cprover_bindings::goto_program::expr::Expr::member
             at /Users/cmzech/kani/cprover_bindings/src/goto_program/expr.rs:733:9
   3: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:476:25
...

    The third line of the stack backtrace points here:

    kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

    Lines 476 to 481 in aaf34f3

    inner_goto_expr
    .member("data", &self.symbol_table)
    // In the case of a vtable fat pointer, this data member is a void pointer,
    // so ensure the pointer has the correct type before dereferencing it.
    .cast_to(self.codegen_ty_stable(inner_mir_typ).to_pointer())
    .dereference()

    which #3644 doesn't change.

  7. celinval
    removed their assignment
    on Jan 24, 2025
  8. feliperodri
    added the
    Bug
    issue type on Apr 1, 2026

  9. feliperodri commented on Sep 25, 2026

    @feliperodri
    feliperodri
    on Sep 25, 2026
    Member

    This also aborts kani autoharness. Verified against main (de756c9): running kani autoharness -Z autoharness on this reproducer panics at cprover_bindings/src/goto_program/expr.rs:907 with Can't apply .member operation to.

    Worth knowing because the blast radius is bigger than the report suggests: with a manual harness this costs you one harness, but under autoharness a single function like this aborts the whole crate sweep, so nothing in the crate gets verified. Adding it to the Autoharness milestone for that reason.

  10. feliperodri
    added this to the Autoharness milestone on Sep 25, 2026
  11. feliperodri
    closed this as completedin #5006on Oct 22, 2026
  12. paulocsanz
    added a commit that references this issue on Oct 23, 2026

    Fix seven compiler crashes found by @nuczyc (model-checking#5006)

    947fcec
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.[F] CrashKani crashed

    Type

    Bug

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions