MIR: Add mir_field_{ref,value}

[qsctr]

I needed to add a few functions to crucible-mir, so this includes a submodule bump for crucible. The corresponding crucible PR is GaloisInc/crucible#1754.

Closes #1983.

[RyanGlScott]

I'm a bit surprised that we would restrict field accesses on repr(transparent) structs to just the primary field, since as far as I can tell, this is not a requirement that the Rust language itself imposes. Is there an implementation reason for needing this restriction in SAW?

[qsctr]

It's mostly because I'm not sure how I would implement resolveSetupVal and matchArg for the secondary fields.

resolveSetupVal for getting a secondary field by value would need to conjure up a value for the field, since the recursive call to resolveSetupVal for the struct won't contain the secondary field RegValues. Since it's a ZST, this would be doable, but the only code I could find that already does this is initialValue from crucible-mir which is in the MirGenerator monad so I don't think I can directly call it from here. And so given that there is no particular need at the moment to support this, I opted to just make it an error.

resolveSetupVal for getting a secondary field by reference would basically need to return an invalid reference I think, because there's no way of extending the existing MirReferencePath to point to a nonexistent field. And our support for invalid pointers to ZSTs in crucible is very limited (see GaloisInc/crucible#1497), so I don't think we would get much further even if we did that.

matchArg for getting a secondary field by value would also need to conjure up a RegValue for the ZST.

matchArg for getting a secondary field by reference would need to go from a pointer to ZST (which might be invalid) to a pointer to the primary field, which is entirely unrelated, and I don't know how we would do that.

[RyanGlScott]

Since it's a ZST, this would be doable, but the only code I could find that already does this is initialValue from crucible-mir which is in the MirGenerator monad so I don't think I can directly call it from here.

For what it's worth, you can also call the mirAggregate_zst* family of functions here instead. For instance, mirAggregate_zstIO has an appropriate type for being called from resolveSetupVal.

resolveSetupVal for getting a secondary field by reference would basically need to return an invalid reference I think, because there's no way of extending the existing MirReferencePath to point to a nonexistent field. And our support for invalid pointers to ZSTs in crucible is very limited (see GaloisInc/crucible#1497), so I don't think we would get much further even if we did that.

Ah, I forgot about GaloisInc/crucible#1497. In that case, I think I'm fine with imposing this restriction, although it would be worth citing GaloisInc/crucible#1497 as justification for it in the comments.

[qsctr]

For what it's worth, you can also call the mirAggregate_zst* family of functions here instead.

I thought that only works for MirAggregate-based ZSTs like (), and not something like a struct whose fields are all ZSTs.

In that case, I think I'm fine with imposing this restriction, although it would be worth citing GaloisInc/crucible#1497 as justification for it in the comments.

Even if GaloisInc/crucible#1497 is resolved, I'm still not sure how we would implement override matching for mir_field_ref on a secondary field of a repr(transparent) struct. To match a pointer to a field of a struct against a mir_field_ref, we match the pointer to the whole struct against the SetupVar for the whole mir_alloc. But if we receive a pointer to a secondary field of a repr(transparent) struct, there's no way of going from that to the struct pointer that it was projected out of, because it isn't actually a projection in crucible-mir. The field pointer would either be an invalid pointer or an entirely separate MirReference with Const_RefRoot.

For instance, if we wanted to verify something like

#[repr(transparent)]
struct S {
  x: i32,
  y: ()
}

fn f(s: &S) -> &() {
  &s.y
}

let f_spec = do {
    s <- mir_fresh_expanded_value "s" (mir_adt S);
    r <- mir_ref_of s;
    mir_execute_func [r];
    mir_return (mir_field_ref r "y");
};

SAW wouldn't be able to tell whether the &() returned from the function came from the &S or not.

[RyanGlScott]

All fair points. Perhaps citing GaloisInc/crucible#1497 is the wrong justification, in that case. Could you take the points that you raise here and convert them into comments so that we have something to point to for justifying why we impose this restriction on repr(transparent) types?

[RyanGlScott]

Perhaps we should just delete this function now that it's a very thin wrapper around fieldOrVariantShortName. (There are only a small number of getEnumVariantShortName call sites anyway.)

[RyanGlScott]

There is quite a bit of rightward code drift here due to indentation—this case expression is nested five levels deep! It would be nice to eliminate some of this drift, either by splitting out certain case expressions into helper functions or by rewriting the code slightly. For instance, the outermost case could be rewritten using a style like:

findStructField col accessMode structTy shortFieldName = do
  adtName <-
    case structTy of
      Mir.TyAdt adtName _ _ -> pure adtName
      _ -> panic ...
  ...

[qsctr]

force push: rebase on #3059 and also bump crucible to master after GaloisInc/crucible#1754 was merged