diff --git a/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py b/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py new file mode 100644 index 00000000..b600877d --- /dev/null +++ b/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py @@ -0,0 +1,3 @@ +from mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin import ( + InstructionCoveragePlugin, +) diff --git a/mythril/laser/ethereum/plugins/implementations/coverage.py b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py similarity index 92% rename from mythril/laser/ethereum/plugins/implementations/coverage.py rename to mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py index ba113b00..75c6bfa4 100644 --- a/mythril/laser/ethereum/plugins/implementations/coverage.py +++ b/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 diff --git a/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py new file mode 100644 index 00000000..2ffa29d6 --- /dev/null +++ b/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) diff --git a/mythril/laser/ethereum/strategy/__init__.py b/mythril/laser/ethereum/strategy/__init__.py index 58672339..140880b0 100644 --- a/mythril/laser/ethereum/strategy/__init__.py +++ b/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):