diff --git a/xen/arch/arm/vgic-v2.c b/xen/arch/arm/vgic-v2.c
index eb5f354..cf4ab89 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,
         vgic_lock_rank(v, rank, flags);
         ipriorityr = ACCESS_ONCE(rank->ipriorityr[rank_index]);
         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;
@@ -509,7 +509,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
                                                       gicd_reg - GICD_IPRIORITYR,
                                                       DABT_WORD)];
         priority = ACCESS_ONCE(*ipriorityr);
-        vgic_reg32_update(&priority, r, info);
+        vreg_reg32_update(&priority, r, info);
         ACCESS_ONCE(*ipriorityr) = priority;
 
         vgic_unlock_rank(v, rank, flags);
@@ -532,7 +532,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);
@@ -554,7 +554,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-its.c b/xen/arch/arm/vgic-v3-its.c
index bfc5acc..9ef792f 100644
--- a/xen/arch/arm/vgic-v3-its.c
+++ b/xen/arch/arm/vgic-v3-its.c
@@ -1015,13 +1015,13 @@ static int vgic_v3_its_mmio_read(struct vcpu *v, mmio_info_t *info,
         if ( have_cmd_lock )
             spin_unlock(&its->vcmd_lock);
 
-        *r = vgic_reg32_extract(reg, info);
+        *r = vreg_reg32_extract(reg, info);
         break;
     }
 
     case VREG32(GITS_IIDR):
         if ( info->dabt.size != DABT_WORD ) goto bad_width;
-        *r = vgic_reg32_extract(GITS_IIDR_VALUE, info);
+        *r = vreg_reg32_extract(GITS_IIDR_VALUE, info);
         break;
 
     case VREG64(GITS_TYPER):
@@ -1031,7 +1031,7 @@ static int vgic_v3_its_mmio_read(struct vcpu *v, mmio_info_t *info,
         reg |= (sizeof(struct vits_itte) - 1) << GITS_TYPER_ITT_SIZE_SHIFT;
         reg |= (its->evid_bits - 1) << GITS_TYPER_IDBITS_SHIFT;
         reg |= (its->devid_bits - 1) << GITS_TYPER_DEVIDS_SHIFT;
-        *r = vgic_reg64_extract(reg, info);
+        *r = vreg_reg64_extract(reg, info);
         break;
 
     case VRANGE32(0x0018, 0x001C):
@@ -1044,7 +1044,7 @@ static int vgic_v3_its_mmio_read(struct vcpu *v, mmio_info_t *info,
     case VREG64(GITS_CBASER):
         if ( !vgic_reg64_check_access(info->dabt) ) goto bad_width;
         spin_lock(&its->its_lock);
-        *r = vgic_reg64_extract(its->cbaser, info);
+        *r = vreg_reg64_extract(its->cbaser, info);
         spin_unlock(&its->its_lock);
         break;
 
@@ -1053,7 +1053,7 @@ static int vgic_v3_its_mmio_read(struct vcpu *v, mmio_info_t *info,
 
         /* CWRITER is only written by the guest, so no extra locking here. */
         reg = its->cwriter;
-        *r = vgic_reg64_extract(reg, info);
+        *r = vreg_reg64_extract(reg, info);
         break;
 
     case VREG64(GITS_CREADR):
@@ -1066,7 +1066,7 @@ static int vgic_v3_its_mmio_read(struct vcpu *v, mmio_info_t *info,
          * progress.
          */
         reg = read_u64_atomic(&its->creadr);
-        *r = vgic_reg64_extract(reg, info);
+        *r = vreg_reg64_extract(reg, info);
         break;
 
     case VRANGE64(0x0098, 0x00F8):
@@ -1075,14 +1075,14 @@ static int vgic_v3_its_mmio_read(struct vcpu *v, mmio_info_t *info,
     case VREG64(GITS_BASER0):           /* device table */
         if ( !vgic_reg64_check_access(info->dabt) ) goto bad_width;
         spin_lock(&its->its_lock);
-        *r = vgic_reg64_extract(its->baser_dev, info);
+        *r = vreg_reg64_extract(its->baser_dev, info);
         spin_unlock(&its->its_lock);
         break;
 
     case VREG64(GITS_BASER1):           /* collection table */
         if ( !vgic_reg64_check_access(info->dabt) ) goto bad_width;
         spin_lock(&its->its_lock);
-        *r = vgic_reg64_extract(its->baser_coll, info);
+        *r = vreg_reg64_extract(its->baser_coll, info);
         spin_unlock(&its->its_lock);
         break;
 
@@ -1097,7 +1097,7 @@ static int vgic_v3_its_mmio_read(struct vcpu *v, mmio_info_t *info,
 
     case VREG32(GITS_PIDR2):
         if ( info->dabt.size != DABT_WORD ) goto bad_width;
-        *r = vgic_reg32_extract(GIC_PIDR2_ARCH_GICv3, info);
+        *r = vreg_reg32_extract(GIC_PIDR2_ARCH_GICv3, info);
         break;
 
     case VRANGE32(0xFFEC, 0xFFFC):
@@ -1258,7 +1258,7 @@ static int vgic_v3_its_mmio_write(struct vcpu *v, mmio_info_t *info,
         spin_lock(&its->its_lock);
         ctlr = its->enabled ? GITS_CTLR_ENABLE : 0;
         reg32 = ctlr;
-        vgic_reg32_update(&reg32, r, info);
+        vreg_reg32_update(&reg32, r, info);
 
         if ( ctlr ^ reg32 )
             its->enabled = vgic_v3_verify_its_status(its,
@@ -1295,7 +1295,7 @@ static int vgic_v3_its_mmio_write(struct vcpu *v, mmio_info_t *info,
         }
 
         reg = its->cbaser;
-        vgic_reg64_update(&reg, r, info);
+        vreg_reg64_update(&reg, r, info);
         sanitize_its_base_reg(&reg);
 
         its->cbaser = reg;
@@ -1309,7 +1309,7 @@ static int vgic_v3_its_mmio_write(struct vcpu *v, mmio_info_t *info,
 
         spin_lock(&its->vcmd_lock);
         reg = ITS_CMD_OFFSET(its->cwriter);
-        vgic_reg64_update(&reg, r, info);
+        vreg_reg64_update(&reg, r, info);
         its->cwriter = ITS_CMD_OFFSET(reg);
 
         if ( its->enabled )
@@ -1344,7 +1344,7 @@ static int vgic_v3_its_mmio_write(struct vcpu *v, mmio_info_t *info,
         }
 
         reg = its->baser_dev;
-        vgic_reg64_update(&reg, r, info);
+        vreg_reg64_update(&reg, r, info);
 
         /* We don't support indirect tables for now. */
         reg &= ~(GITS_BASER_RO_MASK | GITS_BASER_INDIRECT);
@@ -1381,7 +1381,7 @@ static int vgic_v3_its_mmio_write(struct vcpu *v, mmio_info_t *info,
         }
 
         reg = its->baser_coll;
-        vgic_reg64_update(&reg, r, info);
+        vreg_reg64_update(&reg, r, info);
         /* No indirect tables for the collection table. */
         reg &= ~(GITS_BASER_RO_MASK | GITS_BASER_INDIRECT);
         reg |= (sizeof(coll_table_entry_t) - 1) << GITS_BASER_ENTRY_SIZE_SHIFT;
diff --git a/xen/arch/arm/vgic-v3.c b/xen/arch/arm/vgic-v3.c
index 4287ae1..48c7682 100644
--- a/xen/arch/arm/vgic-v3.c
+++ b/xen/arch/arm/vgic-v3.c
@@ -178,7 +178,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
         if ( dabt.size != DABT_WORD ) goto bad_width;
 
         spin_lock_irqsave(&v->arch.vgic.lock, flags);
-        *r = vgic_reg32_extract(!!(v->arch.vgic.flags & VGIC_V3_LPIS_ENABLED),
+        *r = vreg_reg32_extract(!!(v->arch.vgic.flags & VGIC_V3_LPIS_ENABLED),
                                 info);
         spin_unlock_irqrestore(&v->arch.vgic.lock, flags);
         return 1;
@@ -186,7 +186,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):
@@ -208,7 +208,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
         if ( v->domain->arch.vgic.has_its )
             typer |= GICR_TYPER_PLPIS;
 
-        *r = vgic_reg64_extract(typer, info);
+        *r = vreg_reg64_extract(typer, info);
 
         return 1;
     }
@@ -244,7 +244,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
         if ( !vgic_reg64_check_access(dabt) ) goto bad_width;
 
         vgic_lock(v);
-        *r = vgic_reg64_extract(v->domain->arch.vgic.rdist_propbase, info);
+        *r = vreg_reg64_extract(v->domain->arch.vgic.rdist_propbase, info);
         vgic_unlock(v);
         return 1;
 
@@ -257,7 +257,7 @@ static int __vgic_v3_rdistr_rd_mmio_read(struct vcpu *v, mmio_info_t *info,
         if ( !vgic_reg64_check_access(dabt) ) goto bad_width;
 
         spin_lock_irqsave(&v->arch.vgic.lock, flags);
-        *r = vgic_reg64_extract(v->arch.vgic.rdist_pendbase, info);
+        *r = vreg_reg64_extract(v->arch.vgic.rdist_pendbase, info);
         *r &= ~GICR_PENDBASER_PTZ;       /* WO, reads as 0 */
         spin_unlock_irqrestore(&v->arch.vgic.lock, flags);
         return 1;
@@ -283,7 +283,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:
@@ -310,7 +310,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:
@@ -354,7 +354,7 @@ read_reserved:
     return 1;
 
 read_unknown:
-    *r = vgic_reg64_extract(0xdeadbeafdeadbeaf, info);
+    *r = vreg_reg64_extract(0xdeadbeafdeadbeaf, info);
     return 1;
 }
 
@@ -553,7 +553,7 @@ static int __vgic_v3_rdistr_rd_mmio_write(struct vcpu *v, mmio_info_t *info,
         if ( !(v->domain->arch.vgic.rdists_enabled) )
         {
             reg = v->domain->arch.vgic.rdist_propbase;
-            vgic_reg64_update(&reg, r, info);
+            vreg_reg64_update(&reg, r, info);
             reg = sanitize_propbaser(reg);
             v->domain->arch.vgic.rdist_propbase = reg;
         }
@@ -576,7 +576,7 @@ static int __vgic_v3_rdistr_rd_mmio_write(struct vcpu *v, mmio_info_t *info,
         if ( !(v->arch.vgic.flags & VGIC_V3_LPIS_ENABLED) )
         {
             reg = v->arch.vgic.rdist_pendbase;
-            vgic_reg64_update(&reg, r, info);
+            vreg_reg64_update(&reg, r, info);
             reg = sanitize_pendbaser(reg);
             v->arch.vgic.rdist_pendbase = reg;
         }
@@ -690,7 +690,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;
 
@@ -699,7 +699,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;
 
@@ -727,7 +727,7 @@ static int __vgic_v3_distr_common_mmio_read(const char *name, struct vcpu *v,
         ipriorityr = ACCESS_ONCE(rank->ipriorityr[rank_index]);
         vgic_unlock_rank(v, rank, flags);
 
-        *r = vgic_reg32_extract(ipriorityr, info);
+        *r = vreg_reg32_extract(ipriorityr, info);
 
         return 1;
     }
@@ -743,7 +743,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;
     }
@@ -787,7 +787,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;
@@ -798,7 +798,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;
@@ -841,7 +841,7 @@ static int __vgic_v3_distr_common_mmio_write(const char *name, struct vcpu *v,
         ipriorityr = &rank->ipriorityr[REG_RANK_INDEX(8, reg - GICD_IPRIORITYR,
                                                       DABT_WORD)];
         priority = ACCESS_ONCE(*ipriorityr);
-        vgic_reg32_update(&priority, r, info);
+        vreg_reg32_update(&priority, r, info);
         ACCESS_ONCE(*ipriorityr) = priority;
         vgic_unlock_rank(v, rank, flags);
         return 1;
@@ -857,7 +857,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);
@@ -1105,7 +1105,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;
 
@@ -1132,14 +1132,14 @@ static int vgic_v3_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
 
         typer |= (v->domain->arch.vgic.intid_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):
@@ -1232,7 +1232,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;
     }
@@ -1250,7 +1250,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):
@@ -1313,7 +1313,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 )
@@ -1419,7 +1419,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..1253753 100644
--- a/xen/include/asm-arm/vreg.h
+++ b/xen/include/asm-arm/vreg.h
@@ -107,99 +107,99 @@ 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,       \
+#define VREG_REG_HELPERS(sz, offmask)                                   \
+static inline register_t vreg_reg##sz##_extract(uint##sz##_t reg,       \
                                                 const mmio_info_t *info)\
 {                                                                       \
-    return vgic_reg_extract(reg, info->gpa & offmask,                   \
+    return vreg_reg_extract(reg, info->gpa & offmask,                   \
                             info->dabt.size);                           \
 }                                                                       \
                                                                         \
-static inline void vgic_reg##sz##_update(uint##sz##_t *reg,             \
+static inline void vreg_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,                     \
+    vreg_reg_update(&tmp, val, info->gpa & offmask,                     \
                     info->dabt.size);                                   \
                                                                         \
     *reg = tmp;                                                         \
 }                                                                       \
                                                                         \
-static inline void vgic_reg##sz##_setbits(uint##sz##_t *reg,            \
+static inline void vreg_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,                   \
+    vreg_reg_setbits(&tmp, bits, info->gpa & offmask,                   \
                      info->dabt.size);                                  \
                                                                         \
     *reg = tmp;                                                         \
 }                                                                       \
                                                                         \
-static inline void vgic_reg##sz##_clearbits(uint##sz##_t *reg,          \
+static inline void vreg_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,                 \
+    vreg_reg_clearbits(&tmp, bits, info->gpa & offmask,                 \
                        info->dabt.size);                                \
                                                                         \
     *reg = tmp;                                                         \
@@ -211,10 +211,10 @@ 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);
+VREG_REG_HELPERS(32, 0x3);
 
-#undef VGIC_REG_HELPERS
+#undef VREG_REG_HELPERS
 
 #endif /* __ASM_ARM_VREG__ */
