Symbolic test implementation

mythril/laser/ethereum/transaction/symbolic.py

@@ -2,7 +2,7 @@ from mythril.laser.ethereum.transaction.transaction_models import MessageCallTra
 from z3 import BitVec
 from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.cfg import Node, Edge
+from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 
 
 def execute_message_call(laser_evm, callee_address):
@@ -21,7 +21,7 @@ def execute_message_call(laser_evm, callee_address):
             BitVec("origin", 256),
             CalldataType.SYMBOLIC,
         )
-        _setup_global_state_for_execution(transaction)
+        _setup_global_state_for_execution(laser_evm, transaction)
 
     laser_evm.exec()
 
@@ -46,23 +46,23 @@ def execute_contract_creation(laser_evm, contract_initialization_code):
             CalldataType.SYMBOLIC
         )
 
-        _setup_global_state_for_execution(transaction)
+        _setup_global_state_for_execution(laser_evm, transaction)
     laser_evm.exec(True)
 
     return new_account
 
 
-def _setup_global_state_for_execution(self, transaction):
+def _setup_global_state_for_execution(laser_evm, transaction):
     """ Sets up global state and cfg for a transactions execution"""
     global_state = transaction.initial_global_state()
     global_state.transaction_stack.append((transaction, None))
 
     new_node = Node(global_state.environment.active_account.contract_name)
 
-    self.nodes[new_node.uid] = new_node
+    laser_evm.nodes[new_node.uid] = new_node
     if transaction.world_state.node:
-        self.edges.append(Edge(transaction.world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction,
+        laser_evm.edges.append(Edge(transaction.world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction,
                                condition=None))
     global_state.node = new_node
     new_node.states.append(global_state)
-    self.work_list.append(global_state)
+    laser_evm.work_list.append(global_state)

tests/laser/transaction/symbolic_test.py

@@ -0,0 +1,57 @@
+from mythril.laser.ethereum.transaction.symbolic import execute_message_call, execute_contract_creation
+from mythril.laser.ethereum.transaction import MessageCallTransaction, ContractCreationTransaction
+from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.ethereum.state import WorldState
+import unittest.mock as mock
+from unittest.mock import MagicMock
+
+
+def _is_message_call(_, transaction):
+    assert isinstance(transaction, MessageCallTransaction)
+
+
+def _is_contract_creation(_, transaction):
+    assert isinstance(transaction, ContractCreationTransaction)
+
+
+@mock.patch("mythril.laser.ethereum.transaction.symbolic._setup_global_state_for_execution")
+def test_execute_message_call(mocked_setup: MagicMock):
+    # Arrange
+    laser_evm = LaserEVM({})
+
+    world_state = WorldState()
+    world_state.accounts["address"] = "something"
+
+    laser_evm.open_states = [world_state]
+    laser_evm.exec = MagicMock()
+
+    mocked_setup.side_effect = _is_message_call
+
+    # Act
+    execute_message_call(laser_evm, "address")
+
+    # Assert
+    laser_evm.exec.assert_called_once()
+
+    assert len(laser_evm.open_states) == 0
+    mocked_setup.assert_called_once()
+
+
+@mock.patch("mythril.laser.ethereum.transaction.symbolic._setup_global_state_for_execution")
+def test_execute_contract_creation(mocked_setup: MagicMock):
+    # Arrange
+    laser_evm = LaserEVM({})
+
+    laser_evm.open_states = [WorldState(), WorldState()]
+    laser_evm.exec = MagicMock()
+    mocked_setup.side_effect = _is_contract_creation
+
+    # Act
+    new_account = execute_contract_creation(laser_evm, "606000")
+
+    # Assert
+    laser_evm.exec.assert_called_once()
+
+    assert len(laser_evm.open_states) == 0
+    mocked_setup.assert_called()
+