Make some changes

mythril/analysis/solver.py

@@ -169,7 +169,7 @@ def _replace_with_actual_sha(
                     break
             if input_ is None:
                 continue
-            keccak = keccak_function_manager.find_keccak(input_)
+            keccak = keccak_function_manager.find_concrete_keccak(input_)
             hex_keccak = hex(keccak.value)
             if len(hex_keccak) != 66:
                 hex_keccak = "0x" + "0" * (66 - len(hex_keccak)) + hex_keccak[2:]

mythril/laser/ethereum/keccak_function_manager.py

@@ -19,13 +19,24 @@ hash_matcher = "fffffff"  # This is usually the prefix for the hash in the outpu
 
 
 class KeccakFunctionManager:
+    """
+    A bunch of uninterpreted functions are considered like keccak256_160 ,...
+    where keccak256_160 means the input of keccak256() is 160 bit number.
+    the range of these functions are constrained to some mutually disjoint intervals
+    All the hashes modulo 64 are 0 as we need a spread among hashes for array type data structures
+    All the functions are kind of one to one due to constraint of the existence of inverse
+    for each encountered input.
+    For more info https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf
+    """
+
     def __init__(self):
         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:
+    @staticmethod
+    def find_concrete_keccak(data: BitVec) -> BitVec:
         """
         Calculates concrete keccak
         :param data: input bitvecval

mythril/laser/ethereum/state/constraints.py

@@ -95,8 +95,7 @@ class Constraints(list):
         :return: The copied constraint List
         """
         constraint_list = super(Constraints, self).copy()
-        constraints = Constraints(constraint_list, is_possible=self._is_possible)
-        return constraints
+        return Constraints(constraint_list, is_possible=self._is_possible)
 
     def __add__(self, constraints: List[Union[bool, Bool]]) -> "Constraints":
         """
@@ -106,10 +105,7 @@ class Constraints(list):
         """
         constraints_list = self._get_smt_bool_list(constraints)
         constraints_list = super(Constraints, self).__add__(constraints_list)
-        new_constraints = Constraints(
-            constraint_list=constraints_list, is_possible=None
-        )
-        return new_constraints
+        return Constraints(constraint_list=constraints_list, is_possible=None)
 
     def __iadd__(self, constraints: Iterable[Union[bool, Bool]]) -> "Constraints":
         """

tests/laser/evm_testsuite/evm_test.py

@@ -181,7 +181,7 @@ def test_vmtest(
                         actual.symbolic
                         and actual in keccak_function_manager.quick_inverse
                     ):
-                        actual = keccak_function_manager.find_keccak(
+                        actual = keccak_function_manager.find_concrete_keccak(
                             keccak_function_manager.quick_inverse[actual]
                         )
                     else: