Merge pull request #2006 from GaloisInc/T2005-mir_lifetime

Add `mir_lifetime`

doc/manual/manual.md

@@ -2254,6 +2254,7 @@ MIR types are built up using the following functions:
 * `mir_isize : MIRType`
 * `mir_f32 : MIRType`
 * `mir_f64 : MIRType`
+* `mir_lifetime : MIRType`
 * `mir_ref : MIRType -> MIRType`
 * `mir_ref_mut : MIRType -> MIRType`
 * `mir_slice : MIRType -> MIRType`
@@ -3244,6 +3245,40 @@ Note that `mir_enum_value` can only be used to construct a specific variant. If
 you need to construct a symbolic enum value that can range over many potential
 variants, use `mir_fresh_expanded_value` instead.
 
+#### Lifetimes
+
+Rust ADTs can have both type parameters as well as _lifetime_ parameters. The
+following Rust code declares a lifetime parameter `'a` on the struct `S`, as
+well on the function `f` that computes an `S` value:
+
+~~~~ .rs
+pub struct S<'a> {
+    pub x: &'a u32,
+}
+
+pub fn f<'a>(y: &'a u32) -> S<'a> {
+    S { x: y }
+}
+~~~~
+
+When `mir-json` compiles a piece of Rust code that contains lifetime
+parameters, it will instantiate all of the lifetime parameters with a
+placeholder MIR type that is simply called `lifetime`. This is important to
+keep in mind when looking up ADTs with `mir_find_adt`, as you will also need to
+indicate to SAW that the lifetime parameter is instantiated with `lifetime`. In
+order to do so, use `mir_lifetime`. For example, here is how to look up `S`
+with `'a` instantiated to `lifetime`:
+
+~~~~
+s_adt = mir_find_adt m "example::S" [mir_lifetime]
+~~~~
+
+Note that this part of SAW's design is subject to change in the future.
+Ideally, users would not have to care about lifetimes at all at the MIR level;
+see [this issue](https://github.com/GaloisInc/mir-json/issues/58) for further
+discussion on this point. If that issue is fixed, then we will likely remove
+`mir_lifetime`, as it will no longer be necessary.
+
 ### Bitfields
 
 SAW has experimental support for specifying `struct`s with bitfields, such as

intTests/test2005_mir_lifetime/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/test2005_mir_lifetime/test.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":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:6:12: 6:13","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"test.rs:6:5: 6:15"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::e028c0f25e8b6323"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::188545d5524e10a7"}},"pos":"test.rs:6:5: 6:15","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::188545d5524e10a7"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/c76ff53f::f","return_ty":"ty::Adt::188545d5524e10a7","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/c76ff53f::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"test/c76ff53f::S","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/c76ff53f::S::x","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"test/c76ff53f::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/c76ff53f::f","kind":"Item","substs":[]},"name":"test/c76ff53f::f"}],"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::Adt::188545d5524e10a7","ty":{"kind":"Adt","name":"test/c76ff53f::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"test/c76ff53f::S","substs":["nonty::Lifetime"]}}],"roots":["test/c76ff53f::f"]}

intTests/test2005_mir_lifetime/test.rs

@@ -0,0 +1,7 @@
+pub struct S<'a> {
+    pub x: &'a u32,
+}
+
+pub fn f<'a>(y: &'a u32) -> S<'a> {
+    S { x: y }
+}

intTests/test2005_mir_lifetime/test.saw

@@ -0,0 +1,18 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+
+let s_adt = mir_find_adt m "test::S" [mir_lifetime];
+
+let f_spec = do {
+  y_ref <- mir_alloc mir_u32;
+  y_val <- mir_fresh_var "y" mir_u32;
+  mir_points_to y_ref (mir_term y_val);
+
+  mir_execute_func [y_ref];
+
+  let s = mir_struct_value s_adt [y_ref];
+  mir_return s;
+};
+
+mir_verify m "test::f" [] false f_spec z3;

intTests/test2005_mir_lifetime/test.sh

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

saw-remote-api/python/saw_client/mir.py

@@ -42,6 +42,9 @@
 f64 = MIRF64Type()
 """A MIR double-precision floating-point type."""
 
+lifetime = MIRLifetimeType()
+"""A MIR lifetime type."""
+
 u8 = MIRU8Type()
 """A MIR 8-bit unsigned integer type."""
 

saw-remote-api/python/saw_client/mir_type.py

@@ -69,6 +69,10 @@ class MIRIsizeType(MIRType):
     def to_json(self) -> Any:
         return { 'type': 'isize' }
 
+class MIRLifetimeType(MIRType):
+    def to_json(self) -> Any:
+        return { 'type': 'lifetime' }
+
 class MIRRefType(MIRType):
     def __init__(self, referent_type : 'MIRType') -> None:
         self.referent_type = referent_type

saw-remote-api/python/tests/saw/test-files/mir_lifetime.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":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_lifetime.rs:6:12: 6:13","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"mir_lifetime.rs:6:5: 6:15"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::Ref::e028c0f25e8b6323"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::f4c7fe891009a901"}},"pos":"mir_lifetime.rs:6:5: 6:15","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_lifetime.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::f4c7fe891009a901"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"mir_lifetime/10484a10::f","return_ty":"ty::Adt::f4c7fe891009a901","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"mir_lifetime/10484a10::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"mir_lifetime/10484a10::S","orig_substs":["nonty::Lifetime"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"mir_lifetime/10484a10::S::x","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"mir_lifetime/10484a10::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_lifetime/10484a10::f","kind":"Item","substs":[]},"name":"mir_lifetime/10484a10::f"}],"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::Adt::f4c7fe891009a901","ty":{"kind":"Adt","name":"mir_lifetime/10484a10::S::_adtbd21306cbe4f0b9b[0]","orig_def_id":"mir_lifetime/10484a10::S","substs":["nonty::Lifetime"]}}],"roots":["mir_lifetime/10484a10::f"]}

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

@@ -0,0 +1,7 @@
+pub struct S<'a> {
+    pub x: &'a u32,
+}
+
+pub fn f<'a>(y: &'a u32) -> S<'a> {
+    S { x: y }
+}

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

@@ -0,0 +1,49 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import struct
+from saw_client.mir import Contract, FreshVar, MIRAdt, MIRType, SetupVal, lifetime, u32
+
+
+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 FContract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        (_, y) = ref_to_fresh(self, u32, read_only = True)
+
+        self.execute_func(y)
+
+        s = struct(y, mir_adt = self.adt)
+        self.returns(s)
+
+
+class MIRLifetimeTest(unittest.TestCase):
+    def test_mir_lifetime(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        json_name = str(Path('tests', 'saw', 'test-files', 'mir_lifetime.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        s_adt = mir_find_adt(mod, "mir_lifetime::S", lifetime)
+        f_result = mir_verify(mod, 'mir_lifetime::f', FContract(s_adt))
+        self.assertIs(f_result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

saw-remote-api/src/SAWServer/Data/MIRType.hs

@@ -25,6 +25,7 @@ data MIRTypeTag
   | TagIsize
   | TagF32
   | TagF64
+  | TagLifetime
   | TagRef
   | TagRefMut
   | TagSlice
@@ -53,6 +54,7 @@ instance JSON.FromJSON MIRTypeTag where
       "isize" -> pure TagIsize
       "f32" -> pure TagF32
       "f64" -> pure TagF64
+      "lifetime" -> pure TagLifetime
       "ref" -> pure TagRef
       "ref mut" -> pure TagRefMut
       "slice" -> pure TagSlice
@@ -83,6 +85,7 @@ data JSONMIRType
   | JSONTyChar
   | JSONTyFloat !Mir.FloatKind
   | JSONTyInt !Mir.BaseSize
+  | JSONTyLifetime
   | JSONTyRef !JSONMIRType !Mir.Mutability
   | JSONTySlice !JSONMIRType
   | JSONTyStr
@@ -110,6 +113,7 @@ instance JSON.FromJSON JSONMIRType where
           TagIsize -> pure $ JSONTyInt Mir.USize
           TagF32 -> pure $ JSONTyFloat Mir.F32
           TagF64 -> pure $ JSONTyFloat Mir.F64
+          TagLifetime -> pure JSONTyLifetime
           TagRef -> JSONTyRef <$> o .: "referent type" <*> pure Mir.Immut
           TagRefMut -> JSONTyRef <$> o .: "referent type" <*> pure Mir.Mut
           TagSlice -> JSONTySlice <$> o .: "slice type"
@@ -141,6 +145,7 @@ mirType sawenv = go
     go JSONTyChar = Mir.TyChar
     go (JSONTyFloat fk) = Mir.TyFloat fk
     go (JSONTyInt bs) = Mir.TyInt bs
+    go JSONTyLifetime = Mir.TyLifetime
     go (JSONTyRef ty mut) = Mir.TyRef (go ty) mut
     go (JSONTySlice ty) = Mir.TySlice (go ty)
     go JSONTyStr = Mir.TyStr

src/SAWScript/Crucible/MIR/Builtins.hs

@@ -44,6 +44,7 @@ module SAWScript.Crucible.MIR.Builtins
   , mir_isize
   , mir_f32
   , mir_f64
+  , mir_lifetime
   , mir_ref
   , mir_ref_mut
   , mir_slice
@@ -797,6 +798,9 @@ mir_f32 = Mir.TyFloat Mir.F32
 mir_f64 :: Mir.Ty
 mir_f64 = Mir.TyFloat Mir.F64
 
+mir_lifetime :: Mir.Ty
+mir_lifetime = Mir.TyLifetime
+
 mir_ref :: Mir.Ty -> Mir.Ty
 mir_ref ty = Mir.TyRef ty Mir.Immut
 

src/SAWScript/Interpreter.hs

@@ -4168,6 +4168,11 @@ primitives = Map.fromList
     Experimental
     [ "The type of MIR double-precision floating-point values." ]
 
+  , prim "mir_lifetime" "MIRType"
+    (pureVal mir_lifetime)
+    Experimental
+    [ "The type of MIR lifetimes." ]
+
   , prim "mir_ref" "MIRType -> MIRType"
     (pureVal mir_ref)
     Experimental