Failure: Unexpected ShallowInitBox

[R1kM]

Charon commit e0b2b31 aborts on the following code with error message Compilation failed: error: Unexpected ShallowInitBox``

use std::vec;

pub struct Error {
    messages: Vec<u8>,
}

pub struct IntoIter {
  messages: vec::IntoIter<u8>
}

impl Iterator for IntoIter {
    type Item = Error;

    fn next(&mut self) -> Option<Self::Item> {
        Some(Error {
            messages: vec![self.messages.next()?],
        })
    }
}

[Nadrieril]

What happens is that an empty box is allocated, and then in one of the subsequent branches the box is initialized with a value (it is not initialized in other branches). In this case I would like to use Box::new_uninit() and Box::write() to separate the two steps.

[Nadrieril]

Minimized:

fn next(b: bool) -> Option<Vec<u8>> {
    let vec = vec![if b { 42 } else { return None }];
    Some(vec)
}

The MIR looks like:

fn next(_1: bool) -> Option<Vec<u8>> {
    debug b => _1;
    let mut _0: std::option::Option<std::vec::Vec<u8>>;
    let _2: std::vec::Vec<u8>;
    let mut _3: std::boxed::Box<[u8]>;
    let mut _4: std::boxed::Box<[u8; 1]>;
    let mut _5: usize;
    let mut _6: usize;
    let mut _7: *mut u8;
    let mut _8: std::boxed::Box<[u8; 1]>;
    let mut _9: *const [u8; 1];
    scope 1 {
        debug vec => _2;
    }

    bb0: {
        _5 = SizeOf([u8; 1]);
        _6 = AlignOf([u8; 1]);
        // Allocate the box without initializing its contents
        _7 = alloc::alloc::exchange_malloc(move _5, move _6) -> [return: bb1, unwind continue];
    }

    bb1: {
        _8 = ShallowInitBox(move _7, [u8; 1]);
        switchInt(copy _1) -> [0: bb3, otherwise: bb2];
    }

    bb2: {
        _9 = copy (((_8.0: std::ptr::Unique<[u8; 1]>).0: std::ptr::NonNull<[u8; 1]>).0: *const [u8; 1]);
        // Initialize the contents only in this branch
        (*_9) = [const 42_u8];
        _4 = move _8;
        _3 = move _4 as std::boxed::Box<[u8]> (PointerCoercion(Unsize));
        _2 = slice::<impl [u8]>::into_vec::<std::alloc::Global>(move _3) -> [return: bb4, unwind continue];
    }

    bb3: {
        _0 = Option::<Vec<u8>>::None;
        drop(_8) -> [return: bb5, unwind continue];
    }

    bb4: {
        _0 = Option::<Vec<u8>>::Some(move _2);
        goto -> bb5;
    }

    bb5: {
        return;
    }
}