Only propagate code based call annotations (#1211)

* Only propagate code based call annotations

* Move the if condition to a better place

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

@@ -1,7 +1,10 @@
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
 from mythril.laser.ethereum.plugins.signals import PluginSkipState
-from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
+    DependencyAnnotation,
+    WSDependencyAnnotation,
+)
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
@@ -9,64 +12,12 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 from mythril.exceptions import UnsatError
 from mythril.analysis import solver
 from typing import cast, List, Dict, Set
-from copy import copy
 import logging
 
 
 log = logging.getLogger(__name__)
 
 
-class DependencyAnnotation(StateAnnotation):
-    """Dependency Annotation
-
-    This annotation tracks read and write access to the state during each transaction.
-    """
-
-    def __init__(self):
-        self.storage_loaded = []  # type: List
-        self.storage_written = {}  # type: Dict[int, List]
-        self.has_call = False  # type: bool
-        self.path = [0]  # type: List
-        self.blocks_seen = set()  # type: Set[int]
-
-    def __copy__(self):
-        result = DependencyAnnotation()
-        result.storage_loaded = copy(self.storage_loaded)
-        result.storage_written = copy(self.storage_written)
-        result.has_call = self.has_call
-        result.path = copy(self.path)
-        result.blocks_seen = copy(self.blocks_seen)
-        return result
-
-    def get_storage_write_cache(self, iteration: int):
-        if iteration not in self.storage_written:
-            self.storage_written[iteration] = []
-
-        return self.storage_written[iteration]
-
-    def extend_storage_write_cache(self, iteration: int, value: object):
-        if iteration not in self.storage_written:
-            self.storage_written[iteration] = [value]
-        elif value not in self.storage_written[iteration]:
-            self.storage_written[iteration].append(value)
-
-
-class WSDependencyAnnotation(StateAnnotation):
-    """Dependency Annotation for World state
-
-    This  world state annotation maintains a stack of state annotations.
-    It is used to transfer individual state annotations from one transaction to the next.
-    """
-
-    def __init__(self):
-        self.annotations_stack = []
-
-    def __copy__(self):
-        result = WSDependencyAnnotation()
-        result.annotations_stack = copy(self.annotations_stack)
-        return result
-
-
 def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation:
     """ Returns a dependency annotation
 

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

@@ -1,26 +1,16 @@
-from mythril.laser.ethereum.state.annotation import StateAnnotation
-from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
+from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
+    MutationAnnotation,
+)
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
 from mythril.laser.smt import And, symbol_factory
 
 
-class MutationAnnotation(StateAnnotation):
-    """Mutation Annotation
-
-    This is the annotation used by the MutationPruner plugin to record mutations
-    """
-
-    @property
-    def persist_to_world_state(self):
-        # This should persist among calls, and be but as a world state annotation.
-        return True
-
-
 class MutationPruner(LaserPlugin):
     """Mutation pruner plugin
 
@@ -47,16 +37,10 @@ class MutationPruner(LaserPlugin):
         @symbolic_vm.pre_hook("SSTORE")
         def sstore_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
-            assert len(
-                list(global_state.world_state.get_annotations(MutationAnnotation))
-            )
 
         @symbolic_vm.pre_hook("CALL")
         def call_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
-            assert len(
-                list(global_state.world_state.get_annotations(MutationAnnotation))
-            )
 
         @symbolic_vm.laser_hook("add_world_state")
         def world_state_filter_hook(global_state: GlobalState):
@@ -72,8 +56,5 @@ class MutationPruner(LaserPlugin):
                 global_state.current_transaction, ContractCreationTransaction
             ):
                 return
-            if (
+            if len(list(global_state.get_annotations(MutationAnnotation))) == 0:
-                len(list(global_state.world_state.get_annotations(MutationAnnotation)))
-                == 0
-            ):
                 raise PluginSkipWorldState

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

@@ -0,0 +1,65 @@
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+
+from copy import copy
+from typing import Dict, List, Set
+
+
+class MutationAnnotation(StateAnnotation):
+    """Mutation Annotation
+
+    This is the annotation used by the MutationPruner plugin to record mutations
+    """
+
+    def __init__(self):
+        pass
+
+
+class DependencyAnnotation(StateAnnotation):
+    """Dependency Annotation
+
+    This annotation tracks read and write access to the state during each transaction.
+    """
+
+    def __init__(self):
+        self.storage_loaded = []  # type: List
+        self.storage_written = {}  # type: Dict[int, List]
+        self.has_call = False  # type: bool
+        self.path = [0]  # type: List
+        self.blocks_seen = set()  # type: Set[int]
+
+    def __copy__(self):
+        result = DependencyAnnotation()
+        result.storage_loaded = copy(self.storage_loaded)
+        result.storage_written = copy(self.storage_written)
+        result.has_call = self.has_call
+        result.path = copy(self.path)
+        result.blocks_seen = copy(self.blocks_seen)
+        return result
+
+    def get_storage_write_cache(self, iteration: int):
+        if iteration not in self.storage_written:
+            self.storage_written[iteration] = []
+
+        return self.storage_written[iteration]
+
+    def extend_storage_write_cache(self, iteration: int, value: object):
+        if iteration not in self.storage_written:
+            self.storage_written[iteration] = [value]
+        elif value not in self.storage_written[iteration]:
+            self.storage_written[iteration].append(value)
+
+
+class WSDependencyAnnotation(StateAnnotation):
+    """Dependency Annotation for World state
+
+    This  world state annotation maintains a stack of state annotations.
+    It is used to transfer individual state annotations from one transaction to the next.
+    """
+
+    def __init__(self):
+        self.annotations_stack = []
+
+    def __copy__(self):
+        result = WSDependencyAnnotation()
+        result.annotations_stack = copy(self.annotations_stack)
+        return result

mythril/laser/ethereum/state/global_state.py

@@ -53,6 +53,14 @@ class GlobalState:
         self.last_return_data = last_return_data
         self._annotations = annotations or []
 
+    def add_annotations(self, annotations: List[StateAnnotation]):
+        """
+        Function used to add annotations to global state
+        :param annotations:
+        :return:
+        """
+        self._annotations += annotations
+
     def __copy__(self) -> "GlobalState":
         """
 

mythril/laser/ethereum/svm.py

@@ -12,6 +12,9 @@ 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, PluginSkipState
+from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
+    MutationAnnotation,
+)
 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
@@ -354,6 +357,19 @@ class LaserEVM:
                 # First execute the post hook for the transaction ending instruction
                 self._execute_post_hook(op_code, [end_signal.global_state])
 
+                # Propogate codecall based annotations
+                if return_global_state.get_current_instruction()["opcode"] in (
+                    "DELEGATECALL",
+                    "CALLCODE",
+                ):
+                    new_annotations = [
+                        annotation
+                        for annotation in global_state.get_annotations(
+                            MutationAnnotation
+                        )
+                    ]
+                    return_global_state.add_annotations(new_annotations)
+
                 new_global_states = self._end_message_call(
                     copy(return_global_state),
                     global_state,