libsel4: export seL4_IOPageTable{Index,Entry}Bits

This is useful for all x86 IOMMU work, which otherwise has
to duplicate the definitions of VTD_PT_INDEX_BITS in userspace
code. Follow the same pattern as many other existing code in
the libsel4 headers where the kernel depends on it.

Note we can't define seL4_IOPageTableBits in terms of Index + Entry
because the capDL tool does the c-preprocessor to make a YAML file
containing the constant, and it won't do evaluation.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

configs/AARCH64_stm32mp2_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2025, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
+
+set(KernelPlatform "stm32mp2" CACHE STRING "")

configs/RISCV64_ariane_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "ariane" CACHE STRING "")

configs/RISCV64_bananapi-f3_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "bananapi-f3" CACHE STRING "")

configs/RISCV64_cheshire_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "cheshire" CACHE STRING "")

configs/RISCV64_hifive-p550_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "hifive-p550" CACHE STRING "")

configs/RISCV64_polarfire_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "polarfire" CACHE STRING "")

configs/RISCV64_rocketchip-zcu102_verified.cmake

@@ -0,0 +1,11 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "rocketchip" CACHE STRING "")
+set(KernelRiscVPlatform "rocketchip-zcu102" CACHE STRING "")

configs/RISCV64_rocketchip_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "rocketchip" CACHE STRING "")

configs/RISCV64_star64_verified.cmake

@@ -0,0 +1,10 @@
+#!/usr/bin/env -S cmake -P
+#
+# Copyright 2024, Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
+
+set(KernelPlatform "star64" CACHE STRING "")

configs/seL4Config.cmake

@@ -143,6 +143,7 @@ foreach(
         KernelArmCortexA55
         KernelArmCortexA57
         KernelArmCortexA72
+        KernelArmCortexA76
         KernelArchArmV7a
         KernelArchArmV7ve
         KernelArchArmV8a
@@ -194,6 +195,7 @@ config_set(KernelArmCortexA53 ARM_CORTEX_A53 "${KernelArmCortexA53}")
 config_set(KernelArmCortexA55 ARM_CORTEX_A55 "${KernelArmCortexA55}")
 config_set(KernelArmCortexA57 ARM_CORTEX_A57 "${KernelArmCortexA57}")
 config_set(KernelArmCortexA72 ARM_CORTEX_A72 "${KernelArmCortexA72}")
+config_set(KernelArmCortexA76 ARM_CORTEX_A76 "${KernelArmCortexA76}")
 config_set(KernelArchArmV7a ARCH_ARM_V7A "${KernelArchArmV7a}")
 config_set(KernelArchArmV7ve ARCH_ARM_V7VE "${KernelArchArmV7ve}")
 config_set(KernelArchArmV8a ARCH_ARM_V8A "${KernelArchArmV8a}")
@@ -232,6 +234,8 @@ elseif(KernelArmCortexA57)
   set(KernelArmCPU "cortex-a57" CACHE INTERNAL "")
 elseif(KernelArmCortexA72)
   set(KernelArmCPU "cortex-a72" CACHE INTERNAL "")
+elseif(KernelArmCortexA76)
+  set(KernelArmCPU "cortex-a76" CACHE INTERNAL "")
 endif()
 if(KernelArchARM)
   config_set(KernelArmMach ARM_MACH "${KernelArmMach}")

include/arch/arm/arch/kernel/traps.h

@@ -57,3 +57,6 @@ void c_handle_vcpu_fault(word_t hsr)
 VISIBLE SECTION(".vectors.text");
 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
 
+#if defined(CONFIG_ARCH_AARCH64) && defined(CONFIG_DEBUG_BUILD)
+void VISIBLE c_handle_invalid_vector_entry(word_t vect_offset, word_t pc);
+#endif

include/arch/x86/arch/object/structures.h

@@ -16,6 +16,7 @@
 #include <arch/machine/hardware.h>
 #include <arch/machine/registerset.h>
 #include <sel4/arch/constants.h>
+#include <sel4/sel4_arch/constants.h>
 
 enum tcb_arch_cnode_index {
 #ifdef CONFIG_VTX
@@ -54,9 +55,9 @@ typedef struct arch_tcb {
 #define VTD_CT_BITS       8
 #define VTD_CT_SIZE_BITS  (VTD_CT_BITS + VTD_CTE_SIZE_BITS)
 
-#define VTD_PTE_SIZE_BITS 3
+#define VTD_PTE_SIZE_BITS seL4_IOPageTableEntryBits
 #define VTD_PTE_PTR(r)    ((vtd_pte_t*)(r))
-#define VTD_PT_INDEX_BITS       9
+#define VTD_PT_INDEX_BITS seL4_IOPageTableIndexBits
 
 compile_assert(vtd_pt_size_sane, VTD_PT_INDEX_BITS + VTD_PTE_SIZE_BITS == seL4_IOPageTableBits)
 

libsel4/arch_include/arm/sel4/arch/constants_cortex_a76.h

@@ -0,0 +1,28 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+
+#include <sel4/config.h>
+
+#if !defined(CONFIG_ARM_CORTEX_A76)
+#error CONFIG_ARM_CORTEX_A76 is not defined
+#endif
+
+/* Cortex-A76 Manual, Section 17.2.2 */
+#define seL4_NumHWBreakpoints           10
+#define seL4_NumExclusiveBreakpoints     6
+#define seL4_NumExclusiveWatchpoints     4
+
+#ifdef CONFIG_HARDWARE_DEBUG_API
+
+#define seL4_FirstBreakpoint             0
+#define seL4_FirstWatchpoint             6
+
+#define seL4_NumDualFunctionMonitors     0
+#define seL4_FirstDualFunctionMonitor    (-1)
+
+#endif /* CONFIG_HARDWARE_DEBUG_API */

libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h

@@ -38,12 +38,15 @@
 #define seL4_PageDirIndexBits 10
 #define seL4_VSpaceBits seL4_PageDirBits
 
-#define seL4_IOPageTableBits 12
 #define seL4_NumASIDPoolsBits 2
 #define seL4_ASIDPoolBits    12
 #define seL4_ASIDPoolIndexBits 10
 #define seL4_WordSizeBits 2
 
+#define seL4_IOPageTableBits      12
+#define seL4_IOPageTableIndexBits 9
+#define seL4_IOPageTableEntryBits 3
+
 #define seL4_HugePageBits    30 /* 1GB */
 #define seL4_PDPTBits         0
 #define seL4_LargePageBits    22 /* 4MB */
@@ -52,6 +55,7 @@
 SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
 SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits);
 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
+SEL4_SIZE_SANITY(seL4_IOPageTableEntryBits, seL4_IOPageTableIndexBits, seL4_IOPageTableBits);
 #endif
 
 /* Previously large frames were explicitly assumed to be 4M. If not using

libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h

@@ -53,7 +53,10 @@
 #define seL4_PML4IndexBits      9
 #define seL4_VSpaceBits seL4_PML4Bits
 
-#define seL4_IOPageTableBits    12
+#define seL4_IOPageTableBits      12
+#define seL4_IOPageTableIndexBits 9
+#define seL4_IOPageTableEntryBits 3
+
 #define seL4_LargePageBits      21
 #define seL4_HugePageBits       30
 #define seL4_NumASIDPoolsBits    3
@@ -71,6 +74,7 @@ SEL4_SIZE_SANITY(seL4_PageDirEntryBits, seL4_PageDirIndexBits, seL4_PageDirBits)
 SEL4_SIZE_SANITY(seL4_PDPTEntryBits, seL4_PDPTIndexBits, seL4_PDPTBits);
 SEL4_SIZE_SANITY(seL4_PML4EntryBits, seL4_PML4IndexBits, seL4_PML4Bits);
 SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
+SEL4_SIZE_SANITY(seL4_IOPageTableEntryBits, seL4_IOPageTableIndexBits, seL4_IOPageTableBits);
 
 typedef enum {
     seL4_VMFault_IP,

libsel4/sel4_plat_include/bcm2712/sel4/plat/api/constants.h

@@ -0,0 +1,9 @@
+/*
+ * Copyright 2025, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#pragma once
+
+#include <sel4/config.h>
+#include <sel4/arch/constants_cortex_a76.h>

src/arch/arm/64/c_traps.c

@@ -65,3 +65,54 @@ void VISIBLE NORETURN restore_user_context(void)
     );
     UNREACHABLE();
 }
+
+#if defined(CONFIG_DEBUG_BUILD)
+/* See 'arm_vector_table' for details on 'vect_offset' */
+static const char *vect_offset_to_name(word_t vect_offset)
+{
+    switch (vect_offset) {
+    case 0x000:
+        return "Synchronous EL1t/EL2t";
+    case 0x080:
+        return "IRQ EL1t/EL2t";
+    case 0x100:
+        return "FIQ EL1t/EL2t";
+    case 0x180:
+        return "SError EL1t/EL2t";
+    case 0x200:
+        return "Synchronous Current EL";
+    case 0x280:
+        return "IRQ Current EL";
+    case 0x300:
+        return "FIQ Current EL";
+    case 0x380:
+        return "SError Current EL";
+    case 0x400:
+        return "Synchronous 64-bit EL0/EL1";
+    case 0x480:
+        return "IRQ 64-bit EL0/EL1";
+    case 0x500:
+        return "FIQ 64-bit EL0/EL1";
+    case 0x580:
+        return "SError 64-bit EL0/EL1";
+    case 0x600:
+        return "Synchronous 32-bit EL0/EL1";
+    case 0x680:
+        return "IRQ 32-bit EL0/EL1";
+    case 0x700:
+        return "FIQ 32-bit EL0/EL1";
+    case 0x780:
+        return "SError 32-bit EL0/EL1";
+    default:
+        return "<Unknown>";
+    }
+}
+
+void VISIBLE c_handle_invalid_vector_entry(word_t vect_offset, word_t pc)
+{
+    printf("\n\nKERNEL INVALID VECTOR ENTRY!\n");
+    printf("Vector: 0x%"SEL4_PRIx_word" (%s)\n", vect_offset, vect_offset_to_name(vect_offset));
+    printf("Fault attributed to program counter: 0x%"SEL4_PRIx_word"\n", pc);
+    printf("ESR: 0x%"SEL4_PRIx_word" FAR: 0x%"SEL4_PRIx_word"\n", getESR(), getFAR());
+}
+#endif

src/arch/arm/64/traps.S

@@ -10,9 +10,6 @@
 #include <arch/machine/hardware.h>
 #include <arch/machine/registerset.h>
 
-#define VM_EVENT_DATA_ABORT 0
-#define VM_EVENT_PREFETCH_ABORT 1
-
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
 
 #define ELR     elr_el2
@@ -43,28 +40,58 @@
     b       \label
 .endm
 
+#ifdef CONFIG_DEBUG_BUILD
+.macro ventry_invalid
+.align 7
+    /* compute vect_offset argument */
+    adr     x0, .
+    adr     x19, arm_vector_table
+    sub     x0, x0, x19
+    b       invalid_vector_entry
+.endm
+#else
+.macro ventry_invalid
+    ventry invalid_vector_entry
+.endm
+#endif
+
+#ifdef CONFIG_AARCH64_SERROR_IGNORE
+.macro ventry_serror
+.align 7
+    eret
+.endm
+#else
+.macro ventry_serror
+    ventry_invalid
+.endm
+#endif
+
 .section .vectors, "ax"
 
+/* The layout of this table are specified in Table D1-7, 'Vector offsets from
+ * vector table base address' of ARM DDI 0487B.b ID092517.
+ * Each vector entry has 128-byte alignment, and so supports 32 instructions.
+ */
 BEGIN_FUNC(arm_vector_table)
-    ventry  invalid_vector_entry           // Synchronous EL1t/EL2t
-    ventry  invalid_vector_entry           // IRQ EL1t/EL2t
-    ventry  invalid_vector_entry           // FIQ EL1t/EL2t
-    ventry  invalid_vector_entry           // SError EL1t/EL2t
+    ventry_invalid                         // Synchronous EL1t/EL2t
+    ventry_invalid                         // IRQ EL1t/EL2t
+    ventry_invalid                         // FIQ EL1t/EL2t
+    ventry_invalid                         // SError EL1t/EL2t
 
     ventry  cur_el_sync                    // Current EL Synchronous (EL1/2)
     ventry  cur_el_irq                     // IRQ
-    ventry  invalid_vector_entry           // FIQ
-    ventry  cur_el_serr                    // SError
+    ventry_invalid                         // FIQ
+    ventry_serror                          // SError
 
     ventry  lower_el_sync                  // Synchronous 64-bit EL0/EL1
     ventry  lower_el_irq                   // IRQ 64-bit EL0/EL1
-    ventry  invalid_vector_entry           // FIQ 64-bit EL0/EL1
-    ventry  lower_el_serr                  // SError 64-bit EL0/EL1
+    ventry_invalid                         // FIQ 64-bit EL0/EL1
+    ventry_serror                          // SError 64-bit EL0/EL1
 
-    ventry  invalid_vector_entry           // Synchronous 32-bit EL0/EL1
-    ventry  invalid_vector_entry           // IRQ 32-bit EL0/EL1
-    ventry  invalid_vector_entry           // FIQ 32-bit EL0/EL1
-    ventry  invalid_vector_entry           // SError 32-bit EL0/EL1
+    ventry_invalid                         // Synchronous 32-bit EL0/EL1
+    ventry_invalid                         // IRQ 32-bit EL0/EL1
+    ventry_invalid                         // FIQ 32-bit EL0/EL1
+    ventry_invalid                         // SError 32-bit EL0/EL1
 END_FUNC(arm_vector_table)
 
 .section .vectors.text, "ax"
@@ -95,8 +122,13 @@ END_FUNC(arm_vector_table)
     stp     x22, x23, [sp, #PT_ELR_EL1]
 .endm
 
+/* Takes argument x0: vect_offset (in debug builds) */
 BEGIN_FUNC(invalid_vector_entry)
     lsp_i   x19
+#ifdef CONFIG_DEBUG_BUILD
+    mrs     x1, ELR
+    bl      c_handle_invalid_vector_entry
+#endif
     b       halt
 END_FUNC(invalid_vector_entry)
 
@@ -126,6 +158,8 @@ cur_el_ia:
     b       halt
 
 cur_el_inv:
+    /* 0x200 corresponding to the offset in the vector table */
+    mov     x0, #0x200
     b       invalid_vector_entry
 END_FUNC(cur_el_sync)
 
@@ -140,14 +174,6 @@ BEGIN_FUNC(cur_el_irq)
     b       c_handle_interrupt
 END_FUNC(cur_el_irq)
 
-BEGIN_FUNC(cur_el_serr)
-#ifdef CONFIG_AARCH64_SERROR_IGNORE
-    eret
-#else
-    b       invalid_vector_entry
-#endif
-END_FUNC(cur_el_serr)
-
 BEGIN_FUNC(lower_el_sync)
     kernel_enter
 
@@ -228,11 +254,3 @@ BEGIN_FUNC(lower_el_irq)
     lsp_i   x19
     b       c_handle_interrupt
 END_FUNC(lower_el_irq)
-
-BEGIN_FUNC(lower_el_serr)
-#ifdef CONFIG_AARCH64_SERROR_IGNORE
-    eret
-#else
-    b       invalid_vector_entry
-#endif
-END_FUNC(lower_el_serr)

src/arch/arm/config.cmake

@@ -30,6 +30,9 @@ elseif(KernelArmCortexA72)
   # (https://developer.arm.com/documentation/100095/0001/memory-management-unit/about-the-mmu)
   set(KernelArmPASizeBits44 ON)
   math(EXPR KernelPaddrUserTop "(1 << 44)")
+elseif(KernelArmCortexA76)
+  set(KernelArmPASizeBits40 ON)
+  math(EXPR KernelPaddrUserTop "(1 << 40)")
 endif()
 config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
 config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
@@ -78,7 +81,7 @@ config_option(
   "Build as Hypervisor. Utilise ARM virtualisation extensions to build the kernel as a hypervisor"
   DEFAULT ${KernelSel4ArchArmHyp}
   DEPENDS
-    "KernelArmCortexA15 OR KernelArmCortexA35 OR KernelArmCortexA57 OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA72"
+    "KernelArmCortexA15 OR KernelArmCortexA35 OR KernelArmCortexA57 OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA72 OR KernelArmCortexA76"
 )
 
 config_option(KernelArmGicV3 ARM_GIC_V3_SUPPORT "Build support for GICv3" DEFAULT OFF)
@@ -234,7 +237,8 @@ if(KernelAArch32FPUEnableContextSwitch OR KernelSel4ArchAarch64)
 endif()
 
 if(KernelArmCortexA7 OR KernelArmCortexA8 OR KernelArmCortexA15 OR KernelArmCortexA35
-   OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA57 OR KernelArmCortexA72)
+   OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA57 OR KernelArmCortexA72
+   OR KernelArmCortexA76)
   # According to https://developer.arm.com/documentation/100095/0001/functional-description/about-the-cortex-a72-processor-functions/components-of-the-processor
   # the L1 instruction on the Cortex-A72 cache has a 64-byte cache line.
   # Thus, 6 bits are needed.

src/arch/arm/kernel/boot.c

@@ -470,12 +470,7 @@ static BOOT_CODE bool_t try_init_kernel(
         extra_bi_offset += dtb_size;
     }
 
-    if (extra_bi_size > extra_bi_offset) {
-        /* provide a chunk for any leftover padding in the extended boot info */
-        header.id = SEL4_BOOTINFO_HEADER_PADDING;
-        header.len = (extra_bi_size - extra_bi_offset);
-        *(seL4_BootInfoHeader *)(rootserver.extra_bi + extra_bi_offset) = header;
-    }
+    assert(extra_bi_size == extra_bi_offset);
 
     if (config_set(CONFIG_TK1_SMMU)) {
         ndks_boot.bi_frame->ioSpaceCaps = create_iospace_caps(root_cnode_cap);

src/arch/riscv/kernel/boot.c

@@ -324,12 +324,7 @@ static BOOT_CODE bool_t try_init_kernel(
         extra_bi_offset += dtb_size;
     }
 
-    if (extra_bi_size > extra_bi_offset) {
-        /* provide a chunk for any leftover padding in the extended boot info */
-        header.id = SEL4_BOOTINFO_HEADER_PADDING;
-        header.len = (extra_bi_size - extra_bi_offset);
-        *(seL4_BootInfoHeader *)(rootserver.extra_bi + extra_bi_offset) = header;
-    }
+    assert(extra_bi_size == extra_bi_offset);
 
     /* Construct an initial address space with enough virtual addresses
      * to cover the user image + ipc buffer and bootinfo frames */

src/arch/x86/c_traps.c

@@ -147,6 +147,16 @@ void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t sy
         x86_enable_ibrs();
     }
 
+    /* Must happen before NODE_LOCK_SYS so that lock exit via IPI stall restores
+       the correct program counter. */
+    if (config_set(CONFIG_SYSENTER)) {
+        /* increment NextIP to skip sysenter */
+        NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers[NextIP] += 2;
+    } else {
+        /* set FaultIP */
+        setRegister(NODE_STATE(ksCurThread), FaultIP, getRegister(NODE_STATE(ksCurThread), NextIP) - 2);
+    }
+
     NODE_LOCK_SYS;
 
     c_entry_hook();
@@ -156,14 +166,6 @@ void VISIBLE NORETURN c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t sy
     ksKernelEntry.is_fastpath = 1;
 #endif /* TRACK_KERNEL_ENTRIES */
 
-    if (config_set(CONFIG_SYSENTER)) {
-        /* increment NextIP to skip sysenter */
-        NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers[NextIP] += 2;
-    } else {
-        /* set FaultIP */
-        setRegister(NODE_STATE(ksCurThread), FaultIP, getRegister(NODE_STATE(ksCurThread), NextIP) - 2);
-    }
-
 #ifdef CONFIG_FASTPATH
     if (syscall == (syscall_t)SysCall) {
         fastpath_call(cptr, msgInfo);

src/arch/x86/kernel/boot.c

@@ -104,7 +104,7 @@ BOOT_CODE bool_t init_sys_state(
     cap_t         it_vspace_cap;
     cap_t         it_ap_cap;
     cap_t         ipcbuf_cap;
-    word_t        extra_bi_size = sizeof(seL4_BootInfoHeader);
+    word_t        extra_bi_size = 0;
     pptr_t        extra_bi_offset = 0;
     uint32_t      tsc_freq;
     create_frames_of_region_ret_t create_frames_ret;
@@ -226,12 +226,6 @@ BOOT_CODE bool_t init_sys_state(
         extra_bi_offset += 4;
     }
 
-    /* provide a chunk for any leftover padding in the extended boot info */
-    seL4_BootInfoHeader padding_header;
-    padding_header.id = SEL4_BOOTINFO_HEADER_PADDING;
-    padding_header.len = (extra_bi_region.end - extra_bi_region.start) - extra_bi_offset;
-    *(seL4_BootInfoHeader *)(extra_bi_region.start + extra_bi_offset) = padding_header;
-
 #ifdef CONFIG_KERNEL_MCS
     /* set up sched control for each core */
     init_sched_control(root_cnode_cap, CONFIG_MAX_NUM_NODES);

src/plat/bcm2712/config.cmake

@@ -0,0 +1,31 @@
+#
+# Copyright 2025, UNSW
+#
+# SPDX-License-Identifier: GPL-2.0-only
+#
+
+declare_platform(bcm2712 KernelPlatformRpi5 PLAT_BCM2712 KernelArchARM)
+
+if(KernelPlatformRpi5)
+  declare_seL4_arch(aarch64)
+  set(KernelArmCortexA76 ON)
+  set(KernelArchArmV8a ON)
+  config_set(KernelARMPlatform ARM_PLAT rpi5)
+  set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
+  list(APPEND KernelDTSList "tools/dts/rpi5b.dts")
+  list(APPEND KernelDTSList "src/plat/bcm2712/overlay-rpi5.dts")
+  # The 2GB model is assumed, this can be changed with the KernelCustomDTSOverlay
+  # configuration option or adding support for other models like is done for
+  # bcm2711.
+  list(APPEND KernelDTSList "src/plat/bcm2712/overlay-rpi5-2gb.dts")
+
+  # - The clock frequency is 54 MHz as can be seen in bcm2712.dtsi in the
+  #   Linux Kernel under clk_osc, thus TIMER_FREQUENCY = 54000000.
+  # - MAX_IRQ is based on the GIC ITLinesNumber which reports 320.
+  declare_default_headers(
+    TIMER_FREQUENCY 54000000 MAX_IRQ 320 NUM_PPI 32 TIMER drivers/timer/arm_generic.h
+    INTERRUPT_CONTROLLER arch/machine/gic_v2.h KERNEL_WCET 10u)
+endif()
+
+add_sources(DEP "KernelPlatformRpi5" CFILES src/arch/arm/machine/gic_v2.c
+                                            src/arch/arm/machine/l2c_nop.c)

src/plat/bcm2712/overlay-rpi5-2gb.dts

@@ -0,0 +1,12 @@
+/*
+ * Copyright 2025, UNSW
+ * SPDX-License-Identifier: GPL-2.0-only
+ */
+
+/ {
+    memory@0 {
+        device_type = "memory";
+        /* VideoCore memory lives at 0x3fc00000 onwards. */
+        reg = < 0x00000000 0x00000000 0x0 0x3fc00000>;
+    };
+};

src/plat/bcm2712/overlay-rpi5.dts

@@ -0,0 +1,30 @@
+/*
+ * Copyright 2025, UNSW
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ */
+
+/ {
+	chosen {
+		seL4,elfloader-devices =
+		    "serial10",
+		    &{/psci},
+		    &{/timer};
+
+		seL4,kernel-devices =
+		    "serial10",
+		    &{/soc@107c000000/interrupt-controller@7fff9000},
+		    &{/timer};
+	};
+
+	soc@107c000000 {
+		interrupt-controller@7fff9000 {
+			/* vGIC maintenance IRQ necessary for hypervisor mode. */
+			interrupts = <0x01 0x09 0xf04>;
+		};
+	};
+
+    reserved-memory {
+        /delete-node/ linux,cma;
+    };
+};

tools/dts/rpi5b.dts

@@ -0,0 +1,564 @@
+/*
+ * Copyright Linux Kernel Team
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *
+ * This file is derived from an intermediate build stage of the
+ * Linux kernel. The licenses of all input files to this process
+ * are compatible with GPL-2.0-only.
+ */
+/dts-v1/;
+
+/ {
+	compatible = "raspberrypi,5-model-b", "brcm,bcm2712";
+	#address-cells = <0x02>;
+	#size-cells = <0x02>;
+	interrupt-parent = <0x01>;
+	model = "Raspberry Pi 5";
+
+	clocks {
+
+		clk-osc {
+			compatible = "fixed-clock";
+			#clock-cells = <0x00>;
+			clock-output-names = "osc";
+			clock-frequency = <0x337f980>;
+			phandle = <0x18>;
+		};
+
+		clk-vpu {
+			compatible = "fixed-clock";
+			#clock-cells = <0x00>;
+			clock-frequency = <0x2cb41780>;
+			clock-output-names = "vpu-clock";
+			phandle = <0x0b>;
+		};
+
+		clk-uart {
+			compatible = "fixed-clock";
+			#clock-cells = <0x00>;
+			clock-frequency = <0x8ca000>;
+			clock-output-names = "uart-clock";
+			phandle = <0x0a>;
+		};
+
+		clk-emmc2 {
+			compatible = "fixed-clock";
+			#clock-cells = <0x00>;
+			clock-frequency = <0xbebc200>;
+			clock-output-names = "emmc2-clock";
+			phandle = <0x07>;
+		};
+	};
+
+	cpus {
+		#address-cells = <0x01>;
+		#size-cells = <0x00>;
+		phandle = <0x19>;
+
+		cpu@0 {
+			device_type = "cpu";
+			compatible = "arm,cortex-a76";
+			reg = <0x00>;
+			enable-method = "psci";
+			d-cache-size = <0x10000>;
+			d-cache-line-size = <0x40>;
+			d-cache-sets = <0x100>;
+			i-cache-size = <0x10000>;
+			i-cache-line-size = <0x40>;
+			i-cache-sets = <0x100>;
+			next-level-cache = <0x02>;
+			phandle = <0x1a>;
+
+			l2-cache-l0 {
+				compatible = "cache";
+				cache-size = <0x80000>;
+				cache-line-size = <0x40>;
+				cache-sets = <0x400>;
+				cache-level = <0x02>;
+				cache-unified;
+				next-level-cache = <0x03>;
+				phandle = <0x02>;
+			};
+		};
+
+		cpu@1 {
+			device_type = "cpu";
+			compatible = "arm,cortex-a76";
+			reg = <0x100>;
+			enable-method = "psci";
+			d-cache-size = <0x10000>;
+			d-cache-line-size = <0x40>;
+			d-cache-sets = <0x100>;
+			i-cache-size = <0x10000>;
+			i-cache-line-size = <0x40>;
+			i-cache-sets = <0x100>;
+			next-level-cache = <0x04>;
+			phandle = <0x1b>;
+
+			l2-cache-l1 {
+				compatible = "cache";
+				cache-size = <0x80000>;
+				cache-line-size = <0x40>;
+				cache-sets = <0x400>;
+				cache-level = <0x02>;
+				cache-unified;
+				next-level-cache = <0x03>;
+				phandle = <0x04>;
+			};
+		};
+
+		cpu@2 {
+			device_type = "cpu";
+			compatible = "arm,cortex-a76";
+			reg = <0x200>;
+			enable-method = "psci";
+			d-cache-size = <0x10000>;
+			d-cache-line-size = <0x40>;
+			d-cache-sets = <0x100>;
+			i-cache-size = <0x10000>;
+			i-cache-line-size = <0x40>;
+			i-cache-sets = <0x100>;
+			next-level-cache = <0x05>;
+			phandle = <0x1c>;
+
+			l2-cache-l2 {
+				compatible = "cache";
+				cache-size = <0x80000>;
+				cache-line-size = <0x40>;
+				cache-sets = <0x400>;
+				cache-level = <0x02>;
+				cache-unified;
+				next-level-cache = <0x03>;
+				phandle = <0x05>;
+			};
+		};
+
+		cpu@3 {
+			device_type = "cpu";
+			compatible = "arm,cortex-a76";
+			reg = <0x300>;
+			enable-method = "psci";
+			d-cache-size = <0x10000>;
+			d-cache-line-size = <0x40>;
+			d-cache-sets = <0x100>;
+			i-cache-size = <0x10000>;
+			i-cache-line-size = <0x40>;
+			i-cache-sets = <0x100>;
+			next-level-cache = <0x06>;
+			phandle = <0x1d>;
+
+			l2-cache-l3 {
+				compatible = "cache";
+				cache-size = <0x80000>;
+				cache-line-size = <0x40>;
+				cache-sets = <0x400>;
+				cache-level = <0x02>;
+				cache-unified;
+				next-level-cache = <0x03>;
+				phandle = <0x06>;
+			};
+		};
+
+		l3-cache {
+			compatible = "cache";
+			cache-size = <0x200000>;
+			cache-line-size = <0x40>;
+			cache-sets = <0x800>;
+			cache-level = <0x03>;
+			cache-unified;
+			phandle = <0x03>;
+		};
+	};
+
+	psci {
+		method = "smc";
+		compatible = "arm,psci-1.0", "arm,psci-0.2";
+	};
+
+	reserved-memory {
+		ranges;
+		#address-cells = <0x02>;
+		#size-cells = <0x02>;
+		phandle = <0x1e>;
+
+		atf@0 {
+			reg = <0x00 0x00 0x00 0x80000>;
+			no-map;
+		};
+
+		linux,cma {
+			compatible = "shared-dma-pool";
+			size = <0x00 0x4000000>;
+			reusable;
+			linux,cma-default;
+			alloc-ranges = <0x00 0x00 0x00 0x40000000>;
+			phandle = <0x1f>;
+		};
+	};
+
+	soc@107c000000 {
+		compatible = "simple-bus";
+		ranges = <0x00 0x10 0x00 0x80000000>;
+		#address-cells = <0x01>;
+		#size-cells = <0x01>;
+		phandle = <0x20>;
+
+		mmc@fff000 {
+			compatible = "brcm,bcm2712-sdhci", "brcm,sdhci-brcmstb";
+			reg = <0xfff000 0x260 0xfff400 0x200>;
+			reg-names = "host", "cfg";
+			interrupts = <0x00 0x111 0x04>;
+			clocks = <0x07>;
+			clock-names = "sw_sdio";
+			mmc-ddr-3_3v;
+			vqmmc-supply = <0x08>;
+			vmmc-supply = <0x09>;
+			bus-width = <0x04>;
+			sd-uhs-sdr50;
+			sd-uhs-ddr50;
+			sd-uhs-sdr104;
+			phandle = <0x21>;
+		};
+
+		timer@7c003000 {
+			compatible = "brcm,bcm2835-system-timer";
+			reg = <0x7c003000 0x1000>;
+			interrupts = <0x00 0x40 0x04 0x00 0x41 0x04 0x00 0x42 0x04 0x00 0x43 0x04>;
+			clock-frequency = <0xf4240>;
+			phandle = <0x22>;
+		};
+
+		mailbox@7c013880 {
+			compatible = "brcm,bcm2835-mbox";
+			reg = <0x7c013880 0x40>;
+			interrupts = <0x00 0x21 0x04>;
+			#mbox-cells = <0x00>;
+			phandle = <0x15>;
+		};
+
+		serial@7d001000 {
+			compatible = "arm,pl011", "arm,primecell";
+			reg = <0x7d001000 0x200>;
+			interrupts = <0x00 0x79 0x04>;
+			clocks = <0x0a 0x0b>;
+			clock-names = "uartclk", "apb_pclk";
+			arm,primecell-periphid = <0x341011>;
+			status = "okay";
+			phandle = <0x23>;
+		};
+
+		interrupt-controller@7d517000 {
+			compatible = "brcm,bcm7271-l2-intc";
+			reg = <0x7d517000 0x10>;
+			interrupts = <0x00 0xf7 0x04>;
+			interrupt-controller;
+			#interrupt-cells = <0x01>;
+		};
+
+		gpio@7d517c00 {
+			compatible = "brcm,bcm7445-gpio", "brcm,brcmstb-gpio";
+			reg = <0x7d517c00 0x40>;
+			gpio-controller;
+			#gpio-cells = <0x02>;
+			brcm,gpio-bank-widths = <0x11 0x06>;
+			phandle = <0x17>;
+		};
+
+		interrupt-controller@7fff9000 {
+			compatible = "arm,gic-400";
+			reg = <0x7fff9000 0x1000 0x7fffa000 0x2000 0x7fffc000 0x2000 0x7fffe000 0x2000>;
+			interrupt-controller;
+			#interrupt-cells = <0x03>;
+			phandle = <0x01>;
+		};
+
+		interrupt-controller@7d510600 {
+			compatible = "brcm,bcm2711-l2-intc", "brcm,l2-intc";
+			reg = <0x7d510600 0x30>;
+			interrupts = <0x00 0xef 0x04>;
+			interrupt-controller;
+			#interrupt-cells = <0x01>;
+			phandle = <0x10>;
+		};
+
+		pixelvalve@7c410000 {
+			compatible = "brcm,bcm2712-pixelvalve0";
+			reg = <0x7c410000 0x100>;
+			interrupts = <0x00 0x65 0x04>;
+			phandle = <0x24>;
+		};
+
+		pixelvalve@7c411000 {
+			compatible = "brcm,bcm2712-pixelvalve1";
+			reg = <0x7c411000 0x100>;
+			interrupts = <0x00 0x6e 0x04>;
+			phandle = <0x25>;
+		};
+
+		mop@7c500000 {
+			compatible = "brcm,bcm2712-mop";
+			reg = <0x7c500000 0x28>;
+			interrupt-parent = <0x0c>;
+			interrupts = <0x01>;
+			phandle = <0x26>;
+		};
+
+		moplet@7c501000 {
+			compatible = "brcm,bcm2712-moplet";
+			reg = <0x7c501000 0x20>;
+			interrupt-parent = <0x0c>;
+			interrupts = <0x00>;
+			phandle = <0x27>;
+		};
+
+		interrupt-controller@7c502000 {
+			compatible = "brcm,bcm2711-l2-intc", "brcm,l2-intc";
+			reg = <0x7c502000 0x30>;
+			interrupts = <0x00 0x61 0x04>;
+			interrupt-controller;
+			#interrupt-cells = <0x01>;
+			phandle = <0x0c>;
+		};
+
+		clock@7c700000 {
+			compatible = "brcm,brcm2711-dvp";
+			reg = <0x7c700000 0x10>;
+			clocks = <0x0d>;
+			#clock-cells = <0x01>;
+			#reset-cells = <0x01>;
+			phandle = <0x0f>;
+		};
+
+		i2c@7d508200 {
+			compatible = "brcm,brcmstb-i2c";
+			reg = <0x7d508200 0x58>;
+			interrupt-parent = <0x0e>;
+			interrupts = <0x01>;
+			clock-frequency = <0x17cdc>;
+			#address-cells = <0x01>;
+			#size-cells = <0x00>;
+			phandle = <0x11>;
+		};
+
+		i2c@7d508280 {
+			compatible = "brcm,brcmstb-i2c";
+			reg = <0x7d508280 0x58>;
+			interrupt-parent = <0x0e>;
+			interrupts = <0x02>;
+			clock-frequency = <0x17cdc>;
+			#address-cells = <0x01>;
+			#size-cells = <0x00>;
+			phandle = <0x14>;
+		};
+
+		interrupt-controller@7d508380 {
+			compatible = "brcm,bcm7271-l2-intc";
+			reg = <0x7d508380 0x10>;
+			interrupts = <0x00 0xf2 0x04>;
+			interrupt-controller;
+			#interrupt-cells = <0x01>;
+			phandle = <0x0e>;
+		};
+
+		interrupt-controller@7d508400 {
+			compatible = "brcm,bcm7271-l2-intc";
+			reg = <0x7d508400 0x10>;
+			interrupts = <0x00 0xf4 0x04>;
+			interrupt-controller;
+			#interrupt-cells = <0x01>;
+			phandle = <0x28>;
+		};
+
+		hdmi@7c701400 {
+			compatible = "brcm,bcm2712-hdmi0";
+			reg = <0x7c701400 0x300 0x7c701000 0x200 0x7c701d00 0x300 0x7c702000 0x80 0x7c703800 0x200 0x7c704000 0x800 0x7c700100 0x80 0x7d510800 0x100 0x7c720000 0x100>;
+			reg-names = "hdmi", "dvp", "phy", "rm", "packet", "metadata", "csc", "cec", "hd";
+			resets = <0x0f 0x01>;
+			interrupt-parent = <0x10>;
+			interrupts = <0x01 0x02 0x03 0x07 0x08>;
+			interrupt-names = "cec-tx", "cec-rx", "cec-low", "hpd-connected", "hpd-removed";
+			ddc = <0x11>;
+			clocks = <0x12 0x0d 0x12 0x0e 0x0f 0x00 0x13>;
+			clock-names = "hdmi", "bvb", "audio", "cec";
+			phandle = <0x29>;
+		};
+
+		hdmi@7c706400 {
+			compatible = "brcm,bcm2712-hdmi1";
+			reg = <0x7c706400 0x300 0x7c706000 0x200 0x7c706d00 0x300 0x7c707000 0x80 0x7c708800 0x200 0x7c709000 0x800 0x7c700180 0x80 0x7d511000 0x100 0x7c720000 0x100>;
+			reg-names = "hdmi", "dvp", "phy", "rm", "packet", "metadata", "csc", "cec", "hd";
+			resets = <0x0f 0x02>;
+			interrupt-parent = <0x10>;
+			interrupts = <0x0b 0x0c 0x0d 0x0e 0x0f>;
+			interrupt-names = "cec-tx", "cec-rx", "cec-low", "hpd-connected", "hpd-removed";
+			ddc = <0x14>;
+			clocks = <0x12 0x0d 0x12 0x0e 0x0f 0x01 0x13>;
+			clock-names = "hdmi", "bvb", "audio", "cec";
+			phandle = <0x2a>;
+		};
+
+		firmware {
+			compatible = "raspberrypi,bcm2835-firmware", "simple-mfd";
+			#address-cells = <0x01>;
+			#size-cells = <0x01>;
+			mboxes = <0x15>;
+			dma-ranges;
+			phandle = <0x16>;
+
+			clocks {
+				compatible = "raspberrypi,firmware-clocks";
+				#clock-cells = <0x01>;
+				phandle = <0x12>;
+			};
+
+			reset {
+				compatible = "raspberrypi,firmware-reset";
+				#reset-cells = <0x01>;
+				phandle = <0x2b>;
+			};
+		};
+
+		power {
+			compatible = "raspberrypi,bcm2835-power";
+			firmware = <0x16>;
+			#power-domain-cells = <0x01>;
+			phandle = <0x2c>;
+		};
+	};
+
+	axi {
+		compatible = "simple-bus";
+		#address-cells = <0x02>;
+		#size-cells = <0x02>;
+		ranges = <0x00 0x00 0x00 0x00 0x10 0x00 0x10 0x00 0x10 0x00 0x01 0x00 0x14 0x00 0x14 0x00 0x04 0x00 0x18 0x00 0x18 0x00 0x04 0x00 0x1c 0x00 0x1c 0x00 0x04 0x00>;
+		dma-ranges = <0x00 0x00 0x00 0x00 0x10 0x00 0x10 0x00 0x10 0x00 0x01 0x00 0x14 0x00 0x14 0x00 0x04 0x00 0x18 0x00 0x18 0x00 0x04 0x00 0x1c 0x00 0x1c 0x00 0x04 0x00>;
+		phandle = <0x2d>;
+
+		gpu {
+			compatible = "brcm,bcm2712-vc6";
+			phandle = <0x2e>;
+		};
+	};
+
+	timer {
+		compatible = "arm,armv8-timer";
+		interrupts = <0x01 0x0d 0xf08 0x01 0x0e 0xf08 0x01 0x0b 0xf08 0x01 0x0a 0xf08 0x01 0x0c 0xf08>;
+	};
+
+	clk-27M {
+		#clock-cells = <0x00>;
+		compatible = "fixed-clock";
+		clock-frequency = <0x19bfcc0>;
+		clock-output-names = "27MHz-clock";
+		phandle = <0x13>;
+	};
+
+	clk-108M {
+		#clock-cells = <0x00>;
+		compatible = "fixed-clock";
+		clock-frequency = <0x66ff300>;
+		clock-output-names = "108MHz-clock";
+		phandle = <0x0d>;
+	};
+
+	hvs@107c580000 {
+		compatible = "brcm,bcm2712-hvs";
+		reg = <0x10 0x7c580000 0x00 0x1a000>;
+		interrupt-parent = <0x0c>;
+		interrupts = <0x02 0x09 0x10>;
+		interrupt-names = "ch0-eof", "ch1-eof", "ch2-eof";
+		clocks = <0x12 0x04 0x12 0x10>;
+		clock-names = "core", "disp";
+		phandle = <0x2f>;
+	};
+
+	aliases {
+		serial10 = "/soc@107c000000/serial@7d001000";
+	};
+
+	chosen {
+		stdout-path = "serial10:115200n8";
+		phandle = <0x30>;
+	};
+
+	memory@0 {
+		device_type = "memory";
+		reg = <0x00 0x00 0x00 0x28000000>;
+	};
+
+	sd-io-1v8-reg {
+		compatible = "regulator-gpio";
+		regulator-name = "vdd-sd-io";
+		regulator-min-microvolt = <0x1b7740>;
+		regulator-max-microvolt = <0x325aa0>;
+		regulator-boot-on;
+		regulator-always-on;
+		regulator-settling-time-us = <0x1388>;
+		gpios = <0x17 0x03 0x00>;
+		states = <0x1b7740 0x01 0x325aa0 0x00>;
+		phandle = <0x08>;
+	};
+
+	sd-vcc-reg {
+		compatible = "regulator-fixed";
+		regulator-name = "vcc-sd";
+		regulator-min-microvolt = <0x325aa0>;
+		regulator-max-microvolt = <0x325aa0>;
+		regulator-boot-on;
+		enable-active-high;
+		gpios = <0x17 0x04 0x00>;
+		phandle = <0x09>;
+	};
+
+	__symbols__ {
+		clk_osc = "/clocks/clk-osc";
+		clk_vpu = "/clocks/clk-vpu";
+		clk_uart = "/clocks/clk-uart";
+		clk_emmc2 = "/clocks/clk-emmc2";
+		cpus = "/cpus";
+		cpu0 = "/cpus/cpu@0";
+		l2_cache_l0 = "/cpus/cpu@0/l2-cache-l0";
+		cpu1 = "/cpus/cpu@1";
+		l2_cache_l1 = "/cpus/cpu@1/l2-cache-l1";
+		cpu2 = "/cpus/cpu@2";
+		l2_cache_l2 = "/cpus/cpu@2/l2-cache-l2";
+		cpu3 = "/cpus/cpu@3";
+		l2_cache_l3 = "/cpus/cpu@3/l2-cache-l3";
+		l3_cache = "/cpus/l3-cache";
+		rmem = "/reserved-memory";
+		cma = "/reserved-memory/linux,cma";
+		soc = "/soc@107c000000";
+		sdio1 = "/soc@107c000000/mmc@fff000";
+		system_timer = "/soc@107c000000/timer@7c003000";
+		mailbox = "/soc@107c000000/mailbox@7c013880";
+		uart10 = "/soc@107c000000/serial@7d001000";
+		gio_aon = "/soc@107c000000/gpio@7d517c00";
+		gicv2 = "/soc@107c000000/interrupt-controller@7fff9000";
+		aon_intr = "/soc@107c000000/interrupt-controller@7d510600";
+		pixelvalve0 = "/soc@107c000000/pixelvalve@7c410000";
+		pixelvalve1 = "/soc@107c000000/pixelvalve@7c411000";
+		mop = "/soc@107c000000/mop@7c500000";
+		moplet = "/soc@107c000000/moplet@7c501000";
+		disp_intr = "/soc@107c000000/interrupt-controller@7c502000";
+		dvp = "/soc@107c000000/clock@7c700000";
+		ddc0 = "/soc@107c000000/i2c@7d508200";
+		ddc1 = "/soc@107c000000/i2c@7d508280";
+		bsc_irq = "/soc@107c000000/interrupt-controller@7d508380";
+		main_irq = "/soc@107c000000/interrupt-controller@7d508400";
+		hdmi0 = "/soc@107c000000/hdmi@7c701400";
+		hdmi1 = "/soc@107c000000/hdmi@7c706400";
+		firmware = "/soc@107c000000/firmware";
+		firmware_clocks = "/soc@107c000000/firmware/clocks";
+		reset = "/soc@107c000000/firmware/reset";
+		power = "/soc@107c000000/power";
+		axi = "/axi";
+		vc4 = "/axi/gpu";
+		clk_27MHz = "/clk-27M";
+		clk_108MHz = "/clk-108M";
+		hvs = "/hvs@107c580000";
+		chosen = "/chosen";
+		sd_io_1v8_reg = "/sd-io-1v8-reg";
+		sd_vcc_reg = "/sd-vcc-reg";
+	};
+};