diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 72d17e5d..6b1f875d 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -6,7 +6,7 @@ import logging from copy import copy, deepcopy from typing import cast, Callable, List, Union, Tuple from datetime import datetime - +from math import ceil from ethereum import utils from mythril.laser.smt import ( @@ -932,6 +932,34 @@ class Instruction: global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256)) return [global_state] + @staticmethod + def _handle_symbolic_args( + global_state: GlobalState, concrete_memory_offset: int + ) -> None: + """ + In contract creation transaction with dynamic arguments(like arrays, maps) solidity will try to + execute CODECOPY with code size as len(with_args) - len(without_args) which in our case + would be 0, hence we are writing 10 symbol words onto the memory on the assumption that + no one would use 10 array/map arguments for constructor. + :param global_state: The global state + :param concrete_memory_offset: The memory offset on which symbols should be written + :return: + """ + no_of_words = ceil( + min(len(global_state.environment.code.bytecode) / 2, 320) / 32 + ) + global_state.mstate.mem_extend(concrete_memory_offset, 32 * no_of_words) + for i in range(no_of_words): + global_state.mstate.memory.write_word_at( + concrete_memory_offset + i * 32, + global_state.new_bitvec( + "code_{}({})".format( + i + 1, global_state.environment.active_account.contract_name + ), + 256, + ), + ) + @StateTransition() def codecopy_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -992,15 +1020,7 @@ class Instruction: global_state.current_transaction, ContractCreationTransaction ): if concrete_code_offset >= len(bytecode) // 2: - global_state.mstate.mem_extend(concrete_memory_offset, 1) - global_state.mstate.memory[ - concrete_memory_offset - ] = global_state.new_bitvec( - "code({})".format( - global_state.environment.active_account.contract_name - ), - 8, - ) + self._handle_symbolic_args(global_state, concrete_memory_offset) return [global_state] for i in range(size):