MIR: Make it easier to refer to promoted static items

[qsctr]

In Rust you can get unnamed statics from constant promotion: in an expression like &42, the compiler actually generates a static item initialized to 42, so that you can borrow it. However, these statics are given a compiler-generated name in the MIR. This makes it hard to refer to them from SAW without manually inspecting the MIR to find the generated name.

Many SAW scripts have employed a workaround to describe functions which output such static items, by using mir_alloc instead of mir_static:

pub fn f() -> &'static u32 {
    &42
}

let f_spec = do {
    mir_execute_func [];
    x <- mir_alloc mir_u32;
    mir_return x;
};

However, mir_alloc is not meant for this purpose, as when used in the post-state of a spec, it describes that the function performs a memory allocation, which borrowing a static item is not. Indeed, as #2665 describes, using mir_alloc for static items can lead to unsoundness, so after this issue is fixed in #2678, this workaround will no longer be allowed.

In #2678 (comment) and subsequent replies, @RyanGlScott and I discuss ways to make it easier to refer to these unnamed static items in situations like this. Currently we are thinking of something like mir_static_of : MIRModule -> String -> MIRType -> MIRValue -> MIRValue (name is tentative), where mir_static_of mod prefix ty init would return a reference to the static in MIR module mod whose identifier starts with prefix, has type ty, and has initializer value init. The prefix can be used to disambiguate promoted statics from different crates by crate name, since promoted statics are only interned within the same crate. If there are multiple such statics (or none), an error is thrown.

Perhaps a less confusing name for this would be something like mir_static_from_value.

[RyanGlScott]

My hope is that mir_static_of/mir_static_from_value would suffice for most needs in practice, since the hypothesis is that if a single crate contains promoted constants with the same value and type, then rustc will deduplicate them into the same static item, therefore allowing users to look it up using a unique prefix. I don't have any evidence that this actually happens other than anecdotal experience, however.

[spernsteiner]

How would the matching be done? Would it require the target static to have a rendered/ConstVal initializer rather than a MIR body? I ran a few crux-mir test cases related to promotion and it looks like they all had ConstVals, but I'm not sure how consistent mir-json is about that.

Also, it seems like users might try to use this for ordinary non-promoted statics. We should either (1) make sure it works consistently for all statics (modifying mir-json to always emit ConstVals, if needed), or (2) explicitly prevent using this for non-promoted statics (modifying mir-json to record which statics are promoted so the SAW command can filter for them). I like option 2 a bit better because using value-based lookup instead of name-based would make proof scripts fragile: adding a new static with the same value could break proof scripts for otherwise-unrelated code.

[RyanGlScott]

How would the matching be done? Would it require the target static to have a rendered/ConstVal initializer rather than a MIR body? I ran a few crux-mir test cases related to promotion and it looks like they all had ConstVals, but I'm not sure how consistent mir-json is about that.

Yes, a good point. I think it would definitely make our lives easier here to just emit rendered constants for all static items in mir-json. I've opened GaloisInc/mir-json#177 for this task.

Also, it seems like users might try to use this for ordinary non-promoted statics. We should either (1) make sure it works consistently for all statics (modifying mir-json to always emit ConstVals, if needed), or (2) explicitly prevent using this for non-promoted statics (modifying mir-json to record which statics are promoted so the SAW command can filter for them). I like option 2 a bit better because using value-based lookup instead of name-based would make proof scripts fragile: adding a new static with the same value could break proof scripts for otherwise-unrelated code.

I am leaning on the side of recommending that users use mir_static instead of mir_static_of whenever possible, but to still allow using mir_static_of for any static item as an escape hatch. Less fuss on the implementation side that way. In the event that you do need to use mir_static_of, my hope is that having the ability to disambiguate static items by their prefix will reduce the likelihood that things unexpectedly break when you recompile code.