Fix create salt (#1306)

* Remove native tests

* Handle symbolic salt

* Handle symbolic salt

* Add type hint for contract_address

* Bring the instruction gas up

* Fix the tests and the instruction

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

mythril/laser/ethereum/instructions.py

@@ -1697,20 +1697,37 @@ class Instruction:
         gas_price = environment.gasprice
         origin = environment.origin
 
-        contract_address = None
+        contract_address = None  # type: Union[BitVec, int]
-        if create2_salt:
+        Instruction._sha3_gas_helper(global_state, len(code_str[2:]) // 2)
-            salt = hex(create2_salt)[2:]
-            salt = "0" * (64 - len(salt)) + salt
 
-            addr = hex(caller.value)[2:]
+        if create2_salt:
-            addr = "0" * (40 - len(addr)) + addr
+            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(
+                contract_address = int(
-                get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:],
+                    get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[
-                16,
+                        26:
-            )
+                    ],
+                    16,
+                )
         transaction = ContractCreationTransaction(
             world_state=world_state,
             caller=caller,

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
+    value = symbol_factory.BitVecVal(3, 256)
-    salt = 10
+    salt = symbol_factory.BitVecVal(10, 256)
-    og_state.mstate.stack = [salt, 6, 0, value]
+    og_state.mstate.stack = [
+        salt,
+        symbol_factory.BitVecVal(6, 256),
+        symbol_factory.BitVecVal(0, 256),
+        value,
+    ]
     instruction = Instruction("create2", dynamic_loader=None)
 
     # Act + Assert