Add a cmd line flag

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(
+        "--deep-pruning",
+        action="store_true",
+        help="Checks for reachability after every JUMPI. Recommended for long execution timeouts e.g: 10 minutes",
+    )
     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=not args.deep_pruning,
         )
 
         if not disassembler.contracts:

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__)
 
@@ -257,6 +257,12 @@ class LaserEVM:
             except NotImplementedError:
                 log.debug("Encountered unimplemented instruction")
                 continue
+            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

@@ -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,7 +67,7 @@ class MythrilAnalyzer:
         self.disable_dependency_pruning = disable_dependency_pruning
         self.enable_coverage_strategy = enable_coverage_strategy
         self.custom_modules_directory = custom_modules_directory
-
+        args.sparse_pruning = sparse_pruning
         args.solver_timeout = solver_timeout
 
     def dump_statespace(self, contract: EVMContract = None) -> str:

mythril/support/support_args.py

@@ -6,6 +6,7 @@ class Args:
 
     def __init__(self):
         self.solver_timeout = 10000
+        self.sparse_pruning = True
 
 
 args = Args()