ICE: Kani compiler crashes when invoking from_raw_parts for slices #3615
Description
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: [] }