pull/1220/head
Nikhil 5 years ago
parent a5628219dc
commit 856547fa97
  1. 5
      mythril/laser/ethereum/keccak_function_manager.py
  2. 11
      tests/laser/evm_testsuite/evm_test.py

@ -23,6 +23,7 @@ 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.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests
def find_keccak(self, data: BitVec) -> BitVec:
"""
@ -72,8 +73,8 @@ class KeccakFunctionManager:
func, inverse = self.get_function(length)
condition = self._create_condition(func_input=data)
output = func(data)
return output, condition
self.quick_inverse[func(data)] = data
return func(data), condition
def _create_condition(self, func_input: BitVec) -> Bool:
"""

@ -1,6 +1,7 @@
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.transaction.concolic import execute_message_call
from mythril.laser.smt import Expression, BitVec, symbol_factory
@ -176,7 +177,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:

Loading…
Cancel
Save