Final fixes for DSChief (#1257)

* Final fixes

* Update mythril/laser/ethereum/keccak_function_manager.py

Co-Authored-By: JoranHonig <JoranHonig@users.noreply.github.com>

* Update mythril/laser/ethereum/keccak_function_manager.py

Co-Authored-By: JoranHonig <JoranHonig@users.noreply.github.com>

* Remove 64

* Make some changes

* rename store_hashes to hash_result_store

* only append concrete_val if we can successfully find it

otherwise we append the previous concrete_val again

* update documentation accordingly

mythril/analysis/modules/exceptions.py

@@ -31,6 +31,8 @@ class ReachableExceptionsModule(DetectionModule):
         :param state:
         :return:
         """
+        if state.get_current_instruction()["address"] in self.cache:
+            return
         issues = self._analyze_state(state)
         for issue in issues:
             self.cache.add(issue.address)

mythril/analysis/solver.py

@@ -138,6 +138,7 @@ def get_transaction_sequence(
 def _replace_with_actual_sha(
     concrete_transactions: List[Dict[str, str]], model: z3.Model, code=None
 ):
+    concrete_hashes = keccak_function_manager.get_concrete_hash_data(model)
     for tx in concrete_transactions:
         if hash_matcher not in tx["input"]:
             continue
@@ -151,22 +152,14 @@ def _replace_with_actual_sha(
                 continue
             find_input = symbol_factory.BitVecVal(int(data_slice, 16), 256)
             input_ = None
-            for size in keccak_function_manager.store_function:
-                _, inverse = keccak_function_manager.get_function(size)
-                try:
-                    input_ = symbol_factory.BitVecVal(
-                        model.eval(inverse(find_input).raw).as_long(), size
-                    )
-                except AttributeError:
+            for size in concrete_hashes:
+                _, inverse = keccak_function_manager.store_function[size]
+                if find_input.value not in concrete_hashes[size]:
                     continue
-                hex_input = hex(input_.value)[2:]
-                found = False
-                for new_tx in concrete_transactions:
-                    if hex_input in new_tx["input"]:
-                        found = True
-                        break
-                if found:
-                    break
+                input_ = symbol_factory.BitVecVal(
+                    model.eval(inverse(find_input).raw).as_long(), size
+                )
+
             if input_ is None:
                 continue
             keccak = keccak_function_manager.find_concrete_keccak(input_)

mythril/laser/ethereum/keccak_function_manager.py

@@ -10,7 +10,7 @@ from mythril.laser.smt import (
     Bool,
     Or,
 )
-from typing import Dict, Tuple, List
+from typing import Dict, Tuple, List, Optional
 
 TOTAL_PARTS = 10 ** 40
 PART = (2 ** 256 - 1) // TOTAL_PARTS
@@ -33,6 +33,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.hash_result_store = {}  # type: Dict[int, List[BitVec]]
         self.quick_inverse = {}  # type: Dict[BitVec, BitVec]  # This is for VMTests
 
     @staticmethod
@@ -63,6 +64,7 @@ class KeccakFunctionManager:
             func = Function("keccak256_{}".format(length), length, 256)
             inverse = Function("keccak256_{}-1".format(length), 256, length)
             self.store_function[length] = (func, inverse)
+            self.hash_result_store[length] = []
         return func, inverse
 
     @staticmethod
@@ -85,8 +87,27 @@ class KeccakFunctionManager:
 
         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
 
+    def get_concrete_hash_data(self, model) -> Dict[int, List[Optional[int]]]:
+        """
+        returns concrete values of hashes in the self.hash_result_store
+        :param model: The z3 model to query for concrete values
+        :return: A dictionary with concrete hashes { <hash_input_size> : [<concrete_hash>, <concrete_hash>]}
+        """
+        concrete_hashes = {}  # type: Dict[int, List[Optional[int]]]
+        for size in self.hash_result_store:
+            concrete_hashes[size] = []
+            for val in self.hash_result_store[size]:
+                eval_ = model.eval(val.raw)
+                try:
+                    concrete_val = eval_.as_long()
+                    concrete_hashes[size].append(concrete_val)
+                except AttributeError:
+                    continue
+        return concrete_hashes
+
     def _create_condition(self, func_input: BitVec) -> Bool:
         """
         Creates the constraints for hash