diff --git a/include/plat/exynos4/plat/machine/devices.h b/include/plat/exynos4/plat/machine/devices.h
index 930e90cfac3dfbe01a0d7cf6a1eb09ac7ded979f..56dc15c1081759088dee733d26cf145ad85c1063 100644
--- a/include/plat/exynos4/plat/machine/devices.h
+++ b/include/plat/exynos4/plat/machine/devices.h
@@ -12,7 +12,7 @@
#define __PLAT_MACHINE_DEVICES_H
/* These devices are used by the seL4 kernel. */
-#define UART1_PPTR 0xfff01000
+#define UART_PPTR 0xfff01000
#define MCT_PPTR 0xfff02000
#define L2CC_PPTR 0xfff03000
#define GIC_CONTROLLER_PPTR 0xfff04000
diff --git a/include/plat/exynos4/plat/machine/io.h b/include/plat/exynos4/plat/machine/io.h
index 3d8a539a6745abaa44cddd635c518e2f1efe98fa..b95d1b64ce6d8823a434587773b385cb0fe801cf 100644
--- a/include/plat/exynos4/plat/machine/io.h
+++ b/include/plat/exynos4/plat/machine/io.h
@@ -14,11 +14,11 @@
#include <types.h>
#ifdef DEBUG
-void exynos4_uart_putchar(char c);
+void exynos_uart_putchar(char c);
void putDebugChar(unsigned char c);
unsigned char getDebugChar(void);
-#define kernel_putchar(c) exynos4_uart_putchar(c)
+#define kernel_putchar(c) exynos_uart_putchar(c)
#else /* !DEBUG */
#define kernel_putchar(c) ((void)(0))
#endif /* DEBUG */
diff --git a/include/plat/exynos5/plat/machine/io.h b/include/plat/exynos5/plat/machine/io.h
index 7ecfefa7eb83687230cb21ea022f55115645e06a..b95d1b64ce6d8823a434587773b385cb0fe801cf 100644
--- a/include/plat/exynos5/plat/machine/io.h
+++ b/include/plat/exynos5/plat/machine/io.h
@@ -14,11 +14,11 @@
#include <types.h>
#ifdef DEBUG
-void exynos5_uart_putchar(char c);
+void exynos_uart_putchar(char c);
void putDebugChar(unsigned char c);
unsigned char getDebugChar(void);
-#define kernel_putchar(c) exynos5_uart_putchar(c)
+#define kernel_putchar(c) exynos_uart_putchar(c)
#else /* !DEBUG */
#define kernel_putchar(c) ((void)(0))
#endif /* DEBUG */
diff --git a/src/plat/exynos4/machine/Makefile b/src/plat/exynos4/machine/Makefile
index f8bb661840d57daa7140cae325280fe7ff58cc8f..85384f1e56eea008775320755094bb0f09446702 100644
--- a/src/plat/exynos4/machine/Makefile
+++ b/src/plat/exynos4/machine/Makefile
@@ -15,5 +15,5 @@ PLAT_C_SOURCES += machine/hardware.c
PLAT_C_SOURCES += ../exynos_common/mct.c
ifdef DEBUG
- PLAT_C_SOURCES += machine/io.c
+ PLAT_C_SOURCES += ../exynos_common/io.c
endif
diff --git a/src/plat/exynos4/machine/hardware.c b/src/plat/exynos4/machine/hardware.c
index b7391167e443c651fb2071e27f72cba42e1b93b5..619ccba8b7f276f3a559735f1d1f5ed97dfb7d28 100644
--- a/src/plat/exynos4/machine/hardware.c
+++ b/src/plat/exynos4/machine/hardware.c
@@ -279,7 +279,7 @@ map_kernel_devices(void)
/* map kernel device: UART */
map_kernel_frame(
UART1_PADDR,
- UART1_PPTR,
+ UART_PPTR,
VMKernelOnly,
vm_attributes_new(
false, /* armExecuteNever */
diff --git a/src/plat/exynos4/machine/io.c b/src/plat/exynos4/machine/io.c
deleted file mode 100644
index 50a82fe4b74d53013455d81e52fceb3f90efc3ee..0000000000000000000000000000000000000000
--- a/src/plat/exynos4/machine/io.c
+++ /dev/null
@@ -1,72 +0,0 @@
-/*
- * Copyright 2014, General Dynamics C4 Systems
- *
- * This software may be distributed and modified according to the terms of
- * the GNU General Public License version 2. Note that NO WARRANTY is provided.
- * See "LICENSE_GPLv2.txt" for details.
- *
- * @TAG(GD_GPL)
- */
-
-#include <stdint.h>
-#include <util.h>
-#include <machine/io.h>
-#include <plat/machine/devices.h>
-
-#ifdef DEBUG
-
-#define ULCON 0x0000 /* line control */
-#define UCON 0x0004 /* control */
-#define UFCON 0x0008 /* fifo control */
-#define UMCON 0x000C /* modem control */
-#define UTRSTAT 0x0010 /* TX/RX status */
-#define UERSTAT 0x0014 /* RX error status */
-#define UFSTAT 0x0018 /* FIFO status */
-#define UMSTAT 0x001C /* modem status */
-#define UTXH 0x0020 /* TX buffer */
-#define URXH 0x0024 /* RX buffer */
-#define UBRDIV 0x0028 /* baud rate divisor */
-#define UFRACVAL 0x002C /* divisor fractional value */
-#define UINTP 0x0030 /* interrupt pending */
-#define UINTSP 0x0034 /* interrupt source pending */
-#define UINTM 0x0038 /* interrupt mask */
-
-#define UART_REG(X) ((volatile uint32_t *)(UART1_PPTR + (X)))
-
-/* ULCON */
-#define WORD_LENGTH_8 (3<<0)
-
-/* UTRSTAT */
-#define TX_EMPTY (1<<2)
-#define TXBUF_EMPTY (1<<1)
-#define RXBUF_READY (1<<0)
-
-
-void
-exynos4_uart_putchar(char c)
-{
- putDebugChar(c);
- if (c == '\n') {
- putDebugChar('\r');
- }
-}
-
-void
-putDebugChar(unsigned char c)
-{
- while ( (*UART_REG(UTRSTAT) & TXBUF_EMPTY) == 0 );
- *UART_REG(UTXH) = (c & 0xff);
-}
-
-unsigned char
-getDebugChar(void)
-{
- if ( (*UART_REG(UTRSTAT) & RXBUF_READY)) {
- return (unsigned char) * UART_REG(URXH);
- } else {
- return -1;
- }
-}
-
-
-#endif /* DEBUG */
diff --git a/src/plat/exynos5/machine/Makefile b/src/plat/exynos5/machine/Makefile
index 83051690112e212226ce90294b41ead9682b79f1..1f385e56545cef44b9e00836d816e77cb8f548fd 100644
--- a/src/plat/exynos5/machine/Makefile
+++ b/src/plat/exynos5/machine/Makefile
@@ -16,5 +16,5 @@ PLAT_C_SOURCES += machine/hardware.c \
PLAT_C_SOURCES += ../exynos_common/mct.c
ifdef DEBUG
- PLAT_C_SOURCES += machine/io.c
+ PLAT_C_SOURCES += ../exynos_common/io.c
endif
diff --git a/src/plat/exynos5/machine/io.c b/src/plat/exynos_common/io.c
similarity index 87%
rename from src/plat/exynos5/machine/io.c
rename to src/plat/exynos_common/io.c
index 7b06d4fc3ee121ae948ca6bde2025936f1163b6c..91dc7b9b66c7f32fd0db95c8695ab6613e929041 100644
--- a/src/plat/exynos5/machine/io.c
+++ b/src/plat/exynos_common/io.c
@@ -31,20 +31,16 @@
#define UINTSP 0x0034 /* interrupt source pending */
#define UINTM 0x0038 /* interrupt mask */
-//#define UART_REG(X) ((volatile uint32_t *)(UART2_PADDR + (X)))
#define UART_REG(X) ((volatile uint32_t *)(UART_PPTR + (X)))
-/* ULCON */
-#define WORD_LENGTH_8 (3<<0)
-
/* UTRSTAT */
-#define TX_EMPTY (1<<2)
-#define TXBUF_EMPTY (1<<1)
-#define RXBUF_READY (1<<0)
+#define TX_EMPTY BIT(2)
+#define TXBUF_EMPTY BIT(1)
+#define RXBUF_READY BIT(0)
void
-exynos5_uart_putchar(char c)
+exynos_uart_putchar(char c)
{
putDebugChar(c);
if (c == '\n') {