Handle concrete hashes (#1339)

* Handle concrete hashes

* rename hash to keccak

* Use SMT Bool

* Make constraints cleaner

Co-authored-by: Bernhard Mueller <b-mueller@users.noreply.github.com>

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()

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: