diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index d5f201f73e..120f1ae575 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -1854,10 +1854,11 @@ static int __init make_gicv3_domU_node(struct kernel_info *kinfo)
 {
     void *fdt = kinfo->fdt;
     int res = 0;
-    __be32 reg[(GUEST_ROOT_ADDRESS_CELLS + GUEST_ROOT_SIZE_CELLS) * 2];
+    __be32 *reg;
     __be32 *cells;
     struct domain *d = kinfo->d;
     char buf[38];
+    unsigned int i, len = 0;
 
     snprintf(buf, sizeof(buf), "interrupt-controller@%"PRIx64,
              vgic_dist_base(&d->arch.vgic));
@@ -1881,27 +1882,42 @@ static int __init make_gicv3_domU_node(struct kernel_info *kinfo)
     if ( res )
         return res;
 
+    /* reg specifies all re-distributors and Distributor. */
+    len = (GUEST_ROOT_ADDRESS_CELLS + GUEST_ROOT_SIZE_CELLS) *
+          (vgic_rdist_nr(&d->arch.vgic) + 1) * sizeof(__be32);
+    reg = xmalloc_bytes(len);
+    if ( reg == NULL )
+        return -ENOMEM;
+
     cells = &reg[0];
     dt_child_set_range(&cells, GUEST_ROOT_ADDRESS_CELLS, GUEST_ROOT_SIZE_CELLS,
                        vgic_dist_base(&d->arch.vgic), GUEST_GICV3_GICD_SIZE);
-    dt_child_set_range(&cells, GUEST_ROOT_ADDRESS_CELLS, GUEST_ROOT_SIZE_CELLS,
-                       vgic_rdist_base(&d->arch.vgic, 0),
-                       vgic_rdist_size(&d->arch.vgic, 0));
+    for ( i = 0;
+          i < vgic_rdist_nr(&d->arch.vgic);
+          i++, cells += (GUEST_ROOT_ADDRESS_CELLS + GUEST_ROOT_SIZE_CELLS) )
+    {
+        dt_child_set_range(&cells,
+                           GUEST_ROOT_ADDRESS_CELLS, GUEST_ROOT_SIZE_CELLS,
+                           vgic_rdist_base(&d->arch.vgic, i),
+                           vgic_rdist_size(&d->arch.vgic, i));
+    }
 
-    res = fdt_property(fdt, "reg", reg, sizeof(reg));
+    res = fdt_property(fdt, "reg", reg, len);
     if (res)
-        return res;
+        goto out;
 
     res = fdt_property_cell(fdt, "linux,phandle", kinfo->phandle_gic);
     if (res)
-        return res;
+        goto out;
 
     res = fdt_property_cell(fdt, "phandle", kinfo->phandle_gic);
     if (res)
-        return res;
+        goto out;
 
     res = fdt_end_node(fdt);
 
+ out:
+    xfree(reg);
     return res;
 }
 
diff --git a/xen/arch/arm/vgic-v3.c b/xen/arch/arm/vgic-v3.c
index cb5a70c42e..83f996b46c 100644
--- a/xen/arch/arm/vgic-v3.c
+++ b/xen/arch/arm/vgic-v3.c
@@ -1647,8 +1647,8 @@ static inline unsigned int vgic_v3_max_rdist_count(struct domain *d)
      * However DomU get a constructed memory map, so we can go with
      * the architected single redistributor region.
      */
-    return is_hardware_domain(d) ? vgic_v3_hw.nr_rdist_regions :
-               GUEST_GICV3_RDIST_REGIONS;
+    return is_domain_direct_mapped(d) ? vgic_v3_hw.nr_rdist_regions :
+                                        GUEST_GICV3_RDIST_REGIONS;
 }
 
 static int vgic_v3_domain_init(struct domain *d)
@@ -1670,10 +1670,10 @@ static int vgic_v3_domain_init(struct domain *d)
     radix_tree_init(&d->arch.vgic.pend_lpi_tree);
 
     /*
-     * Domain 0 gets the hardware address.
-     * Guests get the virtual platform layout.
+     * 1:1 direct-map domain (including Dom0) gets the hardware address.
+     * Other guests get the virtual platform layout.
      */
-    if ( is_hardware_domain(d) )
+    if ( is_domain_direct_mapped(d) )
     {
         unsigned int first_cpu = 0;
 
diff --git a/xen/include/asm-arm/vgic.h b/xen/include/asm-arm/vgic.h
index 92f6a2d15d..0f7cb32c58 100644
--- a/xen/include/asm-arm/vgic.h
+++ b/xen/include/asm-arm/vgic.h
@@ -291,17 +291,17 @@ static inline paddr_t vgic_dist_base(struct vgic_dist *vgic)
 #ifdef CONFIG_GICV3
 static inline unsigned int vgic_rdist_nr(struct vgic_dist *vgic)
 {
-    return GUEST_GICV3_RDIST_REGIONS;
+    return vgic->nr_regions;
 }
 
 static inline paddr_t vgic_rdist_base(struct vgic_dist *vgic, unsigned int i)
 {
-    return GUEST_GICV3_GICR0_BASE;
+    return vgic->rdist_regions[i].base;
 }
 
 static inline paddr_t vgic_rdist_size(struct vgic_dist *vgic, unsigned int i)
 {
-    return GUEST_GICV3_GICR0_SIZE;
+    return vgic->rdist_regions[i].size;
 }
 #else
 static inline unsigned int vgic_rdist_nr(struct vgic_dist *vgic)
