From ffb50a8fa928b7d39e16d36992531c7b6f2a20c2 Mon Sep 17 00:00:00 2001
From: Nikhil <nikhilparasaram@gmail.com>
Date: Thu, 4 Jul 2019 11:38:31 +0530
Subject: [PATCH] Add LRU cache to speedup

---
 mythril/analysis/modules/dos.py             |  1 +
 mythril/analysis/solver.py                  | 15 ++++++++++-----
 mythril/laser/ethereum/state/constraints.py |  6 ++++++
 3 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/mythril/analysis/modules/dos.py b/mythril/analysis/modules/dos.py
index b788eee0..88024d5e 100644
--- a/mythril/analysis/modules/dos.py
+++ b/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
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 16a74eae..42abb4e1 100644
--- a/mythril/analysis/solver.py
+++ b/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
     )
-    model = get_model(tx_constraints, minimize=minimize)
+
+    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)
diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index 73b33516..1f675ca5 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/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__()