DEFINE(VGIC_V2_CPU_ELRSR,    offsetof(struct vgic_cpu, vgic_v2.vgic_elrsr));
   DEFINE(VGIC_V2_CPU_APR,      offsetof(struct vgic_cpu, vgic_v2.vgic_apr));
   DEFINE(VGIC_V2_CPU_LR,       offsetof(struct vgic_cpu, vgic_v2.vgic_lr));
+  DEFINE(VGIC_V3_CPU_SRE,      offsetof(struct vgic_cpu, vgic_v3.vgic_sre));
   DEFINE(VGIC_V3_CPU_HCR,      offsetof(struct vgic_cpu, vgic_v3.vgic_hcr));
   DEFINE(VGIC_V3_CPU_VMCR,     offsetof(struct vgic_cpu, vgic_v3.vgic_vmcr));
   DEFINE(VGIC_V3_CPU_MISR,     offsetof(struct vgic_cpu, vgic_v3.vgic_misr));
 
  * x0: Register pointing to VCPU struct
  */
 .macro restore_vgic_v3_state
-       // Disable SRE_EL1 access. Necessary, otherwise
-       // ICH_VMCR_EL2.VFIQEn becomes one, and FIQ happens...
-       msr_s   ICC_SRE_EL1, xzr
-       isb
-
        // Compute the address of struct vgic_cpu
        add     x3, x0, #VCPU_VGIC_CPU
 
        // Restore all interesting registers
        ldr     w4, [x3, #VGIC_V3_CPU_HCR]
        ldr     w5, [x3, #VGIC_V3_CPU_VMCR]
+       ldr     w25, [x3, #VGIC_V3_CPU_SRE]
+
+       msr_s   ICC_SRE_EL1, x25
+
+       // make sure SRE is valid before writing the other registers
+       isb
 
        msr_s   ICH_HCR_EL2, x4
        msr_s   ICH_VMCR_EL2, x5
        dsb     sy
 
        // Prevent the guest from touching the GIC system registers
+       // if SRE isn't enabled for GICv3 emulation
+       cbnz    x25, 1f
        mrs_s   x5, ICC_SRE_EL2
        and     x5, x5, #~ICC_SRE_EL2_ENABLE
        msr_s   ICC_SRE_EL2, x5
+1:
 .endm
 
 ENTRY(__save_vgic_v3_state)
 
 #ifdef CONFIG_ARM_GIC_V3
        u32             vgic_hcr;
        u32             vgic_vmcr;
+       u32             vgic_sre;       /* Restored only, change ignored */
        u32             vgic_misr;      /* Saved only */
        u32             vgic_eisr;      /* Saved only */
        u32             vgic_elrsr;     /* Saved only */
 
 
 static void vgic_v3_enable(struct kvm_vcpu *vcpu)
 {
+       struct vgic_v3_cpu_if *vgic_v3 = &vcpu->arch.vgic_cpu.vgic_v3;
+
        /*
         * By forcing VMCR to zero, the GIC will restore the binary
         * points to their reset values. Anything else resets to zero
         * anyway.
         */
-       vcpu->arch.vgic_cpu.vgic_v3.vgic_vmcr = 0;
+       vgic_v3->vgic_vmcr = 0;
+
+       vgic_v3->vgic_sre = 0;
 
        /* Get the show on the road... */
-       vcpu->arch.vgic_cpu.vgic_v3.vgic_hcr = ICH_HCR_EN;
+       vgic_v3->vgic_hcr = ICH_HCR_EN;
 }
 
 static const struct vgic_ops vgic_v3_ops = {