Implement codecopy concretization and add bytecodearray to environment

mythril/laser/ethereum/instructions.py

@@ -516,9 +516,34 @@ class Instruction:
 
     @instruction
     def codecopy_(self, global_state):
-        # FIXME: not implemented
-        state = global_state.mstate
-        start, s1, size = state.stack.pop(), state.stack.pop(), state.stack.pop()
+        memory_offset, code_offset, size = global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), global_state.mstate.stack.pop()
+
+        try:
+            concrete_memory_offset = helper.get_concrete_int(memory_offset)
+        except:
+            logging.debug("Unsupported symbolic memory offset in CODECOPY")
+            return [global_state]
+
+        try:
+            concrete_size = helper.get_concrete_int(size)
+        except:
+            logging.debug("Unsupported symbolic size in CODECOPY")
+            global_state.mstate.mem_extend(concrete_memory_offset, 1)
+            global_state.mstate.memory[concrete_memory_offset] = \
+                BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
+            return [global_state]
+
+        try:
+            concrete_code_offset = helper.get_concrete_int(code_offset)
+        except:
+            logging.debug("Unsupported symbolic code offset in CODECOPY")
+            global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
+            for i in range(concrete_size):
+                global_state.mstate.memory[concrete_memory_offset + i] = \
+                    BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
+            return [global_state]
+
+
         return [global_state]
 
     @instruction

mythril/laser/ethereum/state.py

@@ -66,7 +66,11 @@ class Environment:
         self.active_function_name = ""
 
         self.address = BitVecVal(int(active_account.address, 16), 256)
+
+        # Code contains the instruction models
         self.code = active_account.code
+        # Bytecode contains the actual bytes
+        self.bytecode = []
 
         self.sender = sender
         self.calldata = calldata
@@ -75,6 +79,7 @@ class Environment:
         self.origin = origin
         self.callvalue = callvalue
 
+
     def __str__(self):
         return str(self.as_dict)