diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index ecb33f6c..4404224f 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -169,7 +169,7 @@ def _replace_with_actual_sha( break if input_ is None: continue - keccak = keccak_function_manager.find_keccak(input_) + keccak = keccak_function_manager.find_concrete_keccak(input_) hex_keccak = hex(keccak.value) if len(hex_keccak) != 66: hex_keccak = "0x" + "0" * (66 - len(hex_keccak)) + hex_keccak[2:] diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index f79838a8..6d5262ee 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -19,13 +19,24 @@ hash_matcher = "fffffff" # This is usually the prefix for the hash in the outpu class KeccakFunctionManager: + """ + A bunch of uninterpreted functions are considered like keccak256_160 ,... + where keccak256_160 means the input of keccak256() is 160 bit number. + the range of these functions are constrained to some mutually disjoint intervals + All the hashes modulo 64 are 0 as we need a spread among hashes for array type data structures + All the functions are kind of one to one due to constraint of the existence of inverse + for each encountered input. + For more info https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf + """ + def __init__(self): self.store_function = {} # type: Dict[int, Tuple[Function, Function]] self.interval_hook_for_size = {} # type: Dict[int, int] self._index_counter = TOTAL_PARTS - 34534 self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests - def find_keccak(self, data: BitVec) -> BitVec: + @staticmethod + def find_concrete_keccak(data: BitVec) -> BitVec: """ Calculates concrete keccak :param data: input bitvecval diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 0357b493..b4b101a3 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -95,8 +95,7 @@ class Constraints(list): :return: The copied constraint List """ constraint_list = super(Constraints, self).copy() - constraints = Constraints(constraint_list, is_possible=self._is_possible) - return constraints + return Constraints(constraint_list, is_possible=self._is_possible) def __add__(self, constraints: List[Union[bool, Bool]]) -> "Constraints": """ @@ -106,10 +105,7 @@ class Constraints(list): """ constraints_list = self._get_smt_bool_list(constraints) constraints_list = super(Constraints, self).__add__(constraints_list) - new_constraints = Constraints( - constraint_list=constraints_list, is_possible=None - ) - return new_constraints + return Constraints(constraint_list=constraints_list, is_possible=None) def __iadd__(self, constraints: Iterable[Union[bool, Bool]]) -> "Constraints": """ diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 9b9b913f..8bbca5ca 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -181,7 +181,7 @@ def test_vmtest( actual.symbolic and actual in keccak_function_manager.quick_inverse ): - actual = keccak_function_manager.find_keccak( + actual = keccak_function_manager.find_concrete_keccak( keccak_function_manager.quick_inverse[actual] ) else: