From 027db3fb10cef061169ab1494a8b5009ba91b215 Mon Sep 17 00:00:00 2001 From: Dominik Muhs Date: Thu, 1 Nov 2018 18:17:30 +0100 Subject: [PATCH] Replace specific Z3 hints with broader ExprRef --- mythril/laser/ethereum/call.py | 8 ++++---- mythril/laser/ethereum/instructions.py | 4 ++-- mythril/laser/ethereum/keccak.py | 4 ++-- mythril/laser/ethereum/natives.py | 2 +- mythril/laser/ethereum/state.py | 14 +++++++------- mythril/laser/ethereum/taint_analysis.py | 10 +++++----- .../ethereum/transaction/transaction_models.py | 6 +++--- mythril/laser/ethereum/util.py | 2 +- 8 files changed, 25 insertions(+), 25 deletions(-) diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index b96e5ac3..518428d2 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -1,6 +1,6 @@ import logging from typing import Union -from z3 import simplify, BitVecRef, BitVecNumRef, BoolRef, Extract +from z3 import simplify, ExprRef, Extract import mythril.laser.ethereum.util as util from mythril.laser.ethereum.state import Account, CalldataType, GlobalState, Calldata from mythril.support.loader import DynLoader @@ -57,7 +57,7 @@ def get_call_parameters( def get_callee_address( - global_state: GlobalState, dynamic_loader: DynLoader, symbolic_to_address: BitVecRef + global_state: GlobalState, dynamic_loader: DynLoader, symbolic_to_address: ExprRef ): """ Gets the address of the callee @@ -143,8 +143,8 @@ def get_callee_account( def get_call_data( global_state: GlobalState, - memory_start: Union[int, BitVecNumRef, BoolRef], - memory_size: Union[int, BitVecNumRef, BoolRef], + memory_start: Union[int, ExprRef], + memory_size: Union[int, ExprRef], pad=True, ): """ diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 9fa8613e..941b57f6 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1,7 +1,7 @@ import binascii import logging from copy import copy, deepcopy -from typing import Callable, List +from typing import Callable, List, Union from ethereum import utils from z3 import ( @@ -886,7 +886,7 @@ class Instruction: return self._sload_helper(global_state, str(index)) @staticmethod - def _sload_helper(global_state, index, constraints=None): + def _sload_helper(global_state: GlobalState, index: Union[int, ExprRef], constraints=None): try: data = global_state.environment.active_account.storage[index] except KeyError: diff --git a/mythril/laser/ethereum/keccak.py b/mythril/laser/ethereum/keccak.py index d99c49aa..6899ca35 100644 --- a/mythril/laser/ethereum/keccak.py +++ b/mythril/laser/ethereum/keccak.py @@ -1,11 +1,11 @@ -from z3 import ExprRef, BitVecRef +from z3 import ExprRef class KeccakFunctionManager: def __init__(self): self.keccak_expression_mapping = {} - def is_keccak(self, expression: BitVecRef) -> bool: + def is_keccak(self, expression: ExprRef) -> bool: return str(expression) in self.keccak_expression_mapping.keys() def get_argument(self, expression: str) -> ExprRef: diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py index 8c9eeb60..2de3cfde 100644 --- a/mythril/laser/ethereum/natives.py +++ b/mythril/laser/ethereum/natives.py @@ -3,7 +3,7 @@ import copy import hashlib import logging -from typing import List, Union +from typing import Union from ethereum.utils import ecrecover_to_pub from py_ecc.secp256k1 import N as secp256k1n diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index ae44c5db..0889677f 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -149,7 +149,7 @@ class Storage: self._storage[item] = BitVec("storage_" + str(item), 256) return self._storage[item] - def __setitem__(self, key: str, value: BitVecRef) -> None: + def __setitem__(self, key: str, value: ExprRef) -> None: self._storage[key] = value def keys(self) -> KeysView: @@ -194,10 +194,10 @@ class Account: def __str__(self) -> str: return str(self.as_dict) - def set_balance(self, balance: BitVecRef) -> None: + def set_balance(self, balance: ExprRef) -> None: self.balance = balance - def add_balance(self, balance: BitVecRef) -> None: + def add_balance(self, balance: ExprRef) -> None: self.balance += balance @property @@ -218,11 +218,11 @@ class Environment: def __init__( self, active_account: Account, - sender: BitVecRef, + sender: ExprRef, calldata: Calldata, - gasprice: BitVecRef, - callvalue: BitVecRef, - origin: BitVecRef, + gasprice: ExprRef, + callvalue: ExprRef, + origin: ExprRef, code=None, calldata_type=CalldataType.SYMBOLIC, ): diff --git a/mythril/laser/ethereum/taint_analysis.py b/mythril/laser/ethereum/taint_analysis.py index d014e78f..ff4da314 100644 --- a/mythril/laser/ethereum/taint_analysis.py +++ b/mythril/laser/ethereum/taint_analysis.py @@ -1,7 +1,7 @@ import logging import copy from typing import Union, List, Tuple -from z3 import BitVecNumRef +from z3 import ExprRef import mythril.laser.ethereum.util as helper from mythril.laser.ethereum.cfg import JumpType, Node from mythril.laser.ethereum.state import GlobalState, Environment @@ -238,7 +238,7 @@ class TaintRunner: record.stack[l], record.stack[i] = record.stack[i], record.stack[l] @staticmethod - def mutate_mload(record: TaintRecord, op0: BitVecNumRef) -> None: + def mutate_mload(record: TaintRecord, op0: ExprRef) -> None: _ = record.stack.pop() try: index = helper.get_concrete_int(op0) @@ -250,7 +250,7 @@ class TaintRunner: record.stack.append(record.memory_tainted(index)) @staticmethod - def mutate_mstore(record: TaintRecord, op0: BitVecNumRef) -> None: + def mutate_mstore(record: TaintRecord, op0: ExprRef) -> None: _, value_taint = record.stack.pop(), record.stack.pop() try: index = helper.get_concrete_int(op0) @@ -261,7 +261,7 @@ class TaintRunner: record.memory[index] = value_taint @staticmethod - def mutate_sload(record: TaintRecord, op0: BitVecNumRef) -> None: + def mutate_sload(record: TaintRecord, op0: ExprRef) -> None: _ = record.stack.pop() try: index = helper.get_concrete_int(op0) @@ -273,7 +273,7 @@ class TaintRunner: record.stack.append(record.storage_tainted(index)) @staticmethod - def mutate_sstore(record: TaintRecord, op0: BitVecNumRef) -> None: + def mutate_sstore(record: TaintRecord, op0: ExprRef) -> None: _, value_taint = record.stack.pop(), record.stack.pop() try: index = helper.get_concrete_int(op0) diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 4860e56c..57c747f7 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -8,7 +8,7 @@ from mythril.laser.ethereum.state import ( Account, Calldata, ) -from z3 import BitVec, BitVecNumRef +from z3 import BitVec, ExprRef import array _next_transaction_id = 0 @@ -47,7 +47,7 @@ class MessageCallTransaction: self, world_state: WorldState, callee_account: Account, - caller: BitVecNumRef, + caller: ExprRef, call_data=None, identifier=None, gas_price=None, @@ -119,7 +119,7 @@ class ContractCreationTransaction: def __init__( self, world_state: WorldState, - caller: BitVecNumRef, + caller: ExprRef, identifier=None, callee_account=None, code=None, diff --git a/mythril/laser/ethereum/util.py b/mythril/laser/ethereum/util.py index 966c9c0d..dfa1ff9b 100644 --- a/mythril/laser/ethereum/util.py +++ b/mythril/laser/ethereum/util.py @@ -63,7 +63,7 @@ def pop_bitvec(state: "MachineState") -> BitVecVal: return simplify(item) -def get_concrete_int(item: Union[int, BitVecNumRef, BoolRef]) -> int: +def get_concrete_int(item: Union[int, ExprRef]) -> int: if isinstance(item, int): return item elif isinstance(item, BitVecNumRef):