Handles issue with low constructor loop bound and new way to deal with solver-timeout (#1668)

* Add exit code

* Update docs with tutorial

* Fix docs

* Reformat

* Fix the issue with loop-bound and solver-timeout

* Add test changes

* Restrict hexbytes

mythril/exceptions.py

@@ -20,6 +20,13 @@ class UnsatError(MythrilBaseException):
     pass
 
 
+class SolverTimeOutException(UnsatError):
+    """A Mythril exception denoting the unsatisfiability of a series of
+    constraints."""
+
+    pass
+
+
 class NoContractFoundError(MythrilBaseException):
     """A Mythril exception denoting that a given contract file was not
     found."""

mythril/interfaces/cli.py

@@ -511,9 +511,10 @@ def add_analysis_args(options):
         help="Don't attempt to retrieve contract code, variables and balances from the blockchain",
     )
     options.add_argument(
-        "--sparse-pruning",
+        "--pruning-factor",
-        action="store_true",
+        type=float,
-        help="Checks for reachability after the end of tx. Recommended for short execution timeouts < 1 min",
+        default=1,
+        help="Checks for reachability at the rate of <pruning-factor>. Where 1 means checks every execution",
     )
     options.add_argument(
         "--unconstrained-storage",
@@ -752,7 +753,7 @@ def execute_command(
 
     elif args.command == SAFE_FUNCTIONS_COMMAND:
         args.unconstrained_storage = True
-        args.sparse_pruning = False
+        args.pruning_factor = 1
         args.disable_dependency_pruning = True
         args.no_onchain_data = True
         function_analyzer = MythrilAnalyzer(

mythril/laser/ethereum/state/constraints.py

@@ -1,6 +1,6 @@
 """This module contains the class used to represent state-change constraints in
 the call graph."""
-from mythril.exceptions import UnsatError
+from mythril.exceptions import UnsatError, SolverTimeOutException
 from mythril.laser.smt import symbol_factory, simplify, Bool
 from mythril.support.model import get_model
 from mythril.laser.ethereum.function_managers import keccak_function_manager
@@ -25,13 +25,19 @@ class Constraints(list):
         constraint_list = self._get_smt_bool_list(constraint_list)
         super(Constraints, self).__init__(constraint_list)
 
-    @property
+    def is_possible(self, solver_timeout=None) -> bool:
-    def is_possible(self) -> bool:
         """
+        :param solver_timeout: The default timeout uses analysis timeout from args.solver_timeout
         :return: True/False based on the existence of solution of constraints
         """
         try:
-            get_model(self)
+            get_model(self, solver_timeout=solver_timeout)
+        except SolverTimeOutException:
+            # If it uses the long analysis solver timeout
+            if solver_timeout is None:
+                return False
+            # If it uses a short custom solver timeout
+            return True
         except UnsatError:
             return False
         return True

mythril/laser/ethereum/strategy/extensions/bounded_loops.py

@@ -135,7 +135,7 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
             # TODO: There's probably a nicer way to do this
             if isinstance(
                 state.current_transaction, ContractCreationTransaction
-            ) and count < max(20, self.bound):
+            ) and count < max(128, self.bound):
                 return state
 
             elif count > self.bound:

mythril/laser/ethereum/svm.py

@@ -3,6 +3,7 @@ import logging
 from collections import defaultdict
 from copy import copy
 from datetime import datetime, timedelta
+import random
 from typing import Callable, Dict, DefaultDict, List, Tuple, Optional
 
 from mythril.support.opcodes import OPCODES
@@ -218,7 +219,9 @@ class LaserEVM:
             old_states_count = len(self.open_states)
             if self.use_reachability_check:
                 self.open_states = [
-                    state for state in self.open_states if state.constraints.is_possible
+                    state
+                    for state in self.open_states
+                    if state.constraints.is_possible()
                 ]
                 prune_count = old_states_count - len(self.open_states)
                 if prune_count:
@@ -282,11 +285,11 @@ class LaserEVM:
             except NotImplementedError:
                 log.debug("Encountered unimplemented instruction")
                 continue
-            if args.sparse_pruning is False:
+            if len(new_states) > 1 and random.uniform(0, 1) < args.pruning_factor:
                 new_states = [
                     state
                     for state in new_states
-                    if state.world_state.constraints.is_possible
+                    if state.world_state.constraints.is_possible()
                 ]
 
             self.manage_cfg(op_code, new_states)  # TODO: What about op_code is None?

mythril/mythril/mythril_analyzer.py

@@ -60,7 +60,7 @@ class MythrilAnalyzer:
             if cmd_args.custom_modules_directory
             else ""
         )
-        args.sparse_pruning = cmd_args.sparse_pruning
+        args.pruning_factor = cmd_args.pruning_factor
         args.solver_timeout = cmd_args.solver_timeout
         args.parallel_solving = cmd_args.parallel_solving
         args.unconstrained_storage = cmd_args.unconstrained_storage

mythril/support/model.py

@@ -5,7 +5,7 @@ from pathlib import Path
 from mythril.support.support_args import args
 from mythril.laser.smt import Optimize
 from mythril.laser.ethereum.time_handler import time_handler
-from mythril.exceptions import UnsatError
+from mythril.exceptions import UnsatError, SolverTimeOutException
 import logging
 
 log = logging.getLogger(__name__)
@@ -13,7 +13,13 @@ log = logging.getLogger(__name__)
 
 
 @lru_cache(maxsize=2**23)
-def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
+def get_model(
+    constraints,
+    minimize=(),
+    maximize=(),
+    enforce_execution_time=True,
+    solver_timeout=None,
+):
     """
     Returns a model based on given constraints as a tuple
     :param constraints: Tuple of constraints
@@ -23,7 +29,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
     :return:
     """
     s = Optimize()
-    timeout = args.solver_timeout
+    timeout = solver_timeout or args.solver_timeout
     if enforce_execution_time:
         timeout = min(timeout, time_handler.time_remaining() - 500)
         if timeout <= 0:
@@ -60,4 +66,5 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
         return s.model()
     elif result == unknown:
         log.debug("Timeout/Error encountered while solving expression using z3")
+        raise SolverTimeOutException
     raise UnsatError

mythril/support/support_args.py

@@ -10,7 +10,7 @@ class Args(object, metaclass=Singleton):
 
     def __init__(self):
         self.solver_timeout = 10000
-        self.sparse_pruning = True
+        self.pruning_factor = 1
         self.unconstrained_storage = False
         self.parallel_solving = False
         self.call_depth_limit = 3

requirements.txt

@@ -16,6 +16,7 @@ eth-keys<0.4.0,>=0.2.1
 eth-rlp<0.3.0,>=0.1.0
 eth-typing<3.0.0,>=2.1.0
 eth-utils<2
+hexbytes<0.3.0
 jinja2>=2.9
 MarkupSafe<2.1.0
 mock

tests/graph_test.py

@@ -25,7 +25,7 @@ def test_generate_graph():
             create_timeout=None,
             disable_dependency_pruning=False,
             custom_modules_directory=None,
-            sparse_pruning=True,
+            pruning_factor=0,
             parallel_solving=True,
             unconstrained_storage=True,
             call_depth_limit=3,

tests/mythril/mythril_analyzer_test.py

@@ -32,7 +32,7 @@ def test_fire_lasers(mock_sym, mock_fire_lasers, mock_code_info):
         create_timeout=None,
         disable_dependency_pruning=False,
         custom_modules_directory=None,
-        sparse_pruning=True,
+        pruning_factor=0,
         parallel_solving=True,
         unconstrained_storage=True,
         call_depth_limit=3,

tests/statespace_test.py

@@ -22,7 +22,7 @@ def test_statespace_dump():
             create_timeout=None,
             disable_dependency_pruning=False,
             custom_modules_directory=None,
-            sparse_pruning=True,
+            pruning_factor=0,
             parallel_solving=True,
             unconstrained_storage=True,
             call_depth_limit=3,