Merge pull request #989 from ConsenSys/features/coverage_based_search_strategy

Coverage based search strategy

mythril/laser/ethereum/plugins/implementations/coverage/__init__.py

@@ -0,0 +1,3 @@
+from mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin import (
+    InstructionCoveragePlugin,
+)

mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py

@@ -87,3 +87,12 @@ class InstructionCoveragePlugin(LaserPlugin):
         for _, cv in self.coverage.items():
             total_covered_instructions += sum(cv[1])
         return total_covered_instructions
+
+    def is_instruction_covered(self, bytecode, index):
+        if bytecode not in self.coverage.keys():
+            return False
+
+        try:
+            return self.coverage[bytecode][index]
+        except IndexError:
+            return False

mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py

@@ -0,0 +1,43 @@
+from mythril.laser.ethereum.strategy import BasicSearchStrategy
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.plugins.implementations.coverage import (
+    InstructionCoveragePlugin,
+)
+
+
+class CoverageStrategy(BasicSearchStrategy):
+    """Implements a instruction coverage based search strategy
+
+    This strategy is quite simple and effective, it prioritizes the execution of instructions that have previously been
+    uncovered. Once there is no such global state left in the work list, it will resort to using the super_strategy.
+
+    This strategy is intended to be used "on top of" another one
+    """
+
+    def __init__(
+        self,
+        super_strategy: BasicSearchStrategy,
+        instruction_coverage_plugin: InstructionCoveragePlugin,
+    ):
+        self.super_strategy = super_strategy
+        self.instruction_coverage_plugin = instruction_coverage_plugin
+        BasicSearchStrategy.__init__(
+            self, super_strategy.work_list, super_strategy.max_depth
+        )
+
+    def get_strategic_global_state(self) -> GlobalState:
+        """
+        Returns the first uncovered global state in the work list if it exists,
+        otherwise super_strategy.get_strategic_global_state() is returned.
+        """
+        for global_state in self.work_list:
+            if not self._is_covered(global_state):
+                self.work_list.remove(global_state)
+                return global_state
+        return self.super_strategy.get_strategic_global_state()
+
+    def _is_covered(self, global_state: GlobalState) -> bool:
+        """ Checks if the instruction for the given global state is already covered"""
+        bytecode = global_state.environment.code.bytecode
+        index = global_state.mstate.pc
+        return self.instruction_coverage_plugin.is_instruction_covered(bytecode, index)

mythril/laser/ethereum/strategy/__init__.py

@@ -1,4 +1,6 @@
 from abc import ABC, abstractmethod
+from typing import List
+from mythril.laser.ethereum.state.global_state import GlobalState
 
 
 class BasicSearchStrategy(ABC):
@@ -7,7 +9,7 @@ class BasicSearchStrategy(ABC):
     __slots__ = "work_list", "max_depth"
 
     def __init__(self, work_list, max_depth):
-        self.work_list = work_list
+        self.work_list = work_list  # type: List[GlobalState]
         self.max_depth = max_depth
 
     def __iter__(self):