diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py index f6537d17..452124b4 100644 --- a/mythril/laser/ethereum/keccak_function_manager.py +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -20,9 +20,10 @@ INTERVAL_DIFFERENCE = 10 ** 30 class KeccakFunctionManager: def __init__(self): - self.store_function: Dict[int, Tuple[Function, Function]] = {} - self.interval_hook_for_size: Dict[int, int] = {} - self._index_counter: int = TOTAL_PARTS - 34534 + 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: keccak = symbol_factory.BitVecVal( @@ -67,7 +68,7 @@ class KeccakFunctionManager: URem(func(data), symbol_factory.BitVecVal(64, 256)) == 0, ) constraints.append(condition) - + self.quick_inverse[func(data)] = data return func(data), constraints def get_new_cond(self, val, length: int): diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 244b5844..8afe3d14 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -1,5 +1,6 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.state.world_state import WorldState from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.transaction.concolic import execute_message_call @@ -117,7 +118,6 @@ def test_vmtest( # Arrange if test_name in ignored_test_names: return - world_state = WorldState() for address, details in pre_condition.items(): @@ -178,7 +178,15 @@ def test_vmtest( expected = int(value, 16) actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): - actual = actual.value + if ( + actual.symbolic + and actual in keccak_function_manager.quick_inverse + ): + actual = keccak_function_manager.find_keccak( + keccak_function_manager.quick_inverse[actual] + ) + else: + actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual else: if type(actual) == bytes: