diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 49daf7fc..64798ec0 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/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, diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 09e392be..d2550832 100644 --- a/mythril/laser/ethereum/state.py +++ b/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 diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index a5e2ddac..ccd25d97 100644 --- a/mythril/laser/ethereum/svm.py +++ b/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] diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py index 5109da6f..c27b1057 100644 --- a/mythril/laser/ethereum/transaction.py +++ b/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, [],