From 65a1b457a4ba3e72838434a68c5ce9889d3ce406 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 3 Mar 2023 16:26:40 +1100 Subject: [PATCH] make physBase a static inline function For verification flexible w.r.t kernel placement in physical memory, we need to relate physBase as a named constant to its abstract equivalent. Unfortunately, apart from enums, the C programming language does not have real constants. The C parser follows the C standard and requires enums constants to be storable as int, meaning without major overhaul enums are not sufficient for storing word_t-sized memory addresses. Since the linker scripts can't deal with static inline functions in the constants they need (KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE), we provide the following preprocessor definitions for the linker specifically: * PHYS_BASE_RAW (the numerical value returned by physBase()) * KERNEL_ELF_BASE_RAW * KERNEL_ELF_PADDR_BASE_RAW Signed-off-by: Rafal Kolanski --- include/arch/arm/arch/32/mode/hardware.h | 6 +++++- include/arch/arm/arch/64/mode/hardware.h | 6 +++++- include/arch/riscv/arch/32/mode/hardware.h | 6 +++++- include/arch/riscv/arch/64/mode/hardware.h | 6 +++++- .../plat/pc99/plat/32/plat_mode/machine/hardware.h | 4 ++++ .../plat/pc99/plat/64/plat_mode/machine/hardware.h | 4 ++++ src/arch/arm/32/kernel/vspace.c | 6 +++--- src/arch/arm/common_arm.lds | 4 ++-- src/arch/riscv/common_riscv.lds | 4 ++-- src/plat/pc99/linker.lds | 4 ++-- tools/hardware/outputs/c_header.py | 11 ++++++++++- 11 files changed, 47 insertions(+), 14 deletions(-) diff --git a/include/arch/arm/arch/32/mode/hardware.h b/include/arch/arm/arch/32/mode/hardware.h index 053a8df33..91fcda347 100644 --- a/include/arch/arm/arch/32/mode/hardware.h +++ b/include/arch/arm/arch/32/mode/hardware.h @@ -54,7 +54,7 @@ /* The first physical address to map into the kernel's physical memory * window */ -#define PADDR_BASE physBase +#define PADDR_BASE physBase() /* The base address in virtual memory to use for the 1:1 physical memory * mapping */ @@ -70,9 +70,13 @@ /* The physical memory address to use for mapping the kernel ELF */ #define KERNEL_ELF_PADDR_BASE PADDR_BASE +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_PADDR_BASE_RAW PHYS_BASE_RAW /* The base address in virtual memory to use for the kernel ELF mapping */ #define KERNEL_ELF_BASE (USER_TOP + (KERNEL_ELF_PADDR_BASE & MASK(22))) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_BASE_RAW (USER_TOP + (KERNEL_ELF_PADDR_BASE_RAW & MASK(22))) /* This is a page table mapping at the end of the virtual address space * to map objects with 4KiB pages rather than 4MiB large pages. */ diff --git a/include/arch/arm/arch/64/mode/hardware.h b/include/arch/arm/arch/64/mode/hardware.h index cf99d6e65..caaa6d582 100644 --- a/include/arch/arm/arch/64/mode/hardware.h +++ b/include/arch/arm/arch/64/mode/hardware.h @@ -186,10 +186,14 @@ #endif /* The physical memory address to use for mapping the kernel ELF */ -#define KERNEL_ELF_PADDR_BASE physBase +#define KERNEL_ELF_PADDR_BASE physBase() +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_PADDR_BASE_RAW PHYS_BASE_RAW /* The base address in virtual memory to use for the kernel ELF mapping */ #define KERNEL_ELF_BASE (PPTR_BASE_OFFSET + KERNEL_ELF_PADDR_BASE) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_BASE_RAW (PPTR_BASE_OFFSET + KERNEL_ELF_PADDR_BASE_RAW) /* This is a page table mapping at the end of the virtual address space * to map objects with 4KiB pages rather than 4MiB large pages. */ diff --git a/include/arch/riscv/arch/32/mode/hardware.h b/include/arch/riscv/arch/32/mode/hardware.h index 8b858f780..b6c01a2d3 100644 --- a/include/arch/riscv/arch/32/mode/hardware.h +++ b/include/arch/riscv/arch/32/mode/hardware.h @@ -31,7 +31,7 @@ /* The first physical address to map into the kernel's physical memory * window */ -#define PADDR_BASE physBase +#define PADDR_BASE physBase() /* The base address in virtual memory to use for the 1:1 physical memory * mapping */ @@ -52,9 +52,13 @@ * be on a 1gb boundary as we currently require being able to creating a mapping to this address * as the largest frame size */ #define KERNEL_ELF_PADDR_BASE UL_CONST(0x84000000) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_PADDR_BASE_RAW KERNEL_ELF_PADDR_BASE /* The base address in virtual memory to use for the kernel ELF mapping */ #define KERNEL_ELF_BASE UL_CONST(0xFF800000) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_BASE_RAW KERNEL_ELF_BASE /* The base address in virtual memory to use for the kernel device * mapping region. These are mapped in the kernel page table. */ diff --git a/include/arch/riscv/arch/64/mode/hardware.h b/include/arch/riscv/arch/64/mode/hardware.h index e189948c5..d76cdab39 100644 --- a/include/arch/riscv/arch/64/mode/hardware.h +++ b/include/arch/riscv/arch/64/mode/hardware.h @@ -92,10 +92,14 @@ /* This represents the physical address that the kernel image will be linked to. This needs to * be on a 1gb boundary as we currently require being able to creating a mapping to this address * as the largest frame size */ -#define KERNEL_ELF_PADDR_BASE (physBase + UL_CONST(0x4000000)) +#define KERNEL_ELF_PADDR_BASE (physBase() + UL_CONST(0x4000000)) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_PADDR_BASE_RAW (PHYS_BASE_RAW + UL_CONST(0x4000000)) /* The base address in virtual memory to use for the kernel ELF mapping */ #define KERNEL_ELF_BASE (PPTR_TOP + (KERNEL_ELF_PADDR_BASE & MASK(30))) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_BASE_RAW (PPTR_TOP + (KERNEL_ELF_PADDR_BASE_RAW & MASK(30))) /* The base address in virtual memory to use for the kernel device * mapping region. These are mapped in the kernel page table. */ diff --git a/include/plat/pc99/plat/32/plat_mode/machine/hardware.h b/include/plat/pc99/plat/32/plat_mode/machine/hardware.h index 6e3517aaf..d36daa4dc 100644 --- a/include/plat/pc99/plat/32/plat_mode/machine/hardware.h +++ b/include/plat/pc99/plat/32/plat_mode/machine/hardware.h @@ -75,9 +75,13 @@ /* The physical memory address to use for mapping the kernel ELF */ #define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_PADDR_BASE_RAW KERNEL_ELF_PADDR_BASE /* The base address in virtual memory to use for the kernel ELF mapping */ #define KERNEL_ELF_BASE (PPTR_BASE + KERNEL_ELF_PADDR_BASE) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_BASE_RAW (PPTR_BASE + KERNEL_ELF_PADDR_BASE_RAW) /* The base address in virtual memory to use for the kernel device * mapping region. These are mapped in the kernel page table. */ diff --git a/include/plat/pc99/plat/64/plat_mode/machine/hardware.h b/include/plat/pc99/plat/64/plat_mode/machine/hardware.h index 1be95e558..e530a7e82 100644 --- a/include/plat/pc99/plat/64/plat_mode/machine/hardware.h +++ b/include/plat/pc99/plat/64/plat_mode/machine/hardware.h @@ -88,9 +88,13 @@ /* The physical memory address to use for mapping the kernel ELF */ #define KERNEL_ELF_PADDR_BASE UL_CONST(0x00100000) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_PADDR_BASE_RAW KERNEL_ELF_PADDR_BASE /* Kernel mapping starts directly after the physical memory window */ #define KERNEL_ELF_BASE (PPTR_TOP + KERNEL_ELF_PADDR_BASE) +/* For use by the linker (only integer constants allowed) */ +#define KERNEL_ELF_BASE_RAW (PPTR_TOP + KERNEL_ELF_PADDR_BASE_RAW) /* Put the kernel devices at the very beginning of the top * 1GB. This means they are precisely after the kernel binary diff --git a/src/arch/arm/32/kernel/vspace.c b/src/arch/arm/32/kernel/vspace.c index 4e0b02ccc..4f57027c0 100644 --- a/src/arch/arm/32/kernel/vspace.c +++ b/src/arch/arm/32/kernel/vspace.c @@ -203,7 +203,7 @@ BOOT_CODE void map_kernel_window(void) /* mapping of KERNEL_ELF_BASE (virtual address) to kernel's * KERNEL_ELF_PHYS_BASE */ /* up to end of virtual address space minus 16M using 16M frames */ - phys = physBase; + phys = physBase(); idx = PPTR_BASE >> pageBitsForSize(ARMSection); while (idx < BIT(PD_INDEX_BITS) - SECTIONS_PER_SUPER_SECTION) { @@ -319,7 +319,7 @@ BOOT_CODE void map_kernel_window(void) } /* mapping of PPTR_BASE (virtual address) to kernel's physBase */ /* up to end of virtual address space minus 2M using 2M frames */ - phys = physBase; + phys = physBase(); for (; idx < BIT(PT_INDEX_BITS) - 1; idx++) { pde = pdeS1_pdeS1_section_new( 0, /* Executable */ @@ -2469,7 +2469,7 @@ static exception_t decodeARMFrameInvocation(word_t invLabel, word_t length, #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT /* Don't let applications flush outside of the kernel window */ - if (pstart < physBase || ((end - start) + pstart) > PADDR_TOP) { + if (pstart < physBase() || ((end - start) + pstart) > PADDR_TOP) { userError("Page Flush: Overlaps kernel region."); current_syscall_error.type = seL4_IllegalOperation; return EXCEPTION_SYSCALL_ERROR; diff --git a/src/arch/arm/common_arm.lds b/src/arch/arm/common_arm.lds index 248110795..72f69c453 100644 --- a/src/arch/arm/common_arm.lds +++ b/src/arch/arm/common_arm.lds @@ -12,11 +12,11 @@ ENTRY(_start) -KERNEL_OFFSET = KERNEL_ELF_BASE - KERNEL_ELF_PADDR_BASE; +KERNEL_OFFSET = KERNEL_ELF_BASE_RAW - KERNEL_ELF_PADDR_BASE_RAW; SECTIONS { - . = KERNEL_ELF_BASE; + . = KERNEL_ELF_BASE_RAW; .boot . : AT(ADDR(.boot) - KERNEL_OFFSET) { diff --git a/src/arch/riscv/common_riscv.lds b/src/arch/riscv/common_riscv.lds index 4d45bc09b..8d09ccc6f 100644 --- a/src/arch/riscv/common_riscv.lds +++ b/src/arch/riscv/common_riscv.lds @@ -16,11 +16,11 @@ ENTRY(_start) #include #include -KERNEL_OFFSET = KERNEL_ELF_BASE - KERNEL_ELF_PADDR_BASE; +KERNEL_OFFSET = KERNEL_ELF_BASE_RAW - KERNEL_ELF_PADDR_BASE_RAW; SECTIONS { - . = KERNEL_ELF_BASE; + . = KERNEL_ELF_BASE_RAW; .boot.text . : AT(ADDR(.boot.text) - KERNEL_OFFSET) { diff --git a/src/plat/pc99/linker.lds b/src/plat/pc99/linker.lds index 29072c31d..3fcb28600 100644 --- a/src/plat/pc99/linker.lds +++ b/src/plat/pc99/linker.lds @@ -10,8 +10,8 @@ ENTRY(_start) -KLOAD_PADDR = KERNEL_ELF_PADDR_BASE; -KLOAD_VADDR = KERNEL_ELF_BASE; +KLOAD_PADDR = KERNEL_ELF_PADDR_BASE_RAW; +KLOAD_VADDR = KERNEL_ELF_BASE_RAW; /* WARNING: constants also defined in plat/machine/hardware.h */ #if defined(CONFIG_ARCH_IA32) diff --git a/tools/hardware/outputs/c_header.py b/tools/hardware/outputs/c_header.py index 63fb990c4..9cab57ef0 100644 --- a/tools/hardware/outputs/c_header.py +++ b/tools/hardware/outputs/c_header.py @@ -27,7 +27,7 @@ HEADER_TEMPLATE = '''/* #pragma once -#define physBase {{ "0x{:x}".format(physBase) }} +#define PHYS_BASE_RAW {{ "0x{:x}".format(physBase) }} #ifndef __ASSEMBLER__ @@ -36,6 +36,15 @@ HEADER_TEMPLATE = '''/* #include /* for BOOT_RODATA */ #include /* for p_region_t, kernel_frame_t (arch/types.h) */ +/* Wrap raw physBase location constant to give it a symbolic name in C that's + * visible to verification. This is necessary as there are no real constants + * in C except enums, and enums constants must fit in an int. + */ +static inline CONST word_t physBase(void) +{ + return PHYS_BASE_RAW; +} + /* INTERRUPTS */ {% for irq in kernel_irqs %} /* {{ irq.desc }} */