From dce26a37b274af1a2f35ba30e85f4b57d5120717 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 23 Jan 2019 20:52:57 +0530 Subject: [PATCH] Fix all the mypy errors --- mythril/laser/ethereum/instructions.py | 4 ++-- mythril/laser/ethereum/state/calldata.py | 16 +++++++++++----- mythril/laser/ethereum/state/memory.py | 1 + mythril/laser/ethereum/svm.py | 2 +- mythril/laser/ethereum/util.py | 1 + mythril/laser/smt/bitvec.py | 19 ++++++++++++++++++- 6 files changed, 34 insertions(+), 9 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index e48581a7..615c7d4a 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/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) diff --git a/mythril/laser/ethereum/state/calldata.py b/mythril/laser/ethereum/state/calldata.py index 4a170b2d..26780a4f 100644 --- a/mythril/laser/ethereum/state/calldata.py +++ b/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: diff --git a/mythril/laser/ethereum/state/memory.py b/mythril/laser/ethereum/state/memory.py index affd118c..4fac4120 100644 --- a/mythril/laser/ethereum/state/memory.py +++ b/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, diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index a0f743e7..a373db42 100644 --- a/mythril/laser/ethereum/svm.py +++ b/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)) diff --git a/mythril/laser/ethereum/util.py b/mythril/laser/ethereum/util.py index 6f4f326a..9cb5d950 100644 --- a/mythril/laser/ethereum/util.py +++ b/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) diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index a4905ff6..cfad231d 100644 --- a/mythril/laser/smt/bitvec.py +++ b/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.