Propagate annotations to the parent call, when a call succeeds. (#1197)

* Propagate annotations to the parent call, when a call succeeds.

This makes the MutationPruner behave correctly.

* Add a copy_annotations_from method.

* Run black.

* WIP

* Use persist_to_world_state and the world state instead.

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

@@ -15,7 +15,10 @@ class MutationAnnotation(StateAnnotation):
     This is the annotation used by the MutationPruner plugin to record mutations
     """
 
-    pass
+    @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):
@@ -44,10 +47,16 @@ 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):
@@ -63,5 +72,8 @@ class MutationPruner(LaserPlugin):
                 global_state.current_transaction, ContractCreationTransaction
             ):
                 return
-            if len(list(global_state.get_annotations(MutationAnnotation))) == 0:
+            if (
+                len(list(global_state.world_state.get_annotations(MutationAnnotation)))
+                == 0
+            ):
                 raise PluginSkipWorldState

mythril/laser/ethereum/state/annotation.py

@@ -12,6 +12,8 @@ class StateAnnotation:
     traverse the state space themselves.
     """
 
+    # TODO: Remove this? It seems to be used only in the MutationPruner, and
+    # we could simply use world state annotations if we want them to be persisted.
     @property
     def persist_to_world_state(self) -> bool:
         """If this function returns true then laser will also annotate the