diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index ba75861a..6fbbe583 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -35,6 +35,7 @@ class KeccakFunctionManager: self._index_counter = TOTAL_PARTS - 34534 self.hash_result_store = {} # type: Dict[int, List[BitVec]] self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests + self.concrete_hashes = {} # type: Dict[BitVec, BitVec] @staticmethod def find_concrete_keccak(data: BitVec) -> BitVec: @@ -85,8 +86,14 @@ class KeccakFunctionManager: length = data.size() func, inverse = self.get_function(length) + if data.symbolic is False: + concrete_hash = self.find_concrete_keccak(data) + self.concrete_hashes[data] = concrete_hash + # This condition is essential to avoid some edge cases + condition = And(func(data) == concrete_hash, inverse(func(data)) == data) + return concrete_hash, condition + condition = self._create_condition(func_input=data) - self.quick_inverse[func(data)] = data self.hash_result_store[length].append(func(data)) return func(data), condition @@ -132,7 +139,11 @@ class KeccakFunctionManager: ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, ) - return cond + concrete_cond = symbol_factory.Bool(False) + for key, keccak in self.concrete_hashes.items(): + hash_eq = And(func(func_input) == keccak, key == func_input,) + concrete_cond = Or(concrete_cond, hash_eq) + return And(inv(func(func_input)) == func_input, Or(cond, concrete_cond)) keccak_function_manager = KeccakFunctionManager() diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 8bbca5ca..54c0bd5e 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -177,15 +177,7 @@ def test_vmtest( expected = int(value, 16) actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): - if ( - actual.symbolic - and actual in keccak_function_manager.quick_inverse - ): - actual = keccak_function_manager.find_concrete_keccak( - keccak_function_manager.quick_inverse[actual] - ) - else: - actual = actual.value + actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual else: if type(actual) == bytes: