Reading a static mutable reference crashes with empty mux tree

[sauclovian-g]

foo.rs:

static mut X: u32 = 1;

pub fn f() -> u32 {
   unsafe { X }
}

foo.saw, which is incorrect:

enable_experimental;
m <- mir_load_module "foo.linked-mir.json";

let f_spec = do {
    mir_execute_func [];
    mir_return (mir_term {{ 1 : [32] }});
};
mir_verify m "foo::f" [] false f_spec z3;

Results:

[23:50:41.124] Loading file ".../foo.saw"
[23:50:41.173] Verifying foo/34e0fe10::f[0] ...
[23:50:41.180] Simulating foo/34e0fe10::f[0] ...
[23:50:41.180] Stack trace:
"mir_verify" (.../foo.saw:8:1-8:11)
Symbolic execution failed.
Abort due to assertion failure:
  foo.rs:4:13: 4:14: error: in foo/34e0fe10::f[0]
  attempted to read empty mux tree

It is good that this doesn't verify, since any correct spec needs to engage with the mutable static directly, but this is not how it should be failing.

Closely related to #1960, maybe should just have been a comment there, but seems like potentially a separate problem.

[RyanGlScott]

For some context, "attempted to read empty mux tree" is a rather generic error message that arises whenever you read from uninitialized MIR memory. You can also trigger the same error by doing something like this:

// foo.rs
pub fn f(x: &u32) -> u32 {
    *x
}

// foo.saw
enable_experimental;
m <- mir_load_module "foo.linked-mir.json";

let f_spec = do {
    x <- mir_alloc mir_u32;
    mir_execute_func [x];
};
mir_verify m "foo::f" [] false f_spec z3;

$ ~/Software/saw-1.2/bin/saw foo.saw
[12:23:16.298] Loading file "/home/ryanscott/Documents/Hacking/SAW/foo.saw"
[12:23:16.319] Verifying foo/145181a5::f[0] ...
[12:23:16.330] Simulating foo/145181a5::f[0] ...
[12:23:16.331] Stack trace:
"mir_verify" (/home/ryanscott/Documents/Hacking/SAW/foo.saw:9:1-9:11)
Symbolic execution failed.
Abort due to assertion failure:
  foo.rs:3:5: 3:7: error: in foo/145181a5::f[0]
  attempted to read empty mux tree

(Note that f_spec allocates x but does not initialize it.)

I agree that it would be nice to improve this error message. I haven't thought deeply about the best way to do so, however.