Add experimental dependency pruner

mythril/analysis/symbolic.py

@@ -96,6 +96,7 @@ class SymExecWrapper:
 
         plugin_loader = LaserPluginLoader(self.laser)
         plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
+        plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
         plugin_loader.load(PluginFactory.build_instruction_coverage_plugin())
 
         if run_analysis_modules:

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

@@ -1,68 +1,145 @@
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
-from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
+from mythril.laser.ethereum.plugins.signals import PluginSkipState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.ethereum.util import get_concrete_int
+from mythril.laser.ethereum.transaction.transaction_models import (
+    ContractCreationTransaction,
+)
+from typing import cast, List
 from copy import copy
+import logging
 
+log = logging.getLogger(__name__)
 
-class PathAnnotation(StateAnnotation):
+
+class DependencyAnnotation(StateAnnotation):
     """Dependency Annotation
 
-    This is the annotation used to annotate paths
+    This annotation tracks read and write access to the state.
     """
 
     def __init__(self):
-        self.path = []
+        self.storage_loaded = []  # type: List
+        self.storage_written = []  # type: List
+        self.path = []  # type: List[int]
 
     def __copy__(self):
-        result = PathAnnotation()
+        result = DependencyAnnotation()
+        result.storage_loaded = copy(self.storage_loaded)
+        result.storage_written = copy(self.storage_written)
         result.path = copy(self.path)
         return result
 
 
+def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation:
+
+    annotations = cast(
+        List[DependencyAnnotation],
+        list(state.world_state.get_annotations(DependencyAnnotation)),
+    )
+    if len(annotations) == 0:
+        annotations = cast(
+            List[DependencyAnnotation],
+            list(state.get_annotations(DependencyAnnotation)),
+        )
+
+        if len(annotations) == 0:
+            annotation = DependencyAnnotation()
+            state.annotate(annotation)
+        else:
+            annotation = annotations[0]
+    else:
+        annotation = annotations[0]
+
+    return annotation
+
+
 class DependencyPruner(LaserPlugin):
     """Dependency Pruner Plugin
     """
 
     def __init__(self):
         """Creates DependencyPruner"""
-        pass
+        self.iteration = 0
+        self.dependency_map = {}  # type: Dict[int, List]
 
     def _reset(self):
-        """Reset this plugin"""
+        """TODO: Reset this plugin"""
         pass
 
     def initialize(self, symbolic_vm: LaserEVM):
         """Initializes the DependencyPruner
 
-        Introduces hooks in symbolic_vm to track the desired values
         :param symbolic_vm
         """
         self._reset()
 
         @symbolic_vm.laser_hook("start_sym_trans")
-        def start_sym_exec_hook():
-            pass
-
-        @symbolic_vm.laser_hook("stop_sym_trans")
-        def stop_sym_exec_hook():
-            pass
+        def start_sym_trans_hook():
+            self.iteration += 1
+            logging.info("Starting iteration {}".format(self.iteration))
 
         @symbolic_vm.pre_hook("JUMPDEST")
-        def mutator_hook(global_state: GlobalState):
-            pass
+        def mutator_hook(state: GlobalState):
+            annotation = get_dependency_annotation(state)
+            address = state.get_current_instruction()["address"]
+
+            annotation.path.append(state.get_current_instruction()["address"])
+
+            if self.iteration < 2 or address not in self.dependency_map:
+                return
+
+            if not set(annotation.storage_written).intersection(
+                set(self.dependency_map[address])
+            ):
+                logging.info("Skipping state")
+                raise PluginSkipState
 
         @symbolic_vm.pre_hook("SSTORE")
-        def mutator_hook(global_state: GlobalState):
-            pass
+        def mutator_hook(state: GlobalState):
+            annotation = get_dependency_annotation(state)
+            annotation.storage_written.append(state.mstate.stack[-1])
+            annotation.storage_written = list(
+                set(annotation.storage_written + [state.mstate.stack[-1]])
+            )
+
+        @symbolic_vm.pre_hook("SLOAD")
+        def mutator_hook(state: GlobalState):
+
+            annotation = get_dependency_annotation(state)
+            annotation.storage_loaded.append(state.mstate.stack[-1])
 
         @symbolic_vm.pre_hook("STOP")
-        def mutator_hook(global_state: GlobalState):
-            pass
+        def mutator_hook(state: GlobalState):
+            annotation = get_dependency_annotation(state)
+
+            for index in annotation.storage_loaded:
+
+                for address in annotation.path:
+
+                    if address in self.dependency_map:
+                        self.dependency_map[address] = list(
+                            set(self.dependency_map[address] + [index])
+                        )
+                    else:
+                        self.dependency_map[address] = [index]
 
         @symbolic_vm.laser_hook("add_world_state")
-        def world_state_filter_hook(global_state: GlobalState):
-            # raise PluginSkipWorldState
-            pass
+        def world_state_filter_hook(state: GlobalState):
+
+            if isinstance(state.current_transaction, ContractCreationTransaction):
+                return
+
+            annotation = get_dependency_annotation(state)
+            state.world_state.annotate(annotation)
+
+            """
+            log.info(
+                "Add World State {}\nDependency map: {}\nStorage indices written: {}".format(
+                    state.get_current_instruction()["address"],
+                    self.dependency_map,
+                    annotation.storage_written,
+                )
+            )
+            """

mythril/laser/ethereum/plugins/plugin_factory.py

@@ -30,3 +30,12 @@ class PluginFactory:
         )
 
         return InstructionCoveragePlugin()
+
+    @staticmethod
+    def build_dependency_pruner_plugin() -> LaserPlugin:
+        """ Creates an instance of the mutation pruner plugin"""
+        from mythril.laser.ethereum.plugins.implementations.dependency_pruner import (
+            DependencyPruner,
+        )
+
+        return DependencyPruner()

mythril/laser/ethereum/plugins/signals.py

@@ -15,3 +15,13 @@ class PluginSkipWorldState(PluginSignal):
     """
 
     pass
+
+
+class PluginSkipState(PluginSignal):
+    """ Plugin to skip world state
+
+    Plugins that raise this signal while the add_world_state hook is being executed
+    will force laser to abandon that world state.
+    """
+
+    pass

mythril/laser/ethereum/svm.py

@@ -10,7 +10,7 @@ from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
 from mythril.laser.ethereum.evm_exceptions import VmException
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.iprof import InstructionProfiler
-from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
+from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState
 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
@@ -271,7 +271,12 @@ class LaserEVM:
             self._add_world_state(global_state)
             return [], None
 
-        self._execute_pre_hook(op_code, global_state)
+        try:
+            self._execute_pre_hook(op_code, global_state)
+        except PluginSkipState:
+            self._add_world_state(global_state)
+            return [], None
+
         try:
             new_global_states = Instruction(
                 op_code, self.dynamic_loader, self.iprof