imx8m-evk: add guest memory region to dts

This is a carve out region for virtualisation.

include/arch/arm/arch/32/mode/machine/gic_v2.bf

@@ -0,0 +1,48 @@
+--
+-- Copyright 2019, Data61
+-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+-- ABN 41 687 119 230.
+--
+-- This software may be distributed and modified according to the terms of
+-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
+-- See "LICENSE_GPLv2.txt" for details.
+--
+-- @TAG(DATA61_GPL)
+--
+
+#include <config.h>
+-- Default base size: uint32_t
+base 32
+
+block virq_invalid {
+    padding             2
+    field virqType      2
+    padding             8
+    field virqEOIIRQEN  1
+    padding             19
+}
+
+block virq_active {
+    padding             2
+    field virqType      2
+    padding             8
+    field virqEOIIRQEN  1
+    padding             19
+}
+
+block virq_pending {
+    padding             1
+    field virqGroup     1
+    field virqType      2
+    field virqPriority  5
+    padding             3
+    field virqEOIIRQEN  1
+    padding             9
+    field virqIRQ       10
+}
+
+tagged_union virq virqType {
+    tag virq_invalid    0
+    tag virq_pending    1
+    tag virq_active     2
+}

include/arch/arm/arch/32/mode/object/structures.bf

@@ -475,41 +475,6 @@ block vm_attributes {
     field armPageCacheable 1
 }
 
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-block virq_invalid {
-    padding             2
-    field virqType      2
-    padding             8
-    field virqEOIIRQEN  1
-    padding             19
-}
-
-block virq_active {
-    padding             2
-    field virqType      2
-    padding             8
-    field virqEOIIRQEN  1
-    padding             19
-}
-
-block virq_pending {
-    padding             1
-    field virqGroup     1
-    field virqType      2
-    field virqPriority  5
-    padding             3
-    field virqEOIIRQEN  1
-    padding             9
-    field virqIRQ       10
-}
-
-tagged_union virq virqType {
-    tag virq_invalid    0
-    tag virq_pending    1
-    tag virq_active     2
-}
-#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
-
 #ifdef CONFIG_HARDWARE_DEBUG_API
 -- ARM breakpoint/watchpoint register layouts
 

include/arch/arm/arch/64/mode/machine/gic_v2.bf

@@ -0,0 +1,53 @@
+--
+-- Copyright 2019, Data61
+-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+-- ABN 41 687 119 230.
+--
+-- This software may be distributed and modified according to the terms of
+-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
+-- See "LICENSE_GPLv2.txt" for details.
+--
+-- @TAG(DATA61_GPL)
+--
+
+#include <config.h>
+-- Default base size: uint64_t
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+base 64(48,0)
+
+block virq_invalid {
+    padding             32
+    padding             2
+    field virqType      2
+    padding             8
+    field virqEOIIRQEN  1
+    padding             19
+}
+
+block virq_active {
+    padding             32
+    padding             2
+    field virqType      2
+    padding             8
+    field virqEOIIRQEN  1
+    padding             19
+}
+
+block virq_pending {
+    padding             32
+    padding             1
+    field virqGroup     1
+    field virqType      2
+    field virqPriority  5
+    padding             3
+    field virqEOIIRQEN  1
+    padding             9
+    field virqIRQ       10
+}
+
+tagged_union virq virqType {
+    tag virq_invalid    0
+    tag virq_pending    1
+    tag virq_active     2
+}
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */

include/arch/arm/arch/64/mode/machine/gic_v3.bf

@@ -0,0 +1,68 @@
+--
+-- Copyright 2019, Data61
+-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+-- ABN 41 687 119 230.
+--
+-- This software may be distributed and modified according to the terms of
+-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
+-- See "LICENSE_GPLv2.txt" for details.
+--
+-- @TAG(DATA61_GPL)
+--
+
+#include <config.h>
+-- Default base size: uint64_t
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+base 64(48,0)
+
+block virq_inactive {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pintid        10
+    field vintid        32
+}
+
+block virq_pending {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pintid        10
+    field vintid        32
+}
+
+block virq_active {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pintid        10
+    field vintid        32
+}
+
+block virq_pending_active {
+    field virqType      2
+    field hw            1
+    field group         1
+    padding             4
+    field priority      8
+    padding             6
+    field pinitid       10
+    field vintid        32
+}
+
+tagged_union virq virqType {
+    tag virq_inactive       0
+    tag virq_pending        1
+    tag virq_active         2
+    tag virq_pending_active 3
+}
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */

include/arch/arm/arch/64/mode/object/structures.bf

@@ -365,42 +365,4 @@ block ttbr {
     field_high base_address         48
 }
 
-#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-block virq_invalid {
-    padding             32
-    padding             2
-    field virqType      2
-    padding             8
-    field virqEOIIRQEN  1
-    padding             19
-}
-
-block virq_active {
-    padding             32
-    padding             2
-    field virqType      2
-    padding             8
-    field virqEOIIRQEN  1
-    padding             19
-}
-
-block virq_pending {
-    padding             32
-    padding             1
-    field virqGroup     1
-    field virqType      2
-    field virqPriority  5
-    padding             3
-    field virqEOIIRQEN  1
-    padding             9
-    field virqIRQ       10
-}
-
-tagged_union virq virqType {
-    tag virq_invalid    0
-    tag virq_pending    1
-    tag virq_active     2
-}
-#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
-
 #include <sel4/arch/shared_types.bf>

include/arch/arm/arch/machine/gic_common.h

@@ -15,6 +15,10 @@
 #define GICD_SGIR_CPUTARGETLIST_SHIFT     16
 #define GICD_SGIR_TARGETLISTFILTER_SHIFT  24
 
+/* Bits in the VMCR */
+#define VGIC_VMCR_VENG1 BIT(1)
+#define VGIC_VMCR_VPMR  (0xFFlu << 24lu)
+
 /* Special IRQ's */
 #define SPECIAL_IRQ_START 1020u
 #define IRQ_NONE          1023u

include/arch/arm/arch/machine/gic_v2.h

@@ -17,10 +17,11 @@
 #include <linker.h>
 #include <mode/smp/smp.h>
 #include <model/statedata.h>
-
+#include <mode/machine/gic_v2_gen.h>
 #include "gic_common.h"
 
 #define IRQ_MASK MASK(10u)
+#define GIC_MAX_PRIO 31
 
 /* Helpers for VGIC */
 #define VGIC_HCR_EOI_INVALID_COUNT(hcr) (((hcr) >> 27) & 0x1f)
@@ -297,4 +298,30 @@ static inline void set_gic_vcpu_ctrl_lr(int num, virq_t lr)
     gic_vcpu_ctrl->lr[num] = lr.words[0];
 }
 
+#define GIC_INVALID_IRQ_IDX -1
+static inline int get_vgic_irq_idx(void)
+{
+    uint32_t eisr0 = get_gic_vcpu_ctrl_eisr0();
+    if (eisr0) {
+        return ctzl(eisr0);
+    }
+    uint32_t eisr1 = get_gic_vcpu_ctrl_eisr1();
+    if (eisr1) {
+        return ctzl(eisr1) + 32;
+    }
+
+    return GIC_INVALID_IRQ_IDX;
+}
+
+static inline virq_t gic_virq_pending_new(word_t group, word_t priority, word_t vid)
+{
+    return virq_virq_pending_new(group, priority, 1, vid);
+}
+
+static inline bool_t gic_valid_irq_idx(int irq_idx)
+{
+    return irq_idx < gic_vcpu_num_list_regs;
+}
+
+void gic_handle_virq(int irq_idx);
 #endif /* End of CONFIG_ARM_HYPERVISOR_SUPPORT */

include/arch/arm/arch/machine/gic_v3.h

@@ -14,6 +14,7 @@
 /* tell the kernel we have the set trigger feature */
 #define HAVE_SET_TRIGGER 1
 
+#include <config.h>
 #include <stdint.h>
 #include <util.h>
 #include <linker.h>
@@ -21,6 +22,10 @@
 #include <model/statedata.h>
 #include <armv/machine.h>
 
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+#include <mode/machine/gic_v3_gen.h>
+#endif
+
 #include "gic_common.h"
 
 #define GIC_PRI_LOWEST     0xf0
@@ -28,6 +33,7 @@
 #define GIC_PRI_HIGHEST    0x80 /* Higher priorities belong to Secure-World */
 
 #define IRQ_MASK MASK(16u)
+#define GIC_MAX_PRIO 256
 
 /* Register bits */
 #define GICD_CTL_ENABLE 0x1
@@ -39,7 +45,8 @@
 
 #define GICD_TYPE_LINESNR 0x01f
 
-#define GICC_SRE_EL1_SRE             BIT(0)
+#define GICC_SRE_SRE                BIT(0)
+#define GICC_SRE_EL2_EL1            BIT(3)
 
 #define GICR_WAKER_ProcessorSleep    BIT(1)
 #define GICR_WAKER_ChildrenAsleep    BIT(2)
@@ -73,6 +80,33 @@
 #define MPIDR           " p15, 0,  %0, c0,  c0, 5"
 #endif
 
+#define ICC_SRE_EL2     "S3_4_C12_C9_5"
+
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+#define ICC_SRE ICC_SRE_EL2
+#else
+#define ICC_SRE ICC_SRE_EL1
+#endif
+
+#define ICH_LR0(x) "S3_4_C12_C12_"STRINGIFY(x)
+#define ICH_LR8(x) "S3_4_C12_C13_"STRINGIFY(x)
+
+/* System registers for GIC virtual interface control */
+#define ICH_HCR_EL2     "S3_4_C12_C11_0"
+#define ICH_VTR_EL2     "S3_4_C12_C11_1"
+#define ICH_MISR_EL2    "S3_4_C12_C11_2"
+#define ICH_EISR_EL2    "S3_4_C12_C11_3"
+#define ICH_VMCR_EL2    "S3_4_C12_C11_7"
+
+#define ICH_VMCR_EL2_LISTREGS(x) (((x) & 0x1f) + 1)
+#define VGIC_VTR_NLISTREGS(x) ICH_VMCR_EL2_LISTREGS(x)
+
+#define ICH_HCR_EL2_EN      (1)
+#define VGIC_HCR_EN         ICH_HCR_EL2_EN
+
+#define ICH_MISR_EL2_EOI (1)
+#define VGIC_MISR_EOI    ICH_MISR_EL2_EOI
+
 /* Memory map for GIC distributor */
 struct gic_dist_map {
     uint32_t ctlr;                /* 0x0000 */
@@ -291,3 +325,208 @@ static inline void ackInterrupt(irq_t irq)
 
 }
 
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+/* GIC VCPU Control Interface */
+extern unsigned int gic_vcpu_num_list_regs;
+
+static inline uint32_t get_gic_vcpu_ctrl_hcr(void)
+{
+    word_t hcr = 0;
+    SYSTEM_READ_WORD(ICH_HCR_EL2, hcr);
+    return (uint32_t) hcr;
+}
+
+static inline void set_gic_vcpu_ctrl_hcr(uint32_t hcr)
+{
+    SYSTEM_WRITE_WORD(ICH_HCR_EL2, hcr);
+}
+
+static inline uint32_t get_gic_vcpu_ctrl_vmcr(void)
+{
+    word_t vmcr;
+    SYSTEM_READ_WORD(ICH_VMCR_EL2, vmcr);
+    return (uint32_t) vmcr;
+}
+
+static inline void set_gic_vcpu_ctrl_vmcr(uint32_t vmcr)
+{
+    SYSTEM_WRITE_WORD(ICH_VMCR_EL2, vmcr);
+}
+
+static inline uint32_t get_gic_vcpu_ctrl_apr(void)
+{
+    return 0;
+}
+
+static inline void set_gic_vcpu_ctrl_apr(uint32_t apr)
+{
+    return;
+}
+
+static inline uint32_t get_gic_vcpu_ctrl_vtr(void)
+{
+    word_t vtr;
+    SYSTEM_READ_WORD(ICH_VTR_EL2, vtr);
+    return (uint32_t) vtr;
+}
+
+static inline uint32_t get_gic_vcpu_ctrl_eisr0(void)
+{
+    word_t eisr;
+    SYSTEM_READ_WORD(ICH_EISR_EL2, eisr);
+    return (uint32_t) eisr;
+}
+
+static inline uint32_t get_gic_vcpu_ctrl_misr(void)
+{
+    word_t misr;
+    SYSTEM_READ_WORD(ICH_MISR_EL2, misr);
+    return (uint32_t) misr;
+}
+
+static inline virq_t get_gic_vcpu_ctrl_lr(word_t n)
+{
+    virq_t virq = {0};
+    uint64_t lr = 0;
+    switch (n) {
+    case 0:
+        SYSTEM_READ_WORD(ICH_LR0(0), lr);
+        break;
+    case 1:
+        SYSTEM_READ_WORD(ICH_LR0(1), lr);
+        break;
+    case 2:
+        SYSTEM_READ_WORD(ICH_LR0(2), lr);
+        break;
+    case 3:
+        SYSTEM_READ_WORD(ICH_LR0(3), lr);
+        break;
+    case 4:
+        SYSTEM_READ_WORD(ICH_LR0(4), lr);
+        break;
+    case 5:
+        SYSTEM_READ_WORD(ICH_LR0(5), lr);
+        break;
+    case 6:
+        SYSTEM_READ_WORD(ICH_LR0(6), lr);
+        break;
+    case 7:
+        SYSTEM_READ_WORD(ICH_LR0(7), lr);
+        break;
+    case 8:
+        SYSTEM_READ_WORD(ICH_LR8(0), lr);
+        break;
+    case 9:
+        SYSTEM_READ_WORD(ICH_LR8(1), lr);
+        break;
+    case 10:
+        SYSTEM_READ_WORD(ICH_LR8(2), lr);
+        break;
+    case 11:
+        SYSTEM_READ_WORD(ICH_LR8(3), lr);
+        break;
+    case 12:
+        SYSTEM_READ_WORD(ICH_LR8(4), lr);
+        break;
+    case 13:
+        SYSTEM_READ_WORD(ICH_LR8(5), lr);
+        break;
+    case 14:
+        SYSTEM_READ_WORD(ICH_LR8(6), lr);
+        break;
+    case 15:
+        SYSTEM_READ_WORD(ICH_LR8(7), lr);
+        break;
+    default:
+        fail("GICv3: Invalid ICH_LR_EL2");
+        break;
+    }
+    virq.words[0] = lr;
+    return virq;
+}
+
+static inline void set_gic_vcpu_ctrl_lr(word_t n, virq_t lr)
+{
+    switch (n) {
+    case 0:
+        SYSTEM_WRITE_WORD(ICH_LR0(0), lr.words[0]);
+        break;
+    case 1:
+        SYSTEM_WRITE_WORD(ICH_LR0(1), lr.words[0]);
+        break;
+    case 2:
+        SYSTEM_WRITE_WORD(ICH_LR0(2), lr.words[0]);
+        break;
+    case 3:
+        SYSTEM_WRITE_WORD(ICH_LR0(3), lr.words[0]);
+        break;
+    case 4:
+        SYSTEM_WRITE_WORD(ICH_LR0(4), lr.words[0]);
+        break;
+    case 5:
+        SYSTEM_WRITE_WORD(ICH_LR0(5), lr.words[0]);
+        break;
+    case 6:
+        SYSTEM_WRITE_WORD(ICH_LR0(6), lr.words[0]);
+        break;
+    case 7:
+        SYSTEM_WRITE_WORD(ICH_LR0(7), lr.words[0]);
+        break;
+    case 8:
+        SYSTEM_WRITE_WORD(ICH_LR8(0), lr.words[0]);
+        break;
+    case 9:
+        SYSTEM_WRITE_WORD(ICH_LR8(1), lr.words[0]);
+        break;
+    case 10:
+        SYSTEM_WRITE_WORD(ICH_LR8(2), lr.words[0]);
+        break;
+    case 11:
+        SYSTEM_WRITE_WORD(ICH_LR8(3), lr.words[0]);
+        break;
+    case 12:
+        SYSTEM_WRITE_WORD(ICH_LR8(4), lr.words[0]);
+        break;
+    case 13:
+        SYSTEM_WRITE_WORD(ICH_LR8(5), lr.words[0]);
+        break;
+    case 14:
+        SYSTEM_WRITE_WORD(ICH_LR8(6), lr.words[0]);
+        break;
+    case 15:
+        SYSTEM_WRITE_WORD(ICH_LR8(7), lr.words[0]);
+        break;
+    default:
+        fail("GICv3: Invalid ICH_LR_EL2");
+        break;
+
+    }
+}
+
+#define GIC_INVALID_IRQ_IDX 0
+static inline int get_vgic_irq_idx(void)
+{
+    int irq_idx = GIC_INVALID_IRQ_IDX;
+    uint32_t eisr0 = get_gic_vcpu_ctrl_eisr0();
+
+    for (int i = 0; i < gic_vcpu_num_list_regs; i++) {
+        if (eisr0 & BIT(i)) {
+            irq_idx |= BIT(i);
+        }
+    }
+    return irq_idx;
+}
+
+static inline virq_t gic_virq_pending_new(word_t group, word_t priority, word_t vid)
+{
+    return virq_virq_pending_new(0, group, priority, 0x200, vid);
+}
+
+static inline bool_t gic_valid_irq_idx(int irq_idx)
+{
+    return !(irq_idx & ~MASK(gic_vcpu_num_list_regs));
+}
+
+void gic_handle_virq(int irq_idx);
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
+

include/arch/arm/arch/object/interrupt.h

@@ -6,6 +6,7 @@
 
 #pragma once
 
+#include <config.h>
 #include <types.h>
 #include <api/failures.h>
 #include <object/structures.h>

src/arch/arm/config.cmake

@@ -260,5 +260,17 @@ add_sources(
 )
 
 add_bf_source_old("KernelArchARM" "structures.bf" "include/arch/arm" "arch/object")
+add_bf_source_old(
+    "KernelArchARM"
+    "gic_v2.bf"
+    "include/arch/arm/arch/${KernelWordSize}"
+    "mode/machine"
+)
+add_bf_source_old(
+    "KernelArmHypervisorSupport;Kernel64"
+    "gic_v3.bf"
+    "include/arch/arm/arch/${KernelWordSize}"
+    "mode/machine"
+)
 
 include(src/arch/arm/${KernelWordSize}/config.cmake)

src/arch/arm/machine/gic_v2.c

@@ -230,4 +230,22 @@ volatile struct gich_vcpu_ctrl_map *gic_vcpu_ctrl =
 
 unsigned int gic_vcpu_num_list_regs;
 
+void gic_handle_virq(int irq_idx)
+{
+    virq_t virq = get_gic_vcpu_ctrl_lr(irq_idx);
+    switch (virq_get_virqType(virq)) {
+    case virq_virq_active:
+        virq = virq_virq_active_set_virqEOIIRQEN(virq, 0);
+        break;
+    case virq_virq_pending:
+        virq = virq_virq_pending_set_virqEOIIRQEN(virq, 0);
+        break;
+    case virq_virq_invalid:
+        virq = virq_virq_invalid_set_virqEOIIRQEN(virq, 0);
+        break;
+    }
+    set_gic_vcpu_ctrl_lr(irq_idx, virq);
+    ARCH_NODE_STATE(armHSCurVCPU)->vgic.lr[irq_idx] = virq;
+}
+
 #endif /* End of CONFIG_ARM_HYPERVISOR_SUPPORT */

src/arch/arm/machine/gic_v3.c

@@ -125,10 +125,15 @@ static void gicv3_enable_sre(void)
     uint32_t val = 0;
 
     /* ICC_SRE_EL1 */
-    SYSTEM_READ_WORD(ICC_SRE_EL1, val);
-    val |= GICC_SRE_EL1_SRE;
+    SYSTEM_READ_WORD(ICC_SRE, val);
+    val |= GICC_SRE_SRE;
+    if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
+        /* don't trap to el2 on access to ICC_SRE_EL1 */
+        /* TODO is this what we want permanently @yanyan?? */
+        val |= GICC_SRE_EL2_EL1;
+    }
 
-    SYSTEM_WRITE_WORD(ICC_SRE_EL1, val);
+    SYSTEM_WRITE_WORD(ICC_SRE, val);
     isb();
 }
 
@@ -385,3 +390,18 @@ void setIRQTarget(irq_t irq, seL4_Word target)
 }
 
 #endif /* ENABLE_SMP_SUPPORT */
+#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
+unsigned int gic_vcpu_num_list_regs;
+
+void gic_handle_virq(int irq_idx)
+{
+    for (int i = 0; i < gic_vcpu_num_list_regs; i++) {
+        if (irq_idx & BIT(i)) {
+            virq_t virq = get_gic_vcpu_ctrl_lr(i);
+            assert(virq_get_virqType(virq) == virq_virq_inactive);
+            virq = virq_virq_inactive_set_pintid(virq, 0);
+            set_gic_vcpu_ctrl_lr(i, virq);
+        }
+    }
+}
+#endif

src/arch/arm/object/vcpu.c

@@ -12,7 +12,6 @@
 #include <armv/vcpu.h>
 #include <arch/machine/debug.h> /* Arch_debug[A/Di]ssociateVCPUTCB() */
 #include <arch/machine/debug_conf.h>
-#include <arch/machine/gic_v2.h>
 #include <drivers/timer/arm_generic.h>
 
 BOOT_CODE void vcpu_boot_init(void)
@@ -140,7 +139,6 @@ void VPPIEvent(irq_t irq)
 
 void VGICMaintenance(void)
 {
-    uint32_t eisr0, eisr1;
     uint32_t flags;
 
 #ifdef CONFIG_KERNEL_MCS
@@ -161,44 +159,19 @@ void VGICMaintenance(void)
         return;
     }
 
-    eisr0 = get_gic_vcpu_ctrl_eisr0();
-    eisr1 = get_gic_vcpu_ctrl_eisr1();
     flags = get_gic_vcpu_ctrl_misr();
 
     if (flags & VGIC_MISR_EOI) {
-        int irq_idx;
-        if (eisr0) {
-            irq_idx = ctzl(eisr0);
-        } else if (eisr1) {
-            irq_idx = ctzl(eisr1) + 32;
-        } else {
-            irq_idx = -1;
-        }
+        int irq_idx = get_vgic_irq_idx();
 
         /* the hardware should never give us an invalid index, but we don't
          * want to trust it that far */
-        if (irq_idx == -1  || irq_idx >= gic_vcpu_num_list_regs) {
+        if (irq_idx == GIC_INVALID_IRQ_IDX || !gic_valid_irq_idx(irq_idx)) {
             current_fault = seL4_Fault_VGICMaintenance_new(0, 0);
         } else {
-            virq_t virq = get_gic_vcpu_ctrl_lr(irq_idx);
-            switch (virq_get_virqType(virq)) {
-            case virq_virq_active:
-                virq = virq_virq_active_set_virqEOIIRQEN(virq, 0);
-                break;
-            case virq_virq_pending:
-                virq = virq_virq_pending_set_virqEOIIRQEN(virq, 0);
-                break;
-            case virq_virq_invalid:
-                virq = virq_virq_invalid_set_virqEOIIRQEN(virq, 0);
-                break;
-            }
-            set_gic_vcpu_ctrl_lr(irq_idx, virq);
-            /* decodeVCPUInjectIRQ below checks the vgic.lr register,
-             * so we should also sync the shadow data structure as well */
+            gic_handle_virq(irq_idx);
             assert(ARCH_NODE_STATE(armHSCurVCPU) != NULL && ARCH_NODE_STATE(armHSVCPUActive));
-            if (ARCH_NODE_STATE(armHSCurVCPU) != NULL && ARCH_NODE_STATE(armHSVCPUActive)) {
-                ARCH_NODE_STATE(armHSCurVCPU)->vgic.lr[irq_idx] = virq;
-            } else {
+            if (!ARCH_NODE_STATE(armHSVCPUActive)) {
                 /* FIXME This should not happen */
             }
             current_fault = seL4_Fault_VGICMaintenance_new(irq_idx, 1);
@@ -227,6 +200,7 @@ void vcpu_init(vcpu_t *vcpu)
     /* Virtual Timer interface */
     vcpu->virtTimer.last_pcount = 0;
 #endif
+    vcpu->vgic.vmcr = VGIC_VMCR_VPMR | VGIC_VMCR_VENG1;
 }
 
 void vcpu_switch(vcpu_t *new)
@@ -430,7 +404,7 @@ exception_t decodeVCPUInjectIRQ(cap_t cap, unsigned int length, word_t *buffer)
         current_syscall_error.type = seL4_RangeError;
         return EXCEPTION_SYSCALL_ERROR;
     }
-    if (priority > 31) {
+    if (priority > GIC_MAX_PRIO) {
         current_syscall_error.type = seL4_RangeError;
         current_syscall_error.rangeErrorMin = 0;
         current_syscall_error.rangeErrorMax = 31;
@@ -461,8 +435,7 @@ exception_t decodeVCPUInjectIRQ(cap_t cap, unsigned int length, word_t *buffer)
         current_syscall_error.type = seL4_DeleteFirst;
         return EXCEPTION_SYSCALL_ERROR;
     }
-    virq_t virq = virq_virq_pending_new(group, priority, 1, vid);
-
+    virq_t virq = gic_virq_pending_new(group, priority, vid);
     setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
     return invokeVCPUInjectIRQ(vcpu, index, virq);
 }

src/plat/imx8m-evk/overlay-imx8mq-evk.dts

@@ -26,4 +26,9 @@
 		status = "disabled";
 	};
 
+    guestvm@b0000000 {
+        reg = <0x0 0xb0000000 0x0 0x8000000>;
+        status = "okay";
+    };
+
 };