diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 2caffafc..d51e3585 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1697,20 +1697,37 @@ class Instruction: gas_price = environment.gasprice origin = environment.origin - contract_address = None - if create2_salt: - salt = hex(create2_salt)[2:] - salt = "0" * (64 - len(salt)) + salt + contract_address = None # type: Union[BitVec, int] + Instruction._sha3_gas_helper(global_state, len(code_str[2:]) // 2) - addr = hex(caller.value)[2:] - addr = "0" * (40 - len(addr)) + addr + if create2_salt: + if create2_salt.symbolic: + if create2_salt.size() != 256: + pad = symbol_factory.BitVecVal(0, 256 - create2_salt.size()) + create2_salt = Concat(pad, create2_salt) + address, constraint = keccak_function_manager.create_keccak( + Concat( + symbol_factory.BitVecVal(255, 8), + caller, + create2_salt, + symbol_factory.BitVecVal(int(get_code_hash(code_str), 16), 256), + ) + ) + contract_address = Extract(255, 96, address) + global_state.world_state.constraints.append(constraint) + else: + salt = hex(create2_salt.value)[2:] + salt = "0" * (64 - len(salt)) + salt - Instruction._sha3_gas_helper(global_state, len(code_str[2:]) // 2) + addr = hex(caller.value)[2:] + addr = "0" * (40 - len(addr)) + addr - contract_address = int( - get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:], - 16, - ) + contract_address = int( + get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[ + 26: + ], + 16, + ) transaction = ContractCreationTransaction( world_state=world_state, caller=caller, diff --git a/tests/instructions/create2_test.py b/tests/instructions/create2_test.py index 30cfc239..d98de529 100644 --- a/tests/instructions/create2_test.py +++ b/tests/instructions/create2_test.py @@ -9,6 +9,7 @@ from mythril.laser.ethereum.transaction.transaction_models import ( MessageCallTransaction, TransactionStartSignal, ) +from mythril.laser.smt import symbol_factory from mythril.laser.ethereum.state.calldata import ConcreteCalldata from mythril.support.support_utils import get_code_hash @@ -20,7 +21,7 @@ def generate_salted_address(code_str, salt, caller): addr = hex(caller.value)[2:] addr = "0" * (40 - len(addr)) + addr - salt = hex(salt)[2:] + salt = hex(salt.value)[2:] salt = "0" * (64 - len(salt)) + salt contract_address = int( @@ -46,9 +47,14 @@ def test_create2(): og_state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) ) - value = 3 - salt = 10 - og_state.mstate.stack = [salt, 6, 0, value] + value = symbol_factory.BitVecVal(3, 256) + salt = symbol_factory.BitVecVal(10, 256) + og_state.mstate.stack = [ + salt, + symbol_factory.BitVecVal(6, 256), + symbol_factory.BitVecVal(0, 256), + value, + ] instruction = Instruction("create2", dynamic_loader=None) # Act + Assert