Python bindings: Add test case for proclaim, proclaim_f

Related to #1676.

Author: RyanGlScott

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()