Make global state use worldstate object versus accounts dictionary

mythril/laser/ethereum/instructions.py

@@ -907,7 +907,7 @@ class Instruction:
             # TODO: maybe use BitVec here constrained to 1
             return [global_state]
 
-        transaction = CallTransaction(global_state.accounts,
+        transaction = CallTransaction(global_state.world_state,
                                       callee_account,
                                       BitVecVal(int(environment.active_account.address, 16), 256),
                                       call_data,

mythril/laser/ethereum/state.py

@@ -144,10 +144,11 @@ class GlobalState:
     """
     GlobalState represents the current globalstate
     """
-    def __init__(self, accounts, environment, node, machine_state=None, transaction_stack=None, ret_data=None):
+    def __init__(self, world_state, environment, node, machine_state=None, transaction_stack=None, ret_data=None):
         """ Constructor for GlobalState"""
         self.node = node
-        self.accounts = accounts
+        assert isinstance(world_state, WorldState)
+        self.world_state = world_state
         self.environment = environment
         self.mstate = machine_state if machine_state else MachineState(gas=10000000)
         self.transaction_stack = transaction_stack if transaction_stack else []
@@ -155,11 +156,15 @@ class GlobalState:
         self.last_return_data = ret_data
 
     def __copy__(self):
-        accounts = copy(self.accounts)
+        world_state = copy(self.world_state)
         environment = copy(self.environment)
         mstate = deepcopy(self.mstate)
         transaction_stack = copy(self.transaction_stack)
-        return GlobalState(accounts, environment, self.node, mstate, transaction_stack=transaction_stack, ret_data=self.last_return_data)
+        return GlobalState(world_state, environment, self.node, mstate, transaction_stack=transaction_stack, ret_data=self.last_return_data)
+
+    @property
+    def accounts(self):
+        return self.world_state.accounts
 
     #TODO: remove this, as two instructions are confusing
     def get_current_instruction(self):
@@ -193,6 +198,12 @@ class WorldState:
         """
         return self.accounts[item]
 
+    def __copy__(self):
+        new_world_state = WorldState()
+        new_world_state.accounts = copy(self.accounts)
+        new_world_state.node = self.node
+        return new_world_state
+
     def create_account(self, balance=0):
         """
         Create non-contract account

mythril/laser/ethereum/svm.py

@@ -114,7 +114,7 @@ class LaserEVM:
 
                 # Set execution result in the return_state
                 return_global_state.last_return_data = transaction.return_data
-                return_global_state.accounts = copy(global_state.accounts)
+                return_global_state.world_state = copy(global_state.world_state)
                 return_global_state.environment.active_account =\
                     global_state.accounts[return_global_state.environment.active_account.contract_name]
 

mythril/laser/ethereum/transaction.py

@@ -1,6 +1,6 @@
 import logging
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType
+from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, WorldState
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 from z3 import BitVec
 
@@ -28,6 +28,8 @@ class CallTransaction:
                  origin=BitVec("origin", 256),
                  call_data_type=BitVec("call_data_type", 256)
                  ):
+        assert isinstance(world_state, WorldState)
+
         self.world_state = world_state
         self.callee_account = callee_account
         self.caller = caller
@@ -98,7 +100,7 @@ class MessageCall(Transaction):
         for open_world_state in open_states:
 
             transaction = CallTransaction(
-                open_world_state.accounts,
+                open_world_state,
                 open_world_state[self.callee_address],
                 self.caller,
                 [],