move everything to plugin

mythril/laser/ethereum/cfg.py

@@ -86,30 +86,6 @@ class Node:
             code=code,
         )
 
-    def merge_nodes(self, node: "Node", constraints: Constraints):
-        """
-        Merges two nodes
-        :param node: The node to be merged
-        :param constraints: The merged constraints
-        :return:
-        """
-        self.states += node.states
-        self.uid = get_new_gbl_id()
-        self.flags |= node.flags
-        self.constraints = constraints
-
-    def check_merge_condition(self, node: "Node"):
-        """
-        Checks whether two nodes are merge-able or not
-        :param node: The other node to be merged
-        :return:
-        """
-        return (
-            self.function_name == node.function_name
-            and self.contract_name == node.contract_name
-            and self.start_addr == node.start_addr
-        )
-
 
 class Edge:
     """The respresentation of a call graph edge."""

mythril/laser/ethereum/plugins/implementations/plugin_annotations.py

@@ -89,3 +89,6 @@ class WSDependencyAnnotation(StateAnnotation):
     def merge_annotations(self, other: "WSDependencyAnnotation"):
         for a1, a2 in zip(self.annotations_stack, other.annotations_stack):
             a1.merge_annotation(a2)
+
+    def persist_to_world_state(self) -> bool:
+        return True

mythril/laser/ethereum/plugins/implementations/state_merge.py

@@ -1,12 +1,18 @@
 from copy import copy
-from typing import Dict, List
+from typing import Dict, List, Tuple, cast
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
 from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.cfg import Node, get_new_gbl_id
+from mythril.laser.ethereum.state.constraints import Constraints
+from mythril.laser.smt import symbol_factory, Array, BitVec, If, Or, And, Not, Bool
 import logging
 
 log = logging.getLogger(__name__)
 
+CONSTRAINT_DIFFERENCE_LIMIT = 15
+
 
 class StateMerge(LaserPlugin):
     def initialize(self, symbolic_vm: LaserEVM):
@@ -59,24 +65,213 @@ class StateMerge(LaserPlugin):
             )
             svm.open_states = new_states
 
-    @staticmethod
-    def check_merge_condition(state1: WorldState, state2: WorldState):
+    def check_merge_condition(self, state1: WorldState, state2: WorldState):
         """
         Check whether two world states can be merged
         :param state1:
         :param state2:
         :return: whether the states can be merged or not
         """
-        basic_condition = state1.check_merge_condition(state2)
+        basic_condition = self.check_ws_merge_condition(state1, state2)
         return basic_condition
 
-    @staticmethod
-    def merge_states(state1: WorldState, state2: WorldState) -> WorldState:
+    def merge_states(self, state1: WorldState, state2: WorldState):
         """
         Merge state2 into state1
         :param state1: The state to be merged into
         :param state2: The state which is merged into state1
         :return:
         """
-        state1.merge_states(state2)
-        return state1
+
+        # Merge constraints
+        state1.constraints, condition1, _ = self._merge_constraints(
+            state1.constraints, state2.constraints
+        )
+
+        # Merge balances
+        state1.balances = cast(Array, If(condition1, state1.balances, state2.balances))
+        state1.starting_balances = cast(
+            Array, If(condition1, state1.starting_balances, state2.starting_balances)
+        )
+
+        # Merge accounts
+        for address, account in state2.accounts.items():
+            if address not in state1._accounts:
+                state1.put_account(account)
+            else:
+                self.merge_accounts(
+                    state1._accounts[address], account, condition1, state1.balances
+                )
+
+        # Merge annotations
+        self._merge_annotations(state1, state2)
+
+        # Merge Node
+        self.merge_nodes(state1.node, state2.node, state1.constraints)
+
+    @staticmethod
+    def _merge_constraints(
+        constraints1: Constraints, constraints2: Constraints
+    ) -> Tuple[Constraints, Bool, Bool]:
+        dict1, dict2 = {}, {}
+        for constraint in constraints1:
+            dict1[constraint] = True
+        for constraint in constraints2:
+            dict2[constraint] = True
+        c1, c2 = symbol_factory.Bool(True), symbol_factory.Bool(True)
+        new_constraint1, new_constraint2 = (
+            symbol_factory.Bool(True),
+            symbol_factory.Bool(True),
+        )
+        same_constraints = Constraints()
+        for key in dict1:
+            if key not in dict2:
+                c1 = And(c1, key)
+                if Not(key) not in dict2:
+                    new_constraint1 = And(new_constraint1, key)
+            else:
+                same_constraints.append(key)
+        for key in dict2:
+            if key not in dict1:
+                c2 = And(c2, key)
+                if Not(key) not in dict1:
+                    new_constraint2 = And(new_constraint2, key)
+            else:
+                same_constraints.append(key)
+        merge_constraints = same_constraints + [Or(new_constraint1, new_constraint2)]
+        return merge_constraints, c1, c2
+
+    @staticmethod
+    def _check_constraint_merge(
+        constraints1: Constraints, constraints2: Constraints
+    ) -> bool:
+        dict1, dict2 = {}, {}
+        for constraint in constraints1:
+            dict1[constraint] = True
+        for constraint in constraints2:
+            dict2[constraint] = True
+        c1, c2 = 0, 0
+        for key in dict1:
+            if key not in dict2 and Not(key) not in dict2:
+                c1 += 1
+        for key in dict2:
+            if key not in dict1 and Not(key) not in dict1:
+                c2 += 1
+        if c1 + c2 > CONSTRAINT_DIFFERENCE_LIMIT:
+            return False
+        return True
+
+    def _check_merge_annotations(self, state1: WorldState, state2: WorldState):
+        """
+
+        :param state:
+        :return:
+        """
+        if len(state2.annotations) != len(state1._annotations):
+            return False
+        if (
+            self._check_constraint_merge(state1.constraints, state2.constraints)
+            is False
+        ):
+            return False
+        for v1, v2 in zip(state2.annotations, state1._annotations):
+            if v1.check_merge_annotation(v2) is False:   # type: ignore
+                return False
+        return True
+
+    @staticmethod
+    def _merge_annotations(state1: "WorldState", state2: "WorldState"):
+        """
+
+        :param state:
+        :return:
+        """
+        for v1, v2 in zip(state1.annotations, state2.annotations):
+            v1.merge_annotations(v2)                     # type: ignore
+
+    def check_ws_merge_condition(self, state1: WorldState, state2: WorldState):
+        """
+        Checks whether we can merge these states or not
+        """
+        if state1.node and not self.check_node_merge_condition(
+            state1.node, state2.node
+        ):
+            return False
+
+        for address, account in state2.accounts.items():
+            if (
+                address in state1._accounts
+                and self.check_account_merge_condition(
+                    state1._accounts[address], account
+                )
+                is False
+            ):
+                return False
+        if not self._check_merge_annotations(state1, state2):
+            return False
+
+        return True
+
+    @staticmethod
+    def merge_accounts(
+        account1: Account,
+        account2: Account,
+        path_condition: Bool,
+        merged_balance: Array,
+    ):
+        """
+        Checks the merge-ability
+        :param account1: The account to merge with
+        :param account2: The second account to merge
+        :param path_condition: The constraint for this account
+        :param merged_balance: The merged balance
+        :return:
+        """
+        assert (
+            account1.nonce == account2.nonce
+            and account1.deleted == account2.deleted
+            and account1.code.bytecode == account2.code.bytecode
+        )
+
+        account1._balances = merged_balance
+        account1.balance = lambda: account1._balances[account1.address]
+        account1.storage.merge_storage(account2.storage, path_condition)
+
+    @staticmethod
+    def check_account_merge_condition(account1: Account, account2: Account):
+        """
+        Checks whether we can merge accounts or not
+        """
+        return (
+            account1.nonce == account2.nonce
+            and account1.deleted == account2.deleted
+            and account1.code.bytecode == account2.code.bytecode
+        )
+
+    @staticmethod
+    def merge_nodes(node1: Node, node2: Node, constraints: Constraints):
+        """
+        Merges two nodes
+        :param node1: The node to be merged
+        :param node2: The other node to be merged
+        :param constraints: The merged constraints
+        :return:
+        """
+        node1.states += node2.states
+        node1.uid = get_new_gbl_id()
+        node1.flags |= node2.flags
+        node1.constraints = constraints
+
+    @staticmethod
+    def check_node_merge_condition(node1: Node, node2: Node):
+        """
+        Checks whether two nodes are merge-able or not
+        :param node1: The node to be merged
+        :param node2: The other node to be merged
+        :return: Boolean, True if we can merge
+        """
+        return (
+            node1.function_name == node2.function_name
+            and node1.contract_name == node2.contract_name
+            and node1.start_addr == node2.start_addr
+        )

mythril/laser/ethereum/state/account.py

@@ -186,38 +186,6 @@ class Account:
         )
         self._balances[self.address] += balance
 
-    def merge_accounts(
-        self, account: "Account", path_condition: Bool, merged_balance: Array
-    ):
-        """
-        Checks the merge-ability
-        :param account: The account to merge with
-        :param path_condition: The constraint for this account
-        :param merged_balance: The merged balance
-        :return:
-        """
-        assert (
-            self.nonce == account.nonce
-            and self.deleted == account.deleted
-            and self.code.bytecode == account.code.bytecode
-        )
-
-        self._balances = merged_balance
-        self.balance = lambda: self._balances[self.address]
-        self.storage.merge_storage(account.storage, path_condition)
-
-    def check_merge_condition(self, account: "Account"):
-        """
-        Checks whether we can merge or not
-        :param account: The account to check merge-ability with
-        :return: True if we can merge them
-        """
-        return (
-            self.nonce == account.nonce
-            and self.deleted == account.deleted
-            and self.code.bytecode == account.code.bytecode
-        )
-
     @property
     def as_dict(self) -> Dict:
         """

mythril/laser/ethereum/state/constraints.py

@@ -30,12 +30,6 @@ class Constraints(list):
         self._default_timeout = 100
         self._is_possible = is_possible
 
-    def compress(self):
-        constraint = True
-        for c in self[:]:
-            constraint = And(constraint, c)
-        return constraint
-
     @property
     def is_possible(self) -> bool:
         """

mythril/laser/ethereum/state/global_state.py

@@ -140,6 +140,8 @@ class GlobalState:
         :param annotation:
         """
         self._annotations.append(annotation)
+        if annotation.persist_to_world_state:
+            self.world_state.annotate(annotation)
 
     @property
     def annotations(self) -> List[StateAnnotation]:

mythril/laser/ethereum/state/world_state.py

@@ -9,15 +9,10 @@ from ethereum.utils import mk_contract_address
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.state.constraints import Constraints
-from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
-    WSDependencyAnnotation,
-)
 
 if TYPE_CHECKING:
     from mythril.laser.ethereum.cfg import Node
 
-CONSTRAINT_DIFFERENCE_LIMIT = 15
-
 
 class WorldState:
     """The WorldState class represents the world state as described in the
@@ -26,7 +21,7 @@ class WorldState:
     def __init__(
         self,
         transaction_sequence=None,
-        annotations: List[WSDependencyAnnotation] = None,
+        annotations: List[StateAnnotation] = None,
         constraints: Constraints = None,
     ) -> None:
         """Constructor for the world state. Initializes the accounts record.
@@ -41,130 +36,7 @@ class WorldState:
 
         self.node = None  # type: Optional['Node']
         self.transaction_sequence = transaction_sequence or []
-        self._annotations = annotations or []  # type: List[WSDependencyAnnotation]
-
-    def merge_states(self, state: "WorldState"):
-        """
-        Merge this state with "state"
-        :param state: The state to be merged with
-        :return:
-        """
-
-        # Merge constraints
-        self.constraints, condition1, _ = self._merge_constraints(state.constraints)
-
-        # Merge balances
-        self.balances = cast(Array, If(condition1, self.balances, state.balances))
-        self.starting_balances = cast(
-            Array, If(condition1, self.starting_balances, state.starting_balances)
-        )
-
-        # Merge accounts
-        for address, account in state.accounts.items():
-            if address not in self._accounts:
-                self.put_account(account)
-            else:
-                self._accounts[address].merge_accounts(
-                    account, condition1, self.balances
-                )
-
-        # Merge annotations
-        self._merge_annotations(state)
-
-        # Merge Node
-        self.node.merge_nodes(state.node, self.constraints)
-
-    def _merge_constraints(
-        self, constraints: Constraints
-    ) -> Tuple[Constraints, Bool, Bool]:
-        dict1, dict2 = {}, {}
-        for constraint in self.constraints:
-            dict1[constraint] = True
-        for constraint in constraints:
-            dict2[constraint] = True
-        c1, c2 = symbol_factory.Bool(True), symbol_factory.Bool(True)
-        new_constraint1, new_constraint2 = (
-            symbol_factory.Bool(True),
-            symbol_factory.Bool(True),
-        )
-        same_constraints = Constraints()
-        for key in dict1:
-            if key not in dict2:
-                c1 = And(c1, key)
-                if Not(key) not in dict2:
-                    new_constraint1 = And(new_constraint1, key)
-            else:
-                same_constraints.append(key)
-        for key in dict2:
-            if key not in dict1:
-                c2 = And(c2, key)
-                if Not(key) not in dict1:
-                    new_constraint2 = And(new_constraint2, key)
-            else:
-                same_constraints.append(key)
-        merge_constraints = same_constraints + [Or(new_constraint1, new_constraint2)]
-        return merge_constraints, c1, c2
-
-    def _check_constraint_merge(self, constraints: Constraints) -> bool:
-        dict1, dict2 = {}, {}
-        for constraint in self.constraints:
-            dict1[constraint] = True
-        for constraint in constraints:
-            dict2[constraint] = True
-        c1, c2 = 0, 0
-        for key in dict1:
-            if key not in dict2 and Not(key) not in dict2:
-                c1 += 1
-        for key in dict2:
-            if key not in dict1 and Not(key) not in dict1:
-                c2 += 1
-        if c1 + c2 > CONSTRAINT_DIFFERENCE_LIMIT:
-            return False
-        return True
-
-    def _check_merge_annotations(self, state: "WorldState"):
-        """
-
-        :param state:
-        :return:
-        """
-        if len(state.annotations) != len(self._annotations):
-            return False
-        if self._check_constraint_merge(state.constraints) is False:
-            return False
-        for v1, v2 in zip(state.annotations, self._annotations):
-            if v1.check_merge_annotation(v2) is False:
-                return False
-        return True
-
-    def _merge_annotations(self, state: "WorldState"):
-        """
-
-        :param state:
-        :return:
-        """
-        for v1, v2 in zip(state.annotations, self._annotations):
-            v1.merge_annotations(v2)
-
-    def check_merge_condition(self, state: "WorldState"):
-        """
-        Checks whether we can merge this state with "state" or not
-        :param state: The state to check the merge-ability with
-        :return: True if we can merge them
-        """
-        if self.node and not self.node.check_merge_condition(state.node):
-            return False
-
-        for address, account in state.accounts.items():
-            if (
-                address in self._accounts
-                and self._accounts[address].check_merge_condition(account) is False
-            ):
-                return False
-        if not self._check_merge_annotations(state):
-            return False
-
-        return True
+        self._annotations = annotations or []  # type: List[StateAnnotation]
 
     @property
     def accounts(self):
@@ -272,7 +144,7 @@ class WorldState:
         new_account.storage = storage
         self.put_account(new_account)
 
-    def annotate(self, annotation: WSDependencyAnnotation) -> None:
+    def annotate(self, annotation: StateAnnotation) -> None:
         """
 
         :param annotation:
@@ -280,7 +152,7 @@ class WorldState:
         self._annotations.append(annotation)
 
     @property
-    def annotations(self) -> List[WSDependencyAnnotation]:
+    def annotations(self) -> List[StateAnnotation]:
         """
 
         :return: