Add mir_alloc_static_mut and mir_initialize_static_mut commands

[RyanGlScott]

As part of #1959, I am investigating a way to check whether an override modifies a particular mutable static value or not. Here is a motivating example:

static mut A: u32 = 27;

pub fn side_effect() {
    unsafe { A = 42 };
}

pub fn f() -> u32 {
    side_effect();
    unsafe { A }
}

enable_experimental;

m <- mir_load_module "test.linked-mir.json";

let side_effect_spec = do {
    mir_execute_func [];
};

let f_spec = do {
    let a_init = mir_static_initializer "test::A";
    mir_points_to (mir_static "test::A") a_init;

    mir_execute_func [];

    mir_return a_init;
};

side_effect_ov <- mir_verify m "test::side_effect" [] false side_effect_spec z3;
mir_verify m "test::f" [side_effect_ov] false f_spec z3;

There are two problems with this example:

1. Although side_effect mutates the value of A, side_effect_spec does not mention A at all. This is a bit unsettling, as A is mutable global state that could have an impact when side_effect is used as an override. And in fact...
2. f_spec is an incorrect specification for f, as f should return 42 rather than 27 (which a_init is equal to). Despite this, however, the current version of mir_unsafe_assume_spec #1959 (at the time of writing) will unsoundly verify f_spec as correct. This is because f_spec relies on an override for side_effect that uses side_effect_spec, but side_effect_spec underspecifies what A's value should be in its postconditions.

We want to reject examples like the one above, but how? side_effect_spec underspecifies A, but it is not obvious from looking at side_effect_ov that this is the case, since nothing about side_effect_ov mentions A at all. This suggests that we need a command that explicitly states which mutable static values a function makes use of (either via reads or writes).

To solve this problem, I propose that we introduce a mir_alloc_static_mut : String -> MIRSetup () command, similar to the LLVM backend's llvm_alloc_global command. mir_alloc_static_mut would behave in the following way when used in combination with mir_verify:

1. Before simulating a function with mir_verify, we start with a SymGlobalState that does not contain any mutable static values.
2. After simulating the function with mir_verify, we check if the SymGlobalState contains any mutable static values that were not present in the original SymGlobalState. If so, we know that those mutable statics were written to at some point during simulation.
3. For each of these written-to mutable statics, check to see if the precondition to the function contains a corresponding mir_alloc_static_mut command. If not, throw an error.

Under this plan, the call to mir_verify ... side_effect_spec above would fail, since the side_effect function writes to A but does have a mir_alloc_static_mut command corresponding to A as a precondition. Let's add one:

let side_effect_spec = do {
    mir_alloc_static_mut "test::A";

    mir_execute_func [];
};

This solves problem (1) above.

Problem (2) is still an issue, as side_effect_spec still does not say what the value of A should be in the postcondition, which would cause problems when side_effect_ov is used. But now we have a way to solve problem (2) as well, as there is now a straightforward way to see whether an override uses a mutable static or not: just check all of the mir_alloc_static_mut commands in the preconditions! We can see that there there is a mir_alloc_static_mut "test::A" command in the precondition, but there is no corresponding mir_points_to (mir_global "test::A") ... command in the postcondition, so we can reasonably conclude that side_effect_spec underspecifies A. Therefore, we can throw an error when using side_effect_ov as an override, thereby solving problem (2).

Note that the name mir_alloc_static_mut is perhaps slightly misleading, since the implementation of static values in the crucible-mir memory model does not actually perform any allocation. In the memory model, the GlobalVars backing static values are always allocated before simulation begins, regardless of whether they are used or not. This is arguably an implementation detail, however, and users don't need to care about this that much. Therefore, I propose that we keep the "alloc" convention in the name, as it provides symmetry with the existing mir_alloc_mut command.

Speaking of mir_alloc_mut, the mir_alloc_static_mut command has the same pitfalls as mir_alloc_mut in the sense that mir_alloc_static_mut does not initialize the thing that it references. Therefore, something like this would not work (in contrast with the LLVM backend):

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

mir_alloc_static_mut "test::MyStruct";
mir_points_to (mir_field (mir_static "test::MyStruct) "y") (mir_term {{ 42 : [32] }});
...

We proposed solving this issue on the mir_alloc_mut side by introducing a mir_ref_mut_of : MIRValue -> MIRSetup MIRValue command (see #1999) that allocates a mutable MIR reference and initializes it with a value so that subsequent mir_points_to (mir_field ...) commands will work as expected. Similarly, I propose adding a mir_initialize_static_mut : String -> MIRSetup () command that both "allocates" a static mutable value and initializes it with its mir_static_initializer value. mir_initialize_static_mut would be to mir_alloc_static_mut as mir_ref_mut_of is to mir_alloc_mut.

[sauclovian-g]

This prompted me to check what happens if you just read from static mutables, and hey presto that doesn't work. 🙀 However...

The current behavior of this example seems to be that the bogus side_effect_spec is still accepted, but f_spec fails -- it complains that the state of the mutable static variable A is not described in the postcondition. (It appears to be actually talking about the postcondition of the override spec, not the postcondition of f_spec, but there's no way to determine that from what's printed, which is also a problem.)

Adding mir_points_to (mir_static "test::A") (mir_term {{ 42 : [32] }}); to side_effect_spec makes it correct, and then it works. (Provided f_spec is changed to provide the right return value as well.) Conversely, no amount of attempting to specify the value of A in f_spec makes the proof go through.

My recollection is that only requiring a complete specification for outputs when using a spec as an override (vs. when proving it in the first place) is intentional. Am I misremembering? If not, I think most of the above must have already been done and there's nothing left to do here besides make the error messages comprehensible.

[sauclovian-g]

Also though I think it would be good to make a copy of test_llvm_unsound_global for mir.

[sauclovian-g]

(also, is this obsoleted by #1982?)

[RyanGlScott]

The current behavior of this example seems to be that the bogus side_effect_spec is still accepted, but f_spec fails -- it complains that the state of the mutable static variable A is not described in the postcondition.

Correct. To provide a much-needed update here: I originally opened this issue while still working on #1959 (the implementation of mir_unsafe_assume_spec), and back then, mir_unsafe_assume_spec was much more permissive about not needing to initialize mutable static values in overrides. This was blatantly unsound, so I implemented a very brutal solution for this problem: every MIR override must initialize all mutable static variables used anywhere in the program (not just the function being overridden). When you run the program above with modern SAW, it rejects f_spec (as expected) with the following error message:

$ ~/Software/saw-1.2/bin/saw test.saw
[12:53:14.080] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[12:53:14.101] Verifying test/8fa28ec0::side_effect[0] ...
[12:53:14.111] Simulating test/8fa28ec0::side_effect[0] ...
[12:53:14.111] Checking proof obligations test/8fa28ec0::side_effect[0] ...
[12:53:14.111] Proof succeeded! test/8fa28ec0::side_effect[0]
[12:53:14.113] Verifying test/8fa28ec0::f[0] ...
[12:53:14.125] Simulating test/8fa28ec0::f[0] ...
[12:53:14.126] Matching 1 overrides of  test/8fa28ec0::side_effect[0] ...
[12:53:14.126] Branching on 1 override variants of test/8fa28ec0::side_effect[0] ...
[12:53:14.126] Stack trace:
"mir_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:19:1-19:11)
State of mutable static variable "test/8fa28ec0::A[0]" not described in postcondition

This gets the job done (and does make SAW reject f_spec above, as expected), but at the expense of users needing to be extremely explicit in their overrides. In fact, this is even more explicit than the LLVM backend, where an override only needs to initialize mutable global variables that the function uses in some way. Based on user feedback, we'd like to make the MIR backend work more like the LLVM backend in this way: see #1982.

(also, is this obsoleted by #1982?)

Yes, I think #1982's proposal of needing to explicitly allocate static values (via mir_alloc_static) is a better design. In addition to the benefits listed above, this design would avoid needing to have a special command just for mutable static variables.

My recollection is that only requiring a complete specification for outputs when using a spec as an override (vs. when proving it in the first place) is intentional.

Yes, that is correct. It is sound for a specification not to specify static values in its postconditions, provided that the specification is not used in a compositional override. SAW strives to allow users to make their specifications as fine- or coarse-grained as they'd like, so in this sense, allowing users not to specify static values in postconditions fits in with SAW's existing design philosophy.

I think most of the above must have already been done and there's nothing left to do here besides make the error messages comprehensible.

Are you referring to the State of mutable static variable "test/8fa28ec0::A[0]" not described in postcondition error message? If so, what would you change? (I'm in favor of improving the error message, although I'm wondering which part specifically you'd want to improve.)

[sauclovian-g]

No; that one's fine. I was thinking of other messages mentioned earlier, except that there actually aren't any, so I must have been thinking of some other issue's messages. I'll go make a test_mir_unsound_global and then I think we can call this done.

[sauclovian-g]

That's been merged.