diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index 2eb31ad524..24a024261c 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -1020,7 +1020,7 @@ static int handle_device(struct domain *d, struct dt_device_node *dev)
              * twice the IRQ. This can happen if the IRQ is shared
              */
             vgic_reserve_virq(d, irq);
-            res = route_irq_to_guest(d, irq, dt_node_name(dev));
+            res = route_irq_to_guest(d, irq, irq, dt_node_name(dev));
             if ( res )
             {
                 printk(XENLOG_ERR "Unable to route IRQ %u to domain %u\n",
diff --git a/xen/arch/arm/gic.c b/xen/arch/arm/gic.c
index ba7950bfa1..fe8f69b840 100644
--- a/xen/arch/arm/gic.c
+++ b/xen/arch/arm/gic.c
@@ -126,7 +126,8 @@ void gic_route_irq_to_xen(struct irq_desc *desc, const cpumask_t *cpu_mask,
 /* Program the GIC to route an interrupt to a guest
  *   - desc.lock must be held
  */
-void gic_route_irq_to_guest(struct domain *d, struct irq_desc *desc,
+void gic_route_irq_to_guest(struct domain *d, unsigned int virq,
+                            struct irq_desc *desc,
                             const cpumask_t *cpu_mask, unsigned int priority)
 {
     struct pending_irq *p;
@@ -139,7 +140,7 @@ void gic_route_irq_to_guest(struct domain *d, struct irq_desc *desc,
 
     /* Use vcpu0 to retrieve the pending_irq struct. Given that we only
      * route SPIs to guests, it doesn't make any difference. */
-    p = irq_to_pending(d->vcpu[0], desc->irq);
+    p = irq_to_pending(d->vcpu[0], virq);
     p->desc = desc;
 }
 
diff --git a/xen/arch/arm/irq.c b/xen/arch/arm/irq.c
index cb9c99bf62..beb746ae79 100644
--- a/xen/arch/arm/irq.c
+++ b/xen/arch/arm/irq.c
@@ -31,6 +31,13 @@
 static unsigned int local_irqs_type[NR_LOCAL_IRQS];
 static DEFINE_SPINLOCK(local_irqs_type_lock);
 
+/* Describe an IRQ assigned to a guest */
+struct irq_guest
+{
+    struct domain *d;
+    unsigned int virq;
+};
+
 static void ack_none(struct irq_desc *irq)
 {
     printk("unexpected IRQ trap at irq %02x\n", irq->irq);
@@ -122,18 +129,20 @@ void __cpuinit init_secondary_IRQ(void)
     BUG_ON(init_local_irq_data() < 0);
 }
 
-static inline struct domain *irq_get_domain(struct irq_desc *desc)
+static inline struct irq_guest *irq_get_guest_info(struct irq_desc *desc)
 {
     ASSERT(spin_is_locked(&desc->lock));
-
-    if ( !test_bit(_IRQ_GUEST, &desc->status) )
-        return dom_xen;
-
+    ASSERT(test_bit(_IRQ_GUEST, &desc->status));
     ASSERT(desc->action != NULL);
 
     return desc->action->dev_id;
 }
 
+static inline struct domain *irq_get_domain(struct irq_desc *desc)
+{
+    return irq_get_guest_info(desc)->d;
+}
+
 void irq_set_affinity(struct irq_desc *desc, const cpumask_t *cpu_mask)
 {
     if ( desc != NULL )
@@ -204,7 +213,7 @@ void do_IRQ(struct cpu_user_regs *regs, unsigned int irq, int is_fiq)
 
     if ( test_bit(_IRQ_GUEST, &desc->status) )
     {
-        struct domain *d = irq_get_domain(desc);
+        struct irq_guest *info = irq_get_guest_info(desc);
 
         perfc_incr(guest_irqs);
         desc->handler->end(desc);
@@ -214,7 +223,7 @@ void do_IRQ(struct cpu_user_regs *regs, unsigned int irq, int is_fiq)
 
         /* the irq cannot be a PPI, we only support delivery of SPIs to
          * guests */
-        vgic_vcpu_inject_spi(d, irq);
+        vgic_vcpu_inject_spi(info->d, info->virq);
         goto out_no_end;
     }
 
@@ -378,19 +387,30 @@ err:
     return rc;
 }
 
-int route_irq_to_guest(struct domain *d, unsigned int irq,
-                       const char * devname)
+int route_irq_to_guest(struct domain *d, unsigned int virq,
+                       unsigned int irq, const char * devname)
 {
     struct irqaction *action;
-    struct irq_desc *desc = irq_to_desc(irq);
+    struct irq_guest *info;
+    struct irq_desc *desc;
     unsigned long flags;
     int retval = 0;
 
     action = xmalloc(struct irqaction);
-    if (!action)
+    if ( !action )
         return -ENOMEM;
 
-    action->dev_id = d;
+    info = xmalloc(struct irq_guest);
+    if ( !info )
+    {
+        xfree(action);
+        return -ENOMEM;
+    }
+
+    info->d = d;
+    info->virq = virq;
+
+    action->dev_id = info;
     action->name = devname;
     action->free_on_release = 1;
 
@@ -421,7 +441,7 @@ int route_irq_to_guest(struct domain *d, unsigned int irq,
     if ( retval )
         goto out;
 
-    gic_route_irq_to_guest(d, desc, cpumask_of(smp_processor_id()),
+    gic_route_irq_to_guest(d, virq, desc, cpumask_of(smp_processor_id()),
                            GIC_PRI_IRQ);
     spin_unlock_irqrestore(&desc->lock, flags);
     return 0;
@@ -429,6 +449,7 @@ int route_irq_to_guest(struct domain *d, unsigned int irq,
 out:
     spin_unlock_irqrestore(&desc->lock, flags);
     xfree(action);
+    xfree(info);
 
     return retval;
 }
diff --git a/xen/arch/arm/platforms/xgene-storm.c b/xen/arch/arm/platforms/xgene-storm.c
index eee650e84d..1812e5ba18 100644
--- a/xen/arch/arm/platforms/xgene-storm.c
+++ b/xen/arch/arm/platforms/xgene-storm.c
@@ -75,7 +75,7 @@ static int map_one_spi(struct domain *d, const char *what,
         printk("Failed to reserve vIRQ %u on dom%d\n",
                irq, d->domain_id);
 
-    ret = route_irq_to_guest(d, irq, what);
+    ret = route_irq_to_guest(d, irq, irq, what);
     if ( ret )
         printk("Failed to route %s to dom%d\n", what, d->domain_id);
 
diff --git a/xen/arch/arm/vgic.c b/xen/arch/arm/vgic.c
index fc6f851702..8f91962eee 100644
--- a/xen/arch/arm/vgic.c
+++ b/xen/arch/arm/vgic.c
@@ -382,16 +382,16 @@ void vgic_clear_pending_irqs(struct vcpu *v)
     spin_unlock_irqrestore(&v->arch.vgic.lock, flags);
 }
 
-void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
+void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int virq)
 {
     uint8_t priority;
-    struct vgic_irq_rank *rank = vgic_rank_irq(v, irq);
-    struct pending_irq *iter, *n = irq_to_pending(v, irq);
+    struct vgic_irq_rank *rank = vgic_rank_irq(v, virq);
+    struct pending_irq *iter, *n = irq_to_pending(v, virq);
     unsigned long flags;
     bool_t running;
 
     vgic_lock_rank(v, rank, flags);
-    priority = v->domain->arch.vgic.handler->get_irq_priority(v, irq);
+    priority = v->domain->arch.vgic.handler->get_irq_priority(v, virq);
     vgic_unlock_rank(v, rank, flags);
 
     spin_lock_irqsave(&v->arch.vgic.lock, flags);
@@ -407,7 +407,7 @@ void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
 
     if ( !list_empty(&n->inflight) )
     {
-        gic_raise_inflight_irq(v, irq);
+        gic_raise_inflight_irq(v, virq);
         goto out;
     }
 
@@ -415,7 +415,7 @@ void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
 
     /* the irq is enabled */
     if ( test_bit(GIC_IRQ_GUEST_ENABLED, &n->status) )
-        gic_raise_guest_irq(v, irq, priority);
+        gic_raise_guest_irq(v, virq, priority);
 
     list_for_each_entry ( iter, &v->arch.vgic.inflight_irqs, inflight )
     {
@@ -438,15 +438,15 @@ out:
     }
 }
 
-void vgic_vcpu_inject_spi(struct domain *d, unsigned int irq)
+void vgic_vcpu_inject_spi(struct domain *d, unsigned int virq)
 {
     struct vcpu *v;
 
     /* the IRQ needs to be an SPI */
-    ASSERT(irq >= 32 && irq <= gic_number_lines());
+    ASSERT(virq >= 32 && virq <= vgic_num_irqs(d));
 
-    v = vgic_get_target_vcpu(d->vcpu[0], irq);
-    vgic_vcpu_inject_irq(v, irq);
+    v = vgic_get_target_vcpu(d->vcpu[0], virq);
+    vgic_vcpu_inject_irq(v, virq);
 }
 
 void arch_evtchn_inject(struct vcpu *v)
diff --git a/xen/include/asm-arm/gic.h b/xen/include/asm-arm/gic.h
index b16f98eb4d..bb2a922f10 100644
--- a/xen/include/asm-arm/gic.h
+++ b/xen/include/asm-arm/gic.h
@@ -216,7 +216,8 @@ extern enum gic_version gic_hw_version(void);
 /* Program the GIC to route an interrupt */
 extern void gic_route_irq_to_xen(struct irq_desc *desc, const cpumask_t *cpu_mask,
                                  unsigned int priority);
-extern void gic_route_irq_to_guest(struct domain *, struct irq_desc *desc,
+extern void gic_route_irq_to_guest(struct domain *, unsigned int virq,
+                                   struct irq_desc *desc,
                                    const cpumask_t *cpu_mask,
                                    unsigned int priority);
 
diff --git a/xen/include/asm-arm/irq.h b/xen/include/asm-arm/irq.h
index 435dfcd055..f00eb111a3 100644
--- a/xen/include/asm-arm/irq.h
+++ b/xen/include/asm-arm/irq.h
@@ -40,8 +40,8 @@ void do_IRQ(struct cpu_user_regs *regs, unsigned int irq, int is_fiq);
 void init_IRQ(void);
 void init_secondary_IRQ(void);
 
-int route_irq_to_guest(struct domain *d, unsigned int irq,
-                       const char *devname);
+int route_irq_to_guest(struct domain *d, unsigned int virq,
+                       unsigned int irq, const char *devname);
 void arch_move_irqs(struct vcpu *v);
 
 /* Set IRQ type for an SPI */
diff --git a/xen/include/asm-arm/vgic.h b/xen/include/asm-arm/vgic.h
index 0d0d114af2..aba0d8044c 100644
--- a/xen/include/asm-arm/vgic.h
+++ b/xen/include/asm-arm/vgic.h
@@ -181,8 +181,8 @@ extern int domain_vgic_init(struct domain *d);
 extern void domain_vgic_free(struct domain *d);
 extern int vcpu_vgic_init(struct vcpu *v);
 extern struct vcpu *vgic_get_target_vcpu(struct vcpu *v, unsigned int irq);
-extern void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq);
-extern void vgic_vcpu_inject_spi(struct domain *d, unsigned int irq);
+extern void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int virq);
+extern void vgic_vcpu_inject_spi(struct domain *d, unsigned int virq);
 extern void vgic_clear_pending_irqs(struct vcpu *v);
 extern struct pending_irq *irq_to_pending(struct vcpu *v, unsigned int irq);
 extern struct vgic_irq_rank *vgic_rank_offset(struct vcpu *v, int b, int n, int s);