From 4ea9827d663eb1fde412ede78b2a26710b0a1aec Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Wed, 4 Sep 2019 14:43:58 +0200
Subject: [PATCH] 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.
---
 .../plugins/implementations/mutation_pruner.py   | 16 ++++++++++++++--
 mythril/laser/ethereum/state/annotation.py       |  2 ++
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
index 86755610..fa6aef58 100644
--- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
+++ b/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
diff --git a/mythril/laser/ethereum/state/annotation.py b/mythril/laser/ethereum/state/annotation.py
index 6a321776..0f25a311 100644
--- a/mythril/laser/ethereum/state/annotation.py
+++ b/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