switch ARM verified config to ZynqMP

ARM_verified.cmake (used for verification target "ARM") now targets
ZynqMP platform with FPU enabled.

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

configs/ARM_verified.cmake

@@ -1,21 +1,17 @@
 #!/usr/bin/env -S cmake -P
 #
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
+# Copyright 2020, Data61, 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)
+# SPDX-License-Identifier: GPL-2.0-only
 #
 
 # If this file is executed then build the kernel.elf and kernel_all_pp.c file
 include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
 cmake_script_build_kernel()
 
-set(KernelPlatform "imx6" CACHE STRING "")
+set(KernelPlatform "zynqmp" 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;

include/arch/arm/armv/armv8-a/32/armv/vcpu.h

@@ -0,0 +1 @@
+../../../armv7-a/armv/vcpu.h

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)) {

src/plat/zynqmp/config.cmake

@@ -26,6 +26,8 @@ if(KernelPlatformZynqmp)
         declare_seL4_arch(aarch32)
     elseif("${KernelSel4Arch}" STREQUAL aarch64)
         declare_seL4_arch(aarch64)
+    elseif("${KernelSel4Arch}" STREQUAL arm_hyp)
+        declare_seL4_arch(arm_hyp)
     else()
         fallback_declare_seL4_arch_default(aarch64)
     endif()
@@ -40,7 +42,12 @@ if(KernelPlatformZynqmp)
     if(NOT KernelPlatformUltra96)
         list(APPEND KernelDTSList "tools/dts/zynqmp.dts")
     endif()
+
+    if(KernelSel4ArchAarch32)
+        list(APPEND KernelDTSList "src/plat/zynqmp/overlay-zynqmp32.dts")
+    else()
         list(APPEND KernelDTSList "src/plat/zynqmp/overlay-zynqmp.dts")
+    endif()
 
     declare_default_headers(
         TIMER_FREQUENCY 100000000llu

src/plat/zynqmp/overlay-zynqmp32.dts

@@ -0,0 +1,22 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ */
+
+/ {
+    chosen {
+		seL4,elfloader-devices =
+		    "serial0",
+		    &{/psci};
+		seL4,kernel-devices =
+		    "serial0",
+		    &{/amba_apu@0/interrupt-controller@f9010000},
+		    &{/timer};
+    };
+
+	memory@0 {
+		device_type = "memory";
+		reg = < 0x00 0x00 0x00 0x80000000 >;
+	};
+};