From 677d2eff9fd5f89925d962f5dd17e305f6cdbde6 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 23 Oct 2019 14:23:36 +0200
Subject: [PATCH] add initial classes and documentation for summary generation

---
 .../implementations/summary/__init__.py       |  0
 .../plugins/implementations/summary/core.py   | 72 +++++++++++++++++++
 2 files changed, 72 insertions(+)
 create mode 100644 mythril/laser/ethereum/plugins/implementations/summary/__init__.py
 create mode 100644 mythril/laser/ethereum/plugins/implementations/summary/core.py

diff --git a/mythril/laser/ethereum/plugins/implementations/summary/__init__.py b/mythril/laser/ethereum/plugins/implementations/summary/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/mythril/laser/ethereum/plugins/implementations/summary/core.py b/mythril/laser/ethereum/plugins/implementations/summary/core.py
new file mode 100644
index 00000000..d9cac335
--- /dev/null
+++ b/mythril/laser/ethereum/plugins/implementations/summary/core.py
@@ -0,0 +1,72 @@
+from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.ethereum.plugins.plugin import LaserPlugin
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.smt import K, Array, BaseArray, Bool
+
+from typing import Dict, Tuple, List, Optional
+from copy import copy
+
+import logging
+
+log = logging.getLogger(__name__)
+
+
+class SummaryTrackingAnnotation(StateAnnotation):
+    """ SummaryTrackingAnnotation
+    This annotation is used by the symbolic summary plugin to keep track of data related to a summary that
+    will be computed during the future exploration of the annotated world state.
+    """
+    def __init__():
+        pass
+
+
+class SymbolicSummary:
+    """ Symbolic Summary
+
+    A symbolic summary is an awesome construct that allows mythril to record and re-use partial analysis results
+    """
+    def __init__():
+        pass
+
+
+class SymbolicSummaryPlugin(LaserPlugin):
+
+    def __init__(self):
+        self.summaries = []
+
+    def initialize(self, symbolic_vm: LaserEVM):
+        """Initializes the symbolic summary generating plugin
+
+        Introduces hooks for each instruction
+        :param symbolic_vm: the symbolic virtual machine to initialize this plugin for
+        """
+
+        @symbolic_vm.laser_hook("stop_sym_exec")
+        def stop_sym_exec_hook():
+            # Print results
+            log.info("Generated 0 summaries")
+
+        @symbolic_vm.laser_hook("start_sym_trans")
+        def execute_start_sym_trans_hook():
+            pass
+
+        @symbolic_vm.laser_hook("stop_sym_trans")
+        def execute_stop_sym_trans_hook():
+            pass
+
+    def summary_entry(self, global_state: GlobalState):
+        """ Handles logic for when the analysis reaches an entry point of a to-be recorded symbolic summary
+
+        :param global_state: The state at the entry of the symbolic summary
+        """
+        pass
+
+    def summary_exit(self, global_state: GlobalState):
+        """ Handles logic for when the analysis reaches the summary exit
+
+        This function populates self.summaries with the discovered symbolic summaries
+        :param global_state: The state at the exit of the discovered symbolic summary
+        """
+        pass