Black

mythril/analysis/symbolic.py

@@ -16,7 +16,6 @@ from mythril.laser.ethereum.strategy.basic import (
     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

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", "bfs-bounded"],
-        default="bfs-bounded",
+        choices=["dfs", "bfs", "naive-random", "weighted-random"],
+        default="bfs",
         help="Symbolic execution strategy",
     )
     options.add_argument(

mythril/laser/ethereum/strategy/custom.py

@@ -1,69 +0,0 @@
-from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.ethereum.strategy.basic import BreadthFirstSearchStrategy
-from mythril.laser.ethereum.state.annotation import StateAnnotation
-from mythril.laser.ethereum import util
-from typing import Dict, cast, List
-from copy import copy
-import logging
-
-
-JUMPDEST_LIMIT = 4
-log = logging.getLogger(__name__)
-
-
-class JumpdestCountAnnotation(StateAnnotation):
-    """State annotation used when a path is chosen based on a predictable variable."""
-
-    def __init__(self) -> None:
-        self._jumpdest_count = {}  # type: Dict[int, int]
-
-    def __copy__(self):
-        result = JumpdestCountAnnotation()
-        result._jumpdest_count = copy(self._jumpdest_count)
-        return result
-
-
-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, work_list, max_depth) -> None:
-        super().__init__(work_list, max_depth)
-
-    def get_strategic_global_state(self) -> GlobalState:
-        """
-        :return:
-        """
-
-        state = self.work_list.pop(0)
-
-        opcode = state.get_current_instruction()["opcode"]
-
-        if opcode != "JUMPI":
-            return state
-
-        annotations = cast(
-            List[JumpdestCountAnnotation],
-            list(state.get_annotations(JumpdestCountAnnotation)),
-        )
-
-        if len(annotations) == 0:
-            annotation = JumpdestCountAnnotation()
-            state.annotate(annotation)
-        else:
-            annotation = annotations[0]
-
-        target = int(util.get_concrete_int(state.mstate.stack[-1]))
-
-        try:
-            annotation._jumpdest_count[target] += 1
-        except KeyError:
-            annotation._jumpdest_count[target] = 1
-
-        if annotation._jumpdest_count[target] > JUMPDEST_LIMIT:
-            log.debug("JUMPDEST limit reached, skipping JUMPI")
-            return self.work_list.pop(0)
-
-        return state

mythril/laser/ethereum/strategy/extensions/bounded_loops.py

@@ -0,0 +1,72 @@
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.strategy.basic import BasicSearchStrategy
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.ethereum import util
+from typing import Dict, cast, List
+from copy import copy
+import logging
+
+
+JUMPDEST_LIMIT = 4
+log = logging.getLogger(__name__)
+
+
+class JumpdestCountAnnotation(StateAnnotation):
+    """State annotation that counts the number of jumps per destination."""
+
+    def __init__(self) -> None:
+        self._jumpdest_count = {}  # type: Dict[int, int]
+
+    def __copy__(self):
+        result = JumpdestCountAnnotation()
+        result._jumpdest_count = copy(self._jumpdest_count)
+        return result
+
+
+class BFSBoundedLoopsStrategy(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):
+        self.super_strategy = super_strategy
+        BasicSearchStrategy.__init__(
+            self, super_strategy.work_list, super_strategy.max_depth
+        )
+
+    def get_strategic_global_state(self) -> GlobalState:
+        """
+        :return:
+        """
+
+        while 1:
+
+            state = self.super_strategy.get_strategic_global_state()
+            opcode = state.get_current_instruction()["opcode"]
+
+            if opcode != "JUMPI":
+                return state
+
+            annotations = cast(
+                List[JumpdestCountAnnotation],
+                list(state.get_annotations(JumpdestCountAnnotation)),
+            )
+
+            if len(annotations) == 0:
+                annotation = JumpdestCountAnnotation()
+                state.annotate(annotation)
+            else:
+                annotation = annotations[0]
+
+            target = int(util.get_concrete_int(state.mstate.stack[-1]))
+
+            try:
+                annotation._jumpdest_count[target] += 1
+            except KeyError:
+                annotation._jumpdest_count[target] = 1
+
+            if annotation._jumpdest_count[target] > JUMPDEST_LIMIT:
+                log.debug("JUMPDEST limit reached, skipping JUMPI")
+                continue
+
+            return state

mythril/laser/ethereum/svm.py

@@ -13,7 +13,10 @@ from mythril.laser.ethereum.iprof import InstructionProfiler
 from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
-from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
+from mythril.laser.ethereum.strategy.basic import (
+    BasicSearchStrategy,
+    DepthFirstSearchStrategy,
+)
 from mythril.laser.ethereum.time_handler import time_handler
 from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
@@ -102,6 +105,9 @@ 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 sym_exec(
         self,
         world_state: WorldState = None,