diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index fcd20731..d0f69d94 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -23,7 +23,6 @@ class KeccakFunctionManager: 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.concrete_hash_vals = {} # type: Dict[int, List[BitVec]] def find_keccak(self, data: BitVec) -> BitVec: """ @@ -51,7 +50,6 @@ class KeccakFunctionManager: except KeyError: func = Function("keccak256_{}".format(length), length, 256) inverse = Function("keccak256_{}-1".format(length), 256, length) - self.concrete_hash_vals[length] = [] self.store_function[length] = (func, inverse) return func, inverse @@ -73,14 +71,8 @@ class KeccakFunctionManager: length = data.size() func, inverse = self.get_function(length) - if data.symbolic: - condition = self._create_condition(func_input=data) - output = func(data) - else: - concrete_val = self.find_keccak(data) - condition = And(func(data) == concrete_val, inverse(func(data)) == data) - self.concrete_hash_vals[length].append(concrete_val) - output = concrete_val + condition = self._create_condition(func_input=data) + output = func(data) return output, condition def _create_condition(self, func_input: BitVec) -> Bool: @@ -107,8 +99,6 @@ class KeccakFunctionManager: ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, ) - for val in self.concrete_hash_vals[length]: - cond = Or(cond, func(func_input) == val) return cond