add equality operations

mythril/laser/ethereum/instructions.py

@@ -49,6 +49,7 @@ from mythril.laser.ethereum.transaction import (
     TransactionStartSignal,
     ContractCreationTransaction,
 )
+
 from mythril.support.loader import DynLoader
 from mythril.analysis.solver import get_model
 

mythril/laser/smt/bitvec.py

@@ -1,7 +1,9 @@
 import z3
 
 from mythril.laser.smt.expression import Expression
+from mythril.laser.smt.bool import Bool
 
+# fmt: off
 
 class BitVec(Expression):
     def __init__(self, raw, annotations=None):
@@ -35,6 +37,28 @@ class BitVec(Expression):
         union = self.annotations + other.annotations
         return BitVec(self.raw ^ other.raw, annotations=union)
 
+    def __lt__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return Bool(self.raw < other.raw, annotations=union)
+
+    def __gt__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return Bool(self.raw < other.raw, annotations=union)
+
+    def __eq__(self, other: "BV") -> "BV":
+        union = self.annotations + other.annotations
+        return Bool(self.raw == other.raw, annotations=union)
+
+
+def UGT(a, b):
+    annotations = a.annotations + b.annotations
+    Bool(z3.UGT(a, b), annotations)
+
+
+def ULT(a, b):
+    annotations = a.annotations + b.annotations
+    Bool(z3.ULT(a, b), annotations)
+
 
 def Concat(*args):
     nraw = z3.Concat([a.raw for a in args])

mythril/laser/smt/bool.py

@@ -0,0 +1,9 @@
+import z3
+
+from mythril.laser.smt.expression import Expression
+
+# fmt: off
+
+
+class Bool(Expression):
+    pass