From 124f5affcc3e9c2be694b46d47837d16846f63ca Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 14 Feb 2019 00:06:46 +0530
Subject: [PATCH] Fix the codecopy issue

---
 mythril/laser/ethereum/instructions.py | 40 +++++++++++++++++++-------
 1 file changed, 30 insertions(+), 10 deletions(-)

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):