From 41de34284e1445a577e78ba2a24c9dd242a1d15c Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Tue, 4 Dec 2018 11:58:47 +0100
Subject: [PATCH] Init smt abstraction

---
 mythril/laser/smt/__init__.py   |  0
 mythril/laser/smt/bitvec.py     | 76 +++++++++++++++++++++++++++++++++
 mythril/laser/smt/expression.py | 14 ++++++
 3 files changed, 90 insertions(+)
 create mode 100644 mythril/laser/smt/__init__.py
 create mode 100644 mythril/laser/smt/bitvec.py
 create mode 100644 mythril/laser/smt/expression.py

diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py
new file mode 100644
index 00000000..5f721a3e
--- /dev/null
+++ b/mythril/laser/smt/bitvec.py
@@ -0,0 +1,76 @@
+import z3
+
+from mythril.laser.smt.expression import Expression
+
+
+class BitVec(Expression):
+    def __init__(self, raw, annotations=None):
+        super().__init__(raw, annotations)
+
+    def __add__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return BitVec(self.raw + other.raw, annotations=union)
+
+    def __sub__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return BitVec(self.raw - other.raw, annotations=union)
+
+    def __mul__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return BitVec(self.raw * other.raw, annotations=union)
+
+    def __truediv__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return BitVec(self.raw / other.raw, annotations=union)
+
+
+def UREM(a: BitVec, b: BitVec) -> BitVec:
+    union = a.annotations + b.annotations
+    return BitVec(z3.URem(a.raw, b.raw), annotations=union)
+
+
+def SREM(a: BitVec, b: BitVec) -> BitVec:
+    union = a.annotations + b.annotations
+    return BitVec(z3.SRem(a.raw, b.raw), annotations=union)
+
+
+def UDIV(a: BitVec, b: BitVec) -> BitVec:
+    union = a.annotations + b.annotations
+    return BitVec(z3.UDIV(a.raw, b.raw), annotations=union)
+
+
+def BitVecVal(value, size, annotations=None):
+    raw = z3.BitVecVal(value, size)
+    return BitVec(raw, annotations)
+
+
+def BitVecSym(name, size, annotations=None):
+    raw = z3.BitVec(name, size)
+    return BitVec(raw, annotations)
+
+
+class OverflowAnnotation:
+    def __init__(self, location):
+        self.location = location
+
+    @staticmethod
+    def it_overflows(expression, location):
+        a = OverflowAnnotation(location)
+        expression.annotate(a)
+
+    @staticmethod
+    def does_overflow(expression):
+        locs = []
+        for annotation in expression.annotations:
+            if isinstance(annotation, OverflowAnnotation):
+                locs.append(annotation.location)
+        return len(locs) > 0
+
+
+x = BitVecSym("x", 256)
+
+OverflowAnnotation.it_overflows(x, 10)
+
+y = x + BitVecVal(2, 256)
+
+print(OverflowAnnotation.does_overflow(y))
diff --git a/mythril/laser/smt/expression.py b/mythril/laser/smt/expression.py
new file mode 100644
index 00000000..94b65444
--- /dev/null
+++ b/mythril/laser/smt/expression.py
@@ -0,0 +1,14 @@
+class Expression:
+    def __init__(self, raw, annotations=None):
+        self.raw = raw
+        self._annotations = annotations or []
+
+    @property
+    def annotations(self):
+        return self._annotations
+
+    def annotate(self, annotation):
+        if isinstance(annotation, list):
+            self._annotations += annotation
+        else:
+            self._annotations.append(annotation)