Use dfs by default

mythril/analysis/symbolic.py

@@ -3,6 +3,7 @@ from mythril.laser.ethereum import svm
 import copy
 import logging
 from .ops import get_variable, SStore, Call, VarType
+from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy, BreadthFirstSearchStrategy
 
 
 class SymExecWrapper:
@@ -11,13 +12,20 @@ class SymExecWrapper:
     Wrapper class for the LASER Symbolic virtual machine. Symbolically executes the code and does a bit of pre-analysis for convenience.
     '''
 
-    def __init__(self, contract, address, dynloader=None, max_depth=None, execution_timeout=None):
+    def __init__(self, contract, address, strategy, dynloader=None, max_depth=None, execution_timeout=None):
+        s_strategy = None
+        if strategy == 'dfs':
+            s_strategy = DepthFirstSearchStrategy
+        elif strategy == 'bfs':
+            s_strategy = BreadthFirstSearchStrategy
+        else:
+            raise ValueError("Invalid strategy argument supplied")
 
         account = svm.Account(address, contract.disassembly, contract_name=contract.name)
 
         self.accounts = {address: account}
 
-        self.laser = svm.LaserEVM(self.accounts, dynamic_loader=dynloader, max_depth=max_depth, execution_timeout=execution_timeout)
+        self.laser = svm.LaserEVM(self.accounts, dynamic_loader=dynloader, max_depth=max_depth, execution_timeout=execution_timeout, strategy=s_strategy)
 
         self.laser.sym_exec(address)
 

mythril/interfaces/cli.py

@@ -66,6 +66,9 @@ def main():
     options.add_argument('--max-depth', type=int, default=22, help='Maximum recursion depth for symbolic execution')
     options.add_argument('--execution-timeout', type=int, default=60, help="The amount of seconds to spend on "
                                                                            "symbolic execution")
+    outputs.add_argument('--strategy', choices=['dfs', 'bfs'], default='dfs',
+                         help='Symbolic execution strategy')
+
     options.add_argument('--solc-args', help='Extra arguments for solc')
     options.add_argument('--phrack', action='store_true', help='Phrack-style call graph')
     options.add_argument('--enable-physics', action='store_true', help='enable graph physics simulation')
@@ -194,7 +197,7 @@ def main():
                     exit_with_error(args.outform, "Error saving graph: " + str(e))
 
             else:
-                report = mythril.fire_lasers(address=address,
+                report = mythril.fire_lasers(strategy=args.strategy, address=address,
                                              modules=[m.strip() for m in args.modules.strip().split(",")] if args.modules else [],
                                              verbose_report=args.verbose_report,
                                              max_depth=args.max_depth, execution_timeout=args.execution_timeout)

mythril/laser/ethereum/svm.py

@@ -23,7 +23,7 @@ class LaserEVM:
     """
     Laser EVM class
     """
-    def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, strategy=None):
+    def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, strategy=DepthFirstSearchStrategy):
         self.accounts = accounts
 
         self.nodes = {}
@@ -33,7 +33,7 @@ class LaserEVM:
         self.dynamic_loader = dynamic_loader
 
         self.work_list = []
-        self.strategy = DepthFirstSearchStrategy(self.work_list, max_depth) if strategy is None else strategy
+        self.strategy = strategy(self.work_list, max_depth)
         self.max_depth = max_depth
         self.execution_timeout = execution_timeout
 

mythril/mythril.py

@@ -34,7 +34,6 @@ from mythril.analysis.security import fire_lasers
 from mythril.analysis.report import Report
 from mythril.leveldb.client import EthLevelDB
 
-
 # logging.basicConfig(level=logging.DEBUG)
 
 class Mythril(object):
@@ -316,15 +315,16 @@ class Mythril(object):
                              max_depth=max_depth)
         return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
 
-    def fire_lasers(self, contracts=None, address=None,
+    def fire_lasers(self, strategy, contracts=None, address=None,
                     modules=None,
-                    verbose_report=False, max_depth=None, execution_timeout=None):
+                    verbose_report=False, max_depth=None, execution_timeout=None, ):
+
 
         all_issues = []
         if self.dynld and self.eth is None:
             self.set_api_rpc_infura()
         for contract in (contracts or self.contracts):
-            sym = SymExecWrapper(contract, address,
+            sym = SymExecWrapper(contract, address, strategy,
                                  dynloader=DynLoader(self.eth) if self.dynld else None,
                                  max_depth=max_depth, execution_timeout=execution_timeout)