Merge pull request #1202 from ConsenSys/bug/constructor-arguments

Fixing constructor arguments

mythril/analysis/solver.py

@@ -152,16 +152,17 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
         "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
     ).zfill(40)
 
+    input_ = ""
     if isinstance(transaction, ContractCreationTransaction):
         address = ""
-        input_ = transaction.code.bytecode
-    else:
-        input_ = "".join(
-            [
-                hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
-                for b in transaction.call_data.concrete(model)
-            ]
-        )
+        input_ += transaction.code.bytecode
+
+    input_ += "".join(
+        [
+            hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
+            for b in transaction.call_data.concrete(model)
+        ]
+    )
 
     # Create concrete transaction dict
     concrete_transaction = dict()  # type: Dict[str, str]

mythril/analysis/templates/report_as_markdown.jinja2

@@ -36,7 +36,7 @@ Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{%
 
 {% for step in issue.tx_sequence.steps %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
-Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
+Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }}
 {% else %}
 Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }}
 {% endif %}

mythril/analysis/templates/report_as_text.jinja2

@@ -29,7 +29,7 @@ Transaction Sequence:
 
 {% for step in issue.tx_sequence.steps %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
-Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
+Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }}
 {% else %}
 Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }}
 {% endif %}

mythril/laser/ethereum/instructions.py

@@ -770,34 +770,33 @@ def calldatasize_(self, global_state: GlobalState) -> List[GlobalState]:
         """
         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
@@ -851,6 +850,22 @@ def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
                 )
         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]:
@@ -914,7 +929,17 @@ def codesize_(self, global_state: GlobalState) -> List[GlobalState]:
         state = global_state.mstate
         environment = global_state.environment
         disassembly = environment.code
-        state.stack.append(len(disassembly.bytecode) // 2)
+        if isinstance(global_state.current_transaction, ContractCreationTransaction):
+            # Hacky way to ensure constructor arguments work - Pick some reasonably large size.
+            no_of_bytes = (
+                len(disassembly.bytecode) // 2 + 0x200
+            )  # space for 16 32-byte arguments
+            global_state.mstate.constraints.append(
+                global_state.environment.calldata.size == no_of_bytes
+            )
+        else:
+            no_of_bytes = len(disassembly.bytecode) // 2
+        state.stack.append(no_of_bytes)
         return [global_state]
 
     @StateTransition(enable_gas=False)
@@ -1038,14 +1063,28 @@ def codecopy_(self, global_state: GlobalState) -> List[GlobalState]:
             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
+        ):
+            # Treat creation code after the expected disassembly as calldata.
+            # This is a slightly hacky way to ensure that symbolic constructor
+            # arguments work correctly.
+            offset = code_offset - len(global_state.environment.code.bytecode) // 2
+            log.warning("Doing hacky thing offset: {} size: {}".format(offset, size))
+            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]:

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,
             call_value=symbol_factory.BitVecSym(
                 "call_value{}".format(next_transaction_id), 256
             ),

mythril/laser/ethereum/transaction/transaction_models.py

@@ -201,6 +201,8 @@ def __init__(
             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,
@@ -212,7 +214,7 @@ def __init__(
             origin=origin,
             code=code,
             call_value=call_value,
-            init_call_data=False,
+            init_call_data=True,
         )
 
     def initial_global_state(self) -> GlobalState: