diff --git a/mythril/exceptions.py b/mythril/exceptions.py index cb708213..782c1689 100644 --- a/mythril/exceptions.py +++ b/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.""" diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index f7a2cd0a..bfa3182d 100644 --- a/mythril/interfaces/cli.py +++ b/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", - action="store_true", - help="Checks for reachability after the end of tx. Recommended for short execution timeouts < 1 min", + "--pruning-factor", + type=float, + default=1, + help="Checks for reachability at the rate of . 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( diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 23211928..1b671388 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/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) -> bool: + def is_possible(self, solver_timeout=None) -> 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 diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index 751921bd..604f84d9 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/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: diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 01b905cc..3f808732 100644 --- a/mythril/laser/ethereum/svm.py +++ b/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? diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index e886d77f..f8da1689 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/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 diff --git a/mythril/support/model.py b/mythril/support/model.py index 77e224aa..6997d90d 100644 --- a/mythril/support/model.py +++ b/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 diff --git a/mythril/support/support_args.py b/mythril/support/support_args.py index 8734a36c..10f20288 100644 --- a/mythril/support/support_args.py +++ b/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 diff --git a/requirements.txt b/requirements.txt index 840a9b3d..03036c06 100644 --- a/requirements.txt +++ b/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 diff --git a/tests/graph_test.py b/tests/graph_test.py index cb3d915e..1beaa3cc 100644 --- a/tests/graph_test.py +++ b/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, diff --git a/tests/mythril/mythril_analyzer_test.py b/tests/mythril/mythril_analyzer_test.py index 63df5e9d..45608231 100644 --- a/tests/mythril/mythril_analyzer_test.py +++ b/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, diff --git a/tests/statespace_test.py b/tests/statespace_test.py index e8312743..c3db4635 100644 --- a/tests/statespace_test.py +++ b/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,