ICE: Kani compiler crashes when invoking from_raw_parts for slices

[celinval]

I tried this code:

#![feature(layout_for_ptr)]
#![feature(ptr_metadata)]

use std::ptr;
use std::mem::size_of_val_raw;

#[derive(Clone, Copy, kani::Arbitrary)]
struct Wrapper<T: ?Sized> {
    _size: usize,
    _value: T,
}

#[kani::proof]
pub fn check_size_of_overflows() {
    let var:  Wrapper<[u64; 4]> = kani::any();
    let fat_ptr: *const Wrapper<[u64]> = &var as *const _;
    let (thin_ptr, size) = fat_ptr.to_raw_parts();
    let new_size: usize = kani::any();
    let _new_ptr:  *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size);
}

using the following command line invocation:

kani my_slice.rs

with Kani version: 0.56.0

I expected to see this happen: Verification succeeded

Instead, this happened: Kani compiler crashed

Stack backtrace:

thread 'rustc' panicked at /home/user/workspace/kani-project/kani/cprover_bindings/src/goto_program/expr.rs:733:9:
Can't apply .member operation to
	Expr { value: Symbol { identifier: "_RINvNtNtCsfIIKBCXq9GN_4core3ptr8metadata14from_raw_partsINtCs1vxRXk47s7N_11size_of_dst7WrapperSyEuEBV_::1::var_2::metadata" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }
	_vtable_ptr
stack backtrace:
   0: rust_begin_unwind
   1: core::panicking::panic_fmt
   2: cprover_bindings::goto_program::expr::Expr::member
             at /home/user/workspace/kani-project/kani/cprover_bindings/src/goto_program/expr.rs:733:9
   3: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_aggregate
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:720:47
   4: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_stable
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:918:17
   5: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:66:29
   6: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:33:29
   7: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{{closure}}
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:70:52
   8: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:810:29
   9: core::iter::traits::double_ended::DoubleEndedIterator::rfold
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/double_ended.rs:308:21
  10: <core::iter::adapters::rev::Rev<I> as core::iter::traits::iterator::Iterator>::fold
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/rev.rs:64:9
  11: core::iter::traits::iterator::Iterator::for_each
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:813:9
  12: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:70:13
  13: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}::{{closure}}
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:163:39
  14: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::{{closure}}
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:66:13
  15: std::thread::local::LocalKey<T>::try_with
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:283:12
  16: std::thread::local::LocalKey<T>::with
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:260:9
  17: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:64:9
  18: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:162:29
  19: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:831:15
  20: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:135:29
  21: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:275:63
  22: rustc_smir::rustc_internal::init::{{closure}}
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:192:33
  23: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  24: rustc_smir::rustc_internal::init
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:192:5
  25: rustc_smir::rustc_internal::run::{{closure}}
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:223:53
  26: stable_mir::compiler_interface::run::{{closure}}
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/stable_mir/src/compiler_interface.rs:259:40
  27: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  28: stable_mir::compiler_interface::run
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/stable_mir/src/compiler_interface.rs:259:9
  29: rustc_smir::rustc_internal::run
             at /home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:223:5
  30: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:244:23
  31: <rustc_interface::queries::Linker>::codegen_and_build_linker
  32: rustc_interface::interface::run_compiler::<core::result::Result<(), rustc_span::ErrorGuaranteed>, 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_function: std::ptr::from_raw_parts::<Wrapper<[u64]>, ()>
_RINvNtNtCsfIIKBCXq9GN_4core3ptr8metadata14from_raw_partsINtCs1vxRXk47s7N_11size_of_dst7WrapperSyEuEBV_
[Kani] current codegen location: Loc { file: "/home/user/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/metadata.rs", function: None, start_line: 111, start_col: Some(1), end_line: 114, end_col: Some(14), pragmas: [] }

[carolynzech]

Once this is fixed, we should test whether the fix also resolves #2256

[celinval]

Once this is fixed, we should test whether the fix also resolves #2256

Good call! I think you are right