Set solver timeout and loop bound for analysis modules

mythril/analysis/analysis_args.py

@@ -0,0 +1,28 @@
+from mythril.support.support_utils import Singleton
+
+
+class AnalysisArgs(object, metaclass=Singleton):
+    """
+    This module helps in preventing args being sent through multiple of classes to reach analysis modules
+    """
+
+    def __init__(self):
+        self._loop_bound = 4
+        self._solver_timeout = 100000
+
+    def set_loop_bound(self, loop_bound: int):
+        self._loop_bound = loop_bound
+
+    def set_solver_timeout(self, solver_timeout: int):
+        self._solver_timeout = solver_timeout
+
+    @property
+    def loop_bound(self):
+        return self._loop_bound
+
+    @property
+    def solver_timeout(self):
+        return self._solver_timeout
+
+
+analysis_args = AnalysisArgs()

mythril/analysis/modules/deprecated_ops.py

@@ -35,6 +35,7 @@ class DeprecatedOperationsModule(DetectionModule):
         if state.get_current_instruction()["address"] in self._cache:
             return
         issues = self._analyze_state(state)
+
         for issue in issues:
             self._cache.add(issue.address)
         self._issues.extend(issues)
@@ -74,13 +75,13 @@ class DeprecatedOperationsModule(DetectionModule):
             )
             swc_id = DEPRECATED_FUNCTIONS_USAGE
         else:
-            return
+            return []
         try:
             transaction_sequence = get_transaction_sequence(
                 state, state.mstate.constraints
             )
         except UnsatError:
-            return
+            return []
         issue = Issue(
             contract=state.environment.active_account.contract_name,
             function_name=state.environment.active_function_name,

mythril/analysis/modules/dos.py

@@ -7,6 +7,7 @@ from mythril.analysis.swc_data import DOS_WITH_BLOCK_GAS_LIMIT
 from mythril.analysis.report import Issue
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.solver import get_transaction_sequence, UnsatError
+from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum import util
@@ -90,7 +91,7 @@ class DosModule(DetectionModule):
             else:
                 annotation.jump_targets[target] = 1
 
-            if annotation.jump_targets[target] > 2:
+            if annotation.jump_targets[target] > min(2, analysis_args.loop_bound - 1):
                 annotation.loop_start = address
 
         elif annotation.loop_start is not None:

mythril/analysis/solver.py

@@ -4,6 +4,7 @@ from typing import Dict, Tuple, Union
 from z3 import sat, unknown, FuncInterp
 import z3
 
+from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction import BaseTransaction
@@ -29,7 +30,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
     :return:
     """
     s = Optimize()
-    timeout = 100000
+    timeout = analysis_args.solver_timeout
     if enforce_execution_time:
         timeout = min(timeout, time_handler.time_remaining() - 500)
         if timeout <= 0:

mythril/analysis/symbolic.py

@@ -47,7 +47,7 @@ class SymExecWrapper:
         dynloader=None,
         max_depth=22,
         execution_timeout=None,
-        loop_bound=2,
+        loop_bound=4,
         create_timeout=None,
         transaction_count=2,
         modules=(),

mythril/interfaces/cli.py

@@ -346,6 +346,12 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
         default=86400,
         help="The amount of seconds to spend on symbolic execution",
     )
+    options.add_argument(
+        "--solver-timeout",
+        type=int,
+        default=100000,
+        help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules",
+    )
     options.add_argument(
         "--create-timeout",
         type=int,
@@ -552,6 +558,7 @@ def execute_command(
             enable_iprof=args.enable_iprof,
             disable_dependency_pruning=args.disable_dependency_pruning,
             onchain_storage_access=not args.no_onchain_storage_access,
+            solver_timeout=args.solver_timeout,
         )
 
         if not disassembler.contracts:

mythril/interfaces/old_cli.py

@@ -213,6 +213,12 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
         default=2,
         help="Maximum number of transactions issued by laser",
     )
+    options.add_argument(
+        "--solver-timeout",
+        type=int,
+        default=100000,
+        help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules",
+    )
     options.add_argument(
         "--execution-timeout",
         type=int,
@@ -419,6 +425,7 @@ def execute_command(
         enable_iprof=args.enable_iprof,
         disable_dependency_pruning=args.disable_dependency_pruning,
         onchain_storage_access=not args.no_onchain_storage_access,
+        solver_timeout=args.solver_timeout,
     )
 
     if args.disassemble:

mythril/mythril/mythril_analyzer.py

@@ -10,6 +10,7 @@ from mythril.support.source_support import Source
 from mythril.support.loader import DynLoader
 from mythril.analysis.symbolic import SymExecWrapper
 from mythril.analysis.callgraph import generate_graph
+from mythril.analysis.analysis_args import analysis_args
 from mythril.analysis.traceexplore import get_serializable_statespace
 from mythril.analysis.security import fire_lasers, retrieve_callback_issues
 from mythril.analysis.report import Report, Issue
@@ -39,6 +40,7 @@ class MythrilAnalyzer:
         create_timeout: Optional[int] = None,
         enable_iprof: bool = False,
         disable_dependency_pruning: bool = False,
+        solver_timeout: Optional[int] = None,
     ):
         """
 
@@ -60,6 +62,9 @@ class MythrilAnalyzer:
         self.enable_iprof = enable_iprof
         self.disable_dependency_pruning = disable_dependency_pruning
 
+        analysis_args.set_loop_bound(loop_bound)
+        analysis_args.set_solver_timeout(solver_timeout)
+
     def dump_statespace(self, contract: EVMContract = None) -> str:
         """
         Returns serializable statespace of the contract