`crucible-mir` translation is sensitive to `static` name ordering

[RyanGlScott]

crux-mir is successfully able to verify this program:

static A: Option<u32> = Some(42);
static B: Option<u32> = A;

#[crux::test]
pub fn f() -> u32 {
    B.unwrap_or(27)
}

$ cabal run exe:crux-mir -- test.rs 
test test/f225316c::f[0]: returned 42, ok

[Crux-MIR] ---- FINAL RESULTS ----
[Crux] All goals discharged through internal simplification.
[Crux] Overall status: Valid.

So far, so good. What happens if we rename the static values, however? This program should be equivalent to the first one, as we have simply swapped the names for A and B:

static B: Option<u32> = Some(42);
static A: Option<u32> = B;

#[crux::test]
pub fn f() -> u32 {
    A.unwrap_or(27)
}

But crux-mir fails to run this version of the program:

$ cabal run exe:crux-mir -- test.rs 
test test/efc0f956::f[0]: [Crux] Attempting to prove verification conditions.
FAILED

failures:

---- test/efc0f956::f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux]   test.rs:2:25: 2:26: error: in test/efc0f956::A[0]
[Crux]   Attempted to read uninitialized reference cell
[Crux] Found counterexample for verification goal
[Crux]   test.rs:2:25: 2:26: error: in test/efc0f956::A[0]
[Crux]   attempted to read empty mux tree

[Crux-MIR] ---- FINAL RESULTS ----
[Crux] Goal status:
[Crux]   Total: 2
[Crux]   Proved: 0
[Crux]   Disproved: 2
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

Here is what I think is going on:

1. When translating the static values (using the transStatics function), crucible-mir will translate each of the statics that appear in the statics :: Map DefId Static field of a Collection.
2. Because statics is keyed by DefIds, crucible-mir will iterate through the static values according to the lexicographic ordering of their value names. In the examples above, this means that A will always be translated before B, regardless of the relative ordering of each static value in the source code.
3. In the second example, A's definition depends on B, but we translate A before we have translated B. But crucible-mir translates a constant by fully evaluating its definition, so this means that we have to eagerly evaluate B when translating A. Because B hasn't been translated yet, no value has been written to its corresponding GlobalVar, and this causes the Attempted to read uninitialized reference cell failure seen above when attempting to read from the GlobalVar.

One possible solution here is to implement some sort of dependency analysis that allows crucible-mir to realize when one static value is defined in terms of another. This would likely work well in the small example above, but I could envision this becoming tricky when the right-hand sides of static values are more complex.

Another possible solution would be to make crucible-mir's translation of static values lazier. During simulation, if crucible-mir encounters a static with a GlobalVar that hasn't yet been written to, run the CFG for the static's definition (computed with this code), write the result value to the GlobalVar, and return that value to the simulator. On subsequent attempts to load the static value, use the cached value in the GlobalVar rather than recomputing the CFG. This idea is inspired by crucible-llvm's lazy translation of function CFGs (see https://github.com/GaloisInc/crucible/issues/995).

[RyanGlScott]

A third option is that the rustc API might offer a way to look up what the actual order of static initialization should be. After all, if you write this:

static A: Option<u32> = B;
static B: Option<u32> = Some(42);

Then rustc has to check that B must be initialized before it can initialize A. Perhaps there is a programmatic way of doing this check?