diff --git a/xen/arch/arm/vgic-v2.c b/xen/arch/arm/vgic-v2.c
index dc9f95b..3e35a90 100644
--- a/xen/arch/arm/vgic-v2.c
+++ b/xen/arch/arm/vgic-v2.c
@@ -179,7 +179,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
     case VREG32(GICD_CTLR):
         if ( dabt.size != DABT_WORD ) goto bad_width;
         vgic_lock(v);
-        *r = vgic_reg32_extract(v->domain->arch.vgic.ctlr, info);
+        *r = vreg_reg32_extract(v->domain->arch.vgic.ctlr, info);
         vgic_unlock(v);
         return 1;
 
@@ -194,7 +194,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
             | DIV_ROUND_UP(v->domain->arch.vgic.nr_spis, 32);
         vgic_unlock(v);
 
-        *r = vgic_reg32_extract(typer, info);
+        *r = vreg_reg32_extract(typer, info);
 
         return 1;
     }
@@ -205,7 +205,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
          * XXX Do we need a JEP106 manufacturer ID?
          * Just use the physical h/w value for now
          */
-        *r = vgic_reg32_extract(0x0000043b, info);
+        *r = vreg_reg32_extract(0x0000043b, info);
         return 1;
 
     case VRANGE32(0x00C, 0x01C):
@@ -226,7 +226,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
         rank = vgic_rank_offset(v, 1, gicd_reg - GICD_ISENABLER, DABT_WORD);
         if ( rank == NULL) goto read_as_zero;
         vgic_lock_rank(v, rank, flags);
-        *r = vgic_reg32_extract(rank->ienable, info);
+        *r = vreg_reg32_extract(rank->ienable, info);
         vgic_unlock_rank(v, rank, flags);
         return 1;
 
@@ -235,7 +235,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
         rank = vgic_rank_offset(v, 1, gicd_reg - GICD_ICENABLER, DABT_WORD);
         if ( rank == NULL) goto read_as_zero;
         vgic_lock_rank(v, rank, flags);
-        *r = vgic_reg32_extract(rank->ienable, info);
+        *r = vreg_reg32_extract(rank->ienable, info);
         vgic_unlock_rank(v, rank, flags);
         return 1;
 
@@ -262,7 +262,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
                                                      gicd_reg - GICD_IPRIORITYR,
                                                      DABT_WORD)];
         vgic_unlock_rank(v, rank, flags);
-        *r = vgic_reg32_extract(ipriorityr, info);
+        *r = vreg_reg32_extract(ipriorityr, info);
 
         return 1;
     }
@@ -280,7 +280,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
         vgic_lock_rank(v, rank, flags);
         itargetsr = vgic_fetch_itargetsr(rank, gicd_reg - GICD_ITARGETSR);
         vgic_unlock_rank(v, rank, flags);
-        *r = vgic_reg32_extract(itargetsr, info);
+        *r = vreg_reg32_extract(itargetsr, info);
 
         return 1;
     }
@@ -299,7 +299,7 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
         icfgr = rank->icfg[REG_RANK_INDEX(2, gicd_reg - GICD_ICFGR, DABT_WORD)];
         vgic_unlock_rank(v, rank, flags);
 
-        *r = vgic_reg32_extract(icfgr, info);
+        *r = vreg_reg32_extract(icfgr, info);
 
         return 1;
     }
@@ -424,7 +424,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         if ( dabt.size != DABT_WORD ) goto bad_width;
         /* Ignore all but the enable bit */
         vgic_lock(v);
-        vgic_reg32_update(&v->domain->arch.vgic.ctlr, r, info);
+        vreg_reg32_update(&v->domain->arch.vgic.ctlr, r, info);
         v->domain->arch.vgic.ctlr &= GICD_CTL_ENABLE;
         vgic_unlock(v);
 
@@ -454,7 +454,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         if ( rank == NULL) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
         tr = rank->ienable;
-        vgic_reg32_setbits(&rank->ienable, r, info);
+        vreg_reg32_setbits(&rank->ienable, r, info);
         vgic_enable_irqs(v, (rank->ienable) & (~tr), rank->index);
         vgic_unlock_rank(v, rank, flags);
         return 1;
@@ -465,7 +465,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         if ( rank == NULL) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
         tr = rank->ienable;
-        vgic_reg32_clearbits(&rank->ienable, r, info);
+        vreg_reg32_clearbits(&rank->ienable, r, info);
         vgic_disable_irqs(v, (~rank->ienable) & tr, rank->index);
         vgic_unlock_rank(v, rank, flags);
         return 1;
@@ -508,7 +508,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         ipriorityr = &rank->ipriorityr[REG_RANK_INDEX(8,
                                                       gicd_reg - GICD_IPRIORITYR,
                                                       DABT_WORD)];
-        vgic_reg32_update(ipriorityr, r, info);
+        vreg_reg32_update(ipriorityr, r, info);
         vgic_unlock_rank(v, rank, flags);
         return 1;
     }
@@ -529,7 +529,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         if ( rank == NULL) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
         itargetsr = vgic_fetch_itargetsr(rank, gicd_reg - GICD_ITARGETSR);
-        vgic_reg32_update(&itargetsr, r, info);
+        vreg_reg32_update(&itargetsr, r, info);
         vgic_store_itargetsr(v->domain, rank, gicd_reg - GICD_ITARGETSR,
                              itargetsr);
         vgic_unlock_rank(v, rank, flags);
@@ -551,7 +551,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         rank = vgic_rank_offset(v, 2, gicd_reg - GICD_ICFGR, DABT_WORD);
         if ( rank == NULL) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
-        vgic_reg32_update(&rank->icfg[REG_RANK_INDEX(2, gicd_reg - GICD_ICFGR,
+        vreg_reg32_update(&rank->icfg[REG_RANK_INDEX(2, gicd_reg - GICD_ICFGR,
                                                      DABT_WORD)],
                           r, info);
         vgic_unlock_rank(v, rank, flags);
diff --git a/xen/arch/arm/vgic-v3.c b/xen/arch/arm/vgic-v3.c
index d10757a..e1213d9 100644
--- a/xen/arch/arm/vgic-v3.c
+++ b/xen/arch/arm/vgic-v3.c
@@ -181,7 +181,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
 
     case VREG32(GICR_IIDR):
         if ( dabt.size != DABT_WORD ) goto bad_width;
-        *r = vgic_reg32_extract(GICV3_GICR_IIDR_VAL, info);
+        *r = vreg_reg32_extract(GICV3_GICR_IIDR_VAL, info);
         return 1;
 
     case VREG64(GICR_TYPER):
@@ -199,7 +199,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
         if ( v->arch.vgic.flags & VGIC_V3_RDIST_LAST )
             typer |= GICR_TYPER_LAST;
 
-        *r = vgic_reg64_extract(typer, info);
+        *r = vreg_reg64_extract(typer, info);
 
         return 1;
     }
@@ -257,7 +257,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
     case VREG32(GICR_SYNCR):
         if ( dabt.size != DABT_WORD ) goto bad_width;
         /* RO . But when read it always returns busy bito bit[0] */
-        *r = vgic_reg32_extract(GICR_SYNCR_NOT_BUSY, info);
+        *r = vreg_reg32_extract(GICR_SYNCR_NOT_BUSY, info);
         return 1;
 
     case 0x00C8:
@@ -284,7 +284,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
 
     case VREG32(GICR_PIDR2):
         if ( dabt.size != DABT_WORD ) goto bad_width;
-        *r = vgic_reg32_extract(GICV3_GICR_PIDR2, info);
+        *r = vreg_reg32_extract(GICV3_GICR_PIDR2, info);
          return 1;
 
     case 0xFFEC ... 0xFFFC:
@@ -328,7 +328,7 @@ read_reserved:
     return 1;
 
 read_unknown:
-    *r = vgic_reg64_extract(0xdeadbeafdeadbeaf, info);
+    *r = vreg_reg64_extract(0xdeadbeafdeadbeaf, info);
     return 1;
 }
 
@@ -489,7 +489,7 @@ static int __vgic_v3_distr_common_mmio_read(const char *name, struct vcpu *v,
         rank = vgic_rank_offset(v, 1, reg - GICD_ISENABLER, DABT_WORD);
         if ( rank == NULL ) goto read_as_zero;
         vgic_lock_rank(v, rank, flags);
-        *r = vgic_reg32_extract(rank->ienable, info);
+        *r = vreg_reg32_extract(rank->ienable, info);
         vgic_unlock_rank(v, rank, flags);
         return 1;
 
@@ -498,7 +498,7 @@ static int __vgic_v3_distr_common_mmio_read(const char *name, struct vcpu *v,
         rank = vgic_rank_offset(v, 1, reg - GICD_ICENABLER, DABT_WORD);
         if ( rank == NULL ) goto read_as_zero;
         vgic_lock_rank(v, rank, flags);
-        *r = vgic_reg32_extract(rank->ienable, info);
+        *r = vreg_reg32_extract(rank->ienable, info);
         vgic_unlock_rank(v, rank, flags);
         return 1;
 
@@ -525,7 +525,7 @@ static int __vgic_v3_distr_common_mmio_read(const char *name, struct vcpu *v,
                                                      DABT_WORD)];
         vgic_unlock_rank(v, rank, flags);
 
-        *r = vgic_reg32_extract(ipriorityr, info);
+        *r = vreg_reg32_extract(ipriorityr, info);
 
         return 1;
     }
@@ -541,7 +541,7 @@ static int __vgic_v3_distr_common_mmio_read(const char *name, struct vcpu *v,
         icfgr = rank->icfg[REG_RANK_INDEX(2, reg - GICD_ICFGR, DABT_WORD)];
         vgic_unlock_rank(v, rank, flags);
 
-        *r = vgic_reg32_extract(icfgr, info);
+        *r = vreg_reg32_extract(icfgr, info);
 
         return 1;
     }
@@ -585,7 +585,7 @@ static int __vgic_v3_distr_common_mmio_write(const char *name, struct vcpu *v,
         if ( rank == NULL ) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
         tr = rank->ienable;
-        vgic_reg32_setbits(&rank->ienable, r, info);
+        vreg_reg32_setbits(&rank->ienable, r, info);
         vgic_enable_irqs(v, (rank->ienable) & (~tr), rank->index);
         vgic_unlock_rank(v, rank, flags);
         return 1;
@@ -596,7 +596,7 @@ static int __vgic_v3_distr_common_mmio_write(const char *name, struct vcpu *v,
         if ( rank == NULL ) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
         tr = rank->ienable;
-        vgic_reg32_clearbits(&rank->ienable, r, info);
+        vreg_reg32_clearbits(&rank->ienable, r, info);
         vgic_disable_irqs(v, (~rank->ienable) & tr, rank->index);
         vgic_unlock_rank(v, rank, flags);
         return 1;
@@ -638,7 +638,7 @@ static int __vgic_v3_distr_common_mmio_write(const char *name, struct vcpu *v,
         vgic_lock_rank(v, rank, flags);
         ipriorityr = &rank->ipriorityr[REG_RANK_INDEX(8, reg - GICD_IPRIORITYR,
                                                       DABT_WORD)];
-        vgic_reg32_update(ipriorityr, r, info);
+        vreg_reg32_update(ipriorityr, r, info);
         vgic_unlock_rank(v, rank, flags);
         return 1;
     }
@@ -653,7 +653,7 @@ static int __vgic_v3_distr_common_mmio_write(const char *name, struct vcpu *v,
         rank = vgic_rank_offset(v, 2, reg - GICD_ICFGR, DABT_WORD);
         if ( rank == NULL ) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
-        vgic_reg32_update(&rank->icfg[REG_RANK_INDEX(2, reg - GICD_ICFGR,
+        vreg_reg32_update(&rank->icfg[REG_RANK_INDEX(2, reg - GICD_ICFGR,
                                                      DABT_WORD)],
                           r, info);
         vgic_unlock_rank(v, rank, flags);
@@ -901,7 +901,7 @@ static int vgic_v3_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
     case VREG32(GICD_CTLR):
         if ( dabt.size != DABT_WORD ) goto bad_width;
         vgic_lock(v);
-        *r = vgic_reg32_extract(v->domain->arch.vgic.ctlr, info);
+        *r = vreg_reg32_extract(v->domain->arch.vgic.ctlr, info);
         vgic_unlock(v);
         return 1;
 
@@ -926,14 +926,14 @@ static int vgic_v3_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
 
         typer |= (irq_bits - 1) << GICD_TYPE_ID_BITS_SHIFT;
 
-        *r = vgic_reg32_extract(typer, info);
+        *r = vreg_reg32_extract(typer, info);
 
         return 1;
     }
 
     case VREG32(GICD_IIDR):
         if ( dabt.size != DABT_WORD ) goto bad_width;
-        *r = vgic_reg32_extract(GICV3_GICD_IIDR_VAL, info);
+        *r = vreg_reg32_extract(GICV3_GICD_IIDR_VAL, info);
         return 1;
 
     case VREG32(0x000C):
@@ -1026,7 +1026,7 @@ static int vgic_v3_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
         irouter = vgic_fetch_irouter(rank, gicd_reg - GICD_IROUTER);
         vgic_unlock_rank(v, rank, flags);
 
-        *r = vgic_reg64_extract(irouter, info);
+        *r = vreg_reg64_extract(irouter, info);
 
         return 1;
     }
@@ -1044,7 +1044,7 @@ static int vgic_v3_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
     case VREG32(GICD_PIDR2):
         /* GICv3 identification value */
         if ( dabt.size != DABT_WORD ) goto bad_width;
-        *r = vgic_reg32_extract(GICV3_GICD_PIDR2, info);
+        *r = vreg_reg32_extract(GICV3_GICD_PIDR2, info);
         return 1;
 
     case VRANGE32(0xFFEC, 0xFFFC):
@@ -1107,7 +1107,7 @@ static int vgic_v3_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
 
         vgic_lock(v);
 
-        vgic_reg32_update(&ctlr, r, info);
+        vreg_reg32_update(&ctlr, r, info);
 
         /* Only EnableGrp1A can be changed */
         if ( ctlr & GICD_CTLR_ENABLE_G1A )
@@ -1213,7 +1213,7 @@ static int vgic_v3_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         if ( rank == NULL ) goto write_ignore;
         vgic_lock_rank(v, rank, flags);
         irouter = vgic_fetch_irouter(rank, gicd_reg - GICD_IROUTER);
-        vgic_reg64_update(&irouter, r, info);
+        vreg_reg64_update(&irouter, r, info);
         vgic_store_irouter(v->domain, rank, gicd_reg - GICD_IROUTER, irouter);
         vgic_unlock_rank(v, rank, flags);
         return 1;
diff --git a/xen/include/asm-arm/vreg.h b/xen/include/asm-arm/vreg.h
index 348584f..16207ce 100644
--- a/xen/include/asm-arm/vreg.h
+++ b/xen/include/asm-arm/vreg.h
@@ -107,102 +107,102 @@ static inline bool vreg_emulate_sysreg64(struct cpu_user_regs *regs, union hsr h
 
 #endif
 
-#define VGIC_REG_MASK(size) ((~0UL) >> (BITS_PER_LONG - ((1 << (size)) * 8)))
+#define VREG_REG_MASK(size) ((~0UL) >> (BITS_PER_LONG - ((1 << (size)) * 8)))
 
 /*
  * The check on the size supported by the register has to be done by
- * the caller of vgic_regN_*.
+ * the caller of vreg_regN_*.
  *
- * vgic_reg_* should never be called directly. Instead use the vgic_regN_*
+ * vreg_reg_* should never be called directly. Instead use the vreg_regN_*
  * according to size of the emulated register
  *
  * Note that the alignment fault will always be taken in the guest
  * (see B3.12.7 DDI0406.b).
  */
-static inline register_t vgic_reg_extract(unsigned long reg,
+static inline register_t vreg_reg_extract(unsigned long reg,
                                           unsigned int offset,
                                           enum dabt_size size)
 {
     reg >>= 8 * offset;
-    reg &= VGIC_REG_MASK(size);
+    reg &= VREG_REG_MASK(size);
 
     return reg;
 }
 
-static inline void vgic_reg_update(unsigned long *reg, register_t val,
+static inline void vreg_reg_update(unsigned long *reg, register_t val,
                                    unsigned int offset,
                                    enum dabt_size size)
 {
-    unsigned long mask = VGIC_REG_MASK(size);
+    unsigned long mask = VREG_REG_MASK(size);
     int shift = offset * 8;
 
     *reg &= ~(mask << shift);
     *reg |= ((unsigned long)val & mask) << shift;
 }
 
-static inline void vgic_reg_setbits(unsigned long *reg, register_t bits,
+static inline void vreg_reg_setbits(unsigned long *reg, register_t bits,
                                     unsigned int offset,
                                     enum dabt_size size)
 {
-    unsigned long mask = VGIC_REG_MASK(size);
+    unsigned long mask = VREG_REG_MASK(size);
     int shift = offset * 8;
 
     *reg |= ((unsigned long)bits & mask) << shift;
 }
 
-static inline void vgic_reg_clearbits(unsigned long *reg, register_t bits,
+static inline void vreg_reg_clearbits(unsigned long *reg, register_t bits,
                                       unsigned int offset,
                                       enum dabt_size size)
 {
-    unsigned long mask = VGIC_REG_MASK(size);
+    unsigned long mask = VREG_REG_MASK(size);
     int shift = offset * 8;
 
     *reg &= ~(((unsigned long)bits & mask) << shift);
 }
 
-/* N-bit register helpers */
-#define VGIC_REG_HELPERS(sz, offmask)                                   \
-static inline register_t vgic_reg##sz##_extract(uint##sz##_t reg,       \
-                                                const mmio_info_t *info)\
-{                                                                       \
-    return vgic_reg_extract(reg, info->gpa & offmask,                   \
-                            info->dabt.size);                           \
-}                                                                       \
-                                                                        \
-static inline void vgic_reg##sz##_update(uint##sz##_t *reg,             \
-                                         register_t val,                \
-                                         const mmio_info_t *info)       \
-{                                                                       \
-    unsigned long tmp = *reg;                                           \
-                                                                        \
-    vgic_reg_update(&tmp, val, info->gpa & offmask,                     \
-                    info->dabt.size);                                   \
-                                                                        \
-    *reg = tmp;                                                         \
-}                                                                       \
-                                                                        \
-static inline void vgic_reg##sz##_setbits(uint##sz##_t *reg,            \
-                                          register_t bits,              \
-                                          const mmio_info_t *info)      \
-{                                                                       \
-    unsigned long tmp = *reg;                                           \
-                                                                        \
-    vgic_reg_setbits(&tmp, bits, info->gpa & offmask,                   \
-                     info->dabt.size);                                  \
-                                                                        \
-    *reg = tmp;                                                         \
-}                                                                       \
-                                                                        \
-static inline void vgic_reg##sz##_clearbits(uint##sz##_t *reg,          \
-                                            register_t bits,            \
-                                            const mmio_info_t *info)    \
-{                                                                       \
-    unsigned long tmp = *reg;                                           \
-                                                                        \
-    vgic_reg_clearbits(&tmp, bits, info->gpa & offmask,                 \
-                       info->dabt.size);                                \
-                                                                        \
-    *reg = tmp;                                                         \
+#define VREG_REG_HELPERS(sz, offmask)                                           \
+/* N-bit register helpers */                                                    \
+static inline register_t vreg_reg##sz##_extract(uint##sz##_t reg,               \
+                                                  const mmio_info_t *info)      \
+{                                                                               \
+    return vreg_reg_extract(reg, info->gpa & offmask,                           \
+                            info->dabt.size);                                   \
+}                                                                               \
+                                                                                \
+static inline void vreg_reg##sz##_update(uint##sz##_t *reg,                     \
+                                           register_t val,                      \
+                                           const mmio_info_t *info)             \
+{                                                                               \
+    unsigned long tmp = *reg;                                                   \
+                                                                                \
+    vreg_reg_update(&tmp, val, info->gpa & offmask,                             \
+                    info->dabt.size);                                           \
+                                                                                \
+    *reg = tmp;                                                                 \
+}                                                                               \
+                                                                                \
+static inline void vreg_reg##sz##_setbits(uint##sz##_t *reg,                    \
+                                            register_t bits,                    \
+                                            const mmio_info_t *info)            \
+{                                                                               \
+    unsigned long tmp = *reg;                                                   \
+                                                                                \
+    vreg_reg_setbits(&tmp, bits, info->gpa & offmask,                           \
+                     info->dabt.size);                                          \
+                                                                                \
+    *reg = tmp;                                                                 \
+}                                                                               \
+                                                                                \
+static inline void vreg_reg##sz##_clearbits(uint##sz##_t *reg,                  \
+                                              register_t bits,                  \
+                                              const mmio_info_t *info)          \
+{                                                                               \
+    unsigned long tmp = *reg;                                                   \
+                                                                                \
+    vreg_reg_clearbits(&tmp, bits, info->gpa & offmask,                         \
+                       info->dabt.size);                                        \
+                                                                                \
+    *reg = tmp;                                                                 \
 }
 
 /*
@@ -211,10 +211,9 @@ static inline void vgic_reg##sz##_clearbits(uint##sz##_t *reg,          \
  * unsigned long rather than uint64_t
  */
 #if BITS_PER_LONG == 64
-VGIC_REG_HELPERS(64, 0x7);
+VREG_REG_HELPERS(64, 0x7);
 #endif
-VGIC_REG_HELPERS(32, 0x3);
-
-#undef VGIC_REG_HELPERS
+VREG_REG_HELPERS(32, 0x3);
+#undef VREG_REG_HELPERS
 
 #endif /* __ASM_ARM_VREG__ */
