From 58223c52a745bcc3eae9ac73b6f3e95231bca5a9 Mon Sep 17 00:00:00 2001
From: Bernhard Mueller <bernhard.mueller11@gmail.com>
Date: Thu, 11 Jul 2019 11:47:22 +0200
Subject: [PATCH] Skeleton

---
 mythril/analysis/symbolic.py                  |  5 +-
 .../coverage/coverage_plugin.py               |  2 +-
 .../plugins/implementations/state_merge.py    | 46 +++++++++++++++++++
 .../laser/ethereum/plugins/plugin_factory.py  |  9 ++++
 mythril/laser/ethereum/svm.py                 |  2 +-
 5 files changed, 60 insertions(+), 4 deletions(-)
 create mode 100644 mythril/laser/ethereum/plugins/implementations/state_merge.py

diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py
index e6c2bf24..304939e2 100644
--- a/mythril/analysis/symbolic.py
+++ b/mythril/analysis/symbolic.py
@@ -119,9 +119,10 @@ class SymExecWrapper:
         plugin_loader = LaserPluginLoader(self.laser)
         plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
         plugin_loader.load(PluginFactory.build_instruction_coverage_plugin())
+        plugin_loader.load(PluginFactory.build_state_merge_plugin())
 
-        if not disable_dependency_pruning:
-            plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
+        # if not disable_dependency_pruning:
+        #    plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
 
         world_state = WorldState()
         for account in self.accounts.values():
diff --git a/mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py
index 75c6bfa4..f8886e9e 100644
--- a/mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py
+++ b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py
@@ -70,7 +70,7 @@ class InstructionCoveragePlugin(LaserPlugin):
             self.initial_coverage = self._get_covered_instructions()
 
         @symbolic_vm.laser_hook("stop_sym_trans")
-        def execute_stop_sym_trans_hook():
+        def execute_stop_sym_trans_hook(svm: LaserEVM):
             end_coverage = self._get_covered_instructions()
             log.info(
                 "Number of new instructions covered in tx %d: %d"
diff --git a/mythril/laser/ethereum/plugins/implementations/state_merge.py b/mythril/laser/ethereum/plugins/implementations/state_merge.py
new file mode 100644
index 00000000..b8bdb1d6
--- /dev/null
+++ b/mythril/laser/ethereum/plugins/implementations/state_merge.py
@@ -0,0 +1,46 @@
+from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.ethereum.plugins.plugin import LaserPlugin
+from mythril.laser.smt import symbol_factory, simplify
+import logging
+
+log = logging.getLogger(__name__)
+
+
+class StateMerge(LaserPlugin):
+
+    def initialize(self, symbolic_vm: LaserEVM):
+        """Initializes the mutation pruner
+
+        Introduces hooks for SSTORE operations
+        :param symbolic_vm:
+        :return:
+        """
+
+        @symbolic_vm.laser_hook("stop_sym_trans")
+        def execute_stop_sym_trans_hook(svm: LaserEVM):
+            log.info(svm.open_states)
+
+            open_states = svm.open_states
+
+            if len(open_states) == 0:
+                return
+
+            merged_state = open_states[0]
+            n_states = len(open_states) - 1
+
+            for i in range(0, n_states):
+
+                other_state = open_states.pop(-1)
+                self.merge_states(merged_state, 0, other_state, i)
+
+
+    @staticmethod
+    def merge_states(state1, i1, state2, i2):
+
+        ws_id = symbol_factory.BitVecSym("ws_id", 256)
+
+        state1.node.constraints = [simplify((state1.node.constraints and ws_id == i1) or (state2.node.constraints and ws_id == i2))]
+
+        # TODO Merge annotations
+
+        # TODO Merge storage
diff --git a/mythril/laser/ethereum/plugins/plugin_factory.py b/mythril/laser/ethereum/plugins/plugin_factory.py
index a81f80c4..0f559418 100644
--- a/mythril/laser/ethereum/plugins/plugin_factory.py
+++ b/mythril/laser/ethereum/plugins/plugin_factory.py
@@ -39,3 +39,12 @@ class PluginFactory:
         )
 
         return DependencyPruner()
+
+    @staticmethod
+    def build_state_merge_plugin() -> LaserPlugin:
+        """ Creates an instance of the state merge plugin"""
+        from mythril.laser.ethereum.plugins.implementations.state_merge import (
+            StateMerge,
+        )
+
+        return StateMerge()
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 9755fc33..e55c5550 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -198,7 +198,7 @@ class LaserEVM:
             execute_message_call(self, address)
 
             for hook in self._stop_sym_trans_hooks:
-                hook()
+                hook(self)
 
     def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]:
         """