Merge pull request #1159 from GaloisInc/python_llvm_null

Implement array_val(...) and null() in Python bindings

saw-remote-api/python/saw/llvm.py

@@ -171,6 +171,20 @@ def __init__(self, name : str) -> None:
     def to_json(self) -> Any:
         return {'setup value': 'global lvalue', 'name': self.name}
 
+class NullVal(SetupVal):
+    def to_json(self) -> Any:
+        return {'setup value': 'null'}
+
+class ArrayVal(SetupVal):
+    elements : List[SetupVal]
+
+    def __init__(self, elements : List[SetupVal]) -> None:
+        self.elements = elements
+
+    def to_json(self) -> Any:
+        return {'setup value': 'array',
+                'elements': [element.to_json() for element in self.elements]}
+
 name_regexp = re.compile('^(?P<prefix>.*[^0-9])?(?P<number>[0-9]+)?$')
 
 def next_name(x : str) -> str:
@@ -462,6 +476,10 @@ def to_json(self) -> Any:
             return self.__cached_json
 
 
+def array_val(element: SetupVal, *elements: SetupVal) -> SetupVal:
+    """Returns an ``ArrayVal`` representing an array with the given arguments as elements.
+    The array must be non-empty, and as a result, at least one argument must be provided."""
+    return ArrayVal([element] + list(elements))
 
 # FIXME Is `Any` too permissive here -- can we be a little more precise?
 def cryptol(data : Any) -> 'CryptolTerm':
@@ -486,6 +504,10 @@ def global_var(name: str) -> SetupVal:
     """Returns a ``GlobalVarVal`` representing a pointer to the named global ``name``."""
     return GlobalVarVal(name)
 
+def null() -> SetupVal:
+    """Returns a ``NullVal`` representing a null pointer value."""
+    return NullVal()
+
 def struct(*fields : SetupVal) -> SetupVal:
     """Returns a ``StructVal`` with fields ``fields``."""
     return StructVal(list(fields))

saw-remote-api/python/tests/saw/test-files/llvm_array_swap.c

@@ -0,0 +1,7 @@
+#include <stdint.h>
+
+void array_swap(uint32_t a[2]) {
+    uint32_t tmp = a[0];
+    a[0] = a[1];
+    a[1] = tmp;
+}

saw-remote-api/python/tests/saw/test-files/llvm_assert_null.c

@@ -0,0 +1,3 @@
+int f(int *x) {
+    return (x == (int*)0);
+}

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

@@ -0,0 +1,42 @@
+from pathlib import Path
+import unittest
+from saw import *
+from saw.llvm import Contract, array_val, elem, void
+import saw.llvm_types as ty
+
+
+class ArraySwapContract(Contract):
+    def specification(self):
+        a0 = self.fresh_var(ty.i32, "a0")
+        a1 = self.fresh_var(ty.i32, "a1")
+        a  = self.alloc(ty.array(2, ty.i32),
+                        points_to=array_val(a0, a1))
+
+        self.execute_func(a)
+
+        self.points_to(elem(a, 0), a1)
+        self.points_to(elem(a, 1), a0)
+        self.returns(void)
+
+
+class LLVMArraySwapTest(unittest.TestCase):
+
+    @classmethod
+    def setUpClass(self):
+        connect(reset_server=True)
+
+    @classmethod
+    def tearDownClass(self):
+        disconnect()
+
+    def test_llvm_array_swap(self):
+        if __name__ == "__main__": view(LogResults())
+        bcname = str(Path('tests','saw','test-files', 'llvm_array_swap.bc'))
+        mod = llvm_load_module(bcname)
+
+        result = llvm_verify(mod, 'array_swap', ArraySwapContract())
+        self.assertIs(result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

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

@@ -0,0 +1,47 @@
+from pathlib import Path
+import unittest
+from saw import *
+from saw.llvm import Contract, cryptol, null
+import saw.llvm_types as ty
+
+
+class FContract1(Contract):
+    def specification(self):
+        p = self.alloc(ty.i32)
+
+        self.execute_func(p)
+
+        self.returns(cryptol("0 : [32]"))
+
+
+class FContract2(Contract):
+    def specification(self):
+        self.execute_func(null())
+
+        self.returns(cryptol("1 : [32]"))
+
+
+class LLVMAssertNullTest(unittest.TestCase):
+
+    @classmethod
+    def setUpClass(self):
+        connect(reset_server=True)
+
+    @classmethod
+    def tearDownClass(self):
+        disconnect()
+
+    def test_llvm_assert_null(self):
+        if __name__ == "__main__": view(LogResults())
+        bcname = str(Path('tests','saw','test-files', 'llvm_assert_null.bc'))
+        mod = llvm_load_module(bcname)
+
+        result = llvm_verify(mod, 'f', FContract1())
+        self.assertIs(result.is_success(), True)
+
+        result = llvm_verify(mod, 'f', FContract2())
+        self.assertIs(result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()