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