aarch32/vcpu: save and restore CNTKCTL

Save and restore the CNTKCTL register alongside other virtual timer
registers when switching VCPUs.

Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>

CHANGES.md

@@ -63,6 +63,9 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
     2.1. All registers from `seL4_VCPUReg_TTBR0` to `seL4_VCPUReg_SPSR_EL1` are saved. This range includes
          `seL4_VCPUReg_CPACR`, which overwrites the previously saved value and grants FPU access at EL0 and EL1.
 
+* Fixed: on aarch32 configurations with hypervisor support, `CNTKCTL` was not saved and restored alongside other virtual
+  timer registers. `seL4_VCPUReg_CNTKCTL` has been introduced to mirror `seL4_VCPUReg_CNTKCTL_EL1` from aarch64.
+
 ### Upgrade Notes
 
 ---

include/arch/arm/arch/object/vcpu.h

@@ -78,11 +78,11 @@ struct vcpu {
     word_t regs[seL4_VCPUReg_Num];
     bool_t vppi_masked[n_VPPIEventIRQ];
 #ifdef CONFIG_VTIMER_UPDATE_VOFFSET
-    word_t vcpu_padding;
+    /* word_t vcpu_padding; */
     /* vTimer is 8-bytes wide and has the same 8-byte alignment requirement.
-     * If the sum of n_VPPIEventIRQ and seL4_VCPUReg_Num is even, we do not need
-     * extra padding. If the sum is odd we do. It currently is odd, so the extra
-     * padding above is necessary for the struct to remain packed on 32 bit
+     * If the sum of n_VPPIEventIRQ and seL4_VCPUReg_Num is odd, we do not need
+     * extra padding. If the sum is even we do. It currently is odd, so the extra
+     * padding above is unnecessary for the struct to remain packed on 32 bit
      * platforms.
      */
     struct vTimer virtTimer;
@@ -90,6 +90,10 @@ struct vcpu {
 };
 typedef struct vcpu vcpu_t;
 compile_assert(vcpu_size_correct, sizeof(struct vcpu) <= BIT(VCPU_SIZE_BITS))
+#ifdef CONFIG_VTIMER_UPDATE_VOFFSET
+compile_assert(vcpu_virt_timer_alignment_valid,
+               (seL4_VCPUReg_Num + n_VPPIEventIRQ) % 2 == 1)
+#endif
 
 void VGICMaintenance(void);
 void handleVCPUFault(word_t hsr);

include/arch/arm/armv/armv7-a/armv/vcpu.h

@@ -296,6 +296,18 @@ static inline void set_cntv_ctl(word_t val)
     MCR(CNTV_CTL, val);
 }
 
+static inline word_t get_cntkctl(void)
+{
+    word_t ret = 0;
+    MRC(CNTKCTL, ret);
+    return ret;
+}
+
+static inline void set_cntkctl(word_t val)
+{
+    MCR(CNTKCTL, val);
+}
+
 static inline word_t get_vmpidr(void)
 {
     word_t ret = 0;
@@ -484,6 +496,8 @@ static word_t vcpu_hw_read_reg(word_t reg_index)
         return get_cntv_off_high();
     case seL4_VCPUReg_CNTVOFFlow:
         return get_cntv_off_low();
+    case seL4_VCPUReg_CNTKCTL:
+        return get_cntkctl();
     case seL4_VCPUReg_VMPIDR:
         return get_vmpidr();
     default:
@@ -619,6 +633,9 @@ static void vcpu_hw_write_reg(word_t reg_index, word_t reg)
     case seL4_VCPUReg_CNTVOFFlow:
         set_cntv_off_low(reg);
         break;
+    case seL4_VCPUReg_CNTKCTL:
+        set_cntkctl(reg);
+        break;
     case seL4_VCPUReg_VMPIDR:
         set_vmpidr(reg);
         break;
@@ -853,6 +870,7 @@ static inline bool_t vcpu_reg_saved_when_disabled(word_t field)
     case seL4_VCPUReg_CNTV_CVALlow:
     case seL4_VCPUReg_CNTVOFFhigh:
     case seL4_VCPUReg_CNTVOFFlow:
+    case seL4_VCPUReg_CNTKCTL:
         return true;
     default:
         return false;

libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/constants.h

@@ -117,6 +117,7 @@ typedef enum {
     seL4_VCPUReg_CNTV_CVALlow,
     seL4_VCPUReg_CNTVOFFhigh,
     seL4_VCPUReg_CNTVOFFlow,
+    seL4_VCPUReg_CNTKCTL,
     seL4_VCPUReg_Num,
     SEL4_FORCE_LONG_ENUM(seL4_VCPUReg),
 } seL4_VCPUReg;

src/drivers/timer/generic_timer.c

@@ -71,7 +71,6 @@ static void save_virt_timer(vcpu_t *vcpu)
     vcpu_save_reg(vcpu, seL4_VCPUReg_CNTV_CVAL);
     vcpu_save_reg(vcpu, seL4_VCPUReg_CNTVOFF);
     vcpu_save_reg(vcpu, seL4_VCPUReg_CNTKCTL_EL1);
-    check_export_arch_timer();
 #else
     uint64_t cval = get_cntv_cval_64();
     uint64_t cntvoff = get_cntv_off_64();
@@ -79,7 +78,9 @@ static void save_virt_timer(vcpu_t *vcpu)
     vcpu_write_reg(vcpu, seL4_VCPUReg_CNTV_CVALlow, (word_t)cval);
     vcpu_write_reg(vcpu, seL4_VCPUReg_CNTVOFFhigh, (word_t)(cntvoff >> 32));
     vcpu_write_reg(vcpu, seL4_VCPUReg_CNTVOFFlow, (word_t)cntvoff);
+    vcpu_save_reg(vcpu, seL4_VCPUReg_CNTKCTL);
 #endif
+    check_export_arch_timer();
 #ifdef CONFIG_VTIMER_UPDATE_VOFFSET
     /* Save counter value at the time the vcpu is disabled */
     vcpu->virtTimer.last_pcount = read_cntpct();
@@ -97,6 +98,7 @@ static void restore_virt_timer(vcpu_t *vcpu)
     uint32_t cval_low = vcpu_read_reg(vcpu, seL4_VCPUReg_CNTV_CVALlow);
     uint64_t cval = ((uint64_t)cval_high << 32) | (uint64_t) cval_low;
     set_cntv_cval_64(cval);
+    vcpu_restore_reg(vcpu, seL4_VCPUReg_CNTKCTL);
 #endif
 
     /* Set virtual timer offset */