Add mir_ref_of
/mir_ref_mut_of
functions for allocating references directly from values
#1999
Labels
mir_ref_of
/mir_ref_mut_of
functions for allocating references directly from values
#1999
Currently, in order to allocate a MIR reference that points to a value
v
, one must do something like this:This is a bit verbose, considering that whenever you allocate a reference, you pretty much always want it to point to something. But more than that, it's easy to mess up. Given this Rust code:
Consider this SAW spec example, which assumes that we can point to particular fields of a struct using
mir_field_ref
(see #1983):With the way that the
crucible-mir
memory model works, this would be an error! The entirety of thes
reference must be initialized with a contiguous before one can offset into particular fields usingmir_field_ref
. That is, you'd need to write this spec like so:I can foresee this being a common point of confusion. Offering
mir_ref_of
would make this mistake less likely, since then users would instead write this:This is a much more natural way to approach things, especially since there is a nice correspondence between
mir_ref_of
/mir_ref_mut_of
and the&
/&mut
operators in Rust. We might even discourage the use ofmir_alloc
/mir_alloc_mut
in favor ofmir_ref_of
/mir_ref_mut_of
.Note that if we changed the
crucible-mir
memory model to support partially initializing more things (see GaloisInc/crucible#1109), then this problem wouldn't be quite as severe, as then you could writemir_points_to (mir_field_ref s) (mir_term {{ 42 : [32] }})
without first needing to initialize the entire struct. Even so, havingmir_ref_of
would be a nice convenience.The text was updated successfully, but these errors were encountered: