mir_static and mir_static_initializer

This adds support for the `mir_static` and `mir_static_initializer` functions
in the MIR backend, which are used to write specifications involving top-level
`static` values. These behave like the `llvm_global` and
`llvm_global_initializer` functions in the LLVM backend, but with the following
differences:

1. There is nor MIR counterpart to the `llvm_alloc_global` command, as MIR
   static values are not "allocated" in the same way that LLVM globals are.
   (We still require users to initialize mutable MIR statics, however.)

2. By design, static references created with `mir_static` cannot alias
   allocations created with `mir_alloc`, as the two forms of allocations are
   handled through different mechanisms in the `crucible-mir` memory model.

This checks off one box in #1859.

doc/manual/manual.md

@@ -2788,6 +2788,10 @@ them.
 
 ## Global variables
 
+SAW supports verifying LLVM and MIR specifications involving global variables.
+
+### LLVM global variables
+
 Mutable global variables that are accessed in a function must first be allocated
 by calling `llvm_alloc_global` on the name of the global.
 
@@ -2892,6 +2896,68 @@ point of a call to `f`. This specification also constrains `y` to prevent
 signed integer overflow resulting from the `x + y` expression in `f`,
 which is undefined behavior in C.
 
+### MIR static items
+
+Rust's static items are the MIR version of global variables. A reference to a
+static item can be accessed with the `mir_static` function. This function takes
+a `String` representing a static item's identifier, and this identifier is
+expected to adhere to the naming conventions outlined in the "Running a
+MIR-based verification" section:
+
+* `mir_static : String -> MIRValue`
+
+References to static values can be initialized with the `mir_points_to`
+command, just like with other forms of references. Immutable static items
+(e.g., `static X: u8 = 42`) are initialized implicitly in every SAW
+specification, so there is no need for users to do so manually. Mutable static
+items (e.g., `static mut Y: u8 = 27`), on the other hand, are *not* initialized
+implicitly, and users must explicitly pick a value to initialize them with.
+
+The `mir_static_initializer` function can be used to access the initial value
+of a static item in a MIR program. Like with `mir_static`, the `String`
+supplied as an argument must be a valid identifier:
+
+* `mir_static_initializer : String -> MIRValue`.
+
+As an example of how to use these functions, here is a Rust program involving
+static items:
+
+~~~ .rs
+// statics.rs
+static     S1: u8 = 1;
+static mut S2: u8 = 2;
+
+pub fn f() -> u8 {
+    // Reading a mutable static item requires an `unsafe` block due to
+    // concurrency-related concerns. We are only concerned about the behavior
+    // of this program in a single-threaded context, so this is fine.
+    let s2 = unsafe { S2 };
+    S1 + s2
+}
+~~~
+
+We can write a specification for `f` like so:
+
+~~~
+// statics.saw
+enable_experimental;
+
+let f_spec = do {
+  mir_points_to (mir_static "statics::S2")
+                (mir_static_initializer "statics::S2");
+  // Note that we do not initialize S1, as immutable static items are implicitly
+  // initialized in every specification.
+
+  mir_execute_func [];
+
+  mir_return (mir_term {{ 3 : [8] }});
+};
+
+m <- mir_load_module "statics.linked-mir.json";
+
+mir_verify m "statics::f" [] false f_spec z3;
+~~~
+
 ## Preconditions and Postconditions
 
 Sometimes a function is only well-defined under certain conditions, or

intTests/test_mir_statics/Makefile

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test_mir_statics/test.rs

@@ -0,0 +1,29 @@
+static     S1: u32 = 1;
+static     S2: u32 = 2;
+static mut S3: u32 = 3;
+
+// rustc is very eager to inline immutable, top-level static values, even on the
+// lowest optimization settings. To ensure that S1 isn't inlined, we must
+// introduce this extra layer of indirection.
+pub fn f1_aux() -> &'static u32 {
+    &S1
+}
+
+pub fn f1() -> u32 {
+    *f1_aux()
+}
+
+pub fn f2() -> &'static u32 {
+    &S2
+}
+
+pub fn f3() -> u32 {
+    unsafe {
+        S3 = S3.wrapping_add(1);
+        S3
+    }
+}
+
+pub fn g(r: &u32) -> bool {
+    std::ptr::eq(r, &S1)
+}

intTests/test_mir_statics/test.saw

@@ -0,0 +1,115 @@
+enable_experimental;
+
+// A basic spec that uses the initial value of S1.
+let f1_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_static_initializer "test::S1");
+};
+
+// An alternative spec that uses a different initial value for S1.
+let f1_alt_spec = do {
+  let s1_static = mir_static "test::S1";
+  let init = mir_term {{ 42 : [32] }};
+  mir_points_to s1_static init;
+
+  mir_execute_func [];
+
+  mir_points_to s1_static init;
+  mir_return init;
+};
+
+// A buggy spec that refers to a non-existent static initializer value.
+let f1_fail_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_static_initializer "test::S1_fake");
+};
+
+// A buggy spec that refers to a non-existent static value.
+let f1_fail_alt_spec = do {
+  let s1_static = mir_static "test::S1_fake";
+  let init = mir_term {{ 42 : [32] }};
+  mir_points_to s1_static init;
+
+  mir_execute_func [];
+
+  mir_points_to s1_static init;
+  mir_return init;
+};
+
+// A spec that matches against a static in the return value.
+let f2_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_static "test::S2");
+};
+
+// A basic spec that uses the initial value of S3.
+let f3_spec = do {
+  let s3_static = mir_static "test::S3";
+  mir_points_to s3_static (mir_static_initializer "test::S3");
+
+  mir_execute_func [];
+
+  let ret = mir_term {{ 4 : [32] }};
+  mir_points_to s3_static ret;
+  mir_return ret;
+};
+
+// An alternative spec that uses a different initial value for S3.
+let f3_alt_spec = do {
+  let s3_static = mir_static "test::S3";
+  let init = {{ 42 : [32] }};
+  mir_points_to s3_static (mir_term init);
+
+  mir_execute_func [];
+
+  let ret = mir_term {{ init + 1 }};
+  mir_points_to s3_static ret;
+  mir_return ret;
+};
+
+// A buggy spec that does not initialize S3 (a mutable static value).
+let f3_fail_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_term {{ 4 : [32] }});
+};
+
+// A spec that ensures that fresh allocations do not alias with static
+// references.
+let g_spec = do {
+  r_ref <- mir_alloc mir_u32;
+
+  mir_execute_func [r_ref];
+
+  mir_return (mir_term {{ False }});
+};
+
+// g(&S1) should return True.
+let g_alt_spec = do {
+  mir_execute_func [mir_static "test::S1"];
+
+  mir_return (mir_term {{ True }});
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+mir_verify m "test::f1" [] false f1_spec z3;
+mir_verify m "test::f1" [] false f1_alt_spec z3;
+mir_verify m "test::f2" [] false f2_spec z3;
+mir_verify m "test::f3" [] false f3_spec z3;
+mir_verify m "test::f3" [] false f3_alt_spec z3;
+mir_verify m "test::g" [] false g_spec z3;
+mir_verify m "test::g" [] false g_alt_spec z3;
+
+fails (
+  mir_verify m "test::f1" [] false f1_fail_spec z3
+);
+fails (
+  mir_verify m "test::f1" [] false f1_fail_alt_spec z3
+);
+fails (
+  mir_verify m "test::f3" [] false f3_fail_spec z3
+);

intTests/test_mir_statics/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-remote-api/python/tests/saw/test-files/Makefile

@@ -1,6 +1,7 @@
 C_FILES    := $(wildcard *.c)
 BC_FILES   := $(C_FILES:.c=.bc)
 RS_FILES   := $(wildcard *.rs)
+EXE_FILES  := $(RS_FILES:.rs=)
 JSON_FILES := $(RS_FILES:.rs=.linked-mir.json)
 
 all: $(BC_FILES) $(JSON_FILES)
@@ -10,7 +11,12 @@ all: $(BC_FILES) $(JSON_FILES)
 
 %.linked-mir.json: %.rs
 	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
 
 # This test case crucially relies on the use of -O2.
 llvm_lax_pointer_ordering.bc: llvm_lax_pointer_ordering.c
 	clang -O2 -g -c -emit-llvm -o $@ $<
+
+PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test lib*.mir lib*.rlib $(EXE_FILES)

saw-remote-api/python/tests/saw/test-files/mir_statics.rs

@@ -0,0 +1,29 @@
+static     S1: u32 = 1;
+static     S2: u32 = 2;
+static mut S3: u32 = 3;
+
+// rustc is very eager to inline immutable, top-level static values, even on the
+// lowest optimization settings. To ensure that S1 isn't inlined, we must
+// introduce this extra layer of indirection.
+pub fn f1_aux() -> &'static u32 {
+    &S1
+}
+
+pub fn f1() -> u32 {
+    *f1_aux()
+}
+
+pub fn f2() -> &'static u32 {
+    &S2
+}
+
+pub fn f3() -> u32 {
+    unsafe {
+        S3 = S3.wrapping_add(1);
+        S3
+    }
+}
+
+pub fn g(r: &u32) -> bool {
+    std::ptr::eq(r, &S1)
+}