Skip to content
New issue

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

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

Already on GitHub? # to your account

DST example fails to codegen #566

Closed
adpaco-aws opened this issue Oct 19, 2021 · 1 comment · Fixed by #1880
Closed

DST example fails to codegen #566

adpaco-aws opened this issue Oct 19, 2021 · 1 comment · Fixed by #1880
Assignees
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Milestone

Comments

@adpaco-aws
Copy link
Contributor

The following example from The Rustonomicon/Data Layout/Exotically Sized Types/47.rs shown below

// compile-flags: --edition 2018
#![allow(unused)]
struct MySuperSliceable<T: ?Sized> {
    info: u32,
    data: T,
}

pub fn main() {
    let sized: MySuperSliceable<[u8; 8]> = MySuperSliceable {
        info: 17,
        data: [0; 8],
    };

    let dynamic: &MySuperSliceable<[u8]> = &sized;

    // prints: "17 [0, 0, 0, 0, 0, 0, 0, 0]"
    println!("{} {:?}", dynamic.info, &dynamic.data);
}

fails to codegen with

thread 'rustc' panicked at 'Only an array can be cast to a slice.  Found types Adt(MySuperSliceable, [[u8; 8]]) and Adt(MySuperSliceable, [[u8]])', compiler/rustc_codegen_rmc/src/codegen/rvalue.rs:1076:37
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
@zhassan-aws
Copy link
Contributor

Still crashes with the same signature as of af11d38d93a.

@celinval celinval self-assigned this Mar 22, 2022
@celinval celinval moved this to In Progress in Kani v0.3 May 19, 2022
@celinval celinval assigned jaisnan and unassigned celinval Jun 28, 2022
@jaisnan jaisnan added this to Kani v0.8 Aug 2, 2022
@celinval celinval self-assigned this Nov 1, 2022
celinval added a commit that referenced this issue Nov 2, 2022
For now I just moved the reachability code to this new module. As a follow up PR, I am planning to move the unsized coercion related code into a separate module so it can be used to refactor and fix codegen casting logic (related issues #1531, #566, and #1528) .
celinval added a commit to celinval/kani-dev that referenced this issue Nov 2, 2022
We currently have a few issues with how we are generating code for
casting (model-checking#566, and model-checking#1528). The structure of the code is also hard to
understand and maintain (see model-checking#1531 for more details).

This PR is the first part of the fix I developed.
This change moves the coercion specific code to its own module and it
introduces an iterator that traverses the coercion path.
@celinval celinval moved this to In Progress in Kani 0.15 Nov 2, 2022
@celinval celinval added this to the Maintenance milestone Nov 2, 2022
@celinval celinval removed Area: build [F] Crash Kani crashed labels Nov 9, 2022
@celinval celinval added [F] Crash Kani crashed and removed T- MLP Should Have labels Nov 9, 2022
celinval added a commit that referenced this issue Nov 9, 2022
We currently have a few issues with how we are generating code for casting (#566, and #1528). The structure of the code is also hard to understand and maintain (see #1531 for more details).

This PR is the first part of the fix I developed. This change moves the coercion specific code to its own module and it introduces an iterator that traverses the coercion path.
celinval added a commit to celinval/kani-dev that referenced this issue Nov 9, 2022
Fix issues with how we are generating code for casting (model-checking#566, and model-checking#1528).

Restructure the unsize casting to be done in one pass instead with
deep recursion (model-checking#1531).

This also reuses the code from the reachability analysis, so we don't
have to keep two ways of traversing the same structure.
celinval added a commit to celinval/kani-dev that referenced this issue Nov 9, 2022
Fix issues with how we are generating code for casting (model-checking#566, and model-checking#1528).

Restructure the unsize casting to be done in one pass instead with
deep recursion (model-checking#1531).

This also reuses the code from the reachability analysis, so we don't
have to keep two ways of traversing the same structure.
celinval added a commit that referenced this issue Nov 14, 2022
Fix issues with how we are generating code for casting (#566, and #1528).

Restructure the unsize casting to be done in one pass instead with deep recursion (#1531). This also reuses the code from the reachability analysis, so we don't have to keep two ways of traversing the same structure.
Repository owner moved this from In Progress to Done in Kani v0.3 Nov 14, 2022
@celinval celinval moved this to Done in Kani v0.8 Nov 14, 2022
Repository owner moved this from In Progress to Done in Kani 0.15 Nov 14, 2022
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
No open projects
Status: Done
Status: Done
Status: Done
Development

Successfully merging a pull request may close this issue.

4 participants