Merge pull request #1133 from GaloisInc/wip/T1132

Add llvm_pointer to SAWScript, fix Python's `ptr`

Author: mergify[bot]

CHANGES.md

@@ -24,6 +24,9 @@ To avoid confusion, a new `llvm_alias` function has been introduced, and
 `llvm_struct` is now a synonym for `llvm_alias`. The `llvm_struct` function
 continues to be available for now.
 
+SAWScript includes a new `llvm_pointer : LLVMType -> LLVMType` function for
+constructing LLVM pointer types.
+
 # Version 0.7
 
 ## New Features

intTests/test1132/test.bc

@@ -0,0 +1,7 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+void f(uint8_t **x) {
+  *x = malloc(sizeof(uint8_t));
+  **x = 42;
+}

intTests/test1132/test.c

@@ -0,0 +1,11 @@
+bc <- llvm_load_module "test.bc";
+
+let f_contract = do {
+  x <- llvm_alloc (llvm_pointer (llvm_int 8));
+  llvm_execute_func [x];
+  p <- llvm_alloc (llvm_int 8);
+  llvm_points_to x p;
+  llvm_points_to p (llvm_term {{ 42 : [8] }});
+};
+
+llvm_verify bc "f" [] false f_contract abc;

intTests/test1132/test.saw

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

intTests/test1132/test.sh

@@ -0,0 +1,129 @@
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+pip-wheel-metadata/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+#  Usually these files are written by a python script from a template
+#  before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+.python-version
+
+# pipenv
+#   According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+#   However, in case of collaboration, if having platform-specific dependencies or dependencies
+#   having no cross-platform support, pipenv may install dependencies that don't work, or not
+#   install all needed dependencies.
+#Pipfile.lock
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/

saw-remote-api/python/.gitignore

@@ -27,7 +27,7 @@ def __init__(self, points_to : 'LLVMType') -> None:
         self.points_to = points_to
 
     def to_json(self) -> Any:
-        return {'type': 'pointer', 'points to': self.points_to.to_json()}
+        return {'type': 'pointer', 'to type': self.points_to.to_json()}
 
 class LLVMAliasType(LLVMType):
     def __init__(self, name : str) -> None:

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

@@ -0,0 +1,7 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+void f(uint8_t **x) {
+  *x = malloc(sizeof(uint8_t));
+  **x = 42;
+}

saw-remote-api/python/tests/saw/test-files/llvm_pointer.bc

@@ -0,0 +1,40 @@
+from pathlib import Path
+import unittest
+from saw import *
+from saw.llvm import Contract, cryptol, void
+import saw.llvm_types as ty
+
+
+class FContract(Contract):
+    def specification(self):
+        x = self.alloc(ty.ptr(ty.i8))
+
+        self.execute_func(x)
+
+        p = self.alloc(ty.i8)
+        self.points_to(x, p)
+        self.points_to(p, cryptol("42 : [8]"))
+        self.returns(void)
+
+
+class LLVMPointerTest(unittest.TestCase):
+
+    @classmethod
+    def setUpClass(self):
+        connect(reset_server=True)
+
+    @classmethod
+    def tearDownClass(self):
+        disconnect()
+
+    def test_llvm_pointer(self):
+        if __name__ == "__main__": view(LogResults())
+        bcname = str(Path('tests','saw','test-files', 'llvm_pointer.bc'))
+        mod = llvm_load_module(bcname)
+
+        result = llvm_verify(mod, 'f', FContract())
+        self.assertIs(result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

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

@@ -1746,6 +1746,12 @@ primitives = Map.fromList
     [ "Legacy alternative name for `llvm_alias`."
     ]
 
+  , prim "llvm_pointer"        "LLVMType -> LLVMType"
+    (pureVal llvm_pointer)
+    Current
+    [ "The type of an LLVM pointer that points to the given type."
+    ]
+
   , prim "llvm_load_module"    "String -> TopLevel LLVMModule"
     (pureVal llvm_load_module)
     Current

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

@@ -67,5 +67,8 @@ llvm_alias n = LLVM.Alias (fromString n)
 llvm_packed_struct_type :: [LLVM.Type] -> LLVM.Type
 llvm_packed_struct_type = LLVM.PackedStruct
 
+llvm_pointer :: LLVM.Type -> LLVM.Type
+llvm_pointer = LLVM.PtrTo
+
 llvm_struct_type :: [LLVM.Type] -> LLVM.Type
 llvm_struct_type = LLVM.Struct