Merge branch 'develop' into enhance/886

mythril/analysis/symbolic.py

@@ -12,9 +12,9 @@ from mythril.laser.ethereum.strategy.basic import (
     ReturnWeightedRandomStrategy,
 )
 
-from mythril.laser.ethereum.plugins.implementations.mutation_pruner import (
-    MutationPruner,
-)
+from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
+from mythril.laser.ethereum.plugins.plugin_loader import LaserPluginLoader
+
 
 from mythril.solidity.soliditycontract import EVMContract, SolidityContract
 from .ops import Call, SStore, VarType, get_variable
@@ -86,9 +86,10 @@ class SymExecWrapper:
             requires_statespace=requires_statespace,
             enable_iprof=enable_iprof,
         )
-        mutation_plugin = MutationPruner()
 
-        mutation_plugin.initialize(self.laser)
+        plugin_loader = LaserPluginLoader(self.laser)
+        plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
+        plugin_loader.load(PluginFactory.build_instruction_coverage_plugin())
 
         self.laser.register_hooks(
             hook_type="pre",

mythril/laser/ethereum/plugins/implementations/benchmark.py

@@ -7,6 +7,7 @@ import logging
 log = logging.getLogger(__name__)
 
 
+# TODO: introduce dependency on coverage plugin
 class BenchmarkPlugin(LaserPlugin):
     """Benchmark Plugin
 

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

@@ -21,6 +21,11 @@ class InstructionCoveragePlugin(LaserPlugin):
 
     """
 
+    def __init__(self):
+        self.coverage = {}  # type: Dict[str, Tuple[int, List[bool]]]
+        self.initial_coverage = 0
+        self.tx_id = 0
+
     def initialize(self, symbolic_vm: LaserEVM):
         """Initializes the instruction coverage plugin
 
@@ -28,12 +33,14 @@ class InstructionCoveragePlugin(LaserPlugin):
         :param symbolic_vm:
         :return:
         """
-        coverage = {}  # type: Dict[str, Tuple[int, List[bool]]]
+        self.coverage = {}
+        self.initial_coverage = 0
+        self.tx_id = 0
 
         @symbolic_vm.laser_hook("stop_sym_exec")
         def stop_sym_exec_hook():
             # Print results
-            for code, code_cov in coverage.items():
+            for code, code_cov in self.coverage.items():
                 cov_percentage = sum(code_cov[1]) / float(code_cov[0]) * 100
 
                 log.info(
@@ -47,13 +54,45 @@ class InstructionCoveragePlugin(LaserPlugin):
             # Record coverage
             code = global_state.environment.code.bytecode
 
-            if code not in coverage.keys():
+            if code not in self.coverage.keys():
                 number_of_instructions = len(
                     global_state.environment.code.instruction_list
                 )
-                coverage[code] = (
+                self.coverage[code] = (
                     number_of_instructions,
                     [False] * number_of_instructions,
                 )
 
-            coverage[code][1][global_state.mstate.pc] = True
+            self.coverage[code][1][global_state.mstate.pc] = True
+
+        @symbolic_vm.laser_hook("start_sym_trans")
+        def execute_start_sym_trans_hook():
+            self.initial_coverage = self._get_covered_instructions()
+
+        @symbolic_vm.laser_hook("stop_sym_trans")
+        def execute_stop_sym_trans_hook():
+            end_coverage = self._get_covered_instructions()
+            log.info(
+                "Number of new instructions covered in tx %d: %d"
+                % (self.tx_id, end_coverage - self.initial_coverage)
+            )
+            self.tx_id += 1
+
+    def _get_covered_instructions(self) -> int:
+        """Gets the total number of covered instructions for all accounts in
+        the svm.
+        :return:
+        """
+        total_covered_instructions = 0
+        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/plugins/plugin_factory.py

@@ -1,11 +1,4 @@
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
-from mythril.laser.ethereum.plugins.implementations.benchmark import BenchmarkPlugin
-from mythril.laser.ethereum.plugins.implementations.mutation_pruner import (
-    MutationPruner,
-)
-from mythril.laser.ethereum.plugins.implementations.coverage import (
-    InstructionCoveragePlugin,
-)
 
 
 class PluginFactory:
@@ -14,14 +7,26 @@ class PluginFactory:
     @staticmethod
     def build_benchmark_plugin(name: str) -> LaserPlugin:
         """ Creates an instance of the benchmark plugin with the given name """
+        from mythril.laser.ethereum.plugins.implementations.benchmark import (
+            BenchmarkPlugin,
+        )
+
         return BenchmarkPlugin(name)
 
     @staticmethod
     def build_mutation_pruner_plugin() -> LaserPlugin:
         """ Creates an instance of the mutation pruner plugin"""
+        from mythril.laser.ethereum.plugins.implementations.mutation_pruner import (
+            MutationPruner,
+        )
+
         return MutationPruner()
 
     @staticmethod
     def build_instruction_coverage_plugin() -> LaserPlugin:
         """ Creates an instance of the instruction coverage plugin"""
+        from mythril.laser.ethereum.plugins.implementations.coverage import (
+            InstructionCoveragePlugin,
+        )
+
         return InstructionCoveragePlugin()

mythril/laser/ethereum/plugins/plugin_loader.py

@@ -2,6 +2,9 @@ from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
 
 from typing import List
+import logging
+
+log = logging.getLogger(__name__)
 
 
 class LaserPluginLoader:
@@ -16,13 +19,14 @@ class LaserPluginLoader:
         :param symbolic_vm: symbolic virtual machine to load plugins for
         """
         self.symbolic_vm = symbolic_vm
-        self.laser_plugins: List[LaserPlugin] = []
+        self.laser_plugins = []  # type: List[LaserPlugin]
 
     def load(self, laser_plugin: LaserPlugin) -> None:
         """ Loads the plugin
 
         :param laser_plugin: plugin that will be loaded in the symbolic virtual machine
         """
+        log.info("Loading plugin: {}".format(str(laser_plugin)))
         laser_plugin.initialize(self.symbolic_vm)
         self.laser_plugins.append(laser_plugin)
 

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):

mythril/laser/ethereum/svm.py

@@ -72,8 +72,6 @@ class LaserEVM:
         self.world_state = world_state
         self.open_states = [world_state]
 
-        self.coverage = {}  # type: Dict[str, Tuple[int, List[bool]]]
-
         self.total_states = 0
         self.dynamic_loader = dynamic_loader
 
@@ -97,6 +95,10 @@ class LaserEVM:
 
         self._add_world_state_hooks = []  # type: List[Callable]
         self._execute_state_hooks = []  # type: List[Callable]
+
+        self._start_sym_trans_hooks = []  # type: List[Callable]
+        self._stop_sym_trans_hooks = []  # type: List[Callable]
+
         self._start_sym_exec_hooks = []  # type: List[Callable]
         self._stop_sym_exec_hooks = []  # type: List[Callable]
 
@@ -158,10 +160,6 @@ class LaserEVM:
                 len(self.edges),
                 self.total_states,
             )
-        for code, coverage in self.coverage.items():
-            cov = sum(coverage[1]) / float(coverage[0]) * 100
-
-            log.info("Achieved {:.2f}% coverage for code: {}".format(cov, code))
 
         if self.iprof is not None:
             log.info("Instruction Statistics:\n{}".format(self.iprof))
@@ -170,42 +168,25 @@ class LaserEVM:
             hook()
 
     def _execute_transactions(self, address):
-        """This function executes multiple transactions on the address based on
-        the coverage.
+        """This function executes multiple transactions on the address
 
         :param address: Address of the contract
         :return:
         """
-        self.coverage = {}
         for i in range(self.transaction_count):
-            initial_coverage = self._get_covered_instructions()
-
             self.time = datetime.now()
             log.info(
                 "Starting message call transaction, iteration: {}, {} initial states".format(
                     i, len(self.open_states)
                 )
             )
+            for hook in self._start_sym_trans_hooks:
+                hook()
 
             execute_message_call(self, address)
 
-            end_coverage = self._get_covered_instructions()
-
-            log.info(
-                "Number of new instructions covered in tx %d: %d"
-                % (i, end_coverage - initial_coverage)
-            )
-
-    def _get_covered_instructions(self) -> int:
-        """Gets the total number of covered instructions for all accounts in
-        the svm.
-
-        :return:
-        """
-        total_covered_instructions = 0
-        for _, cv in self.coverage.items():
-            total_covered_instructions += sum(cv[1])
-        return total_covered_instructions
+            for hook in self._stop_sym_trans_hooks:
+                hook()
 
     def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]:
         """
@@ -284,7 +265,6 @@ class LaserEVM:
 
         self._execute_pre_hook(op_code, global_state)
         try:
-            self._measure_coverage(global_state)
             new_global_states = Instruction(
                 op_code, self.dynamic_loader, self.iprof
             ).evaluate(global_state)
@@ -389,23 +369,6 @@ class LaserEVM:
 
         return new_global_states
 
-    def _measure_coverage(self, global_state: GlobalState) -> None:
-        """
-
-        :param global_state:
-        """
-        code = global_state.environment.code.bytecode
-        number_of_instructions = len(global_state.environment.code.instruction_list)
-        instruction_index = global_state.mstate.pc
-
-        if code not in self.coverage.keys():
-            self.coverage[code] = (
-                number_of_instructions,
-                [False] * number_of_instructions,
-            )
-
-        self.coverage[code][1][instruction_index] = True
-
     def manage_cfg(self, opcode: str, new_states: List[GlobalState]) -> None:
         """
 
@@ -527,6 +490,10 @@ class LaserEVM:
             self._start_sym_exec_hooks.append(hook)
         elif hook_type == "stop_sym_exec":
             self._stop_sym_exec_hooks.append(hook)
+        elif hook_type == "start_sym_trans":
+            self._start_sym_trans_hooks.append(hook)
+        elif hook_type == "stop_sym_trans":
+            self._stop_sym_trans_hooks.append(hook)
         else:
             raise ValueError(
                 "Invalid hook type %s. Must be one of {add_world_state}", hook_type

mythril/version.py

@@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
 as for importing into Python.
 """
 
-VERSION = "v0.20.2"  # NOQA
+VERSION = "v0.20.3"  # NOQA

requirements.txt

@@ -27,3 +27,4 @@ rlp>=1.0.1
 transaction>=2.2.1
 z3-solver-mythril>=4.8.4.1
 pysha3
+matplotlib

setup.py

@@ -97,6 +97,7 @@ setup(
         "configparser>=3.5.0",
         "persistent>=4.2.0",
         "ethereum-input-decoder>=0.2.2",
+        "matplotlib",
     ],
     tests_require=["mypy", "pytest>=3.6.0", "pytest_mock", "pytest-cov"],
     python_requires=">=3.5",