Merge pull request #1352 from ConsenSys/remove_branch_pruning

Remove branch pruning

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()

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
 

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:

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

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:

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:
         """

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

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()

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)

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()
 

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)