From 2fd420c4458a2770c3d2d6217c6a8fb6a4d1677b Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 23 Oct 2019 14:25:33 +0200
Subject: [PATCH] add body to the stub function exit implementations

---
 .../plugins/implementations/summary/core.py   | 45 +++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/mythril/laser/ethereum/plugins/implementations/summary/core.py b/mythril/laser/ethereum/plugins/implementations/summary/core.py
index ca772c9d..f4efcd95 100644
--- a/mythril/laser/ethereum/plugins/implementations/summary/core.py
+++ b/mythril/laser/ethereum/plugins/implementations/summary/core.py
@@ -106,3 +106,48 @@ class SymbolicSummaryPlugin(LaserPlugin):
     def _restore_previous_state(global_state: GlobalState, tracking_annotation: SummaryTrackingAnnotation):
         """Restores the previous persistent variables to the global state"""
         pass
+
+    @staticmethod
+    def _get_and_remove_summary_tracking_annotation(global_state: GlobalState) -> Optional[SummaryTrackingAnnotation]:
+        """ Retrieves symbolic summary from the global state"""
+        summary_annotation: List[SummaryTrackingAnnotation] = list(
+            global_state.get_annotations(SummaryTrackingAnnotation))
+        if len(summary_annotation) != 1:
+            logging.warning(
+                f"Unexpected number of summary tracking annotations found: {len(summary_annotation)}\nSkipping..."
+            )
+
+        summary_annotation: SummaryTrackingAnnotation = summary_annotation[0]
+        global_state.annotations.remove(summary_annotation)
+        return summary_annotation
+
+    def _record_symbolic_summary(self, global_state: GlobalState, tracking_annotation: SummaryTrackingAnnotation):
+        """Records a summary between tracking_annotation.entry and global_state"""
+        storage_mutations = []
+        # TODO: record return value
+        return_value = None
+
+        for index, account in global_state.world_state.accounts.items():
+            storage_mutations.append((index, account.storage._standard_storage))
+
+        condition = global_state.mstate.constraints[:]
+        for constraint in tracking_annotation.entry.mstate.constraints:
+            condition.remove(constraint)
+
+        summary = SymbolicSummary(
+            storage_effect=storage_mutations,
+            condition=condition,
+            return_value=return_value,
+            entry=tracking_annotation.entry.mstate.pc,
+            exit=global_state.mstate.pc
+        )
+        self.summaries.append(summary)
+
+    @staticmethod
+    def _restore_previous_state(global_state: GlobalState, tracking_annotation: SummaryTrackingAnnotation):
+        """Restores the previous persistent variables to the global state"""
+        for account in global_state.world_state.accounts:
+            for og_storage, sym_storage in tracking_annotation.storage_pairs:
+                account.storage.replace(sym_storage, og_storage)
+        for constraint in tracking_annotation.storage_constraints:
+            global_state.mstate.constraints.remove(constraint)