Add LRU cache to speedup

mythril/analysis/modules/dos.py

@@ -104,6 +104,7 @@ class DOS(DetectionModule):
             description_tail = "{} is executed in a loop. Be aware that the transaction may fail to execute if the loop is unbounded and the necessary gas exceeds the block gas limit.".format(
                 operation
             )
+
             try:
                 transaction_sequence = get_transaction_sequence(
                     state, state.mstate.constraints

mythril/analysis/solver.py

@@ -1,10 +1,10 @@
 """This module contains analysis module helpers to solve path constraints."""
-from typing import Dict, List, Union
+from functools import lru_cache
+from typing import Dict, Tuple, Union
 from z3 import sat, unknown, FuncInterp
 import z3
 
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.ethereum.state.world_state import Account
 from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction import BaseTransaction
 from mythril.laser.smt import UGE, Optimize, symbol_factory
@@ -18,6 +18,7 @@ import logging
 log = logging.getLogger(__name__)
 
 
+@lru_cache(maxsize=10000000)
 def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
     """
 
@@ -95,7 +96,11 @@ def get_transaction_sequence(
     tx_constraints, minimize = _set_minimisation_constraints(
         transaction_sequence, constraints.copy(), [], 5000
     )
+
+    try:
         model = get_model(tx_constraints, minimize=minimize)
+    except UnsatError:
+        raise UnsatError
 
     min_price_dict = {}  # type: Dict[str, int]
     for transaction in transaction_sequence:
@@ -166,7 +171,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
 
 def _set_minimisation_constraints(
     transaction_sequence, constraints, minimize, max_size
-):
+) -> Tuple[Constraints, tuple]:
     """ Set constraints that minimise key transaction values
 
     Constraints generated:
@@ -188,4 +193,4 @@ def _set_minimisation_constraints(
         minimize.append(transaction.call_data.calldatasize)
         minimize.append(transaction.call_value)
 
-    return constraints, minimize
+    return constraints, tuple(minimize)

mythril/laser/ethereum/state/constraints.py

@@ -82,6 +82,9 @@ class Constraints(list):
         constraint_list = super(Constraints, self).copy()
         return Constraints(constraint_list, is_possible=self._is_possible)
 
+    def copy(self) -> "Constraints":
+        return self.__copy__()
+
     def __deepcopy__(self, memodict=None) -> "Constraints":
         """
 
@@ -117,3 +120,6 @@ class Constraints(list):
             constraint if isinstance(constraint, Bool) else Bool(constraint)
             for constraint in constraints
         ]
+
+    def __hash__(self):
+        return tuple(self[:]).__hash__()