Skeleton

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:
+        # if not disable_dependency_pruning:
-            plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
+        #    plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
 
         world_state = WorldState()
         for account in self.accounts.values():

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"

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

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()

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]:
         """