Merge pull request #1936 from GaloisInc/T1676

MIR: Achieve feature (+ documentation) parity between SAWScript and Python

Author: mergify[bot]

saw-remote-api/python/CHANGELOG.md

@@ -24,6 +24,11 @@
   an error.
 * Add a `tuple_value()` function for constructing MIR tuples. Using this
   function with LLVM or JVM verification will raise an error.
+* The `proclaim` function (which is the Python counterpart to to
+  `{llvm,jvm,mir}_assert` in SAWScript) is no longer deprecated.
+* Add a `proclaim_f` function. This behaves like the `proclaim` function, except
+  that it takes a `cry_f`-style format string as an argument. That is,
+  `proclaim_f(...)` is equivalent to `proclaim(cry_f(...))`.
 
 ## 1.0.1 -- YYYY-MM-DD
 

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

@@ -516,10 +516,15 @@ def ghost_value(self, var: GhostVariable, value: cryptoltypes.CryptolJSON) -> No
         else:
             raise Exception("wrong state")
 
-    @deprecated
     def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None:
-        """DEPRECATED: Use ``precondition`` or ``postcondition`` instead. This method will
-        eventually be removed."""
+        """Asserts ``proposition`` for the function ``Contract`` being
+        specified.
+
+        Usable either before or after ``execute_func`` in the contract
+        specification. If this is used before ``execute_func``, then
+        ``proposition`` is asserted as a precondition. If this is used after
+        ``execute_func``, then ``proposition`` is asserted as a postcondition.
+        """
         if not isinstance(proposition, CryptolTerm):
             condition = Condition(CryptolTerm(proposition))
         else:
@@ -531,6 +536,12 @@ def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSO
         else:
             raise Exception("wrong state")
 
+    def proclaim_f(self, s : str) -> None:
+        """Proclaims an assertion using a ``cry_f``-style format string, i.e.
+        ``proclaim_f(...)`` is equivalent to ``proclaim(cry_f(...))``"""
+        expression = to_cryptol_str_customf(s, frames=1, filename="<proclaim_f>")
+        return self.proclaim(expression)
+
     def precondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None:
         """Establishes ``proposition`` as a precondition for the function ```Contract```
         being specified.
@@ -572,6 +583,8 @@ def postcondition_f(self, s : str) -> None:
         return self.postcondition(expression)
 
     def returns(self, val : Union[Void,SetupVal]) -> None:
+        """Declare the return value for the function ``Contract`` being
+        specified."""
         if self.__state == 'post':
             if self.__returns is None:
                 self.__returns = val

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

@@ -9,36 +9,78 @@
 ##################################################
 
 bool_ty = MIRBoolType()
+"""A MIR boolean type."""
+
 char_ty = MIRCharType()
-str_ty  = MIRStrType()
+"""A MIR character type."""
+
+str_ty = MIRStrType()
+"""A MIR string type. Currently, SAW can only handle references to strings
+(``&str``)."""
+
+i8 = MIRI8Type()
+"""A MIR 8-bit signed integer type."""
+
+i16 = MIRI16Type()
+"""A MIR 16-bit signed integer type."""
+
+i32 = MIRI32Type()
+"""A MIR 32-bit signed integer type."""
+
+i64 = MIRI64Type()
+"""A MIR 64-bit signed integer type."""
+
+i128 = MIRI128Type()
+"""A MIR 128-bit signed integer type."""
 
-i8    = MIRI8Type()
-i16   = MIRI16Type()
-i32   = MIRI32Type()
-i64   = MIRI64Type()
-i128  = MIRI128Type()
 isize = MIRIsizeType()
+"""A MIR signed integer type that is pointer-sized."""
 
 f32 = MIRF32Type()
+"""A MIR single-precision floating-point type."""
+
 f64 = MIRF64Type()
+"""A MIR double-precision floating-point type."""
+
+u8 = MIRU8Type()
+"""A MIR 8-bit unsigned integer type."""
+
+u16 = MIRU16Type()
+"""A MIR 16-bit unsigned integer type."""
+
+u32 = MIRU32Type()
+"""A MIR 32-bit unsigned integer type."""
+
+u64 = MIRU64Type()
+"""A MIR 64-bit unsigned integer type."""
+
+u128 = MIRU128Type()
+"""A MIR 128-bit unsigned integer type."""
 
-u8    = MIRU8Type()
-u16   = MIRU16Type()
-u32   = MIRU32Type()
-u64   = MIRU64Type()
-u128  = MIRU128Type()
 usize = MIRUsizeType()
+"""A MIR unsigned integer type that is pointer-sized."""
 
 def adt_ty(adt: MIRAdt) -> 'MIRAdtType':
-    """An algebraic data type (ADT), i.e., a struct or an enum."""
+    """A MIR algebraic data type (ADT), i.e., a struct or an enum."""
     return MIRAdtType(adt)
 
 def array_ty(size : int, ty : 'MIRType') -> 'MIRArrayType':
     """``[ty; size]``, i.e. a MIR array of ``size`` elements of type ``ty``."""
     return MIRArrayType(ty, size)
 
+def ref_ty(ty : 'MIRType') -> 'MIRRefType':
+    """``&ty``, i.e., an immutable MIR reference type pointing to something of
+    type ``ty``."""
+    return MIRRefType(ty)
+
+def ref_mut_ty(ty : 'MIRType') -> 'MIRRefMutType':
+    """``&mut ty``, i.e., a mutable MIR reference type pointing to something of
+    type ``ty``."""
+    return MIRRefMutType(ty)
+
 def slice_ty(ty : MIRType) -> 'MIRSliceType':
-    """``[ty]``, i.e., a MIR slice to a type ``ty``."""
+    """``[ty]``, i.e., a MIR slice to a type ``ty``. Currently, SAW can only
+    handle references to slices (``&[ty]``)"""
     return MIRSliceType(ty)
 
 def tuple_ty(*tuple_types : MIRType) -> 'MIRTupleType':

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

@@ -69,6 +69,22 @@ class MIRIsizeType(MIRType):
     def to_json(self) -> Any:
         return { 'type': 'isize' }
 
+class MIRRefType(MIRType):
+    def __init__(self, referent_type : 'MIRType') -> None:
+        self.referent_type = referent_type
+
+    def to_json(self) -> Any:
+        return { 'type': 'ref',
+                 'referent type': self.referent_type.to_json() }
+
+class MIRRefMutType(MIRType):
+    def __init__(self, referent_type : 'MIRType') -> None:
+        self.referent_type = referent_type
+
+    def to_json(self) -> Any:
+        return { 'type': 'ref mut',
+                 'referent type': self.referent_type.to_json() }
+
 class MIRSliceType(MIRType):
     def __init__(self, slice_type : 'MIRType') -> None:
         self.slice_type = slice_type

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

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::i32"}},"pos":"mir_proclaim.rs:2:5: 2:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::423c819a0b13bfc4"}},"pos":"mir_proclaim.rs:2:5: 2:10","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::i32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"int","size":4,"val":"1"},"ty":"ty::i32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::423c819a0b13bfc4"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _2 + const 1_i32`, which would overflow","pos":"mir_proclaim.rs:2:5: 2:10","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}},"pos":"mir_proclaim.rs:2:5: 2:10","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::i32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::423c819a0b13bfc4"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_proclaim.rs:3:2: 3:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::i32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::423c819a0b13bfc4"}]},"name":"mir_proclaim/87c4cc87::f","return_ty":"ty::i32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_proclaim/87c4cc87::f","kind":"Item","substs":[]},"name":"mir_proclaim/87c4cc87::f"}],"tys":[{"name":"ty::i32","ty":{"intkind":{"kind":"I32"},"kind":"Int"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::423c819a0b13bfc4","ty":{"kind":"Tuple","tys":["ty::i32","ty::bool"]}}],"roots":["mir_proclaim/87c4cc87::f"]}

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

@@ -0,0 +1,3 @@
+pub fn f(x: i32) -> i32 {
+    x + 1
+}

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

@@ -0,0 +1,50 @@
+from pathlib import Path
+import unittest
+from saw_client import *
+from saw_client.crucible import cry, cry_f
+from saw_client.mir import Contract, i32
+
+
+class FContract1(Contract):
+    def specification(self):
+        x = self.fresh_var(i32, 'x')
+        self.proclaim(cry_f('{x} < 0x7fffffff'))
+
+        self.execute_func(x)
+
+        r = self.fresh_var(i32, 'r')
+        self.proclaim(cry_f('{r} == {x} + 1'))
+        self.proclaim(cry_f('{r} <= 0x7fffffff'))
+        self.returns(r)
+
+
+# Like FContract1, but using `proclaim_f` instead of `proclaim`.
+class FContract2(Contract):
+    def specification(self):
+        x = self.fresh_var(i32, 'x')
+        self.proclaim_f('{x} < 0x7fffffff')
+
+        self.execute_func(x)
+
+        r = self.fresh_var(i32, 'r')
+        self.proclaim_f('{r} == {x} + 1')
+        self.proclaim_f('{r} <= 0x7fffffff')
+        self.returns(r)
+
+
+class ProclaimTest(unittest.TestCase):
+    def test_proclaim(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        bcname = str(Path('tests','saw','test-files', 'mir_proclaim.linked-mir.json'))
+        mod = mir_load_module(bcname)
+
+        result1 = mir_verify(mod, 'mir_proclaim::f', FContract1())
+        self.assertIs(result1.is_success(), True)
+
+        result2 = mir_verify(mod, 'mir_proclaim::f', FContract2())
+        self.assertIs(result2.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

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

@@ -16,6 +16,7 @@ data MIRTypeTag
   = TagAdt
   | TagArray
   | TagBool
+  | TagChar
   | TagI8
   | TagI16
   | TagI32
@@ -24,6 +25,8 @@ data MIRTypeTag
   | TagIsize
   | TagF32
   | TagF64
+  | TagRef
+  | TagRefMut
   | TagSlice
   | TagStr
   | TagTuple
@@ -41,6 +44,7 @@ instance JSON.FromJSON MIRTypeTag where
       "adt" -> pure TagAdt
       "array" -> pure TagArray
       "bool" -> pure TagBool
+      "char" -> pure TagChar
       "i8" -> pure TagI8
       "i16" -> pure TagI16
       "i32" -> pure TagI32
@@ -49,6 +53,8 @@ instance JSON.FromJSON MIRTypeTag where
       "isize" -> pure TagIsize
       "f32" -> pure TagF32
       "f64" -> pure TagF64
+      "ref" -> pure TagRef
+      "ref mut" -> pure TagRefMut
       "slice" -> pure TagSlice
       "str" -> pure TagStr
       "tuple" -> pure TagTuple
@@ -74,8 +80,10 @@ data JSONMIRType
   = JSONTyAdt !ServerName
   | JSONTyArray !JSONMIRType !Int
   | JSONTyBool
+  | JSONTyChar
   | JSONTyFloat !Mir.FloatKind
   | JSONTyInt !Mir.BaseSize
+  | JSONTyRef !JSONMIRType !Mir.Mutability
   | JSONTySlice !JSONMIRType
   | JSONTyStr
   | JSONTyTuple ![JSONMIRType]
@@ -93,6 +101,7 @@ instance JSON.FromJSON JSONMIRType where
           TagAdt -> JSONTyAdt <$> o .: "ADT server name"
           TagArray -> JSONTyArray <$> o .: "element type" <*> o .: "size"
           TagBool -> pure JSONTyBool
+          TagChar -> pure JSONTyChar
           TagI8 -> pure $ JSONTyInt Mir.B8
           TagI16 -> pure $ JSONTyInt Mir.B16
           TagI32 -> pure $ JSONTyInt Mir.B32
@@ -101,6 +110,8 @@ instance JSON.FromJSON JSONMIRType where
           TagIsize -> pure $ JSONTyInt Mir.USize
           TagF32 -> pure $ JSONTyFloat Mir.F32
           TagF64 -> pure $ JSONTyFloat Mir.F64
+          TagRef -> JSONTyRef <$> o .: "referent type" <*> pure Mir.Immut
+          TagRefMut -> JSONTyRef <$> o .: "referent type" <*> pure Mir.Mut
           TagSlice -> JSONTySlice <$> o .: "slice type"
           TagStr -> pure JSONTyStr
           TagTuple -> JSONTyTuple <$> o .: "tuple types"
@@ -127,8 +138,10 @@ mirType sawenv = go
 
     go (JSONTyArray ty n) = Mir.TyArray (go ty) n
     go JSONTyBool = Mir.TyBool
+    go JSONTyChar = Mir.TyChar
     go (JSONTyFloat fk) = Mir.TyFloat fk
     go (JSONTyInt bs) = Mir.TyInt bs
+    go (JSONTyRef ty mut) = Mir.TyRef (go ty) mut
     go (JSONTySlice ty) = Mir.TySlice (go ty)
     go JSONTyStr = Mir.TyStr
     go (JSONTyTuple ts) = Mir.TyTuple (map go ts)