Bug: Wrong Box structure unpacking in `--mir elaborated`

[ssyram]

The following codes:

struct Fields {
  a: i32,
  b: String,
}
fn use_box(b: Box<Fields>) {
  let str = b.b;
  assert!(str.len() > 0);
}
fn main() { }

When run with ./charon/bin/charon rustc --preset=eurydice --mir elaborated -- test.rs, it produces LLBC that is quite strange, as the following:

fn use_box(@1: alloc::boxed::Box<Fields>[{built_in impl MetaSized for Fields}, {built_in impl Sized for Global}])
{
    ...
    let b@1: alloc::boxed::Box<Fields>[{built_in impl MetaSized for Fields}, {built_in impl Sized for Global}]; // arg #1
    ...
    let @8: *const Fields; // anonymous local
    ...
    @8 := transmute<NonNull<Fields>, *const Fields>(copy ((*(b@1)).0))
    ...
}

This is strange:

• the deref for b@1 directly produces should result in Field? But after the deref it further access the first field, seemingly treated (*(b@1)) as just the Box type?
• Further, the casting from NonNull to *const is also strange -- it should be just a field access?

[ssyram]

BTW, in Eurydice, we now also like the idea of Builtin Box type: we can conveniently treat Box<T> as just T *.

[Nadrieril]

Yeah this is one of the things we need to reconstruct in Charon as part of supporting elaborated MIR properly. This is tracked in #543. Thanks for the bug report though, it's nice to have an issue for that.

[ssyram]

Thanks! Seems like a while away from fixing. To temporarily handle this bug, I've implemented a new pattern in my branch of Eurydice. At least now it functions as before.

[Nadrieril]

It seems rather easy to fix but that's indeed not a priority if you have a workaround.

[ssyram]

Sure, the current priority for us is still to properly drop.