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 <rafal.kolanski@proofcraft.systems>

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. */

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. */

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. */

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. */

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. */

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

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;

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

src/arch/riscv/common_riscv.lds

@@ -16,11 +16,11 @@ ENTRY(_start)
 #include <sel4/plat/api/constants.h>
 #include <plat/machine/devices_gen.h>
 
-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)
     {

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)

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 <linker.h>         /* for BOOT_RODATA */
 #include <basic_types.h>    /* 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 }} */