From f61f6c03643fab9b696ccd7a8b7629f8701f1d7e Mon Sep 17 00:00:00 2001
From: Nikhil <nikhilparasaram@gmail.com>
Date: Tue, 22 Oct 2019 15:06:23 +0100
Subject: [PATCH] Make some changes

---
 mythril/analysis/solver.py                        |  2 +-
 mythril/laser/ethereum/keccak_function_manager.py | 13 ++++++++++++-
 mythril/laser/ethereum/state/constraints.py       |  8 ++------
 tests/laser/evm_testsuite/evm_test.py             |  2 +-
 4 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index ecb33f6c..4404224f 100644
--- a/mythril/analysis/solver.py
+++ b/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:]
diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py
index f79838a8..6d5262ee 100644
--- a/mythril/laser/ethereum/keccak_function_manager.py
+++ b/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
diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index 0357b493..b4b101a3 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/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":
         """
diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py
index 9b9b913f..8bbca5ca 100644
--- a/tests/laser/evm_testsuite/evm_test.py
+++ b/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: