diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index 213ad017dc..d5f201f73e 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -1802,8 +1802,12 @@ static int __init make_gicv2_domU_node(struct kernel_info *kinfo)
     int res = 0;
     __be32 reg[(GUEST_ROOT_ADDRESS_CELLS + GUEST_ROOT_SIZE_CELLS) * 2];
     __be32 *cells;
+    struct domain *d = kinfo->d;
+    char buf[38];
 
-    res = fdt_begin_node(fdt, "interrupt-controller@"__stringify(GUEST_GICD_BASE));
+    snprintf(buf, sizeof(buf), "interrupt-controller@%"PRIx64,
+             vgic_dist_base(&d->arch.vgic));
+    res = fdt_begin_node(fdt, buf);
     if ( res )
         return res;
 
@@ -1825,9 +1829,9 @@ static int __init make_gicv2_domU_node(struct kernel_info *kinfo)
 
     cells = &reg[0];
     dt_child_set_range(&cells, GUEST_ROOT_ADDRESS_CELLS, GUEST_ROOT_SIZE_CELLS,
-                       GUEST_GICD_BASE, GUEST_GICD_SIZE);
+                       vgic_dist_base(&d->arch.vgic), GUEST_GICD_SIZE);
     dt_child_set_range(&cells, GUEST_ROOT_ADDRESS_CELLS, GUEST_ROOT_SIZE_CELLS,
-                       GUEST_GICC_BASE, GUEST_GICC_SIZE);
+                       vgic_cpu_base(&d->arch.vgic), GUEST_GICC_SIZE);
 
     res = fdt_property(fdt, "reg", reg, sizeof(reg));
     if (res)
@@ -1852,8 +1856,12 @@ static int __init make_gicv3_domU_node(struct kernel_info *kinfo)
     int res = 0;
     __be32 reg[(GUEST_ROOT_ADDRESS_CELLS + GUEST_ROOT_SIZE_CELLS) * 2];
     __be32 *cells;
+    struct domain *d = kinfo->d;
+    char buf[38];
 
-    res = fdt_begin_node(fdt, "interrupt-controller@"__stringify(GUEST_GICV3_GICD_BASE));
+    snprintf(buf, sizeof(buf), "interrupt-controller@%"PRIx64,
+             vgic_dist_base(&d->arch.vgic));
+    res = fdt_begin_node(fdt, buf);
     if ( res )
         return res;
 
@@ -1875,9 +1883,10 @@ static int __init make_gicv3_domU_node(struct kernel_info *kinfo)
 
     cells = &reg[0];
     dt_child_set_range(&cells, GUEST_ROOT_ADDRESS_CELLS, GUEST_ROOT_SIZE_CELLS,
-                       GUEST_GICV3_GICD_BASE, GUEST_GICV3_GICD_SIZE);
+                       vgic_dist_base(&d->arch.vgic), GUEST_GICV3_GICD_SIZE);
     dt_child_set_range(&cells, GUEST_ROOT_ADDRESS_CELLS, GUEST_ROOT_SIZE_CELLS,
-                       GUEST_GICV3_GICR0_BASE, GUEST_GICV3_GICR0_SIZE);
+                       vgic_rdist_base(&d->arch.vgic, 0),
+                       vgic_rdist_size(&d->arch.vgic, 0));
 
     res = fdt_property(fdt, "reg", reg, sizeof(reg));
     if (res)
diff --git a/xen/include/asm-arm/new_vgic.h b/xen/include/asm-arm/new_vgic.h
index 97d622bff6..9097522b27 100644
--- a/xen/include/asm-arm/new_vgic.h
+++ b/xen/include/asm-arm/new_vgic.h
@@ -186,6 +186,30 @@ struct vgic_cpu {
     uint32_t num_id_bits;
 };
 
+static inline paddr_t vgic_cpu_base(struct vgic_dist *vgic)
+{
+    return GUEST_GICC_BASE;
+}
+
+static inline paddr_t vgic_dist_base(struct vgic_dist *vgic)
+{
+    return GUEST_GICD_BASE;
+}
+
+static inline unsigned int vgic_rdist_nr(struct vgic_dist *vgic)
+{
+    return 0;
+}
+
+static inline paddr_t vgic_rdist_base(struct vgic_dist *vgic, unsigned int i)
+{
+    return INVALID_PADDR;
+}
+
+static inline paddr_t vgic_rdist_size(struct vgic_dist *vgic, unsigned int i)
+{
+    return 0;
+}
 #endif /* __ASM_ARM_NEW_VGIC_H */
 
 /*
diff --git a/xen/include/asm-arm/vgic.h b/xen/include/asm-arm/vgic.h
index 62c2ae538d..e1bc5113da 100644
--- a/xen/include/asm-arm/vgic.h
+++ b/xen/include/asm-arm/vgic.h
@@ -277,6 +277,47 @@ enum gic_sgi_mode;
  */
 #define REG_RANK_INDEX(b, n, s) ((((n) >> s) & ((b)-1)) % 32)
 
+static inline paddr_t vgic_cpu_base(struct vgic_dist *vgic)
+{
+    return GUEST_GICC_BASE;
+}
+
+static inline paddr_t vgic_dist_base(struct vgic_dist *vgic)
+{
+    return GUEST_GICD_BASE;
+}
+
+#ifdef CONFIG_GICV3
+static inline unsigned int vgic_rdist_nr(struct vgic_dist *vgic)
+{
+    return GUEST_GICV3_RDIST_REGIONS;
+}
+
+static inline paddr_t vgic_rdist_base(struct vgic_dist *vgic, unsigned int i)
+{
+    return GUEST_GICV3_GICR0_BASE;
+}
+
+static inline paddr_t vgic_rdist_size(struct vgic_dist *vgic, unsigned int i)
+{
+    return GUEST_GICV3_GICR0_SIZE;
+}
+#else
+static inline unsigned int vgic_rdist_nr(struct vgic_dist *vgic)
+{
+    return 0;
+}
+
+static inline paddr_t vgic_rdist_base(struct vgic_dist *vgic, unsigned int i)
+{
+    return INVALID_PADDR;
+}
+
+static inline paddr_t vgic_rdist_size(struct vgic_dist *vgic, unsigned int i)
+{
+    return INVALID_PADDR;
+}
+#endif
 
 extern struct vcpu *vgic_get_target_vcpu(struct vcpu *v, unsigned int virq);
 extern void vgic_remove_irq_from_queues(struct vcpu *v, struct pending_irq *p);
