Fix all the mypy errors

mythril/laser/ethereum/instructions.py

@@ -718,14 +718,14 @@ class Instruction:
             return [global_state]
 
         try:
-            dstart = util.get_concrete_int(op1)      # type: Union[int, BitVec]
+            dstart = util.get_concrete_int(op1)  # type: Union[int, BitVec]
         except TypeError:
             log.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
             dstart = simplify(op1)
 
         size_sym = False
         try:
-            size = util.get_concrete_int(op2)    # type: Union[int, BitVec]
+            size = util.get_concrete_int(op2)  # type: Union[int, BitVec]
         except TypeError:
             log.debug("Unsupported symbolic size in CALLDATACOPY")
             size = simplify(op2)

mythril/laser/ethereum/state/calldata.py

@@ -34,14 +34,14 @@ class BaseCalldata:
         self.tx_id = tx_id
 
     @property
-    def calldatasize(self) -> Expression:
+    def calldatasize(self) -> BitVec:
         """
 
         :return: Calldata size for this calldata object
         """
         result = self.size
         if isinstance(result, int):
-            return symbol_factory.BitVecVal(result, 256)
+            return BitVec(symbol_factory.BitVecVal(result, 256))
         return result
 
     def get_word_at(self, offset: int) -> Expression:
@@ -267,18 +267,24 @@ class BasicSymbolicCalldata(BaseCalldata):
         :param tx_id: Id of the transaction that the calldata is for.
         """
         self._reads = []  # type: List[Tuple[Union[int, BitVec], BitVec]]
-        self._size = BitVec(str(tx_id) + "_calldatasize", 256)
+        self._size = BitVec(symbol_factory.BitVecSym(str(tx_id) + "_calldatasize", 256))
         super().__init__(tx_id)
 
     def _load(self, item: Union[int, BitVec], clean=False) -> Any:
         expr_item = (
-            symbol_factory.BitVecVal(item, 256) if isinstance(item, int) else item
+            BitVec(symbol_factory.BitVecVal(item, 256))
+            if isinstance(item, int)
+            else item
         )  # type: BitVec
 
         symbolic_base_value = If(
             expr_item >= self._size,
             symbol_factory.BitVecVal(0, 8),
-            BitVec("{}_calldata_{}".format(self.tx_id, str(item)), 8),
+            BitVec(
+                symbol_factory.BitVecSym(
+                    "{}_calldata_{}".format(self.tx_id, str(item)), 8
+                )
+            ),
         )
         return_value = symbolic_base_value
         for r_index, r_value in self._reads:

mythril/laser/ethereum/state/memory.py

@@ -83,6 +83,7 @@ class Memory:
             assert len(_bytes) == 32
             self[index : index + 32] = list(bytearray(_bytes))
         except (Z3Exception, AttributeError):  # BitVector or BoolRef
+            value = cast(Union[BitVec, Bool], value)
             if isinstance(value, Bool):
                 value_to_write = If(
                     value,

mythril/laser/ethereum/svm.py

@@ -97,7 +97,7 @@ class LaserEVM:
         self.pre_hooks = defaultdict(list)  # type: DefaultDict[str, List[Callable]]
         self.post_hooks = defaultdict(list)  # type: DefaultDict[str, List[Callable]]
 
-        self._add_world_state_hooks = []    # type: List[Callable]
+        self._add_world_state_hooks = []  # type: List[Callable]
         self.iprof = InstructionProfiler() if enable_iprof else None
 
         log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))

mythril/laser/ethereum/util.py

@@ -84,6 +84,7 @@ def pop_bitvec(state: "MachineState") -> BitVec:
     elif isinstance(item, int):
         return symbol_factory.BitVecVal(item, 256)
     else:
+        item = cast(BitVec, item)
         return simplify(item)
 
 

mythril/laser/smt/bitvec.py

@@ -11,7 +11,6 @@ Annotations = List[Any]
 
 # fmt: off
 
-
 class BitVec(Expression[z3.BitVecRef]):
     """A bit vector symbol."""
 
@@ -140,6 +139,24 @@ class BitVec(Expression[z3.BitVecRef]):
         union = self.annotations + other.annotations
         return Bool(self.raw > other.raw, annotations=union)
 
+    def __le__(self, other: "BitVec") -> Bool:
+        """Create a signed less than expression.
+
+        :param other:
+        :return:
+        """
+        union = self.annotations + other.annotations
+        return Bool(self.raw <= other.raw, annotations=union)
+
+    def __ge__(self, other: "BitVec") -> Bool:
+        """Create a signed greater than expression.
+
+        :param other:
+        :return:
+        """
+        union = self.annotations + other.annotations
+        return Bool(self.raw >= other.raw, annotations=union)
+
     # MYPY: fix complains about overriding __eq__
     def __eq__(self, other: Union[int, "BitVec"]) -> Bool:  # type: ignore
         """Create an equality expression.