Merge pull request #1941 from GaloisInc/T1859-mir-globals

`mir_static` and `mir_static_initializer`

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -273,8 +273,8 @@ addArg tpr argRef msb =
                  , MS.conditionType = "add argument value"
                  , MS.conditionContext = ""
                  }
-        msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs :)
-        msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs' :)
+        msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :)
+        msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs' :)
 
     msbSpec . MS.csArgBindings . at (fromIntegral idx) .= Just (ty, sv)
   where
@@ -318,7 +318,7 @@ setReturn tpr argRef msb =
                  , MS.conditionType = "set return value"
                  , MS.conditionContext = ""
                  }
-        msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs :)
+        msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :)
 
     msbSpec . MS.csRetValue .= Just sv
   where

crucible-mir-comp/src/Mir/Compositional/Override.hs

@@ -208,7 +208,8 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
         -- to allocation `alloc` before we see the PointsTo for `alloc` itself.
         -- This ensures we can obtain a MirReference for each PointsTo that we
         -- see.
-        forM_ (reverse $ ms ^. MS.csPreState . MS.csPointsTos) $ \(MirPointsTo md alloc svs) -> do
+        forM_ (reverse $ ms ^. MS.csPreState . MS.csPointsTos) $ \(MirPointsTo md ref svs) -> do
+            alloc <- setupVarAllocIndex ref
             allocSub <- use MS.setupValueSub
             Some ptr <- case Map.lookup alloc allocSub of
                 Just x -> return x
@@ -311,7 +312,8 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
     -- figuring out which memory is accessible and mutable and thus needs to be
     -- clobbered, and for adding appropriate fresh variables and `PointsTo`s to
     -- the post state.
-    forM_ (ms ^. MS.csPostState . MS.csPointsTos) $ \(MirPointsTo _md alloc svs) -> do
+    forM_ (ms ^. MS.csPostState . MS.csPointsTos) $ \(MirPointsTo _md ref svs) -> do
+        alloc <- setupVarAllocIndex ref
         Some ptr <- case Map.lookup alloc allocMap of
             Just x -> return x
             Nothing -> error $ "post PointsTos are out of order: no ref for " ++ show alloc
@@ -589,3 +591,20 @@ checkDisjoint bak refs = go refs
             assert bak disjoint $ GenericSimError $
                 "references " ++ show alloc ++ " and " ++ show alloc' ++ " must not overlap"
         go rest
+
+-- | Take a 'MS.SetupValue' that is assumed to be a bare 'MS.SetupVar' and
+-- extract the underlying 'MS.AllocIndex'. If this assumption does not hold,
+-- this function will raise an error.
+--
+-- This is used in conjunction with 'MirPointsTo' values. With the way that
+-- @crucible-mir-comp@ is currently set up, the only sort of 'MS.SetupValue'
+-- that will be put into a 'MirPointsTo' value's left-hand side is a
+-- 'MS.SetupVar', so we can safely use this function on such 'MS.SetupValue's.
+-- Other parts of SAW can break this assumption (e.g., if you wrote something
+-- like @mir_points_to (mir_static "X") ...@ in a SAW specification), but these
+-- parts of SAW are not used in @crucible-mir-comp@.
+setupVarAllocIndex :: Applicative m => MS.SetupValue MIR -> m MS.AllocIndex
+setupVarAllocIndex (MS.SetupVar idx) = pure idx
+setupVarAllocIndex val =
+  error $ "setupVarAllocIndex: Expected SetupVar, received: "
+       ++ show (MS.ppSetupValue val)

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,30 @@
+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.
+#[inline(never)]
+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,30 @@
+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.
+#[inline(never)]
+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)
+}