diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index dac47f46..55ebf39d 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -16,6 +16,9 @@ from mythril.laser.ethereum.strategy.basic import ( ReturnWeightedRandomStrategy, BasicSearchStrategy, ) +from mythril.laser.ethereum.strategy.extensions.bounded_loops import ( + BoundedLoopsStrategy, +) from mythril.laser.smt import symbol_factory, BitVec from typing import Union, List, Dict, Type from mythril.solidity.soliditycontract import EVMContract, SolidityContract @@ -37,6 +40,7 @@ class SymExecWrapper: dynloader=None, max_depth=22, execution_timeout=None, + loop_bound=4, create_timeout=None, transaction_count=2, modules=(), @@ -69,8 +73,6 @@ class SymExecWrapper: s_strategy = ReturnRandomNaivelyStrategy elif strategy == "weighted-random": s_strategy = ReturnWeightedRandomStrategy - elif strategy == "bfs-bounded": - s_strategy = BFSBoundedLoopsStrategy else: raise ValueError("Invalid strategy argument supplied") @@ -89,6 +91,9 @@ class SymExecWrapper: enable_iprof=enable_iprof, ) + if loop_bound is not None: + self.laser.extend_strategy(BoundedLoopsStrategy, loop_bound) + plugin_loader = LaserPluginLoader(self.laser) plugin_loader.load(PluginFactory.build_mutation_pruner_plugin()) plugin_loader.load(PluginFactory.build_instruction_coverage_plugin()) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 5bdf0ea9..2d3a63e1 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -209,6 +209,7 @@ def create_parser(parser: argparse.ArgumentParser) -> None: type=int, default=4, help="Bound loops at n iterations", + metavar="N", ) options.add_argument( "-t", @@ -413,6 +414,7 @@ def execute_command( address=address, max_depth=args.max_depth, execution_timeout=args.execution_timeout, + loop_bound=args.loop_bound, create_timeout=args.create_timeout, enable_iprof=args.enable_iprof, onchain_storage_access=not args.no_onchain_storage_access, diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index d92e0e92..10525ffa 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py @@ -22,14 +22,22 @@ class JumpdestCountAnnotation(StateAnnotation): return result -class BFSBoundedLoopsStrategy(BasicSearchStrategy): +class BoundedLoopsStrategy(BasicSearchStrategy): """Adds loop pruning to the search strategy. Ignores JUMPI instruction if the destination was targeted >JUMPDEST_LIMIT times. """ - def __init__(self, super_strategy: BasicSearchStrategy, loop_bound: int): + def __init__(self, super_strategy: BasicSearchStrategy, *args) -> None: + """""" + self.super_strategy = super_strategy - self.jumpdest_limit = loop_bound + self.jumpdest_limit = args[0][0] + + log.info( + "Loaded search strategy extension: Loop bounds (limit = {})".format( + self.jumpdest_limit + ) + ) BasicSearchStrategy.__init__( self, super_strategy.work_list, super_strategy.max_depth diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 51536a3f..b7086497 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -105,8 +105,8 @@ class LaserEVM: log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader)) - def extend_strategy(self, strategy: BasicSearchStrategy) -> None: - self.strategy = strategy(self.strategy) + def extend_strategy(self, extension: BasicSearchStrategy, *args) -> None: + self.strategy = extension(self.strategy, args) def sym_exec( self, diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index d4d4cd5b..9433278e 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/mythril/mythril/mythril_analyzer.py @@ -35,6 +35,7 @@ class MythrilAnalyzer: address: Optional[str] = None, max_depth: Optional[int] = None, execution_timeout: Optional[int] = None, + loop_bound: Optional[int] = None, create_timeout: Optional[int] = None, enable_iprof: bool = False, ): @@ -53,6 +54,7 @@ class MythrilAnalyzer: self.address = address self.max_depth = max_depth self.execution_timeout = execution_timeout + self.loop_bound = loop_bound self.create_timeout = create_timeout self.enable_iprof = enable_iprof @@ -142,12 +144,14 @@ class MythrilAnalyzer: ), max_depth=self.max_depth, execution_timeout=self.execution_timeout, + loop_bound=self.loop_bound, create_timeout=self.create_timeout, transaction_count=transaction_count, modules=modules, compulsory_statespace=False, enable_iprof=self.enable_iprof, ) + issues = fire_lasers(sym, modules) except KeyboardInterrupt: log.critical("Keyboard Interrupt")