diff --git a/core/arch/arm/kernel/user_ta.c b/core/arch/arm/kernel/user_ta.c
index 050f423..1c6db3b 100644
--- a/core/arch/arm/kernel/user_ta.c
+++ b/core/arch/arm/kernel/user_ta.c
@@ -16,6 +16,7 @@
 #include <kernel/tee_misc.h>
 #include <kernel/tee_ta_manager.h>
 #include <kernel/thread.h>
+#include <kernel/user_mode_ctx.h>
 #include <kernel/user_ta.h>
 #include <kernel/user_ta_store.h>
 #include <ldelf.h>
@@ -303,23 +304,7 @@
 
 static void dump_state_no_ldelf_dbg(struct user_ta_ctx *utc)
 {
-	struct vm_region *r;
-	char flags[7] = { '\0', };
-	size_t n = 0;
-
-	TAILQ_FOREACH(r, &utc->uctx.vm_info.regions, link) {
-		paddr_t pa = 0;
-
-		if (r->mobj)
-			mobj_get_pa(r->mobj, r->offset, 0, &pa);
-
-		mattr_perm_to_str(flags, sizeof(flags), r->attr);
-		EMSG_RAW(" region %2zu: va 0x%0*" PRIxVA " pa 0x%0*" PRIxPA
-			 " size 0x%06zx flags %s",
-			 n, PRIxVA_WIDTH, r->va, PRIxPA_WIDTH, pa, r->size,
-			 flags);
-		n++;
-	}
+	user_mode_ctx_print_mappings(&utc->uctx);
 }
 
 static TEE_Result dump_state_ldelf_dbg(struct user_ta_ctx *utc)
diff --git a/core/include/kernel/user_mode_ctx.h b/core/include/kernel/user_mode_ctx.h
index 5480db4..59e2e33 100644
--- a/core/include/kernel/user_mode_ctx.h
+++ b/core/include/kernel/user_mode_ctx.h
@@ -21,4 +21,7 @@
 	assert(is_user_mode_ctx(ctx));
 	return container_of(ctx, struct user_mode_ctx, ctx);
 }
+
+void user_mode_ctx_print_mappings(struct user_mode_ctx *umctx);
+
 #endif /*__KERNEL_USER_MODE_CTX_H*/
diff --git a/core/kernel/sub.mk b/core/kernel/sub.mk
index 2841bd3..55319a3 100644
--- a/core/kernel/sub.mk
+++ b/core/kernel/sub.mk
@@ -16,3 +16,4 @@
 srcs-y += scattered_array.c
 srcs-y += huk_subkey.c
 srcs-$(CFG_SHOW_CONF_ON_BOOT) += show_conf.c
+srcs-y += user_mode_ctx.c
diff --git a/core/kernel/user_mode_ctx.c b/core/kernel/user_mode_ctx.c
new file mode 100644
index 0000000..12906f3
--- /dev/null
+++ b/core/kernel/user_mode_ctx.c
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: BSD-2-Clause
+/*
+ * Copyright (c) 2019, Linaro Limited
+ */
+
+#include <kernel/user_mode_ctx.h>
+#include <trace.h>
+#include <mm/mobj.h>
+
+void user_mode_ctx_print_mappings(struct user_mode_ctx *uctx)
+{
+	struct vm_region *r = NULL;
+	char flags[7] = { '\0', };
+	size_t n = 0;
+
+	TAILQ_FOREACH(r, &uctx->vm_info.regions, link) {
+		paddr_t pa = 0;
+
+		if (r->mobj)
+			mobj_get_pa(r->mobj, r->offset, 0, &pa);
+
+		mattr_perm_to_str(flags, sizeof(flags), r->attr);
+		EMSG_RAW(" region %2zu: va 0x%0*" PRIxVA " pa 0x%0*" PRIxPA
+			 " size 0x%06zx flags %s",
+			 n, PRIxVA_WIDTH, r->va, PRIxPA_WIDTH, pa, r->size,
+			 flags);
+		n++;
+	}
+}