crucible-mir
: Allow any value to be partially initialized
#1109
Labels
crucible-mir
: Allow any value to be partially initialized
#1109
Currently,
crucible-mir
uses the following conventions for translating structs and tuples intoRegValue
s:(v_1 : t_1, ..., v_n : t_n)
is translated to aRegValue
of typeStructRepr [MaybeRepr t_1, ..., MaybeRepr t_n]
. The use ofMaybeRepr
reflects the fact that MIR can partially initialize the fields of a struct, so anUnassigned
value indicates that a field has not yet been initialized.S { v_1 : t_1, ..., v_n : t_n }
is translated to aRegValue
of typeAnyRepr
, where the packed representation is of typeStructRepr [f_1, ..., f_n]
, where eachf_i
is one of the following:t_i
, if the typet_i
has a reasonable initial value (seecanInitialize
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 theStructRepr [MaybeRepr t_1, ..., MaybeRepr t_n]
—that is, we should no longer usecanInitialize
. I have two motivations for this:This makes the treatment of tuples and structs much more uniform throughout the code.
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 asEmpty :> Unassigned :> ... :> Unassigned
.An alternative would be to create fresh symbolic values for fields that
canInitialize
returnsTrue
on. (This is the approach taken bycrucible-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 anUnassigned
value will immediately error during simulation, which means that a user is more likely to notice the mistake.The text was updated successfully, but these errors were encountered: