make kernel device frame handling more generic

The structure actually describes kernel frames and not kernel devices.
In most of the cases a peripherals will fit into one page, but some can
need more pages. On some platform there are no kernel devices at all.
Provides the macro NUM_KERNEL_DEVICE_FRAMES as simple way to find out if
there are mapping that hides the corner cases. This eventually allows
implementing a generic handling even on RISC-V without much overhead, so
the hack for HiFive/Spike can be removed.

Signed-off-by: Axel Heider <axelheider@gmx.de>

include/arch/arm/arch/bootinfo.h

@@ -14,8 +14,9 @@
 
 /* The maximum number of reserved regions is:
  * - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
- * - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
+ * - 1 for each kernel frame (NUM_KERNEL_DEVICE_FRAMES, there might be none)
  * - 1 for each mode-reserved region. (MODE_RESERVED)
  * - 1 each for kernel, dtb, and user image. (3)
  */
-#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + NUM_KERNEL_DEVICE_FRAMES + \
+                          MODE_RESERVED + 3)

include/arch/riscv/arch/bootinfo.h

@@ -10,13 +10,9 @@
 
 /* The maximum number of reserved regions is:
  * - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
- * - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
+ * - 1 for each kernel region (NUM_KERNEL_DEVICE_FRAMES, there might be none)
  * - 1 for each mode-reserved region. (MODE_RESERVED)
  * - 1 each for kernel, dtb, and user image. (3)
  */
-#ifdef CONFIG_PLAT_HIFIVE
+#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + NUM_KERNEL_DEVICE_FRAMES + \
-#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
+                          MODE_RESERVED + 3)
-#else
-/* spike has no devices, and ARRAY_SIZE(NULL) is invalid. */
-#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + MODE_RESERVED + 3)
-#endif

src/arch/arm/machine/hardware.c

@@ -21,8 +21,12 @@ void setNextPC(tcb_t *thread, word_t v)
 
 BOOT_CODE void map_kernel_devices(void)
 {
-    for (int i = 0; i < ARRAY_SIZE(kernel_devices); i++) {
+    /* If there are no kernel device frames at all, then kernel_device_frames is
-        const kernel_frame_t *frame = &kernel_devices[i];
+     * NULL. Thus we can't use ARRAY_SIZE(kernel_device_frames) here directly,
+     * but have to use NUM_KERNEL_DEVICE_FRAMES that is defined accordingly.
+     */
+    for (int i = 0; i < NUM_KERNEL_DEVICE_FRAMES; i++) {
+        const kernel_frame_t *frame = &kernel_device_frames[i];
         /* all frames are supposed to describe device memory, so they should
          * never be marked as executable.
          */

src/arch/riscv/machine/hardware.c

@@ -40,12 +40,12 @@ void setNextPC(tcb_t *thread, word_t v)
 
 BOOT_CODE void map_kernel_devices(void)
 {
-    if (kernel_devices == NULL) {
+    /* If there are no kernel device frames at all, then kernel_device_frames is
-        return;
+     * NULL. Thus we can't use ARRAY_SIZE(kernel_device_frames) here directly,
-    }
+     * but have to use NUM_KERNEL_DEVICE_FRAMES that is defined accordingly.
-
+     */
-    for (int i = 0; i < (sizeof(kernel_devices) / sizeof(kernel_frame_t)); i++) {
+    for (int i = 0; i < NUM_KERNEL_DEVICE_FRAMES; i++) {
-        const kernel_frame_t *frame = &kernel_devices[i];
+        const kernel_frame_t *frame = &kernel_device_frames[i];
         map_kernel_frame(frame->paddr, frame->pptr, VMKernelOnly);
         if (!frame->userAvailable) {
             reserve_region((p_region_t) {

tools/hardware/outputs/c_header.py

@@ -61,7 +61,7 @@ HEADER_TEMPLATE = '''/*
 
 #ifndef __ASSEMBLER__
 {% if len(kernel_regions) > 0 %}
-static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
+static const kernel_frame_t BOOT_RODATA kernel_device_frames[] = {
     {% for group in kernel_regions %}
     {% if group.has_macro() %}
     {{ group.get_macro() }}
@@ -88,19 +88,30 @@ static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
     {% endif %}
     {% endfor %}
 };
+/* Elements in kernel_device_frames may be enabled in specific configurations
+ * only, but the ARRAY_SIZE() macro will automatically take care of this.
+ * However, one corner case remains unsolved where all elements are disabled
+ * and this becomes an empty array effectively. Then the C parser used in the
+ * formal verification process will fail, because it follows the strict C rules
+ * which do not allow empty arrays. Luckily, we have not met this case yet...
+ */
+#define NUM_KERNEL_DEVICE_FRAMES ARRAY_SIZE(kernel_device_frames)
 {% else %}
-static const kernel_frame_t BOOT_RODATA *const kernel_devices = NULL;
+/* The C parser used for formal verification process follows strict C rules,
+ * which do not allow empty arrays. Thus this is defined as NULL.
+ */
+static const kernel_frame_t BOOT_RODATA *const kernel_device_frames = NULL;
+#define NUM_KERNEL_DEVICE_FRAMES 0
 {% endif %}
 
 /* PHYSICAL MEMORY */
 static const p_region_t BOOT_RODATA avail_p_regs[] = {
     {% for reg in physical_memory %}
+    /* {{ reg.owner.path }} */
     {
-        /* {{ reg.owner.path }} */
         .start = {{ "0x{:x}".format(reg.base) }},
         .end   = {{ "0x{:x}".format(reg.base + reg.size) }}
     },
-
     {% endfor %}
 };