Support `SizeOf` and `AlignOf` MIR instructions

[xldenis]

The SizeOf and AlignOf Rvalues are used in the MIR generated by vec! having some basic support for those operations would be greatly beneficial. Specifically, we need to support the following pattern:

        _4 = SizeOf([bool; 2]);          // scope 2 at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/alloc/src/macros.rs:52:13: 52:47
        _5 = AlignOf([bool; 2]);         // scope 2 at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/alloc/src/macros.rs:52:13: 52:47
        _6 = alloc::alloc::exchange_malloc(move _4, move _5) -> [return: bb1, unwind: bb8]; // scope 2 at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/alloc/src/macros.rs:52:13: 52:47

[jhjourdan]

We need to take care about portability of the proofs, though. What is the status of portability right now? E.g., what do we assume about usize?

[xldenis]

We need to take care about portability of the proofs, though.

That's the tricky thing, especially in the presence of generics, what is SizeOf([T; 2])?

E.g., what do we assume about usize?

Right now usize = u64. I wonder, could we relax the definition of usize to have an indeterminate upper bound? Would that be too painful?

[xldenis]

The idea I have here is that once we have cloneable types in Creusot, a type module defines the type, but also the size_of and align_of of the type, potentially depending on predicates coming from other types. During generation we can ask rustc for this information and fill in symbolic values where it isn't available.

[jhjourdan]

That looks like a plan, indeed.

[xldenis]

I'm going to close this as wont-fix as there is no real roadmap for this being added (nor a usecase).