Implement global_lvalue and global_initializer in Python bindings

This checks off the first two bullet points of #1153. The third bullet point,
related to `llvm_alloc_global`, is left as future work.

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

@@ -153,6 +153,24 @@ def to_json(self) -> Any:
         return {'setup value': 'field',
                 'base': self.base.to_json(), 'field': self.field_name}
 
+class GlobalInitializerVal(SetupVal):
+    name : str
+
+    def __init__(self, name : str) -> None:
+        self.name = name
+
+    def to_json(self) -> Any:
+        return {'setup value': 'global initializer', 'name': self.name}
+
+class GlobalLValueVal(SetupVal):
+    name : str
+
+    def __init__(self, name : str) -> None:
+        self.name = name
+
+    def to_json(self) -> Any:
+        return {'setup value': 'global lvalue', 'name': self.name}
+
 name_regexp = re.compile('^(?P<prefix>.*[^0-9])?(?P<number>[0-9]+)?$')
 
 def next_name(x : str) -> str:
@@ -458,6 +476,16 @@ def field(base : SetupVal, field_name : str) -> 'FieldVal':
     """Returns a ``FieldVal`` using the field ``field_name`` of the struct ``base``."""
     return FieldVal(base, field_name)
 
+# It's tempting to name this `global` to mirror SAWScript's `llvm_global`,
+# but that would clash with the Python keyword `global`.
+def global_lvalue(name: str) -> 'GlobalLValueVal':
+    """Returns a ``GlobalLValueVal`` representing a pointer to the named global ``name``."""
+    return GlobalLValueVal(name)
+
+def global_initializer(name: str) -> 'GlobalInitializerVal':
+    """Returns a ``GlobalInitializerVal`` representing the value of the initializer of a named global ``name``."""
+    return GlobalInitializerVal(name)
+
 def struct(*fields : SetupVal) -> StructVal:
     """Returns a ``StructVal`` with fields ``fields``."""
     return StructVal(list(fields))

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

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

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

@@ -0,0 +1,38 @@
+from pathlib import Path
+import unittest
+from saw import *
+from saw.llvm import Contract, global_lvalue, global_initializer
+import saw.llvm_types as ty
+
+
+class FContract(Contract):
+    def specification(self):
+        x_init = global_initializer("x")
+        self.points_to(global_lvalue("x"), x_init)
+
+        self.execute_func()
+
+        self.returns(x_init)
+
+
+class LLVMGlobalTest(unittest.TestCase):
+
+    @classmethod
+    def setUpClass(self):
+        connect(reset_server=True)
+
+    @classmethod
+    def tearDownClass(self):
+        disconnect()
+
+    def test_llvm_global(self):
+        if __name__ == "__main__": view(LogResults())
+        bcname = str(Path('tests','saw','test-files', 'llvm_global.bc'))
+        mod = llvm_load_module(bcname)
+
+        result = llvm_verify(mod, 'f', FContract())
+        self.assertIs(result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()