`crucible-mir`: Allow any value to be partially initialized

[RyanGlScott]

Currently, crucible-mir uses the following conventions for translating structs and tuples into RegValues:

• A tuple value (v_1 : t_1, ..., v_n : t_n) is translated to a RegValue of type StructRepr [MaybeRepr t_1, ..., MaybeRepr t_n]. The use of MaybeRepr reflects the fact that MIR can partially initialize the fields of a struct, so an Unassigned value indicates that a field has not yet been initialized.
• A struct value S { v_1 : t_1, ..., v_n : t_n } is translated to a RegValue of type AnyRepr, where the packed representation is of type StructRepr [f_1, ..., f_n], where each f_i is one of the following:
  • t_i, if the type t_i has a reasonable initial value (see canInitialize for how this is determined).
  • MaybeRepr t_i otherwise.

Despite the fact that tuples and structs are conceptually quite similar, they use rather different StructRepr conventions. I propose to simplify things by making both tuples and structs use the StructRepr [MaybeRepr t_1, ..., MaybeRepr t_n]—that is, we should no longer use canInitialize. I have two motivations for this:

1. This makes the treatment of tuples and structs much more uniform throughout the code.

2. In SAW, it is convenient to be able to have tuple and struct values with uninitialized fields. Notably, this is convenient to use for SAW overrides, as we want to invalidate mutable allocations used in an override after it has been applied to ensure that they are used in a sound manner. With the StructRepr [MaybeRepr t_1, ..., MaybeRepr t_n] convention, created one of these structs is as simple as Empty :> Unassigned :> ... :> Unassigned.

   An alternative would be to create fresh symbolic values for fields that canInitialize returns True on. (This is the approach taken by crucible-mir-comp here.) I'm not as fond of this approach, however, as it has the disadvantage that if a user underspecifies the value that a mutable allocation points to, their mistake will likely go unnoticed until simulation is finished. On the other hand, reading from an Unassigned value will immediately error during simulation, which means that a user is more likely to notice the mistake.

[RyanGlScott]

Upon further discussion with @spernsteiner and @andreistefanescu, we've come to the conclusion that in the long-term, it would be convenient to allow partial initialization of any value, not just struct fields. This would allow us to do the following:

1. Partial initialization of static items.
2. Invalidating memory of any type in a SAW compositional override.
3. Verifying unsafe code involving MaybeUninit.

This would likely require the same plan as above: use MaybeRepr in more places. I'll edit the title of this issue to reflect the more general goal.