diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 1895eefe..d010be0a 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -758,34 +758,33 @@ class Instruction: """ state = global_state.mstate environment = global_state.environment - state.stack.append(environment.calldata.calldatasize) - return [global_state] - @StateTransition() - def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: - """ + if isinstance(global_state.current_transaction, ContractCreationTransaction): + log.debug("Attempt to use CALLDATASIZE in creation transaction") + state.stack.append(0) + else: + state.stack.append(environment.calldata.calldatasize) - :param global_state: - :return: - """ - state = global_state.mstate + return [global_state] + + @staticmethod + def _calldata_copy_helper(global_state, state, mstart, dstart, size): environment = global_state.environment - op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() try: - mstart = util.get_concrete_int(op0) + mstart = util.get_concrete_int(mstart) except TypeError: log.debug("Unsupported symbolic memory offset in CALLDATACOPY") return [global_state] try: - dstart = util.get_concrete_int(op1) # type: Union[int, BitVec] + dstart = util.get_concrete_int(dstart) # type: Union[int, BitVec] except TypeError: log.debug("Unsupported symbolic calldata offset in CALLDATACOPY") - dstart = simplify(op1) + dstart = simplify(dstart) try: - size = util.get_concrete_int(op2) # type: Union[int, BitVec] + size = util.get_concrete_int(size) # type: Union[int, BitVec] except TypeError: log.debug("Unsupported symbolic size in CALLDATACOPY") size = 320 # The excess size will get overwritten @@ -839,6 +838,22 @@ class Instruction: ) return [global_state] + @StateTransition() + def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: + """ + + :param global_state: + :return: + """ + state = global_state.mstate + op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() + + if isinstance(global_state.current_transaction, ContractCreationTransaction): + log.debug("Attempt to use CALLDATACOPY in creation transaction") + return [global_state] + + return self._calldata_copy_helper(global_state, state, op0, op1, op2) + # Environment @StateTransition() def address_(self, global_state: GlobalState) -> List[GlobalState]: @@ -902,7 +917,12 @@ class Instruction: state = global_state.mstate environment = global_state.environment disassembly = environment.code - no_of_bytes = min(len(disassembly.bytecode) / 2, 320) + (len(disassembly.bytecode) / 2) + if isinstance(global_state.current_transaction, ContractCreationTransaction): + # Hacky way to ensure constructor arguments work - Max size is 5000 + # FIXME: Perhaps add some constraint here to ensure that concretization works correctly + no_of_bytes = len(disassembly.bytecode) // 2 + 5000 + else: + no_of_bytes = len(disassembly.bytecode) // 2 state.stack.append(no_of_bytes) return [global_state] @@ -1027,14 +1047,24 @@ class Instruction: global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), ) - return self._code_copy_helper( - code=global_state.environment.code.bytecode, - memory_offset=memory_offset, - code_offset=code_offset, - size=size, - op="CODECOPY", - global_state=global_state, - ) + + if ( + isinstance(global_state.current_transaction, ContractCreationTransaction) + and code_offset >= len(global_state.environment.code.bytecode) // 2 + ): + offset = code_offset - len(global_state.environment.code.bytecode) // 2 + return self._calldata_copy_helper( + global_state, global_state.mstate, memory_offset, offset, size + ) + else: + return self._code_copy_helper( + code=global_state.environment.code.bytecode, + memory_offset=memory_offset, + code_offset=code_offset, + size=size, + op="CODECOPY", + global_state=global_state, + ) @StateTransition() def extcodesize_(self, global_state: GlobalState) -> List[GlobalState]: diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 2212e805..ae18d3a3 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -85,6 +85,8 @@ def execute_contract_creation( new_account = None for open_world_state in open_states: next_transaction_id = get_next_transaction_id() + # call_data "should" be '[]', but it is easier to model the calldata symbolically + # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly" transaction = ContractCreationTransaction( world_state=open_world_state, identifier=next_transaction_id, @@ -98,7 +100,7 @@ def execute_contract_creation( code=Disassembly(contract_initialization_code), caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256), contract_name=contract_name, - call_data=[], + call_data=None, # Hrmm call_value=symbol_factory.BitVecSym( "call_value{}".format(next_transaction_id), 256 ), diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index c2b18b9c..97f2f694 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -197,6 +197,8 @@ class ContractCreationTransaction(BaseTransaction): 0, concrete_storage=True, creator=caller.value ) callee_account.contract_name = contract_name + # init_call_data "should" be false, but it is easier to model the calldata symbolically + # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly" super().__init__( world_state=world_state, callee_account=callee_account, @@ -208,7 +210,7 @@ class ContractCreationTransaction(BaseTransaction): origin=origin, code=code, call_value=call_value, - init_call_data=False, + init_call_data=True, ) def initial_global_state(self) -> GlobalState: