Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add mir_ref_of/mir_ref_mut_of functions for allocating references directly from values #1999

Open
RyanGlScott opened this issue Dec 19, 2023 · 0 comments
Labels
crucible/mir Related to crucible-mir verification enhancement

Comments

@RyanGlScott
Copy link
Contributor

Currently, in order to allocate a MIR reference that points to a value v, one must do something like this:

ref <- mir_alloc ty;
mir_points_to ref v;

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:

pub struct S {
    pub x: u32,
    pub y: u32,
}

pub fn get_x(s: &S) -> u32 {
    s.x
}

Consider this SAW spec example, which assumes that we can point to particular fields of a struct using mir_field_ref (see #1983):

let s_adt = mir_find_adt "example::S" [];

let get_x_42_spec = do {
  s <- mir_alloc (mir_adt s_adt);
  mir_points_to (mir_field_ref s) (mir_term {{ 42 : [32] }});

  mir_execute_func [s];
}

With the way that the crucible-mir memory model works, this would be an error! The entirety of the s reference must be initialized with a contiguous before one can offset into particular fields using mir_field_ref. That is, you'd need to write this spec like so:

let get_x_spec = do {
  s <- mir_alloc (mir_adt s_adt);
  s_val <- mir_fresh_expanded_value "s_val" (mir_adt s_adt);
  mir_points_to s s_val;
  mir_points_to (mir_field_ref s) (mir_term {{ 42 : [32] }});

  mir_execute_func [s];
}

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:

let get_x_spec = do {
  s_val <- mir_fresh_expanded_value "s_val" (mir_adt s_adt);
  s <- mir_ref_of s_val;
  mir_points_to (mir_field_ref s) (mir_term {{ 42 : [32] }});

  mir_execute_func [s];
}

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 of mir_alloc/mir_alloc_mut in favor of mir_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 write mir_points_to (mir_field_ref s) (mir_term {{ 42 : [32] }}) without first needing to initialize the entire struct. Even so, having mir_ref_of would be a nice convenience.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crucible/mir Related to crucible-mir verification enhancement
Projects
None yet
Development

No branches or pull requests

1 participant