aarch32: tune user_context struct for verification

Verification requires packed structures for reasoning (no implicit
padding).

The FPU context starts with 64-bit words, which the C parser assumes
have 8-byte alignment. Unfortunately, for this version of the kernel,
aarch32 has an odd number of word_t (32-bit) registers, resulting in an
extra word of implicit padding.

This type of manual padding is naturally fragile and will break as soon
as a user register is added or removed from the user context.

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>

configs/ARM_verified.cmake

@@ -15,7 +15,9 @@
 include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
 cmake_script_build_kernel()
 
-set(KernelPlatform "imx6" CACHE STRING "")
+set(KernelPlatform "imx8mm-evk" CACHE STRING "")
+set(KernelSel4Arch "aarch32" CACHE STRING "")
+set(KernelAArch32FPUEnableContextSwitch ON CACHE BOOL "")
 set(KernelVerificationBuild ON CACHE BOOL "")
 set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
 set(KernelMaxNumNodes "1" CACHE STRING "")

include/arch/arm/arch/32/mode/machine/registerset.h

@@ -232,6 +232,12 @@ typedef struct user_fpu_state {
  */
 struct user_context {
     word_t registers[n_contextRegisters];
+    /* user_fpu_state_t is 64-bit aligned, and we have an odd number of
+     * registers in the user context. This results in a verified configuration
+     * with padding. Verification requires packed structures without implicit
+     * padding, so we pad manually.
+     */
+    word_t odd_n_contextRegisters_padding;
 #ifdef ARM_BASE_CP14_SAVE_AND_RESTORE
     user_breakpoint_state_t breakpointState;
 #endif /* CONFIG_HARDWARE_DEBUG_API */

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

@@ -257,6 +257,8 @@ static inline interrupt_t getActiveIRQ(void)
  * seL4 expects two states: active->inactive.
  * We ignore the active state in GIC to conform
  */
+/** MODIFIES: phantom_machine_state */
+/** DONT_TRANSLATE */
 static inline bool_t isIRQPending(void)
 {
     uint32_t val = 0;

src/arch/arm/32/object/objecttype.c

@@ -566,12 +566,14 @@ exception_t Arch_decodeInvocation(word_t invLabel, word_t length, cptr_t cptr,
 
 void
 Arch_prepareThreadDelete(tcb_t * thread) {
+#ifdef CONFIG_HAVE_FPU
+    fpuThreadDelete(thread);
+#endif
+
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
     if (thread->tcbArch.tcbVCPU) {
         dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread);
     }
-#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
-    /* No action required on ARM. */
 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
 }
 

src/arch/arm/64/object/objecttype.c

@@ -415,6 +415,10 @@ exception_t Arch_decodeInvocation(word_t label, word_t length, cptr_t cptr,
 
 void
 Arch_prepareThreadDelete(tcb_t * thread) {
+#ifdef CONFIG_HAVE_FPU
+    fpuThreadDelete(thread);
+#endif
+
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
     if (thread->tcbArch.tcbVCPU) {
         dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread);

src/arch/arm/config.cmake

@@ -160,7 +160,7 @@ config_option(
         operations in a multithreading environment, instead of relying on \
         software emulation of FPU/VFP from the C library (e.g. mfloat-abi=soft)."
     DEFAULT ON
-    DEPENDS "KernelSel4ArchAarch32;NOT KernelArchArmV6;NOT KernelVerificationBuild"
+    DEPENDS "KernelSel4ArchAarch32;NOT KernelArchArmV6"
     DEFAULT_DISABLED OFF
 )
 

src/arch/arm/machine/gic_v3.c

@@ -313,9 +313,9 @@ void setIRQTrigger(irq_t irq, bool_t trigger)
     }
 
     if (trigger) {
-        icfgr |= (0b10 << bit);
+        icfgr |= (2 << bit);
     } else {
-        icfgr &= ~(0b11 << bit);
+        icfgr &= ~(3 << bit);
     }
 
     if (HW_IRQ_IS_PPI(hw_irq)) {