Add functions to fit with z3 library

mythril/laser/smt/__init__.py

@@ -38,6 +38,7 @@ class _SmtSymbolFactory(SymbolFactory):
     An implementation of a SymbolFactory that creates symbols using
     the classes in: mythril.laser.smt
     """
+
     @staticmethod
     def BitVecVal(value: int, size: int, annotations=None):
         """ Creates a new bit vector with a concrete value """
@@ -56,6 +57,7 @@ class _Z3SymbolFactory(SymbolFactory):
     An implementation of a SymbolFactory that directly returns
     z3 symbols
     """
+
     @staticmethod
     def BitVecVal(value: int, size: int, annotations=None):
         """ Creates a new bit vector with a concrete value """
@@ -69,4 +71,3 @@ class _Z3SymbolFactory(SymbolFactory):
 
 # This is the instance that other parts of mythril should use
 symbol_factory = _Z3SymbolFactory()
-

mythril/laser/smt/bitvec.py

@@ -108,4 +108,3 @@ def SRem(a: BitVec, b: BitVec) -> BitVec:
 def UDiv(a: BitVec, b: BitVec) -> BitVec:
     union = a.annotations + b.annotations
     return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)
-

mythril/laser/smt/bool.py

@@ -8,10 +8,17 @@ from mythril.laser.smt.expression import Expression
 class Bool(Expression):
 
     @property
-    def is_false(self):
+    def is_false(self) -> bool:
         return z3.is_false(self.raw)
 
     @property
-    def is_true(self):
+    def is_true(self) -> bool:
         return z3.is_true(self.raw)
 
+
+def is_false(a: Bool) -> bool:
+    return is_false(a)
+
+
+def is_true(a: Bool) -> bool:
+    return is_true(a)