Implement interpreter for symbolic expressions

1 files changed, 22 insertions, 0 deletions

diff --git a/utils.py b/utils.py
index 1390283..f2c2256 100644
--- a/utils.py
+++ b/utils.py
@@ -14,3 +14,25 @@ def check_version(version: str):
     if sys.version_info.major < major and sys.version_info.minor < minor:
         raise EnvironmentError("Expected at least Python 3.7")
 
+def to_str(expr):
+    """Convert a claripy expression to a nice string representation.
+
+    Actually, the resulting representation is not very nice at all. It mostly
+    serves debugging purposes.
+    """
+    import claripy
+
+    if not issubclass(type(expr), claripy.ast.Base):
+        return f'{type(expr)}[{str(expr)}]'
+
+    assert(expr.depth > 0)
+    if expr.depth == 1:
+        if expr.symbolic:
+            name = expr._encoded_name.decode()
+            return f'symbol[{name}]'
+        else:
+            assert(expr.concrete)
+            return f'value{expr.length}[{hex(expr.v)}]'
+
+    args = [to_str(child) for child in expr.args]
+    return f'expr[{str(expr.op)}({", ".join(args)})]'