Fix the bug: Static union values can panic Kani

[thanhnguyen-aws]

This PR fixes the bug: Static union values can panic Kani.

The reason behind the bug is Kani's translation of Union type is not consistent with its layout defined by Rust. Specifically, the size of the Union is not just the max of its fields but that maximum should be round up to a multiple of its alignment.
See:
https://web.mit.edu/rust-lang_v1.25/arch/amd64_ubuntu1404/share/doc/rust/html/reference/type-layout.html#:~:text=The%20layout%20of%20a%20type,also%20part%20of%20type%20layout

In this PR, I add another variant for DataComponent: DataComponent::UnionField, with a padded_type of a Union (a struct which contains a padding and the real field type) to fix the translated layout and support reasoning about transmute function for union type.

Resolves #4097

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[carolynzech]

I'm wondering if we can do something similar to #3401 instead of adding a padding field?

In particular, we already have logic for codegen_alignment_padding, so I'd prefer not to introduce a second way of reasoning about alignment and padding if we can avoid it.

[carolynzech]

I'm not following why we need a separate DatatypeComponent field for unions. Can't we represent the Type as a vector of DatatypeComponent::Field and DatatypeComponent::Padding like we do for structs and enums? So in the example of this test, we'd end up with a Type constructed from a vector of DataTypeComponents where the first item is the [u8; 3] field, the second element is 1 byte of padding, the third element is the u16 field, and the fourth element is 2 bytes of padding.

Happy to take this discussion offline if that's easier. I would prefer to use the same padding infrastructure that we have for structs and enums if possible. Perhaps it isn't possible, but if it's not I'm not seeing why.

[thanhnguyen-aws]

I'm not following why we need a separate DatatypeComponent field for unions. Can't we represent the Type as a vector of DatatypeComponent::Field and DatatypeComponent::Padding like we do for structs and enums? So in the example of this test, we'd end up with a Type constructed from a vector of DataTypeComponents where the first item is the [u8; 3] field, the second element is 1 byte of padding, the third element is the u16 field, and the fourth element is 2 bytes of padding.

Happy to take this discussion offline if that's easier. I would prefer to use the same padding infrastructure that we have for structs and enums if possible. Perhaps it isn't possible, but if it's not I'm not seeing why.

It is difficult to come up with a short answer for it, but after trying several ways of implementation, I feel that this is the most convenient way, for the following observations:

1. There are two things that we need to deal with: projection and transmute. For projection, we need to convert the union to the type of the field (with the layout of that type). But for transmute, we need to wrap the type in a struct with some padding, and use the exact layout of the union.
2. It is not convenient to use Vec of Padding and Field like the case of struct, because in union, when we want to deal with transmute or calculate the length, for each Field we need the information of its following Padding, so Vec.iter() is not convenient.
3. If we wrap a Field and a Padding into a struct, and use it as the type of the union field, it is not convenient to implement projection because we need to deal with union separately (not consistent with other types). Many related functions: lookup_field_type, lookup_field do not take the parent type as argument, so modifying them just for union does not look pretty. In contrast, for enum, although it is translated into union, we can do the wrapping because all if its variants are translated into struct types and we can add the padding inside it directly.
4. The wrapped struct (the padded_typ of UnionField) is only used in to_irep, so keeping the typ field to be the original mir type makes dealing with union consistent with other types everywhere else.