Add support for vec macro

[zhassan-aws]

The vec macro is convenient for creating vectors.

Currently, Charon fails to compile it, e.g.:

fn foo() {
    let _v = vec![1];
}

$ charon
   Compiling vec_macro v0.1.0 (/home/ubuntu/examples/aeneas/vec_macro)
error: Nullary operations are not supported
 --> src/main.rs:2:14
  |
2 |     let _v = vec![1];
  |              ^^^^^^^
  |
  = note: this error originates in the macro `vec` (in Nightly builds, run with -Z macro-backtrace for more info)

[ ERROR charon_driver:180] The extraction encountered 1 errors
error: could not compile `vec_macro` (bin "vec_macro") due to previous error

[Nadrieril]

The macro expands to:

fn foo() {
    let _v = <[_]>::into_vec(#[rustc_box] ::alloc::boxed::Box::new([1]));
}

That looks easy, unfortunately the #[rustc_box] does some magic and the MIR ends up looking like:

bb0:
    StorageLive(_1),
    StorageLive(_2),
    StorageLive(_3),
    _4 = SizeOf([i32; 1]),
    _5 = AlignOf([i32; 1]),
    _6 = alloc::alloc::exchange_malloc(move _4, move _5) -> [return: bb1, unwind: bb8],
bb1:
    StorageLive(_7),
    _7 = ShallowInitBox(move _6, [i32; 1]),
    (*_7) = [const 1_i32],
    _3 = move _7,
    _2 = move _3 as std::boxed::Box<[i32]> (Pointer(Unsize)),
    drop(_3) -> [return: bb2, unwind: bb6],
bb2:
    drop(_7) -> [return: bb3, unwind: bb7],
bb3:
    _1 = std::slice::<impl [i32]>::into_vec::<std::alloc::Global>(move _2) -> [return: bb4, unwind: bb7],

I think we should be able to simplify the malloc+ShallowInitBox into a Box::new(). Then there's an unsized coercion, which we also don't support. I'll see how @sonmarcho wants to approach this.

In the mean time, you can use this charon-compatible alternative:

macro_rules! vec {
    ($($x:tt)*) => {
        Vec::from([$($x)*])
    }
}