Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ICE: Kani compiler crashes due to incorrect handling of Adt with slice tail #3638

Open
celinval opened this issue Oct 23, 2024 · 0 comments · May be fixed by #3644
Open

ICE: Kani compiler crashes due to incorrect handling of Adt with slice tail #3638

celinval opened this issue Oct 23, 2024 · 0 comments · May be fixed by #3644
Assignees
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed

Comments

@celinval
Copy link
Contributor

I tried this code:

// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

#![feature(ptr_metadata)]

use std::ptr::NonNull;

#[derive(kani::Arbitrary)]
struct Wrapper<T: ?Sized>(usize, T);

#[cfg(kani)]
#[kani::proof]
fn main() {
    // Create a SampleTrait object from SampleStruct
    let original: Wrapper<[u8; 10]> = kani::any();
    let slice: &Wrapper<[u8]> = &original;

    // Get the raw data pointer and metadata for the trait object
    let slice_ptr = NonNull::new(slice as *const _ as *mut ()).unwrap();
    let metadata = std::ptr::metadata(slice);

    // Create NonNull<dyn SampleTrait> from the data pointer and metadata
    let nonnull: NonNull<Wrapper<[u8]>> =
        NonNull::from_raw_parts(slice_ptr, metadata);

}

using the following command line invocation:

kani slice_tail.rs

with Kani version: 0.56.0

I expected to see this happen: verification succeed

Instead, this happened: Kani compiler crashed

$ kani adt_slice.rs 
Kani Rust Verifier 0.56.0 (standalone)
thread 'rustc' panicked at /tmp/workspace/kani-project/kani/cprover_bindings/src/goto_program/expr.rs:733:9:
Can't apply .member operation to
	Expr { value: Symbol { identifier: "_RINvNtNtCsfIIKBCXq9GN_4core3ptr8metadata18from_raw_parts_mutINtCsgncW3vUYF2n_9adt_slice7WrapperShEuEBZ_::1::var_2::metadata" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }
	_vtable_ptr
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::ptr::from_raw_parts_mut::<Wrapper<[u8]>, ()>
_RINvNtNtCsfIIKBCXq9GN_4core3ptr8metadata18from_raw_parts_mutINtCsgncW3vUYF2n_9adt_slice7WrapperShEuEBZ_
[Kani] current codegen location: Loc { file: "/tmp/.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: 125, start_col: Some(1), end_line: 128, end_col: Some(12), pragmas: [] }
warning: 2 warnings emitted

error: /tmp/workspace/kani-project/kani/target/kani/bin/kani-compiler exited with status exit status: 101
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants