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::::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::::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::::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::::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::::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: 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::::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::::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::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::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::::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: ::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::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::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: ::codegen_crate at /home/user/workspace/kani-project/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:244:23 31: ::codegen_and_build_linker 32: 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_function: std::ptr::from_raw_parts::, ()> _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