From da0aad03309f20213dc31c8f15713352a2baf9ab Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Mon, 5 Jul 2021 04:36:47 +0200 Subject: [PATCH] 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 --- include/arch/arm/arch/bootinfo.h | 5 +++-- include/arch/riscv/arch/bootinfo.h | 10 +++------- src/arch/arm/machine/hardware.c | 8 ++++++-- src/arch/riscv/machine/hardware.c | 12 ++++++------ tools/hardware/outputs/c_header.py | 19 +++++++++++++++---- 5 files changed, 33 insertions(+), 21 deletions(-) diff --git a/include/arch/arm/arch/bootinfo.h b/include/arch/arm/arch/bootinfo.h index deb567995..dd1424edf 100644 --- a/include/arch/arm/arch/bootinfo.h +++ b/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) diff --git a/include/arch/riscv/arch/bootinfo.h b/include/arch/riscv/arch/bootinfo.h index 394f4d64b..2cf129991 100644 --- a/include/arch/riscv/arch/bootinfo.h +++ b/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 + ARRAY_SIZE(kernel_devices) + 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 +#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + NUM_KERNEL_DEVICE_FRAMES + \ + MODE_RESERVED + 3) diff --git a/src/arch/arm/machine/hardware.c b/src/arch/arm/machine/hardware.c index a84a12583..427ec4485 100644 --- a/src/arch/arm/machine/hardware.c +++ b/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++) { - const kernel_frame_t *frame = &kernel_devices[i]; + /* If there are no kernel device frames at all, then kernel_device_frames is + * 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. */ diff --git a/src/arch/riscv/machine/hardware.c b/src/arch/riscv/machine/hardware.c index 9775e9ce9..eb86f9b83 100644 --- a/src/arch/riscv/machine/hardware.c +++ b/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) { - return; - } - - for (int i = 0; i < (sizeof(kernel_devices) / sizeof(kernel_frame_t)); i++) { - const kernel_frame_t *frame = &kernel_devices[i]; + /* If there are no kernel device frames at all, then kernel_device_frames is + * 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]; map_kernel_frame(frame->paddr, frame->pptr, VMKernelOnly); if (!frame->userAvailable) { reserve_region((p_region_t) { diff --git a/tools/hardware/outputs/c_header.py b/tools/hardware/outputs/c_header.py index 58d157b71..1c2d0c70d 100644 --- a/tools/hardware/outputs/c_header.py +++ b/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 %} };