diff --git a/mythril/analysis/analysis_args.py b/mythril/analysis/analysis_args.py index fcd5fc36..e69de29b 100644 --- a/mythril/analysis/analysis_args.py +++ b/mythril/analysis/analysis_args.py @@ -1,30 +0,0 @@ -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 = 3 - self._solver_timeout = 10000 - - def set_loop_bound(self, loop_bound: int): - if loop_bound is not None: - self._loop_bound = loop_bound - - def set_solver_timeout(self, solver_timeout: int): - if solver_timeout is not None: - 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() diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index e761f220..e2abe169 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -1,10 +1,9 @@ """This module contains analysis module helpers to solve path constraints.""" -from functools import lru_cache from typing import Dict, List, Tuple, Union -from z3 import sat, unknown, FuncInterp +from z3 import FuncInterp import z3 -from mythril.analysis.analysis_args import analysis_args +from mythril.support.model import get_model from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.ethereum.keccak_function_manager import ( @@ -12,8 +11,7 @@ from mythril.laser.ethereum.keccak_function_manager import ( hash_matcher, ) from mythril.laser.ethereum.transaction import BaseTransaction -from mythril.laser.smt import UGE, Optimize, symbol_factory -from mythril.laser.ethereum.time_handler import time_handler +from mythril.laser.smt import UGE, symbol_factory from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, @@ -23,44 +21,6 @@ import logging log = logging.getLogger(__name__) -# LRU cache works great when used in powers of 2 -@lru_cache(maxsize=2 ** 23) -def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): - """ - - :param constraints: - :param minimize: - :param maximize: - :param enforce_execution_time: Bool variable which enforces --execution-timeout's time - :return: - """ - s = Optimize() - timeout = analysis_args.solver_timeout - if enforce_execution_time: - timeout = min(timeout, time_handler.time_remaining() - 500) - if timeout <= 0: - raise UnsatError - s.set_timeout(timeout) - for constraint in constraints: - if type(constraint) == bool and not constraint: - raise UnsatError - - constraints = [constraint for constraint in constraints if type(constraint) != bool] - - for constraint in constraints: - s.add(constraint) - for e in minimize: - s.minimize(e) - for e in maximize: - s.maximize(e) - result = s.check() - if result == sat: - return s.model() - elif result == unknown: - log.debug("Timeout encountered while solving expression using z3") - raise UnsatError - - def pretty_print_model(model): """ Pretty prints a z3 model diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index cbca1286..a8596946 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -446,6 +446,11 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): action="store_true", 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", + ) options.add_argument( "--phrack", action="store_true", help="Phrack-style call graph" ) @@ -673,6 +678,7 @@ def execute_command( custom_modules_directory=args.custom_modules_directory if args.custom_modules_directory else "", + sparse_pruning=args.sparse_pruning, ) if not disassembler.contracts: diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 419bc873..67f1b44e 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -1,10 +1,9 @@ """This module contains the class used to represent state-change constraints in the call graph.""" - -from mythril.laser.smt import Solver, Bool, symbol_factory, simplify - +from mythril.exceptions import UnsatError +from mythril.laser.smt import Bool, simplify +from mythril.support.model import get_model from typing import Iterable, List, Optional, Union -from z3 import unsat class Constraints(list): @@ -14,21 +13,14 @@ class Constraints(list): """ - def __init__( - self, - constraint_list: Optional[List[Bool]] = None, - is_possible: Optional[bool] = None, - ) -> None: + def __init__(self, constraint_list: Optional[List[Bool]] = None,) -> None: """ :param constraint_list: List of constraints - :param is_possible: Whether it is possible to satisfy the constraints or not """ constraint_list = constraint_list or [] constraint_list = self._get_smt_bool_list(constraint_list) super(Constraints, self).__init__(constraint_list) - self._default_timeout = 100 - self._is_possible = is_possible @property def is_possible(self) -> bool: @@ -36,19 +28,11 @@ class Constraints(list): :return: True/False based on the existence of solution of constraints """ - if self._is_possible is not None: - return self._is_possible - solver = Solver() - solver.set_timeout(self._default_timeout) - for constraint in self[:]: - constraint = ( - symbol_factory.Bool(constraint) - if isinstance(constraint, bool) - else constraint - ) - solver.add(constraint) - self._is_possible = solver.check() != unsat - return self._is_possible + try: + get_model(tuple(self[:])) + except UnsatError: + return False + return True def append(self, constraint: Union[bool, Bool]) -> None: """ @@ -59,7 +43,6 @@ class Constraints(list): simplify(constraint) if isinstance(constraint, Bool) else Bool(constraint) ) super(Constraints, self).append(constraint) - self._is_possible = None def pop(self, index: int = -1) -> None: """ @@ -81,7 +64,7 @@ class Constraints(list): :return: The copied constraint List """ constraint_list = super(Constraints, self).copy() - return Constraints(constraint_list, is_possible=self._is_possible) + return Constraints(constraint_list) def copy(self) -> "Constraints": return self.__copy__() @@ -102,7 +85,7 @@ class Constraints(list): """ constraints_list = self._get_smt_bool_list(constraints) constraints_list = super(Constraints, self).__add__(constraints_list) - return Constraints(constraint_list=constraints_list, is_possible=None) + return Constraints(constraint_list=constraints_list) def __iadd__(self, constraints: Iterable[Union[bool, Bool]]) -> "Constraints": """ @@ -112,7 +95,6 @@ class Constraints(list): """ list_constraints = self._get_smt_bool_list(constraints) super(Constraints, self).__iadd__(list_constraints) - self._is_possible = None return self @staticmethod diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index d0ce1ad2..39e0eaae 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -29,7 +29,7 @@ from mythril.laser.ethereum.transaction import ( execute_message_call, ) from mythril.laser.smt import symbol_factory - +from mythril.support.support_args import args log = logging.getLogger(__name__) @@ -203,6 +203,15 @@ class LaserEVM: self.time = datetime.now() for i in range(self.transaction_count): + if len(self.open_states) == 0: + break + old_states_count = len(self.open_states) + self.open_states = [ + state for state in self.open_states if state.constraints.is_possible + ] + prune_count = old_states_count - len(self.open_states) + if prune_count: + log.info("Pruned {} unreachable states".format(prune_count)) log.info( "Starting message call transaction, iteration: {}, {} initial states".format( i, len(self.open_states) @@ -248,11 +257,12 @@ class LaserEVM: except NotImplementedError: log.debug("Encountered unimplemented instruction") continue - new_states = [ - state - for state in new_states - if state.world_state.constraints.is_possible - ] + if args.sparse_pruning is False: + new_states = [ + state + for state in new_states + if state.world_state.constraints.is_possible + ] self.manage_cfg(op_code, new_states) # TODO: What about op_code is None? if new_states: diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index 50a6cd58..8b239c8d 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/mythril/mythril/mythril_analyzer.py @@ -9,9 +9,9 @@ from mythril.laser.ethereum.iprof import InstructionProfiler from . import MythrilDisassembler from mythril.support.source_support import Source from mythril.support.loader import DynLoader +from mythril.support.support_args import args 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 @@ -45,6 +45,7 @@ class MythrilAnalyzer: solver_timeout: Optional[int] = None, enable_coverage_strategy: bool = False, custom_modules_directory: str = "", + sparse_pruning: bool = False, ): """ @@ -66,9 +67,8 @@ class MythrilAnalyzer: self.disable_dependency_pruning = disable_dependency_pruning self.enable_coverage_strategy = enable_coverage_strategy self.custom_modules_directory = custom_modules_directory - - analysis_args.set_loop_bound(loop_bound) - analysis_args.set_solver_timeout(solver_timeout) + args.sparse_pruning = sparse_pruning + args.solver_timeout = solver_timeout def dump_statespace(self, contract: EVMContract = None) -> str: """ diff --git a/mythril/support/model.py b/mythril/support/model.py new file mode 100644 index 00000000..36f7a6b5 --- /dev/null +++ b/mythril/support/model.py @@ -0,0 +1,49 @@ +from functools import lru_cache +from z3 import sat, unknown + +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 +import logging + +log = logging.getLogger(__name__) + +# LRU cache works great when used in powers of 2 + + +@lru_cache(maxsize=2 ** 23) +def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): + """ + Returns a model based on given constraints as a tuple + :param constraints: Tuple of constraints + :param minimize: Tuple of minimization conditions + :param maximize: Tuple of maximization conditions + :param enforce_execution_time: Bool variable which enforces --execution-timeout's time + :return: + """ + s = Optimize() + timeout = args.solver_timeout + if enforce_execution_time: + timeout = min(timeout, time_handler.time_remaining() - 500) + if timeout <= 0: + raise UnsatError + s.set_timeout(timeout) + for constraint in constraints: + if type(constraint) == bool and not constraint: + raise UnsatError + + constraints = [constraint for constraint in constraints if type(constraint) != bool] + + for constraint in constraints: + s.add(constraint) + for e in minimize: + s.minimize(e) + for e in maximize: + s.maximize(e) + result = s.check() + if result == sat: + return s.model() + elif result == unknown: + log.debug("Timeout encountered while solving expression using z3") + raise UnsatError diff --git a/mythril/support/support_args.py b/mythril/support/support_args.py new file mode 100644 index 00000000..b44691de --- /dev/null +++ b/mythril/support/support_args.py @@ -0,0 +1,12 @@ +class Args: + """ + This module helps in preventing args being sent through multiple of classes to reach + any analysis/laser module + """ + + def __init__(self): + self.solver_timeout = 10000 + self.sparse_pruning = True + + +args = Args() diff --git a/tests/graph_test.py b/tests/graph_test.py index ac33cabd..1e318e65 100644 --- a/tests/graph_test.py +++ b/tests/graph_test.py @@ -13,6 +13,7 @@ def test_generate_graph(): continue contract = EVMContract(input_file.read_text()) disassembler = MythrilDisassembler() + disassembler.contracts.append(contract) analyzer = MythrilAnalyzer( disassembler=disassembler, @@ -20,6 +21,7 @@ def test_generate_graph(): execution_timeout=5, max_depth=30, address=(util.get_indexed_address(0)), + solver_timeout=10000, ) analyzer.graph_html(transaction_count=1) diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 54c0bd5e..c12ddd68 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -1,6 +1,7 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.time_handler import time_handler from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.transaction.concolic import execute_message_call @@ -130,9 +131,9 @@ def test_vmtest( world_state.put_account(account) account.set_balance(int(details["balance"], 16)) + time_handler.start_execution(10000) laser_evm = LaserEVM() laser_evm.open_states = [world_state] - # Act laser_evm.time = datetime.now() diff --git a/tests/statespace_test.py b/tests/statespace_test.py index 6682ab7c..607d9c46 100644 --- a/tests/statespace_test.py +++ b/tests/statespace_test.py @@ -18,6 +18,7 @@ def test_statespace_dump(): execution_timeout=5, max_depth=30, address=(util.get_indexed_address(0)), + solver_timeout=10000, ) analyzer.dump_statespace(contract=contract)