RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

Create device untypeds at boot for all arches

Browse Source 
Currently on x86 device untypeds are generated by passing the entire
address space minus any parts that are reserved by the kernel or that
are "real" memory (e.g. kernel image, physical RAM).

On ARM and RISC-V, device untypeds were generated at compile-time from
a device tree. This patch moves ARM and RISC-V to use the same approach
as x86, and moves the code from x86 into a common location that's
shared between the three architectures.

Co-Authored-By: Anna Lyons <anna@gh.st>
This commit is contained in:
Simon Shields
2019-10-08 12:16:41 +11:00
parent 28c1ff4b4b
commit b5c56244f1
20 changed files with 260 additions and 217 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
config.cmake
View File

@@ -198,6 +198,7 @@ endif()
# Enshrine common variables in the config
config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}")
config_set(KernelPaddrUserTop PADDR_USER_DEVICE_TOP "${KernelPaddrUserTop}")
# System parameters
config_string(

30
include/arch/arm/arch/bootinfo.h Normal file
View File

@@ -0,0 +1,30 @@
/*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(DATA61_GPL)
*/
#ifndef __ARCH_BOOTINFO_H
#define __ARCH_BOOTINFO_H
/* Modifiers:
* + 1: allow the kernel to release its own boot data region
* + 1: possible gap between ELF images and rootserver objects;
* see arm/arch_init_freemem */
#define MAX_NUM_FREEMEM_REG (ARRAY_SIZE(avail_p_regs) + MODE_RESERVED + 1 + 1)
/* The maximum number of reserved regions is:
* - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
* - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
* - 1 for each mode-reserved region. (MODE_RESERVED)
* - 1 each for kernel, dtb, and user image. (3)
*/
#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
#endif

1
include/arch/arm/arch/types.h
View File

@@ -52,6 +52,7 @@ typedef struct kernel_frame {
paddr_t paddr;
pptr_t pptr;
int armExecuteNever;
int userAvailable;
} kernel_frame_t;
#endif

31
include/arch/riscv/arch/bootinfo.h Normal file
View File

@@ -0,0 +1,31 @@
/*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(DATA61_GPL)
*/
#ifndef __ARCH_BOOTINFO_H
#define __ARCH_BOOTINFO_H
#define MAX_NUM_FREEMEM_REG 16
/* The maximum number of reserved regions is:
* - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
* - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
* - 1 for each mode-reserved region. (MODE_RESERVED)
* - 1 each for kernel, dtb, and user image. (3)
*/
#ifndef CONFIG_PLAT_SPIKE
#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
#else
/* spike has no devices, and ARRAY_SIZE(NULL) is invalid. */
#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + MODE_RESERVED + 3)
#endif
#endif

2
include/arch/riscv/arch/machine/hardware.h
View File

@@ -54,6 +54,8 @@
#define PAGE_BITS seL4_PageBits
#define MODE_RESERVED 0
/* MMU RISC-V related definitions. See RISC-V manual priv-1.10 */
/* Extract the n-level PT index from a virtual address. This works for any

1
include/arch/riscv/arch/types.h
View File

@@ -49,6 +49,7 @@ typedef dom_t seL4_Domain;
typedef struct kernel_frame {
paddr_t paddr;
pptr_t pptr;
int userAvailable;
} kernel_frame_t;
#endif

29
include/arch/x86/arch/bootinfo.h Normal file
View File

@@ -0,0 +1,29 @@
/*
* Copyright 2019, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(DATA61_GPL)
*/
#ifndef __ARCH_BOOTINFO_H
#define __ARCH_BOOTINFO_H
#define MAX_NUM_FREEMEM_REG 16
/*
* The maximum number of reserved regions we have is:
* - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
* - 1 for each kernel device:
* - ioapics (CONFIG_MAX_NUM_IOAPIC)
* - iommus (MAX_NUM_DRHU)
* - apic (1)
* - the reserved MSI region (1)
*/
#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + CONFIG_MAX_NUM_IOAPIC + MAX_NUM_DRHU + 2)
#endif

22
include/kernel/boot.h
View File

@@ -12,6 +12,7 @@
#define __KERNEL_BOOT_H
#include <bootinfo.h>
#include <arch/bootinfo.h>
#ifndef CONFIG_ARCH_ARM
#define MAX_NUM_FREEMEM_REG 16
@@ -23,6 +24,23 @@
#define MAX_NUM_FREEMEM_REG (ARRAY_SIZE(avail_p_regs) + MODE_RESERVED + 1 + 1)
#endif
#ifdef CONFIG_ARCH_X86
#else
/* The maximum number of reserved regions is:
* - 1 for each physical memory region (MAX_NUM_FREEMEM_REG)
* - 1 for each kernel device (ARRAY_SIZE(kernel_devices))
* - 1 for each mode-reserved region. (MODE_RESERVED)
* - 1 each for kernel, dtb, and user image. (3)
*/
#ifndef CONFIG_PLAT_SPIKE
#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + ARRAY_SIZE(kernel_devices) + MODE_RESERVED + 3)
#else
/* spike has no devices */
#define MAX_NUM_RESV_REG (MAX_NUM_FREEMEM_REG + MODE_RESERVED + 3)
#endif
#endif
/*
* Resolve naming differences between the abstract specifications
* of the bootstrapping phase and the runtime phase of the kernel.
@@ -35,6 +53,8 @@ typedef cte_t *slot_ptr_t;
/* (node-local) state accessed only during bootstrapping */
typedef struct ndks_boot {
p_region_t reserved[MAX_NUM_RESV_REG];
word_t resv_count;
region_t freemem[MAX_NUM_FREEMEM_REG];
seL4_BootInfo *bi_frame;
seL4_SlotPos slot_pos_cur;
@@ -53,6 +73,7 @@ static inline bool_t is_reg_empty(region_t reg)
void init_freemem(word_t n_available, const p_region_t *available,
word_t n_reserved, region_t *reserved,
v_region_t it_v_reg, word_t extra_bi_size_bits);
bool_t reserve_region(p_region_t reg);
bool_t insert_region(region_t reg);
void write_slot(slot_ptr_t slot_ptr, cap_t cap);
cap_t create_root_cnode(void);
@@ -62,6 +83,7 @@ void write_it_pd_pts(cap_t root_cnode_cap, cap_t it_pd_cap);
bool_t create_idle_thread(void);
bool_t create_untypeds_for_region(cap_t root_cnode_cap, bool_t device_memory, region_t reg,
seL4_SlotPos first_untyped_slot);
bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before);
bool_t create_kernel_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg, seL4_SlotPos first_untyped_slot);
void bi_finalise(void);
void create_domain_cap(cap_t root_cnode_cap);

4
include/plat/pc99/plat/32/plat_mode/machine/hardware.h
View File

@@ -49,10 +49,6 @@
#define PADDR_TOP (PPTR_TOP - BASE_OFFSET)
/* The maximum physical address for device untypeds that we export to
* the user */
#define PADDR_USER_DEVICE_TOP 0xffff0000
/* The kernel base offset is a way to translate the kernel image segment
* from virtual to physical. This translation must be a single offset for
* for the entire segment (i.e. the kernel image must be contiguous both

4
include/plat/pc99/plat/64/plat_mode/machine/hardware.h
View File

@@ -62,10 +62,6 @@
#define KERNEL_BASE_OFFSET (KERNEL_BASE - PADDR_BASE)
#define kernelBase KERNEL_BASE
/* The maximum physical address for device untypeds that we export to
* the user */
#define PADDR_USER_DEVICE_TOP BIT(47)
#define BASE_OFFSET PPTR_BASE
#ifndef __ASSEMBLER__

17
src/arch/arm/kernel/boot.c
View File

@@ -130,25 +130,10 @@ BOOT_CODE static bool_t create_untypeds(cap_t root_cnode_cap, region_t boot_mem_
{
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
region_t dev_reg;
word_t i;
slot_pos_before = ndks_boot.slot_pos_cur;
create_device_untypeds(root_cnode_cap, slot_pos_before);
create_kernel_untypeds(root_cnode_cap, boot_mem_reuse_reg, slot_pos_before);
UNUSED paddr_t current_region_pos = 0;
for (i = 0; i < get_num_dev_p_regs(); i++) {
/* It is required that untyped regions are non-overlapping.
* We assume that hardware regions are defined in ascending order to make
* overlapping checks simpler
*/
assert(get_dev_p_reg(i).start >= current_region_pos);
current_region_pos = get_dev_p_reg(i).end;
dev_reg = paddr_to_pptr_reg(get_dev_p_reg(i));
if (!create_untypeds_for_region(root_cnode_cap, true,
dev_reg, slot_pos_before)) {
return false;
}
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {

17
src/arch/arm/machine/hardware.c
View File

@@ -28,16 +28,6 @@ BOOT_CODE int get_num_avail_p_regs(void)
return sizeof(avail_p_regs) / sizeof(p_region_t);
}
BOOT_CODE int get_num_dev_p_regs(void)
{
return sizeof(dev_p_regs) / sizeof(p_region_t);
}
BOOT_CODE p_region_t get_dev_p_reg(word_t i)
{
return dev_p_regs[i];
}
BOOT_CODE const p_region_t *get_avail_p_regs(void)
{
return (const p_region_t *) avail_p_regs;
@@ -51,6 +41,13 @@ BOOT_CODE void map_kernel_devices(void)
VMKernelOnly,
vm_attributes_new(kernel_devices[i].armExecuteNever,
false, false));
if (!kernel_devices[i].userAvailable) {
p_region_t reg = {
.start = kernel_devices[i].paddr,
.end = kernel_devices[i].paddr + (1 << PAGE_BITS),
};
reserve_region(reg);
}
}
}

13
src/arch/riscv/kernel/boot.c
View File

@@ -46,22 +46,11 @@ BOOT_CODE static bool_t create_untypeds(cap_t root_cnode_cap, region_t boot_mem_
{
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
region_t dev_reg;
slot_pos_before = ndks_boot.slot_pos_cur;
create_device_untypeds(root_cnode_cap, slot_pos_before);
bool_t res = create_kernel_untypeds(root_cnode_cap, boot_mem_reuse_reg, slot_pos_before);
UNUSED paddr_t current_region_pos = 0;
for (int i = 0; i < get_num_dev_p_regs(); i++) {
assert(get_dev_p_reg(i).start >= current_region_pos);
current_region_pos = get_dev_p_reg(i).end;
dev_reg = paddr_to_pptr_reg(get_dev_p_reg(i));
if (!create_untypeds_for_region(root_cnode_cap, true,
dev_reg, slot_pos_before)) {
return false;
}
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after

30
src/arch/riscv/machine/hardware.c
View File

@@ -58,29 +58,6 @@ BOOT_CODE p_region_t *get_avail_p_regs(void)
return (p_region_t *) avail_p_regs;
}
BOOT_CODE int get_num_dev_p_regs(void)
{
if (dev_p_regs != NULL) {
return (sizeof(dev_p_regs) / sizeof(p_region_t));
} else {
return 0;
}
}
BOOT_CODE p_region_t get_dev_p_reg(word_t i)
{
/* We need this if guard as some RISC-V configurations don't declare any
* device regions and some compilers complain about indexing an empty array
* due to not being able to infer that get_dev_p_reg is only called if
* dev_p_regs contains entries.
*/
if (get_num_dev_p_regs() == 0) {
printf("%s: No devices present.\n", __func__);
halt();
}
return dev_p_regs[i];
}
BOOT_CODE void map_kernel_devices(void)
{
if (kernel_devices == NULL) {
@@ -90,6 +67,13 @@ BOOT_CODE void map_kernel_devices(void)
for (int i = 0; i < (sizeof(kernel_devices) / sizeof(kernel_frame_t)); i++) {
map_kernel_frame(kernel_devices[i].paddr, KDEV_PPTR,
VMKernelOnly);
if (!kernel_devices[i].userAvailable) {
p_region_t reg = {
.start = kernel_devices[i].paddr,
.end = kernel_devices[i].paddr + (1 << PAGE_BITS),
};
reserve_region(reg);
}
}
}

125
src/arch/x86/kernel/boot.c
View File

@@ -71,140 +71,17 @@ BOOT_CODE static void init_irqs(cap_t root_cnode_cap)
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapIRQControl), cap_irq_control_cap_new());
}
/* The maximum number of reserved regions we have is 1 for each physical memory region (+ MAX_NUM_FREEMEM_REG)
* plus 1 for each kernel device. For kernel devices we have the ioapics (+ CONFIG_MAX_NUM_IOAPIC),
* iommus (+ MAX_NUM_DRHU), apic (+ 1) and the reserved MSI region (+ 1) */
#define NUM_RESERVED_REGIONS (MAX_NUM_FREEMEM_REG + CONFIG_MAX_NUM_IOAPIC + MAX_NUM_DRHU + 2)
typedef struct allocated_p_region {
p_region_t regs[NUM_RESERVED_REGIONS];
word_t cur_pos;
} allocated_p_region_t;
BOOT_BSS static allocated_p_region_t allocated_p_regions;
BOOT_CODE static void merge_regions(void)
{
unsigned int i, j;
/* Walk through all the regions and see if any can get merged */
for (i = 1; i < allocated_p_regions.cur_pos;) {
if (allocated_p_regions.regs[i - 1].end == allocated_p_regions.regs[i].start) {
/* move this down */
allocated_p_regions.regs[i - 1].end = allocated_p_regions.regs[i].end;
/* fill the rest down */
for (j = i; j < allocated_p_regions.cur_pos - 1; j++) {
allocated_p_regions.regs[j] = allocated_p_regions.regs[j + 1];
}
allocated_p_regions.cur_pos--;
/* don't increment 'i' since we want to recheck that the
* region we just moved to this slot doesn't also need merging */
} else {
i++;
}
}
}
static UNUSED BOOT_CODE bool_t p_region_overlaps(p_region_t reg)
{
unsigned int i;
for (i = 0; i < allocated_p_regions.cur_pos; i++) {
if (allocated_p_regions.regs[i].start < reg.end &&
allocated_p_regions.regs[i].end > reg.start) {
return true;
}
}
return false;
}
BOOT_CODE bool_t add_allocated_p_region(p_region_t reg)
{
unsigned int i, j;
assert(reg.start <= reg.end);
assert(!p_region_overlaps(reg));
/* Walk the existing regions and see if we can merge with an existing
* region, or insert in order */
for (i = 0; i < allocated_p_regions.cur_pos; i++) {
/* see if we can merge before or after this region */
if (allocated_p_regions.regs[i].end == reg.start) {
allocated_p_regions.regs[i].end = reg.end;
merge_regions();
return true;
}
if (allocated_p_regions.regs[i].start == reg.end) {
allocated_p_regions.regs[i].start = reg.start;
merge_regions();
return true;
}
/* see if this new one should be inserted before */
if (reg.end < allocated_p_regions.regs[i].start) {
/* ensure there's space to bump the regions up */
if (allocated_p_regions.cur_pos + 1 == NUM_RESERVED_REGIONS) {
printf("Ran out of reserved physical regions\n");
return false;
}
/* Copy the regions up to make a gap */
for (j = allocated_p_regions.cur_pos; j != i; j--) {
allocated_p_regions.regs[j] = allocated_p_regions.regs[j - 1];
}
/* Put this region in the gap */
allocated_p_regions.regs[i] = reg;
allocated_p_regions.cur_pos++;
return true;
}
}
/* nothing else matched, put this one at the end */
if (i + 1 == NUM_RESERVED_REGIONS) {
printf("Ran out of reserved physical regions\n");
return false;
}
allocated_p_regions.regs[i] = reg;
allocated_p_regions.cur_pos = i + 1;
return true;
}
BOOT_CODE void init_allocated_p_regions(void)
{
allocated_p_regions.cur_pos = 0;
}
BOOT_CODE static bool_t create_untypeds(
cap_t root_cnode_cap,
region_t boot_mem_reuse_reg)
{
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
word_t i;
paddr_t start = 0;
slot_pos_before = ndks_boot.slot_pos_cur;
create_device_untypeds(root_cnode_cap, slot_pos_before);
create_kernel_untypeds(root_cnode_cap, boot_mem_reuse_reg, slot_pos_before);
for (i = 0; i < allocated_p_regions.cur_pos; i++) {
if (start != allocated_p_regions.regs[i].start) {
if (!create_untypeds_for_region(root_cnode_cap, true,
paddr_to_pptr_reg((p_region_t) {
start, allocated_p_regions.regs[i].start
}),
slot_pos_before)) {
return false;
}
}
start = allocated_p_regions.regs[i].end;
}
if (start != PADDR_USER_DEVICE_TOP) {
if (!create_untypeds_for_region(root_cnode_cap, true,
paddr_to_pptr_reg((p_region_t) {
start, PADDR_USER_DEVICE_TOP
}),
slot_pos_before)) {
return false;
}
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->untyped = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after

4
src/arch/x86/kernel/boot_sys.c
View File

@@ -218,7 +218,7 @@ static BOOT_CODE bool_t add_mem_p_regs(p_region_t reg)
printf("Adding physical memory region 0x%lx-0x%lx\n", reg.start, reg.end);
boot_state.mem_p_regs.list[boot_state.mem_p_regs.count] = reg;
boot_state.mem_p_regs.count++;
return add_allocated_p_region(reg);
return reserve_region(reg);
}
/*
@@ -562,7 +562,6 @@ static BOOT_CODE bool_t try_boot_sys_mbi1(
* include all the physical memory in the kernel window, but also includes any
* important or kernel devices. */
boot_state.mem_p_regs.count = 0;
init_allocated_p_regions();
if (mbi->part1.flags & MULTIBOOT_INFO_MMAP_FLAG) {
if (!parse_mem_map(mbi->part2.mmap_length, mbi->part2.mmap_addr)) {
return false;
@@ -626,7 +625,6 @@ static BOOT_CODE bool_t try_boot_sys_mbi2(
* include all the physical memory in the kernel window, but also includes any
* important or kernel devices. */
boot_state.mem_p_regs.count = 0;
init_allocated_p_regions();
boot_state.mb_mmap_info.mmap_length = 0;
boot_state.vbe_info.vbeMode = -1;

6
src/arch/x86/kernel/vspace.c
View File

@@ -140,7 +140,7 @@ BOOT_CODE bool_t map_kernel_window_devices(pte_t *pt, uint32_t num_ioapic, paddr
if (!phys) {
return false;
}
if (!add_allocated_p_region((p_region_t) {
if (!reserve_region((p_region_t) {
phys, phys + 0x1000
})) {
return false;
@@ -152,7 +152,7 @@ BOOT_CODE bool_t map_kernel_window_devices(pte_t *pt, uint32_t num_ioapic, paddr
idx++;
for (i = 0; i < num_ioapic; i++) {
phys = ioapic_paddrs[i];
if (!add_allocated_p_region((p_region_t) {
if (!reserve_region((p_region_t) {
phys, phys + 0x1000
})) {
return false;
@@ -176,7 +176,7 @@ BOOT_CODE bool_t map_kernel_window_devices(pte_t *pt, uint32_t num_ioapic, paddr
/* map kernel devices: IOMMUs */
for (i = 0; i < num_drhu; i++) {
phys = (paddr_t)drhu_list[i];
if (!add_allocated_p_region((p_region_t) {
if (!reserve_region((p_region_t) {
phys, phys + 0x1000
})) {
return false;

115
src/kernel/boot.c
View File

@@ -27,6 +27,77 @@ ndks_boot_t ndks_boot BOOT_DATA;
rootserver_mem_t rootserver BOOT_DATA;
static region_t rootserver_mem BOOT_DATA;
BOOT_CODE static void merge_regions(void)
{
/* Walk through reserved regions and see if any can be merged */
for (word_t i = 1; i < ndks_boot.resv_count;) {
if (ndks_boot.reserved[i - 1].end == ndks_boot.reserved[i].start) {
/* extend earlier region */
ndks_boot.reserved[i - 1].end = ndks_boot.reserved[i].end;
/* move everything else down */
for (word_t j = i + 1; j < ndks_boot.resv_count; j++) {
ndks_boot.reserved[j - 1] = ndks_boot.reserved[j];
}
ndks_boot.resv_count--;
/* don't increment i in case there are multiple adjacent regions */
} else {
i++;
}
}
}
BOOT_CODE bool_t reserve_region(p_region_t reg)
{
word_t i;
assert(reg.start <= reg.end);
if (reg.start == reg.end) {
return true;
}
/* keep the regions in order */
for (i = 0; i < ndks_boot.resv_count; i++) {
/* Try and merge the region to an existing one, if possible */
if (ndks_boot.reserved[i].start == reg.end) {
ndks_boot.reserved[i].start = reg.start;
merge_regions();
return true;
}
if (ndks_boot.reserved[i].end == reg.start) {
ndks_boot.reserved[i].end = reg.end;
merge_regions();
return true;
}
/* Otherwise figure out where it should go. */
if (ndks_boot.reserved[i].start > reg.end) {
/* move regions down, making sure there's enough room */
if (ndks_boot.resv_count + 1 >= MAX_NUM_RESV_REG) {
printf("Can't mark region 0x%lx-0x%lx as reserved, try increasing MAX_NUM_RESV_REG (currently %d)\n",
reg.start, reg.end, (int)MAX_NUM_RESV_REG);
return false;
}
for (word_t j = ndks_boot.resv_count; j > i; j--) {
ndks_boot.reserved[j] = ndks_boot.reserved[j - 1];
}
/* insert the new region */
ndks_boot.reserved[i] = reg;
ndks_boot.resv_count++;
return true;
}
}
if (i + 1 == MAX_NUM_RESV_REG) {
printf("Can't mark region 0x%lx-0x%lx as reserved, try increasing MAX_NUM_RESV_REG (currently %d)\n",
reg.start, reg.end, (int)MAX_NUM_RESV_REG);
return false;
}
ndks_boot.reserved[i] = reg;
ndks_boot.resv_count++;
return true;
}
BOOT_CODE bool_t insert_region(region_t reg)
{
word_t i;
@@ -37,6 +108,7 @@ BOOT_CODE bool_t insert_region(region_t reg)
}
for (i = 0; i < MAX_NUM_FREEMEM_REG; i++) {
if (is_reg_empty(ndks_boot.freemem[i])) {
reserve_region(pptr_to_paddr_reg(reg));
ndks_boot.freemem[i] = reg;
return true;
}
@@ -550,6 +622,40 @@ BOOT_CODE bool_t create_untypeds_for_region(
return true;
}
BOOT_CODE bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before)
{
paddr_t start = 0;
for (word_t i = 0; i < ndks_boot.resv_count; i++) {
if (start < ndks_boot.reserved[i].start) {
region_t reg = paddr_to_pptr_reg((p_region_t) {
start, ndks_boot.reserved[i].start
});
if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) {
return false;
}
}
start = ndks_boot.reserved[i].end;
}
if (start < CONFIG_PADDR_USER_DEVICE_TOP) {
region_t reg = paddr_to_pptr_reg((p_region_t) {
start, CONFIG_PADDR_USER_DEVICE_TOP
});
/*
* The auto-generated bitfield code will get upset if the
* end pptr is larger than the maximum pointer size for this architecture.
*/
if (reg.end > PPTR_TOP) {
reg.end = PPTR_TOP;
}
if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) {
return false;
}
}
return true;
}
BOOT_CODE bool_t create_kernel_untypeds(cap_t root_cnode_cap, region_t boot_mem_reuse_reg,
seL4_SlotPos first_untyped_slot)
{
@@ -640,6 +746,7 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
a++;
} else if (reserved[r].end <= avail_reg[a].start) {
/* the reserved region is below the available region - skip it*/
reserve_region(pptr_to_paddr_reg(reserved[r]));
r++;
} else if (reserved[r].start >= avail_reg[a].end) {
/* the reserved region is above the available region - take the whole thing */
@@ -651,6 +758,7 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
/* the region overlaps with the start of the available region.
* trim start of the available region */
avail_reg[a].start = MIN(avail_reg[a].end, reserved[r].end);
reserve_region(pptr_to_paddr_reg(reserved[r]));
r++;
} else {
assert(reserved[r].start < avail_reg[a].end);
@@ -661,6 +769,7 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
insert_region(m);
if (avail_reg[a].end > reserved[r].end) {
avail_reg[a].start = reserved[r].end;
reserve_region(pptr_to_paddr_reg(reserved[r]));
r++;
} else {
a++;
@@ -669,6 +778,12 @@ BOOT_CODE void init_freemem(word_t n_available, const p_region_t *available,
}
}
for (; r < n_reserved; r++) {
if (reserved[r].start < reserved[r].end) {
reserve_region(pptr_to_paddr_reg(reserved[r]));
}
}
/* no more reserved regions - add the rest */
for (; a < n_available; a++) {
if (avail_reg[a].start < avail_reg[a].end) {

4
src/plat/pc99/machine/hardware.c
View File

@@ -24,8 +24,8 @@ 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 (PADDR_USER_DEVICE_TOP > 0xFFFFFFF8) {
if (!add_allocated_p_region((p_region_t) {
if (CONFIG_PADDR_USER_DEVICE_TOP > 0xFFFFFFF8) {
if (!reserve_region((p_region_t) {
(word_t)0xFFFFFFF8, (word_t)0xFFFFFFF8 + 8
})) {
return false;

21
tools/hardware/outputs/c_header.py
View File

@@ -91,6 +91,11 @@ static const kernel_frame_t BOOT_RODATA kernel_devices[] = {
{% if args.arch == 'arm' %}
true, /* armExecuteNever */
{% endif %}
{% if group.user_ok %}
true, /* userAvailable */
{% else %}
false, /* userAvailable */
{% endif %}
},
{% endfor %}
{% if group.has_macro() %}
@@ -109,18 +114,6 @@ static const p_region_t BOOT_RODATA avail_p_regs[] = {
{% endfor %}
};
/* DEVICE MEMORY */
/* using {{ physBits }} bits of address space */
/* excluded regions:
{% for reg in excluded_regions %}
* {{ "0x{:x}".format(reg.base) }} - {{ "0x{:x}".format(reg.base + reg.size) }} {{ reg.desc }} {{ reg.user_ok }}
{% endfor %}
*/
static const p_region_t BOOT_RODATA dev_p_regs[] = {
{% for reg in device_regions %}
{ {{ "0x{:x}".format(reg.base) }}, {{ "0x{:x}".format(reg.base + reg.size) }} },
{% endfor %}
};
#endif /* !__ASSEMBLER__ */
#endif /* __PLAT_DEVICES_GEN_H */
@@ -183,15 +176,11 @@ def run(tree: fdt.FdtParser, hardware: rule.HardwareYaml, config: config.Config,
physical_memory, reserved, physBase = memory.get_physical_memory(tree, config)
kernel_regions, kernel_macros = get_kernel_devices(tree, hardware)
kernel_irqs = get_interrupts(tree, hardware)
device_regions = memory.get_addrspace_exclude(
list(reserved) + kernel_regions + physical_memory, config)
template = Environment(loader=BaseLoader, trim_blocks=True,
lstrip_blocks=True).from_string(HEADER_TEMPLATE)
template_args = dict(builtins.__dict__, **{
'args': args,
'device_regions': device_regions,
'excluded_regions': list(reserved) + kernel_regions + physical_memory,
'kernel_irqs': kernel_irqs,
'kernel_macros': kernel_macros,
'kernel_regions': kernel_regions,