diff --git a/saw-remote-api/python/saw/llvm.py b/saw-remote-api/python/saw/llvm.py index 169aae8e68..96c4cc97ca 100644 --- a/saw-remote-api/python/saw/llvm.py +++ b/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 GlobalVarVal(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.*[^0-9])?(?P[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) +def global_initializer(name: str) -> 'GlobalInitializerVal': + """Returns a ``GlobalInitializerVal`` representing the value of the initializer of a named global ``name``.""" + return GlobalInitializerVal(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_var(name: str) -> 'GlobalVarVal': + """Returns a ``GlobalVarVal`` representing a pointer to the named global ``name``.""" + return GlobalVarVal(name) + def struct(*fields : SetupVal) -> StructVal: """Returns a ``StructVal`` with fields ``fields``.""" return StructVal(list(fields)) diff --git a/saw-remote-api/python/tests/saw/test-files/llvm_global.bc b/saw-remote-api/python/tests/saw/test-files/llvm_global.bc new file mode 100644 index 0000000000..8b27768e00 Binary files /dev/null and b/saw-remote-api/python/tests/saw/test-files/llvm_global.bc differ diff --git a/saw-remote-api/python/tests/saw/test-files/llvm_global.c b/saw-remote-api/python/tests/saw/test-files/llvm_global.c new file mode 100644 index 0000000000..d58d7e324c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/llvm_global.c @@ -0,0 +1,5 @@ +const int x = 0; + +int f() { + return x; +} diff --git a/saw-remote-api/python/tests/saw/test_llvm_global.py b/saw-remote-api/python/tests/saw/test_llvm_global.py new file mode 100644 index 0000000000..a1b5dc3458 --- /dev/null +++ b/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_initializer, global_var +import saw.llvm_types as ty + + +class FContract(Contract): + def specification(self): + x_init = global_initializer("x") + self.points_to(global_var("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()