Add bfs-bounded strategy

mythril/analysis/modules/dos.py

@@ -70,7 +70,7 @@ class DOS(DetectionModule):
 
                 try:
                     self._jumpdest_count[transaction][target] += 1
-                    if self._jumpdest_count[transaction][target] == 4:
+                    if self._jumpdest_count[transaction][target] == 3:
 
                         annotation = (
                             LoopAnnotation(address, target)

mythril/analysis/symbolic.py

@@ -15,8 +15,8 @@ from mythril.laser.ethereum.strategy.basic import (
     ReturnRandomNaivelyStrategy,
     ReturnWeightedRandomStrategy,
     BasicSearchStrategy,
-
 )
+from mythril.laser.ethereum.strategy.custom import BFSBoundedLoopsStrategy
 from mythril.laser.smt import symbol_factory, BitVec
 from typing import Union, List, Dict, Type
 from mythril.solidity.soliditycontract import EVMContract, SolidityContract
@@ -69,6 +69,8 @@ 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")
 

mythril/interfaces/cli.py

@@ -200,8 +200,8 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
 
     options.add_argument(
         "--strategy",
-        choices=["dfs", "bfs", "naive-random", "weighted-random"],
-        default="bfs",
+        choices=["dfs", "bfs", "naive-random", "weighted-random", "bfs-bounded"],
+        default="bfs-bounded",
         help="Symbolic execution strategy",
     )
     options.add_argument(

mythril/laser/ethereum/strategy/custom.py

@@ -1,13 +1,22 @@
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.strategy.basic import BreadthFirstSearchStrategy
+from mythril.laser.ethereum import util
+import logging
+
+
+JUMPDEST_LIMIT = 4
+log = logging.getLogger(__name__)
 
 
 class BFSBoundedLoopsStrategy(BreadthFirstSearchStrategy):
     """Implements a breadth first search strategy that prunes loops.
+    JUMPI instructions are skipped after a jump destination has been
+    targeted JUMPDEST_LIMIT times.
     """
 
-    def __init__(self):
-        pass
+    def __init__(self, work_list, max_depth) -> None:
+        super().__init__(work_list, max_depth)
+        self._jumpdest_count = {}  # type: Dict[object, dict]
 
     def get_strategic_global_state(self) -> GlobalState:
         """
@@ -16,4 +25,30 @@ class BFSBoundedLoopsStrategy(BreadthFirstSearchStrategy):
 
         state = self.work_list.pop(0)
 
+        opcode = state.get_current_instruction()["opcode"]
+
+        if opcode == "JUMPI":
+
+            transaction = state.current_transaction
+            target = util.get_concrete_int(state.mstate.stack[-1])
+
+            if transaction in self._jumpdest_count:
+
+                try:
+                    if self._jumpdest_count[transaction][target] == JUMPDEST_LIMIT:
+                        log.info("Skipping JUMPI")
+                        return self.work_list.pop(0)
+                except KeyError:
+                    self._jumpdest_count[transaction][target] = 0
+
+                self._jumpdest_count[transaction][target] += 1
+
+            else:
+                self._jumpdest_count[transaction] = {}
+                self._jumpdest_count[transaction][target] = 0
+
+            log.info(
+                "JUMPDEST COUNT: {}".format(self._jumpdest_count[transaction][target])
+            )
+
         return state