diff --git a/include/api/bootinfo_types.h b/include/api/bootinfo_types.h
new file mode 120000
index 0000000000000000000000000000000000000000..26fe18d1a2c8af55c55e13327cde4de80ba4219c
--- /dev/null
+++ b/include/api/bootinfo_types.h
@@ -0,0 +1 @@
+../../libsel4/include/sel4/bootinfo_types.h
\ No newline at end of file
diff --git a/include/api/types.h b/include/api/types.h
index b4a077c0f1cb6f8237c147dbfe473d822c42173c..080261d2b04c2006b7489b754cc0e1b8f7811e58 100644
--- a/include/api/types.h
+++ b/include/api/types.h
@@ -23,7 +23,6 @@
/* cap_rights_t defined in api/types.bf */
typedef word_t prio_t;
-typedef word_t dom_t;
enum domainConstants {
minDom = 0,
diff --git a/include/arch/arm/arch/types.h b/include/arch/arm/arch/types.h
index 536bf70cc873c6d466ee50d88d9bc6722d9dc461..fa888db18410c161f0a65c2bcbe07691fc72a20f 100644
--- a/include/arch/arm/arch/types.h
+++ b/include/arch/arm/arch/types.h
@@ -22,6 +22,7 @@ typedef word_t paddr_t;
typedef word_t pptr_t;
typedef word_t cptr_t;
typedef word_t node_id_t;
+typedef word_t dom_t;
typedef uint8_t hw_asid_t;
@@ -34,5 +35,9 @@ enum hwASIDConstants {
typedef word_t seL4_Word;
typedef cptr_t seL4_CPtr;
typedef uint32_t seL4_Uint32;
+typedef uint8_t seL4_Uint8;
+typedef node_id_t seL4_NodeId;
+typedef dom_t seL4_Domain;
+typedef paddr_t seL4_PAddr;
#endif
diff --git a/include/arch/x86/arch/types.h b/include/arch/x86/arch/types.h
index d74e7a51329e483b82756f81f4038551f9a4f082..f26434756a9a0fdd7ae8bb3989855f951c2798b8 100644
--- a/include/arch/x86/arch/types.h
+++ b/include/arch/x86/arch/types.h
@@ -24,10 +24,14 @@ typedef word_t cptr_t;
typedef word_t dev_id_t;
typedef word_t cpu_id_t;
typedef word_t node_id_t;
+typedef word_t dom_t;
/* for libsel4 headers that the kernel shares */
typedef word_t seL4_Word;
typedef cptr_t seL4_CPtr;
typedef uint32_t seL4_Uint32;
-
+typedef uint8_t seL4_Uint8;
+typedef node_id_t seL4_NodeId;
+typedef paddr_t seL4_PAddr;
+typedef dom_t seL4_Domain;
#endif
diff --git a/include/bootinfo.h b/include/bootinfo.h
index 37345dfe53ffc8b69a63422b1abeaec07c7d59fd..5b4a8e9382b28bddd0bee0e6d311c9eb7aef9063 100644
--- a/include/bootinfo.h
+++ b/include/bootinfo.h
@@ -13,65 +13,14 @@
#include <config.h>
#include <types.h>
+#include <api/bootinfo_types.h>
-#define BI_PTR(r) ((bi_t*)(r))
+#define BI_PTR(r) ((seL4_BootInfo*)(r))
#define BI_REF(p) ((word_t)(p))
-
-/* bootinfo data structures (directly corresponding to abstract specification) */
-
#define BI_FRAME_SIZE_BITS PAGE_BITS
-
-/* fixed cap positions in root CNode */
-#define BI_CAP_NULL 0 /* null cap */
-#define BI_CAP_IT_TCB 1 /* initial thread's TCB cap */
-#define BI_CAP_IT_CNODE 2 /* initial thread's root CNode cap */
-#define BI_CAP_IT_VSPACE 3 /* initial thread's vspace root cap */
-#define BI_CAP_IRQ_CTRL 4 /* global IRQ controller cap */
-#define BI_CAP_ASID_CTRL 5 /* global ASID controller cap */
-#define BI_CAP_IT_ASID_POOL 6 /* initial thread's ASID pool cap */
-#define BI_CAP_IO_PORT 7 /* global IO port cap (null cap if not supported) */
-#define BI_CAP_IO_SPACE 8 /* global IO space cap (null cap if no IOMMU support) */
-#define BI_CAP_BI_FRAME 9 /* bootinfo frame cap */
-#define BI_CAP_IT_IPCBUF 10 /* initial thread's IPC buffer frame cap */
-#define BI_CAP_DOM 11 /* domain cap */
-#define BI_CAP_DYN_START 12 /* slot where dynamically allocated caps start */
-
-/* type definitions */
-
-typedef word_t slot_pos_t;
-
-typedef struct slot_region {
- slot_pos_t start;
- slot_pos_t end;
-} slot_region_t;
-
-#define S_REG_EMPTY (slot_region_t){ .start = 0, .end = 0 }
-
-typedef struct bi_dev_reg {
- paddr_t base_paddr; /* base physical address of device region */
- uint32_t frame_size_bits; /* size (2^n bytes) of a device-region frame */
- slot_region_t frame_caps; /* device-region frame caps */
-} bi_dev_reg_t;
-
-typedef struct bi {
- node_id_t node_id;
- uint32_t num_nodes;
- uint32_t num_iopt_levels; /* number of IOMMU PT levels (0 if no IOMMU support) */
- vptr_t ipcbuf_vptr; /* vptr to initial thread's IPC buffer */
- slot_region_t null_caps; /* null caps (empty slots) */
- slot_region_t sh_frame_caps; /* shared-frame caps */
- slot_region_t ui_frame_caps; /* userland-image frame caps */
- slot_region_t ui_paging_caps; /* userland-image paging structure caps */
- slot_region_t ut_obj_caps; /* untyped-object caps (UT caps) */
- paddr_t ut_obj_paddr_list [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each UT cap */
- uint8_t ut_obj_size_bits_list[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each UT cap */
- uint8_t it_cnode_size_bits; /* initial thread's root CNode size (2^n slots) */
- uint32_t num_dev_regs; /* number of device regions */
- bi_dev_reg_t dev_reg_list[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
- dom_t it_domain; /* initial thread's domain ID */
-} bi_t;
+#define S_REG_EMPTY (seL4_SlotRegion){ .start = 0, .end = 0 }
/* adjust constants in config.h if this assert fails */
-compile_assert(bi_size, sizeof(bi_t) <= BIT(BI_FRAME_SIZE_BITS))
+compile_assert(bi_size, sizeof(seL4_BootInfo) <= BIT(BI_FRAME_SIZE_BITS))
#endif
diff --git a/include/kernel/boot.h b/include/kernel/boot.h
index 28f23f36afc0e513a49d429aceb687d3fdf54a0c..791044587e9f6732f235cefd3737dfa3f9236a5d 100644
--- a/include/kernel/boot.h
+++ b/include/kernel/boot.h
@@ -32,9 +32,9 @@ typedef cte_t* slot_ptr_t;
typedef struct ndks_boot {
region_t freemem[MAX_NUM_FREEMEM_REG];
- bi_t* bi_frame;
- slot_pos_t slot_pos_cur;
- slot_pos_t slot_pos_max;
+ seL4_BootInfo* bi_frame;
+ seL4_SlotPos slot_pos_cur;
+ seL4_SlotPos slot_pos_max;
} ndks_boot_t;
extern ndks_boot_t ndks_boot;
@@ -67,7 +67,7 @@ pptr_t allocate_bi_frame(node_id_t node_id, word_t num_nodes, vptr_t ipcbuf_vptr
void create_bi_frame_cap(cap_t root_cnode_cap, cap_t pd_cap, pptr_t pptr, vptr_t vptr);
typedef struct create_frames_of_region_ret {
- slot_region_t region;
+ seL4_SlotRegion region;
bool_t success;
} create_frames_of_region_ret_t;
diff --git a/libsel4/include/sel4/bootinfo.h b/libsel4/include/sel4/bootinfo.h
index 9390100edb26e2774b5ba6e1b3f4c5ddd3e7659e..e4fcb81c400951477d6bc019a2f30674c08f743c 100644
--- a/libsel4/include/sel4/bootinfo.h
+++ b/libsel4/include/sel4/bootinfo.h
@@ -12,61 +12,7 @@
#define __LIBSEL4_BOOTINFO_H
#include <sel4/types.h>
-
-/* caps with fixed slot potitions in the root CNode */
-
-enum {
- seL4_CapNull = 0, /* null cap */
- seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
- seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
- seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
- seL4_CapIRQControl = 4, /* global IRQ controller cap */
- seL4_CapASIDControl = 5, /* global ASID controller cap */
- seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
- seL4_CapIOPort = 7, /* global IO port cap (null cap if not supported) */
- seL4_CapIOSpace = 8, /* global IO space cap (null cap if no IOMMU support) */
- seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
- seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
- seL4_CapDomain = 11, /* global domain controller cap */
- seL4_NumInitialCaps = 12
-};
-
-/* Legacy code will have assumptions on the vspace root being a Page Directory
- * type, so for now we define one to the other */
-#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
-
-/* types */
-
-typedef struct {
- seL4_Word start; /* first CNode slot position OF region */
- seL4_Word end; /* first CNode slot position AFTER region */
-} seL4_SlotRegion;
-
-typedef struct {
- seL4_Word basePaddr; /* base physical address of device region */
- seL4_Uint32 frameSizeBits; /* size (2^n bytes) of a device-region frame */
- seL4_SlotRegion frames; /* device-region frame caps */
-} seL4_DeviceRegion;
-
-typedef struct {
- seL4_Word nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
- seL4_Uint32 numNodes; /* number of seL4 nodes (1 if uniprocessor) */
- seL4_Uint32 numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
- seL4_IPCBuffer* ipcBuffer; /* pointer to initial thread's IPC buffer */
- seL4_SlotRegion empty; /* empty slots (null caps) */
- seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
- seL4_SlotRegion userImageFrames; /* userland-image frame caps */
- seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
- seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
- seL4_Word untypedPaddrList [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each untyped cap */
- seL4_Uint8 untypedSizeBitsList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each untyped cap */
- seL4_Uint8 initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
- seL4_Uint32 numDeviceRegions; /* number of device regions */
- seL4_DeviceRegion deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
- seL4_Uint32 initThreadDomain; /* Initial thread's domain ID */
-} seL4_BootInfo;
-
-/* function declarations */
+#include <sel4/bootinfo_types.h>
void seL4_InitBootInfo(seL4_BootInfo* bi);
seL4_BootInfo* seL4_GetBootInfo(void);
diff --git a/libsel4/include/sel4/bootinfo_types.h b/libsel4/include/sel4/bootinfo_types.h
new file mode 100644
index 0000000000000000000000000000000000000000..5b302022f44ea78ce887cbf5045894ae7abae8e0
--- /dev/null
+++ b/libsel4/include/sel4/bootinfo_types.h
@@ -0,0 +1,69 @@
+/*
+ * Copyright 2014, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ */
+
+#ifndef __LIBSEL4_BOOTINFO_TYPES_H
+#define __LIBSEL4_BOOTINFO_TYPES_H
+
+/* caps with fixed slot potitions in the root CNode */
+
+enum {
+ seL4_CapNull = 0, /* null cap */
+ seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
+ seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
+ seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
+ seL4_CapIRQControl = 4, /* global IRQ controller cap */
+ seL4_CapASIDControl = 5, /* global ASID controller cap */
+ seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
+ seL4_CapIOPort = 7, /* global IO port cap (null cap if not supported) */
+ seL4_CapIOSpace = 8, /* global IO space cap (null cap if no IOMMU support) */
+ seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
+ seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
+ seL4_CapDomain = 11, /* global domain controller cap */
+ seL4_NumInitialCaps = 12
+};
+
+/* Legacy code will have assumptions on the vspace root being a Page Directory
+ * type, so for now we define one to the other */
+#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
+
+/* types */
+typedef seL4_Word seL4_SlotPos;
+
+typedef struct {
+ seL4_SlotPos start; /* first CNode slot position OF region */
+ seL4_SlotPos end; /* first CNode slot position AFTER region */
+} seL4_SlotRegion;
+
+typedef struct {
+ seL4_Word basePaddr; /* base physical address of device region */
+ seL4_Word frameSizeBits; /* size (2^n bytes) of a device-region frame */
+ seL4_SlotRegion frames; /* device-region frame caps */
+} seL4_DeviceRegion;
+
+typedef struct {
+ seL4_NodeId nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
+ seL4_Word numNodes; /* number of seL4 nodes (1 if uniprocessor) */
+ seL4_Word numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
+ seL4_IPCBuffer* ipcBuffer; /* pointer to initial thread's IPC buffer */
+ seL4_SlotRegion empty; /* empty slots (null caps) */
+ seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
+ seL4_SlotRegion userImageFrames; /* userland-image frame caps */
+ seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
+ seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
+ seL4_PAddr untypedPaddrList [CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* physical address of each untyped cap */
+ seL4_Uint8 untypedSizeBitsList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* size (2^n) bytes of each untyped cap */
+ seL4_Uint8 initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
+ seL4_Word numDeviceRegions; /* number of device regions */
+ seL4_DeviceRegion deviceRegions[CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS]; /* device regions */
+ seL4_Domain initThreadDomain; /* Initial thread's domain ID */
+} seL4_BootInfo;
+
+
+#endif // __LIBSEL4_BOOTINFO_TYPES_H
diff --git a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/types.h b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/types.h
index b7edadd88b558f5fa13c59b78653f631cacd5658..d0ffc08d8a96dcb8cf94d34ce957a3ec32a1b5f0 100644
--- a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/types.h
+++ b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/types.h
@@ -15,6 +15,9 @@
typedef seL4_Uint32 seL4_Word;
typedef seL4_Word seL4_CPtr;
+typedef seL4_Word seL4_NodeId;
+typedef seL4_Word seL4_PAddr;
+typedef seL4_Word seL4_Domain;
typedef struct seL4_UserContext_ {
/* frame registers */
diff --git a/src/arch/arm/32/kernel/vspace.c b/src/arch/arm/32/kernel/vspace.c
index 19b91688dd7df28b0e6731f2a712880527ab0a96..1147b46cbade64cc16a74e32c5828db7505e4601 100644
--- a/src/arch/arm/32/kernel/vspace.c
+++ b/src/arch/arm/32/kernel/vspace.c
@@ -358,8 +358,8 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
cap_t pd_cap;
vptr_t pt_vptr;
pptr_t pt_pptr;
- slot_pos_t slot_pos_before;
- slot_pos_t slot_pos_after;
+ seL4_SlotPos slot_pos_before;
+ seL4_SlotPos slot_pos_after;
pptr_t pd_pptr;
/* create PD obj and cap */
@@ -378,7 +378,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
pd_pptr /* capPDBasePtr */
);
slot_pos_before = ndks_boot.slot_pos_cur;
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pd_cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pd_cap);
/* create all PT objs and caps necessary to cover userland image */
@@ -398,7 +398,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
- ndks_boot.bi_frame->ui_paging_caps = (slot_region_t) {
+ ndks_boot.bi_frame->userImagePaging = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
@@ -408,22 +408,22 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
BOOT_CODE bool_t
create_device_frames(cap_t root_cnode_cap)
{
- slot_pos_t slot_pos_before;
- slot_pos_t slot_pos_after;
+ seL4_SlotPos slot_pos_before;
+ seL4_SlotPos slot_pos_after;
vm_page_size_t frame_size;
region_t dev_reg;
- bi_dev_reg_t bi_dev_reg;
+ seL4_DeviceRegion bi_dev_reg;
cap_t frame_cap;
word_t i;
pptr_t f;
- ndks_boot.bi_frame->num_dev_regs = get_num_dev_p_regs();
- if (ndks_boot.bi_frame->num_dev_regs > CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS) {
+ ndks_boot.bi_frame->numDeviceRegions = get_num_dev_p_regs();
+ if (ndks_boot.bi_frame->numDeviceRegions > CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS) {
printf("Kernel init: Too many device regions for boot info\n");
- ndks_boot.bi_frame->num_dev_regs = CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS;
+ ndks_boot.bi_frame->numDeviceRegions = CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS;
}
- for (i = 0; i < ndks_boot.bi_frame->num_dev_regs; i++) {
+ for (i = 0; i < ndks_boot.bi_frame->numDeviceRegions; i++) {
/* write the frame caps of this device region into the root CNode and update the bootinfo */
dev_reg = paddr_to_pptr_reg(get_dev_p_reg(i));
/* use 1M frames if possible, otherwise use 4K frames */
@@ -447,12 +447,12 @@ create_device_frames(cap_t root_cnode_cap)
slot_pos_after = ndks_boot.slot_pos_cur;
/* add device-region entry to bootinfo */
- bi_dev_reg.base_paddr = pptr_to_paddr((void*)dev_reg.start);
- bi_dev_reg.frame_size_bits = pageBitsForSize(frame_size);
- bi_dev_reg.frame_caps = (slot_region_t) {
+ bi_dev_reg.basePaddr = pptr_to_paddr((void*)dev_reg.start);
+ bi_dev_reg.frameSizeBits = pageBitsForSize(frame_size);
+ bi_dev_reg.frames = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
- ndks_boot.bi_frame->dev_reg_list[i] = bi_dev_reg;
+ ndks_boot.bi_frame->deviceRegions[i] = bi_dev_reg;
}
return true;
diff --git a/src/arch/arm/kernel/boot.c b/src/arch/arm/kernel/boot.c
index 7feeba8b893bd46190a9ceaa6ed415aa99df299f..3e7a63d1f2829f8cf111cbf2d6a5e8ccf5ba34f1 100644
--- a/src/arch/arm/kernel/boot.c
+++ b/src/arch/arm/kernel/boot.c
@@ -133,10 +133,9 @@ init_irqs(cap_t root_cnode_cap)
setIRQState(IRQTimer, KERNEL_TIMER_IRQ);
/* provide the IRQ control cap */
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IRQ_CTRL), cap_irq_control_cap_new());
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
}
-
/* This and only this function initialises the CPU. It does NOT initialise any kernel state. */
BOOT_CODE static void
@@ -262,7 +261,7 @@ try_init_kernel(
if (!create_frames_ret.success) {
return false;
}
- ndks_boot.bi_frame->ui_frame_caps = create_frames_ret.region;
+ ndks_boot.bi_frame->userImageFrames = create_frames_ret.region;
/* create/initialise the initial thread's ASID pool */
it_ap_cap = create_it_asid_pool(root_cnode_cap);
@@ -310,7 +309,7 @@ try_init_kernel(
}
/* no shared-frame caps (ARM has no multikernel support) */
- ndks_boot.bi_frame->sh_frame_caps = S_REG_EMPTY;
+ ndks_boot.bi_frame->sharedFrames = S_REG_EMPTY;
/* finalise the bootinfo frame */
bi_finalise();
diff --git a/src/arch/x86/32/kernel/vspace.c b/src/arch/x86/32/kernel/vspace.c
index 765cbcefb9588d13b37e7347e89f2516030d572c..6717a961da99d3b1381c0445dfe8942f60218d3f 100644
--- a/src/arch/x86/32/kernel/vspace.c
+++ b/src/arch/x86/32/kernel/vspace.c
@@ -439,8 +439,8 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
cap_t vspace_cap;
vptr_t vptr;
pptr_t pptr;
- slot_pos_t slot_pos_before;
- slot_pos_t slot_pos_after;
+ seL4_SlotPos slot_pos_before;
+ seL4_SlotPos slot_pos_after;
slot_pos_before = ndks_boot.slot_pos_cur;
if (PDPT_BITS == 0) {
@@ -457,7 +457,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
if (!provide_cap(root_cnode_cap, pd_cap)) {
return cap_null_cap_new();
}
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pd_cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pd_cap);
vspace_cap = pd_cap;
} else {
cap_t pdpt_cap;
@@ -505,7 +505,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
/* now that PDs exist we can copy the global mappings */
copyGlobalMappings((vspace_root_t*)pdpt_pptr);
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE), pdpt_cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), pdpt_cap);
vspace_cap = pdpt_cap;
}
@@ -527,7 +527,7 @@ create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
- ndks_boot.bi_frame->ui_paging_caps = (slot_region_t) {
+ ndks_boot.bi_frame->userImagePaging = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
diff --git a/src/arch/x86/kernel/boot.c b/src/arch/x86/kernel/boot.c
index 1098dab9372dfabc8153ccb1482e0acfd6e933a4..1322565169096810534539a27002f13dc7031c81 100644
--- a/src/arch/x86/kernel/boot.c
+++ b/src/arch/x86/kernel/boot.c
@@ -59,7 +59,7 @@ init_irqs(cap_t root_cnode_cap)
}
Arch_irqStateInit();
/* provide the IRQ control cap */
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IRQ_CTRL), cap_irq_control_cap_new());
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
}
BOOT_CODE static bool_t
@@ -68,11 +68,11 @@ create_device_frames(
dev_p_regs_t* dev_p_regs
)
{
- slot_pos_t slot_pos_before;
- slot_pos_t slot_pos_after;
+ seL4_SlotPos slot_pos_before;
+ seL4_SlotPos slot_pos_after;
vm_page_size_t frame_size;
region_t dev_reg;
- bi_dev_reg_t bi_dev_reg;
+ seL4_DeviceRegion bi_dev_reg;
cap_t frame_cap;
uint32_t i;
pptr_t f;
@@ -101,15 +101,15 @@ create_device_frames(
slot_pos_after = ndks_boot.slot_pos_cur;
/* add device-region entry to bootinfo */
- bi_dev_reg.base_paddr = pptr_to_paddr((void*)dev_reg.start);
- bi_dev_reg.frame_size_bits = pageBitsForSize(frame_size);
- bi_dev_reg.frame_caps = (slot_region_t) {
+ bi_dev_reg.basePaddr = pptr_to_paddr((void*)dev_reg.start);
+ bi_dev_reg.frameSizeBits = pageBitsForSize(frame_size);
+ bi_dev_reg.frames = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
- ndks_boot.bi_frame->dev_reg_list[i] = bi_dev_reg;
+ ndks_boot.bi_frame->deviceRegions[i] = bi_dev_reg;
}
- ndks_boot.bi_frame->num_dev_regs = dev_p_regs->count;
+ ndks_boot.bi_frame->numDeviceRegions = dev_p_regs->count;
return true;
}
@@ -219,7 +219,7 @@ init_sys_state(
/* create the IO port cap */
write_slot(
- SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IO_PORT),
+ SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIOPort),
cap_io_port_cap_new(
0, /* first port */
NUM_IO_PORTS - 1 /* last port */
@@ -276,7 +276,7 @@ init_sys_state(
if (!create_frames_ret.success) {
return false;
}
- ndks_boot.bi_frame->ui_frame_caps = create_frames_ret.region;
+ ndks_boot.bi_frame->userImageFrames = create_frames_ret.region;
/* create the initial thread's ASID pool */
it_ap_cap = create_it_asid_pool(root_cnode_cap);
@@ -318,12 +318,12 @@ init_sys_state(
}
/* write number of IOMMU PT levels into bootinfo */
- ndks_boot.bi_frame->num_iopt_levels = x86KSnumIOPTLevels;
+ ndks_boot.bi_frame->numIOPTLevels = x86KSnumIOPTLevels;
/* write IOSpace master cap */
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IO_SPACE), master_iospace_cap());
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIOSpace), master_iospace_cap());
} else {
- ndks_boot.bi_frame->num_iopt_levels = -1;
+ ndks_boot.bi_frame->numIOPTLevels = -1;
}
/* convert the remaining free memory into UT objects and provide the caps */
diff --git a/src/kernel/boot.c b/src/kernel/boot.c
index 60364e52345b44c9ab56b24160dc87b56ec301c6..31d9297540576d0e67c25cdb889150db9cef697c 100644
--- a/src/kernel/boot.c
+++ b/src/kernel/boot.c
@@ -131,7 +131,7 @@ write_slot(slot_ptr_t slot_ptr, cap_t cap)
*/
compile_assert(root_cnode_size_valid,
CONFIG_ROOT_CNODE_SIZE_BITS < 32 - seL4_SlotBits &&
- (1U << CONFIG_ROOT_CNODE_SIZE_BITS) >= BI_CAP_DYN_START)
+ (1U << CONFIG_ROOT_CNODE_SIZE_BITS) >= seL4_NumInitialCaps)
BOOT_CODE cap_t
create_root_cnode(void)
@@ -158,7 +158,7 @@ create_root_cnode(void)
);
/* write the root CNode cap into the root CNode */
- write_slot(SLOT_PTR(pptr, BI_CAP_IT_CNODE), cap);
+ write_slot(SLOT_PTR(pptr, seL4_CapInitThreadCNode), cap);
return cap;
}
@@ -200,7 +200,7 @@ create_domain_cap(cap_t root_cnode_cap)
}
cap = cap_domain_cap_new();
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_DOM), cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapDomain), cap);
}
@@ -220,7 +220,7 @@ create_ipcbuf_frame(cap_t root_cnode_cap, cap_t pd_cap, vptr_t vptr)
/* create a cap of it and write it into the root CNode */
cap = create_mapped_it_frame_cap(pd_cap, pptr, vptr, IT_ASID, false, false);
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), cap);
return cap;
}
@@ -237,7 +237,7 @@ create_bi_frame_cap(
/* create a cap of it and write it into the root CNode */
cap = create_mapped_it_frame_cap(pd_cap, pptr, vptr, IT_ASID, false, false);
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_BI_FRAME), cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapBootInfoFrame), cap);
}
BOOT_CODE pptr_t
@@ -259,14 +259,14 @@ allocate_bi_frame(
/* initialise bootinfo-related global state */
ndks_boot.bi_frame = BI_PTR(pptr);
- ndks_boot.slot_pos_cur = BI_CAP_DYN_START;
+ ndks_boot.slot_pos_cur = seL4_NumInitialCaps;
- BI_PTR(pptr)->node_id = node_id;
- BI_PTR(pptr)->num_nodes = num_nodes;
- BI_PTR(pptr)->num_iopt_levels = 0;
- BI_PTR(pptr)->ipcbuf_vptr = ipcbuf_vptr;
- BI_PTR(pptr)->it_cnode_size_bits = CONFIG_ROOT_CNODE_SIZE_BITS;
- BI_PTR(pptr)->it_domain = ksDomSchedule[ksDomScheduleIdx].domain;
+ BI_PTR(pptr)->nodeID = node_id;
+ BI_PTR(pptr)->numNodes = num_nodes;
+ BI_PTR(pptr)->numIOPTLevels = 0;
+ BI_PTR(pptr)->ipcBuffer = (seL4_IPCBuffer *) ipcbuf_vptr;
+ BI_PTR(pptr)->initThreadCNodeSizeBits = CONFIG_ROOT_CNODE_SIZE_BITS;
+ BI_PTR(pptr)->initThreadDomain = ksDomSchedule[ksDomScheduleIdx].domain;
return pptr;
}
@@ -294,8 +294,8 @@ create_frames_of_region(
{
pptr_t f;
cap_t frame_cap;
- slot_pos_t slot_pos_before;
- slot_pos_t slot_pos_after;
+ seL4_SlotPos slot_pos_before;
+ seL4_SlotPos slot_pos_after;
slot_pos_before = ndks_boot.slot_pos_cur;
@@ -314,7 +314,7 @@ create_frames_of_region(
slot_pos_after = ndks_boot.slot_pos_cur;
return (create_frames_of_region_ret_t) {
- (slot_region_t) { slot_pos_before, slot_pos_after }, true
+ (seL4_SlotRegion) { slot_pos_before, slot_pos_after }, true
};
}
@@ -332,11 +332,11 @@ create_it_asid_pool(cap_t root_cnode_cap)
}
memzero(ASID_POOL_PTR(ap_pptr), 1 << seL4_ASIDPoolBits);
ap_cap = cap_asid_pool_cap_new(IT_ASID >> asidLowBits, ap_pptr);
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_ASID_POOL), ap_cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadASIDPool), ap_cap);
/* create ASID control cap */
write_slot(
- SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_ASID_CTRL),
+ SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapASIDControl),
cap_asid_control_cap_new()
);
@@ -385,7 +385,7 @@ create_initial_thread(
Arch_initContext(&tcb->tcbArch.tcbContext);
/* derive a copy of the IPC buffer cap for inserting */
- dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), ipcbuf_cap);
+ dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer), ipcbuf_cap);
if (dc_ret.status != EXCEPTION_NONE) {
printf("Failed to derive copy of IPC Buffer\n");
return false;
@@ -394,17 +394,17 @@ create_initial_thread(
/* initialise TCB (corresponds directly to abstract specification) */
cteInsert(
root_cnode_cap,
- SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_CNODE),
+ SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadCNode),
SLOT_PTR(pptr, tcbCTable)
);
cteInsert(
it_pd_cap,
- SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_VSPACE),
+ SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace),
SLOT_PTR(pptr, tcbVTable)
);
cteInsert(
dc_ret.cap,
- SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF),
+ SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadIPCBuffer),
SLOT_PTR(pptr, tcbBuffer)
);
tcb->tcbIPCBuffer = ipcbuf_vptr;
@@ -423,7 +423,7 @@ create_initial_thread(
/* create initial thread's TCB cap */
cap = cap_thread_cap_new(TCB_REF(tcb));
- write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_TCB), cap);
+ write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadTCB), cap);
#ifdef DEBUG
setThreadName(tcb, "rootserver");
@@ -437,14 +437,14 @@ provide_untyped_cap(
cap_t root_cnode_cap,
pptr_t pptr,
word_t size_bits,
- slot_pos_t first_untyped_slot
+ seL4_SlotPos first_untyped_slot
)
{
bool_t ret;
word_t i = ndks_boot.slot_pos_cur - first_untyped_slot;
if (i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS) {
- ndks_boot.bi_frame->ut_obj_paddr_list[i] = pptr_to_paddr((void*)pptr);
- ndks_boot.bi_frame->ut_obj_size_bits_list[i] = size_bits;
+ ndks_boot.bi_frame->untypedPaddrList[i] = pptr_to_paddr((void*)pptr);
+ ndks_boot.bi_frame->untypedSizeBitsList[i] = size_bits;
ret = provide_cap(root_cnode_cap, cap_untyped_cap_new(0, size_bits, pptr));
} else {
printf("Kernel init: Too many untyped regions for boot info\n");
@@ -465,7 +465,7 @@ BOOT_CODE static bool_t
create_untypeds_for_region(
cap_t root_cnode_cap,
region_t reg,
- slot_pos_t first_untyped_slot
+ seL4_SlotPos first_untyped_slot
)
{
word_t align_bits;
@@ -495,8 +495,8 @@ create_untypeds_for_region(
BOOT_CODE bool_t
create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
{
- slot_pos_t slot_pos_before;
- slot_pos_t slot_pos_after;
+ seL4_SlotPos slot_pos_before;
+ seL4_SlotPos slot_pos_after;
word_t i;
region_t reg;
@@ -517,7 +517,7 @@ create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
}
slot_pos_after = ndks_boot.slot_pos_cur;
- ndks_boot.bi_frame->ut_obj_caps = (slot_region_t) {
+ ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
return true;
@@ -526,9 +526,9 @@ create_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg)
BOOT_CODE void
bi_finalise(void)
{
- slot_pos_t slot_pos_start = ndks_boot.slot_pos_cur;
- slot_pos_t slot_pos_end = ndks_boot.slot_pos_max;
- ndks_boot.bi_frame->null_caps = (slot_region_t) {
+ seL4_SlotPos slot_pos_start = ndks_boot.slot_pos_cur;
+ seL4_SlotPos slot_pos_end = ndks_boot.slot_pos_max;
+ ndks_boot.bi_frame->empty = (seL4_SlotRegion) {
slot_pos_start, slot_pos_end
};
}