Merge pull request #1916 from GaloisInc/T1859-mir-verify-points-to

Support `mir_alloc`, `mir_alloc_mut`, and `mir_points_to`

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

@@ -267,8 +267,14 @@ addArg tpr argRef msb =
             return (sv, sv')
 
         let (svs, svs') = unzip svPairs
-        msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo (fr ^. frAlloc) svs :)
-        msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo (fr ^. frAlloc) svs' :)
+        let md = MS.ConditionMetadata
+                 { MS.conditionLoc = loc
+                 , MS.conditionTags = mempty
+                 , 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.csArgBindings . at (fromIntegral idx) .= Just (ty, sv)
   where
@@ -287,6 +293,7 @@ setReturn tpr argRef msb =
   ovrWithBackend $ \bak ->
   execBuilderT msb $ do
     let sym = backendGetSym bak
+    loc <- liftIO $ W4.getCurrentProgramLoc sym
     let ty = case msb ^. msbSpec . MS.csRet of
             Just x -> x
             Nothing -> M.TyTuple []
@@ -305,7 +312,13 @@ setReturn tpr argRef msb =
             let shp = tyToShapeEq col (fr ^. frMirType) (fr ^. frType)
             regToSetup bak Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
 
-        msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo (fr ^. frAlloc) svs :)
+        let md = MS.ConditionMetadata
+                 { MS.conditionLoc = loc
+                 , MS.conditionTags = mempty
+                 , MS.conditionType = "set return value"
+                 , MS.conditionContext = ""
+                 }
+        msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (fr ^. frAlloc) svs :)
 
     msbSpec . MS.csRetValue .= Just sv
   where
@@ -616,7 +629,7 @@ substMethodSpec sc sm ms = do
         sv' <- goSetupValue sv
         return (ty, sv')
 
-    goPointsTo (MirPointsTo alloc svs) = MirPointsTo alloc <$> mapM goSetupValue svs
+    goPointsTo (MirPointsTo md alloc svs) = MirPointsTo md alloc <$> mapM goSetupValue svs
 
     goSetupValue sv = case sv of
         MS.SetupVar _ -> return sv

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

@@ -208,7 +208,7 @@ 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 alloc svs) -> do
+        forM_ (reverse $ ms ^. MS.csPreState . MS.csPointsTos) $ \(MirPointsTo md alloc svs) -> do
             allocSub <- use MS.setupValueSub
             Some ptr <- case Map.lookup alloc allocSub of
                 Just x -> return x
@@ -223,12 +223,6 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
                 ref' <- lift $ mirRef_offsetSim (ptr ^. mpType) (ptr ^. mpRef) iSym
                 rv <- lift $ readMirRefSim (ptr ^. mpType) ref'
                 let shp = tyToShapeEq col ty (ptr ^. mpType)
-                let md = MS.ConditionMetadata
-                         { MS.conditionLoc = loc
-                         , MS.conditionTags = mempty
-                         , MS.conditionType = "points-to"
-                         , MS.conditionContext = ""
-                         }
                 matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) md shp rv sv
 
         -- Validity checks
@@ -317,7 +311,7 @@ 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 alloc svs) -> do
+    forM_ (ms ^. MS.csPostState . MS.csPointsTos) $ \(MirPointsTo _md alloc svs) -> do
         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

doc/manual/manual.md

@@ -2105,8 +2105,6 @@ some parts of `mir_verify` are not currently implemented, so it is possible
 that using `mir_verify` on some programs will fail. Features that are not yet
 implemented include the following:
 
-* MIR specifications involving memory allocations (i.e., neither the
-  `mir_alloc` nor the `mir_points_to` commands are functional)
 * MIR specifications that use overrides (i.e., the `[MIRSpec]` argument to
   `mir_verify` must always be the empty list at present)
 * The ability to construct MIR `struct` or `enum` values in specifications
@@ -2435,6 +2433,9 @@ but there is also a `mir_alloc_mut` function for creating a mutable reference:
 
 * `mir_alloc_mut : MIRType -> MIRSetup SetupValue`
 
+MIR tracks whether references are mutable or immutable at the type level, so it
+is important to use the right allocation command for a given reference type.
+
 In LLVM, it's also possible to construct fresh pointers that do not
 point to allocated memory (which can be useful for functions that
 manipulate pointers but not the values they point to):
@@ -2459,15 +2460,19 @@ will not modify. Unlike `llvm_alloc`, regions allocated with
 
 ## Specifying Heap Values
 
-Pointers returned by `llvm_alloc` don't, initially, point to
-anything. So if you pass such a pointer directly into a function that
-tried to dereference it, symbolic execution will fail with a message
-about an invalid load. For some functions, such as those that are
-intended to initialize data structures (writing to the memory pointed
-to, but never reading from it), this sort of uninitialized memory is
-appropriate. In most cases, however, it's more useful to state that a
-pointer points to some specific (usually symbolic) value, which you can
-do with the `llvm_points_to` command.
+Pointers returned by `llvm_alloc`, `jvm_alloc_{array,object}`, or
+`mir_alloc{,_mut}` don't initially point to anything. So if you pass such a
+pointer directly into a function that tried to dereference it, symbolic
+execution will fail with a message about an invalid load. For some functions,
+such as those that are intended to initialize data structures (writing to the
+memory pointed to, but never reading from it), this sort of uninitialized
+memory is appropriate. In most cases, however, it's more useful to state that a
+pointer points to some specific (usually symbolic) value, which you can do with
+the *points-to* family of commands.
+
+### LLVM heap values
+
+LLVM verification primarily uses the `llvm_points_to` command:
 
 * `llvm_points_to : SetupValue -> SetupValue -> LLVMSetup ()`
 takes two `SetupValue` arguments, the first of which must be a pointer,
@@ -2490,6 +2495,49 @@ introduced this additional function to make it clear when a type
 reinterpretation is intentional. As an alternative, one
 may instead use `llvm_cast_pointer` to line up the static types.
 
+### JVM heap values
+
+JVM verification has two categories of commands for specifying heap values.
+One category consists of the `jvm_*_is` commands, which allow users to directly
+specify what value a heap object points to. There are specific commands for
+each type of JVM heap object:
+
+* `jvm_array_is : JVMValue -> Term -> JVMSetup ()` declares that an array (the
+  first argument) contains a sequence of values (the second argument).
+* `jvm_elem_is : JVMValue -> Int -> JVMValue -> JVMSetup ()` declares that an
+  array (the first argument) has an element at the given index (the second
+  argument) containing the given value (the third argument).
+* `jvm_field_is : JVMValue -> String -> JVMValue -> JVMSetup ()` declares that
+  an object (the first argument) has a field (the second argument) containing
+  the given value (the third argument).
+* `jvm_static_field_is : String -> JVMValue -> JVMSetup ()` declares that a
+  named static field (the first argument) contains the given value (the second
+  argument). By default, the field name is assumed to belong to the same class
+  as the method being specified. Static fields belonging to other classes can
+  be selected using the `<classname>.<fieldname>` syntax in the first argument.
+
+Another category consists of the `jvm_modifies_*` commands. Like the `jvm_*_is`
+commands, these specify that a JVM heap object points to valid memory, but
+unlike the `jvm_*_is` commands, they leave the exact value being pointed to as
+unspecified. These are useful for writing partial specifications for methods
+that modify some heap value, but without saying anything specific about the new
+value.
+
+* `jvm_modifies_array : JVMValue -> JVMSetup ()`
+* `jvm_modifies_elem : JVMValue -> Int -> JVMSetup ()`
+* `jvm_modifies_field : JVMValue -> String -> JVMSetup ()`
+* `jvm_modifies_static_field : String -> JVMSetup ()`
+
+### MIR heap values
+
+MIR verification has a single `mir_points_to` command:
+
+* `mir_points_to : SetupValue -> SetupValue -> MIRSetup ()`
+takes two `SetupValue` arguments, the first of which must be a reference,
+and states that the memory specified by that reference should contain the
+value given in the second argument (which may be any type of
+`SetupValue`).
+
 ## Working with Compound Types
 
 The commands mentioned so far give us no way to specify the values of

intTests/test_mir_points_to/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_points_to/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:6:10: 6:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:6:5: 6:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}]},"name":"test/398eaa54::write_to_ref","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:7","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/398eaa54::read_from_ref","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/398eaa54::write_to_ref","kind":"Item","substs":[]},"name":"test/398eaa54::write_to_ref"},{"inst":{"def_id":"test/398eaa54::read_from_ref","kind":"Item","substs":[]},"name":"test/398eaa54::read_from_ref"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::953fce25114368d0","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}}],"roots":["test/398eaa54::read_from_ref","test/398eaa54::write_to_ref"]}

intTests/test_mir_points_to/test.rs

@@ -0,0 +1,7 @@
+pub fn read_from_ref(x: &u32) -> u32 {
+    *x
+}
+
+pub fn write_to_ref(x: &mut u32, y: u32) {
+    *x = y
+}

intTests/test_mir_points_to/test.saw

@@ -0,0 +1,54 @@
+enable_experimental;
+
+let read_from_ref_spec = do {
+  ptr <- mir_alloc mir_u32;
+  x <- mir_fresh_var "x" mir_u32;
+  mir_points_to ptr (mir_term x);
+
+  mir_execute_func [ptr];
+
+  mir_return (mir_term x);
+};
+
+// This spec will cause SAW to read from uninitialized memory.
+
+let read_from_ref_spec_bad = do {
+  ptr <- mir_alloc mir_u32;
+
+  mir_execute_func [ptr];
+
+  mir_return (mir_term {{ 42 : [32] }});
+};
+
+let write_to_ref_spec = do {
+  ptr <- mir_alloc_mut mir_u32;
+  y <- mir_fresh_var "y" mir_u32;
+
+  mir_execute_func [ptr, mir_term y];
+
+  mir_points_to ptr (mir_term y);
+};
+
+// This spec contains a type error, as `write_to_ref` expects a mutable
+// reference, but the spec allocates an immutable reference.
+
+let write_to_ref_spec_bad = do {
+  ptr <- mir_alloc mir_u32;
+  y <- mir_fresh_var "y" mir_u32;
+
+  mir_execute_func [ptr, mir_term y];
+
+  mir_points_to ptr (mir_term y);
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+mir_verify m "test::read_from_ref" [] false read_from_ref_spec z3;
+mir_verify m "test::write_to_ref" [] false write_to_ref_spec z3;
+
+fails (
+  mir_verify m "test::read_from_ref" [] false read_from_ref_spec_bad z3
+);
+fails (
+  mir_verify m "test::write_to_ref" [] false write_to_ref_spec_bad z3
+);

intTests/test_mir_points_to/test.sh

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

saw-remote-api/CHANGELOG.md

@@ -1,5 +1,19 @@
 # Revision history for saw-remote-api
 
+## next -- TBA
+
+* Add remote API support for SAW's experimental MIR verification support:
+
+  * The `SAW/MIR/load module` command loads a MIR JSON file into SAW.
+  * The `SAW/MIR/verify` command performs verification of a MIR function.
+
+  See the [remote API
+  documentation](https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/docs/SAW.rst#sawmirload-module-command)
+  for more detailed APIs for each of these commands. For more information about
+  how SAW's MIR verification support works in general, see the `mir_*` commands
+  documented in the [SAW
+  manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md).
+
 ## 1.0.0 -- 2023-06-26
 
 * The v1.0.0 release is made in tandem with the SAW 1.0 release. See the

saw-remote-api/python/CHANGELOG.md

@@ -1,5 +1,18 @@
 # Revision history for saw-client
 
+## next -- TBA
+
+* Add Python bindings for SAW's experimental MIR verification support:
+
+  * The `mir_load_module` function loads a MIR JSON file into SAW.
+  * The `mir_verify` function performs verification of a MIR function.
+  * The `saw_client.mir` module contains utility functions for constructing
+    MIR types.
+
+  For more information about how SAW's MIR verification support works in
+  general, see the `mir_*` commands documented in the [SAW
+  manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md).
+
 ## 1.0.1 -- YYYY-MM-DD
 
 * Add `solver_cache.py` implementing an interface for interacting with SAW

saw-remote-api/python/tests/saw/test-files/mir_points_to.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"mir_points_to.rs:2:5: 2:7","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"mir_points_to.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"mir_points_to/5452b69b::read_from_ref","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"mir_points_to.rs:6:10: 6:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::953fce25114368d0"}},"pos":"mir_points_to.rs:6:5: 6:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_points_to.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}]},"name":"mir_points_to/5452b69b::write_to_ref","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_points_to/5452b69b::read_from_ref","kind":"Item","substs":[]},"name":"mir_points_to/5452b69b::read_from_ref"},{"inst":{"def_id":"mir_points_to/5452b69b::write_to_ref","kind":"Item","substs":[]},"name":"mir_points_to/5452b69b::write_to_ref"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::Ref::953fce25114368d0","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}}],"roots":["mir_points_to/5452b69b::read_from_ref","mir_points_to/5452b69b::write_to_ref"]}

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

@@ -0,0 +1,7 @@
+pub fn read_from_ref(x: &u32) -> u32 {
+    *x
+}
+
+pub fn write_to_ref(x: &mut u32, y: u32) {
+    *x = y
+}

saw-remote-api/python/tests/saw/test_mir_points_to.py

@@ -0,0 +1,56 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import cry, cry_f
+from saw_client.mir import Contract, FreshVar, MIRType, SetupVal, u32, void
+
+
+def ref_to_fresh(c : Contract, ty : MIRType, name : Optional[str] = None,
+                 read_only : bool = False) -> Tuple[FreshVar, SetupVal]:
+    """Add to ``Contract`` ``c`` an allocation of a reference of type ``ty`` initialized to an unknown fresh value.
+    If ``read_only == True`` then the allocated memory is immutable.
+
+    :returns A fresh variable bound to the reference's initial value and the newly allocated reference. (The fresh
+             variable will be assigned ``name`` if provided/available.)"""
+    var = c.fresh_var(ty, name)
+    ptr = c.alloc(ty, points_to = var, read_only = read_only)
+    return (var, ptr)
+
+
+class ReadFromRefContract(Contract):
+    def specification(self) -> None:
+        (x, x_p) = ref_to_fresh(self, u32, "x", read_only = True)
+
+        self.execute_func(x_p)
+
+        self.returns_f('{x}')
+
+
+class WriteToRefContract(Contract):
+    def specification(self) -> None:
+        ptr = self.alloc(u32, read_only = False)
+        y = self.fresh_var(u32, 'y')
+
+        self.execute_func(ptr, y)
+
+        self.points_to(ptr, y)
+        self.returns(void)
+
+
+class MIRPointsToTest(unittest.TestCase):
+    def test_mir_points_to(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        json_name = str(Path('tests', 'saw', 'test-files', 'mir_points_to.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        read_from_ref_result = mir_verify(mod, 'mir_points_to::read_from_ref', ReadFromRefContract())
+        self.assertIs(read_from_ref_result.is_success(), True)
+
+        write_to_ref_result = mir_verify(mod, 'mir_points_to::write_to_ref', WriteToRefContract())
+        self.assertIs(write_to_ref_result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()