From d7592efc0d5ae09dbbdd03c0aea6478f9eb0b6cd Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Fri, 13 Mar 2020 19:36:30 +0000
Subject: [PATCH] Add a cmd line flag

---
 mythril/interfaces/cli.py           | 6 ++++++
 mythril/laser/ethereum/svm.py       | 8 +++++++-
 mythril/mythril/mythril_analyzer.py | 3 ++-
 mythril/support/support_args.py     | 1 +
 4 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py
index cbca1286..f8825895 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(
+        "--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:
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 6ad001d3..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__)
 
@@ -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:
diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py
index be4fbb97..8b239c8d 100644
--- a/mythril/mythril/mythril_analyzer.py
+++ b/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:
diff --git a/mythril/support/support_args.py b/mythril/support/support_args.py
index a50bf514..b44691de 100644
--- a/mythril/support/support_args.py
+++ b/mythril/support/support_args.py
@@ -6,6 +6,7 @@ class Args:
 
     def __init__(self):
         self.solver_timeout = 10000
+        self.sparse_pruning = True
 
 
 args = Args()