rework physical address space limits

- add KernelPhysAddressSpaceBits and PHYS_ADDR_SPACE_BITS
- add KernelPhysAddrTop and CONFIG_PHYS_ADDR_TOP
- make CONFIG_PADDR_USER_DEVICE_TOP an alias
- remove KernelPaddrUserTop from CMake
- remove KernelArmPASizeBits40 from CMake
- remove KernelArmPASizeBits44 from CMake
- improve comment why the last page is always excluded

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

CHANGES

@@ -44,6 +44,8 @@ Upcoming release: BREAKING
   This change is reflected in the definition of the seL4_UserTop constant that holds the largest user virtual address.
 * aarch32 VM fault messages now deliver original (untranslated) faulting IP in a hypervisor context, matching
   aarch64 behaviour.
+* Added CONFIG_PHYS_ADDR_SPACE_BITS (KernelPhysAddressSpaceBits), from this CONFIG_PHYS_ADDR_TOP (KernelPhysAddrTop)
+  gets derived in the generic CMake files. PADDR_USER_DEVICE_TOP (KernelPaddrUserTop) is kept as an alias.
 
 ## Upgrade Notes
 ---

config.cmake

@@ -202,7 +202,7 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
                 --compat-strings-out "${compatibility_outfile}" --c-header --header-out
                 "${device_dest}" --hardware-config "${config_file}" --hardware-schema
                 "${config_schema}" --yaml --yaml-out "${platform_yaml}" --sel4arch
-                "${KernelSel4Arch}" --addrspace-max "${KernelPaddrUserTop}"
+                "${KernelSel4Arch}" --phys-addr-space-bits "${KernelPhysAddressSpaceBits}"
             RESULT_VARIABLE error
         )
         if(error)
@@ -224,7 +224,13 @@ endif()
 
 # Enshrine common variables in the config
 config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}")
-config_set(KernelPaddrUserTop PADDR_USER_DEVICE_TOP "${KernelPaddrUserTop}")
+
+config_set(KernelPhysAddressSpaceBits PHYS_ADDR_SPACE_BITS "${KernelPhysAddressSpaceBits}")
+# Calculate the highest address that this still in the physical address space
+# here in CMake, so we derive integers that are inside the target's C inter
+# range.
+math(EXPR KernelPhysAddrTop "(1 << ${KernelPhysAddressSpaceBits}) - 1")
+config_set(KernelPhysAddrTop PHYS_ADDR_TOP "SEL4_WORD_CONST(${KernelPhysAddrTop})")
 
 # System parameters
 config_string(

include/arch/arm/arch/64/mode/hardware.h

@@ -215,8 +215,8 @@
    asserts check that the kernel config won't lead to UTs being created that aren't
    representable. */
 #ifndef __ASSEMBLER__
-compile_assert(ut_max_less_than_cannonical, CONFIG_PADDR_USER_DEVICE_TOP <= BIT(47));
+compile_assert(ut_max_less_than_cannonical, CONFIG_PHYS_ADDR_SPACE_BITS <= 47);
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-compile_assert(ut_max_is_cannonical, (PPTR_BASE + CONFIG_PADDR_USER_DEVICE_TOP) <= BIT(48));
+compile_assert(ut_max_is_cannonical, PPTR_BASE + CONFIG_PHYS_ADDR_TOP <= BIT(48));
 #endif
 #endif

include/config.h

@@ -13,8 +13,17 @@
 #define ENABLE_SMP_SUPPORT
 #endif
 
+/* keep some names for legacy compatibility */
+#ifdef CONFIG_ARCH_ARM
+#if (CONFIG_PHYS_ADDR_SPACE_BITS == 40)
+#define CONFIG_ARM_PA_SIZE_BITS_40 1
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
-#ifdef CONFIG_ARM_PA_SIZE_BITS_40
-#define AARCH64_VSPACE_S2_START_L1
-#endif
-#endif
+#define AARCH64_VSPACE_S2_START_L1 CONFIG_AARCH64_VSPACE_S2_START_L1
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
+#elif (CONFIG_PHYS_ADDR_SPACE_BITS == 44)
+#define CONFIG_ARM_PA_SIZE_BITS_44 1
+#endif /* PHYS_ADDR_SPACE_BITS */
+#endif /* CONFIG_ARCH_ARM */
+
+/* CONFIG_PADDR_USER_DEVICE_TOP is no longer set by the CMake configuration. */
+#define CONFIG_PADDR_USER_DEVICE_TOP CONFIG_PHYS_ADDR_TOP

src/arch/arm/config.cmake

@@ -10,39 +10,75 @@ if(KernelArchARM)
     set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES pde_C)
 endif()
 
-set(KernelArmPASizeBits40 OFF)
-set(KernelArmPASizeBits44 OFF)
-if(KernelArmCortexA35)
+if(KernelArmCortexA7)
+    # nothing special
+elseif(KernelArmCortexA8)
+    # nothing special
+elseif(KernelArmCortexA9)
+    # nothing special
+elseif(KernelArmCortexA15)
+    # supports a 40-bit physical address space via LPAE
+elseif(KernelArmCortexA17)
+    # supports a 40-bit physical address space via LPAE
+elseif(KernelArmCortexA35)
     set(KernelArmICacheVIPT ON)
-    set(KernelArmPASizeBits40 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 40)")
+    set(KernelPhysAddressSpaceBits 40)
 elseif(KernelArmCortexA53)
     set(KernelArmICacheVIPT ON)
-    set(KernelArmPASizeBits40 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 40)")
+    set(KernelPhysAddressSpaceBits 40)
 elseif(KernelArmCortexA55)
     set(KernelArmICacheVIPT ON)
-    set(KernelArmPASizeBits40 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 40)")
+    set(KernelPhysAddressSpaceBits 40)
 elseif(KernelArmCortexA57)
-    set(KernelArmPASizeBits44 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 44)")
+    set(KernelPhysAddressSpaceBits 44)
+#elseif(KernelArmCortexA65)
+#    set(KernelPhysAddressSpaceBits 44)
 elseif(KernelArmCortexA72)
-    # For Cortex-A72 in AArch64 state, the physical address range is 44 bits
-    # (https://developer.arm.com/documentation/100095/0001/memory-management-unit/about-the-mmu)
-    set(KernelArmPASizeBits44 ON)
-    math(EXPR KernelPaddrUserTop "(1 << 44)")
+    # https://developer.arm.com/documentation/100095/0003/Memory-Management-Unit/About-the-MMU
+    set(KernelPhysAddressSpaceBits 44)
+#elseif(KernelArmCortexA73)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA75)
+#    set(KernelPhysAddressSpaceBits 44)
+#elseif(KernelArmCortexA76)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA77)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA78)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA78AE)
+#    set(KernelPhysAddressSpaceBits 48)
+#elseif(KernelArmCortexA510)
+#    set(KernelPhysAddressSpaceBits 40)
+#elseif(KernelArmCortexA710)
+#    set(KernelPhysAddressSpaceBits 40)
+else()
+    # In ARMv8, ID_AA64MMFR0_EL1.PARange gives the physical address space size,
+    # values are:
+    #   0:     32 bits (4 GB)
+    #   1:     36 bits (64 GB)
+    #   2:     40 bits (1 TB)
+    #   3:     42 bits (4 TB)
+    #   4:     44 bits (16 TB)
+    #   5:     48 bits (256 TB)
+    #   6:     52 bits (4 PB, added in Armv8.2-A, implies FEAT_LPA)
+    #   7-15:  reserved
+    # A general comparison table for can be found at
+    # https://developer.arm.com/-/media/Arm%20Developer%20Community/PDF/Cortex-A%20R%20M%20datasheets/Arm%20Cortex-A%20Comparison%20Table_v4.ashx
+    message(FATAL_ERROR "unsupported ARM core")
 endif()
-config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
-config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
+
 config_set(KernelArmICacheVIPT ARM_ICACHE_VIPT "${KernelArmICacheVIPT}")
 
+# In 32-bit mode (AARCH32) seL4 can handle a maximum physical address space of
+# 32 bits, even if the core supports LPAE that technically allows mapping pages
+# from larger addresses.
 if(KernelSel4ArchAarch32)
-    # 64-bit targets may be building in 32-bit mode,
-    # so make sure maximum paddr is 32-bit.
-    math(EXPR KernelPaddrUserTop "(1 << 32) - 1")
+    set(KernelPhysAddressSpaceBits 32)
 endif()
 
+config_set(KernelArmICacheVIPT ARM_ICACHE_VIPT "${KernelArmICacheVIPT}")
+
 include(src/arch/arm/armv/armv7-a/config.cmake)
 include(src/arch/arm/armv/armv8-a/config.cmake)
 
@@ -91,7 +127,7 @@ config_option(
 
 config_option(KernelArmGicV3 ARM_GIC_V3_SUPPORT "Build support for GICv3" DEFAULT OFF)
 
-if(KernelArmPASizeBits40 AND ARM_HYPERVISOR_SUPPORT)
+if((KernelPhysAddressSpaceBits EQUAL 40) AND ARM_HYPERVISOR_SUPPORT)
     config_set(KernelAarch64VspaceS2StartL1 AARCH64_VSPACE_S2_START_L1 "ON")
 else()
     config_set(KernelAarch64VspaceS2StartL1 AARCH64_VSPACE_S2_START_L1 "OFF")

src/arch/riscv/config.cmake

@@ -50,21 +50,25 @@ endif()
 
 if(KernelSel4ArchRiscV32)
     set(KernelPTLevels 2 CACHE STRING "" FORCE)
-endif()
-if(KernelPTLevels EQUAL 2)
-    if(KernelSel4ArchRiscV32)
-        # seL4 on RISCV32 uses 32-bit ints for addresses,
-        # so limit the maximum paddr to 32-bits.
-        math(EXPR KernelPaddrUserTop "(1 << 32) - 1")
+    # Actually, RV32 with Sv32 supports a 34-bit (16 GiByte) physical address
+    # space. However, we only support a 32-bit address space at the moment when
+    # targeting 32-bit architectures.
+    set(KernelPhysAddressSpaceBits 32)
+elseif(KernelSel4ArchRiscV64)
+    # The RISC-V privileged spec v1.12 defines that RV64 always uses a 56-bit
+    # physical address space.
+    if(KernelPTLevels EQUAL 3)
+        # structures.bf limits us to a 39-bit physical address space in Sv39
+        # mode with a 39-bit VA space and 3 page table levels
+        set(KernelPhysAddressSpaceBits 39)
     else()
-        math(EXPR KernelPaddrUserTop "1 << 34")
+        # Sv48: 48-bit VA space with 4 page table levels (unsupported)
+        # Sv57: 57-bit VA space with 5 page table levels (unsupported)
+        # Sv64: details still unclear
+        message(FATAL_ERROR "KernelPTLevels=${KernelPTLevels} is unsupported")
     endif()
-elseif(KernelPTLevels EQUAL 3)
-    # RISC-V technically supports 56-bit paddrs,
-    # but structures.bf limits us to using 39 of those bits.
-    math(EXPR KernelPaddrUserTop "1 << 39")
-elseif(KernelPTLevels EQUAL 4)
-    math(EXPR KernelPaddrUserTop "1 << 56")
+else()
+    message(FATAL_ERROR "unsuppored RISC-V architecture")
 endif()
 
 if(KernelRiscvExtD)

src/arch/x86/config.cmake

@@ -346,9 +346,9 @@ config_option(
 
 if(KernelSel4ArchIA32)
     set(KernelSetTLSBaseSelf ON)
-    math(EXPR KernelPaddrUserTop "0xffff0000")
+    set(KernelPhysAddressSpaceBits 32)
 else()
-    math(EXPR KernelPaddrUserTop "1 << 47")
+    set(KernelPhysAddressSpaceBits 47)
 endif()
 if(KernelSel4ArchX86_64 AND NOT KernelFSGSBaseInst)
     set(KernelSetTLSBaseSelf ON)

src/kernel/boot.c

@@ -666,9 +666,10 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap,
         start = ndks_boot.reserved[i].end;
     }
 
-    if (start < CONFIG_PADDR_USER_DEVICE_TOP) {
+    if (start < CONFIG_PHYS_ADDR_TOP) {
         region_t reg = paddr_to_pptr_reg((p_region_t) {
-            start, CONFIG_PADDR_USER_DEVICE_TOP
+            .start = start,
+            .end = CONFIG_PHYS_ADDR_TOP
         });
 
         if (!create_untypeds_for_region(root_cnode_cap, true, reg, first_untyped_slot)) {

src/plat/pc99/machine/hardware.c

@@ -17,16 +17,50 @@
 
 BOOT_CODE bool_t platAddDevices(void)
 {
-    /* remove the MSI region as poking at this is undefined and may allow for
-     * the user to generate arbitrary MSI interrupts. Only need to consider
-     * this if it would actually be in the user device region */
-    if (CONFIG_PADDR_USER_DEVICE_TOP > 0xFFFFFFF8) {
-        if (!reserve_region((p_region_t) {
-        (word_t)0xFFFFFFF8, (word_t)0xFFFFFFF8 + 8
-        })) {
+
+    /* The last 64 KiByte page of the physical address space is not allowed to
+     * be used to to prevent userland from exploiting a corner case. If e.g. a
+     * syscall is placed at the very last instruction, the hardware generates a
+     * return address of that address +2, which is non-canonical. The kernel
+     * loads that invalid address into sysret and this may cause undefined
+     * behavior eventually.
+     * See also https://sel4.atlassian.net/browse/SELFOUR-1179.
+     */
+    p_region_t p_reg_reserved = {
+        .start = ROUND_DOWN(CONFIG_PHYS_ADDR_TOP, 16),
+        .end   = CONFIG_PHYS_ADDR_TOP
+    };
+
+    if (!reserve_region(p_reg_reserved)) {
+        printf("ERROR: could not reserve last 64k of phys memory "
+               "[0x%"SEL4_PRIx_word": 0x%08"SEL4_PRIx_word"\n",
+               p_reg_reserved.start, p_reg_reserved.end);
+        return false;
+    }
+
+#ifndef CONFIG_ARCH_IA32
+
+    /* remove the 8 byte MSI region [0xfffffff8 - ffffffff] at the end of the
+     * 32-bit address range, as poking at this area is undefined and may allow
+     * for the user to generate arbitrary MSI interrupts. Only need to consider
+     * this if it would actually be in the user device region.
+     */
+    p_region_t p_reg_msi = {
+        .start = SEL4_WORD_CONST(0xfffffff8),
+        .end   = SEL4_WORD_CONST(0xffffffff)
+    };
+
+    if (CONFIG_PHYS_ADDR_TOP > p_reg_msi.start) {
+        if (!reserve_region(p_reg_msi)) {
+            printf("ERROR: could not reserve MSI region "
+                   "[0x%"SEL4_PRIx_word": 0x%08"SEL4_PRIx_word"\n",
+                   p_reg_msi.start, p_reg_msi.end);
             return false;
         }
     }
+
+#endif /* not CONFIG_ARCH_IA32 */
+
     return true;
 }
 

tools/hardware/config.py

@@ -17,9 +17,9 @@ class Config:
     ''' Abstract config class '''
     arch = 'unknown'
 
-    def __init__(self, sel4arch, addrspace_max):
+    def __init__(self, sel4arch, phys_addr_space_bits):
         self.sel4arch = sel4arch
-        self.addrspace_max = addrspace_max
+        self.phys_addr_space_bits = phys_addr_space_bits
 
     def get_kernel_phys_align(self) -> int:
         ''' Used to align the base of physical memory. Returns alignment size in bits. '''
@@ -41,6 +41,9 @@ def get_device_page_bits(self) -> int:
         '''
         return self.get_page_bits()
 
+    def get_phys_addr_space_bits(self) -> int:
+        ''' Return the physical address space in 2^n bits. '''
+        return self.phys_addr_space_bits
 
 class ARMConfig(Config):
     ''' Config class for ARM '''
@@ -70,14 +73,14 @@ def get_device_page_bits(self) -> int:
         raise ValueError('Unsupported sel4arch "{}" specified.'.format(self.sel4arch))
 
 
-def get_arch_config(sel4arch: str, addrspace_max: int) -> Config:
+def get_arch_config(sel4arch: str, phys_addr_space_bits: int) -> Config:
     ''' Return an appropriate Config object for the given architecture '''
 
     for (ctor, arch_list) in [
         (ARMConfig,   ['aarch32', 'aarch64', 'arm_hyp']),
         (RISCVConfig, ['riscv32', 'riscv64']),
     ]:
         if sel4arch in arch_list:
-            return ctor(sel4arch, addrspace_max)
+            return ctor(sel4arch, phys_addr_space_bits)
 
     raise ValueError('Unsupported sel4arch "{}" specified.'.format(sel4arch))

tools/hardware/utils/memory.py

@@ -129,7 +129,7 @@ def visitor(node: WrappedNode):
         Region(
             0,
             hardware.utils.align_down(
-                hw_yaml.config.addrspace_max,
+                2**hw_yaml.config.get_phys_addr_space_bits(),
                 hw_yaml.config.get_smallest_kernel_object_alignment()))
     }
 

tools/hardware_gen.py

@@ -49,7 +49,7 @@ def add_task_args(outputs: dict, parser: argparse.ArgumentParser):
 def main(args: argparse.Namespace):
     ''' Parse the DT and hardware config YAML and run each
     selected output method. '''
-    cfg = hardware.config.get_arch_config(args.sel4arch, args.addrspace_max)
+    cfg = hardware.config.get_arch_config(args.sel4arch, args.phys_addr_space_bits)
     parsed_dt = FdtParser(args.dtb)
     rules = yaml.load(args.hardware_config, Loader=yaml.FullLoader)
     schema = yaml.load(args.hardware_schema, Loader=yaml.FullLoader)
@@ -75,9 +75,9 @@ def main(args: argparse.Namespace):
                         required=True, type=argparse.FileType('r'))
     parser.add_argument('--sel4arch', help='seL4 architecture to generate for',
                         required=True)
-    parser.add_argument('--addrspace-max',
-                        help='maximum address that is available as device untyped', type=int, default=32)
-
+    parser.add_argument('--phys-addr-space-bits',
+                        help='size of the physical address space, which is available as device untyped',
+                        type=int, default=32)
     parser.add_argument('--enable-profiling', help='enable profiling',
                         action='store_const', const=True, default=False)