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

boot: print half-open regions as [a..b)

Browse Source 
Memory regions in the boot code are represented as top-end-exclusive
and so printing them as [a..b] is at best misleading (especially
as the elfloader code that runs beforehand uses [a..b] for inclusive
ranges). The boot log now looks like this (QEMU AArch64):

    ELF-loading image 'rootserver' to 40239000
      paddr=[40239000..4061efff]
      vaddr=[400000..7e5fff]
      virt_entry=40e3f8
    Enabling MMU and paging
    Jumping to kernel-image entry point...

    Bootstrapping kernel
    Warning: Could not infer GIC interrupt target ID, assuming 0.
    available phys memory regions: 1
      [40000000..80000000)
    reserved virt address space regions: 3
      [ffffff8040000000..ffffff8040237000)
      [ffffff8040237000..ffffff8040238e11)
      [ffffff8040239000..ffffff804061f000)
    Booting all finished, dropped to user space

Signed-off-by: julia <git.ts@trainwit.ch>
This commit is contained in:
julia
2025-07-31 13:28:35 +10:00
committed by Indan Zupancic
parent 1dde1fcb27
commit 638593b1aa
3 changed files with 10 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -398,7 +398,7 @@ static BOOT_CODE bool_t try_init_kernel(
* kernel window we cannot access it.
*/
if (dtb_phys_end >= PADDR_TOP) {
printf("ERROR: DTB at [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] "
printf("ERROR: DTB at [%"SEL4_PRIx_word"..%"SEL4_PRIx_word") "
"exceeds PADDR_TOP (%"SEL4_PRIx_word")\n",
dtb_phys_addr, dtb_phys_end, PADDR_TOP);
return false;
@@ -423,7 +423,7 @@ static BOOT_CODE bool_t try_init_kernel(
* work properly. Unfortunately, the definition of USER_TOP differs
* between platforms (int, long), so we have to cast here to play safe.
*/
printf("ERROR: userland image virt [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]"
printf("ERROR: userland image virt [%"SEL4_PRIx_word"..%"SEL4_PRIx_word")"
"exceeds USER_TOP (%"SEL4_PRIx_word")\n",
it_v_reg.start, it_v_reg.end, (word_t)USER_TOP);
return false;

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

@@ -258,7 +258,7 @@ static BOOT_CODE bool_t try_init_kernel(
* kernel window we cannot access it.
*/
if (dtb_phys_end >= PADDR_TOP) {
printf("ERROR: DTB at [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] "
printf("ERROR: DTB at [%"SEL4_PRIx_word"..%"SEL4_PRIx_word") "
"exceeds PADDR_TOP (%"SEL4_PRIx_word")\n",
dtb_phys_addr, dtb_phys_end, PADDR_TOP);
return false;
@@ -283,7 +283,7 @@ static BOOT_CODE bool_t try_init_kernel(
* to work properly. Unfortunately, the definition of USER_TOP differs
* between platforms (int, long), so we have to cast here to play safe.
*/
printf("ERROR: userland image virt [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]"
printf("ERROR: userland image virt [%"SEL4_PRIx_word"..%"SEL4_PRIx_word")"
"exceeds USER_TOP (%"SEL4_PRIx_word")\n",
it_v_reg.start, it_v_reg.end, (word_t)USER_TOP);
return false;

12
src/kernel/boot.c
View File

@@ -140,7 +140,7 @@ BOOT_CODE static bool_t insert_region(region_t reg)
* don't stop the boot process here, but return an error. The caller should
* decide how bad this is.
*/
printf("no free memory slot left for [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"],"
printf("no free memory slot left for [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"),"
" consider increasing MAX_NUM_FREEMEM_REG (%u)\n",
reg.start, reg.end, (unsigned int)MAX_NUM_FREEMEM_REG);
@@ -785,7 +785,7 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap)
});
if (!create_untypeds_for_region(root_cnode_cap, true, reg, first_untyped_slot)) {
printf("ERROR: creation of untypeds for device region #%u at"
" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n",
" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word") failed\n",
(unsigned int)i, reg.start, reg.end);
return false;
}
@@ -801,7 +801,7 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap)
if (!create_untypeds_for_region(root_cnode_cap, true, reg, first_untyped_slot)) {
printf("ERROR: creation of untypeds for top device region"
" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n",
" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word") failed\n",
reg.start, reg.end);
return false;
}
@@ -825,7 +825,7 @@ BOOT_CODE bool_t create_untypeds(cap_t root_cnode_cap)
ndks_boot.freemem[i] = REG_EMPTY;
if (!create_untypeds_for_region(root_cnode_cap, false, reg, first_untyped_slot)) {
printf("ERROR: creation of untypeds for free memory region #%u at"
" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"] failed\n",
" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word") failed\n",
(unsigned int)i, reg.start, reg.end);
return false;
}
@@ -877,7 +877,7 @@ BOOT_CODE static bool_t check_available_memory(word_t n_available,
/* Force ordering and exclusivity of available regions. */
for (word_t i = 0; i < n_available; i++) {
const p_region_t *r = &available[i];
printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]\n", r->start, r->end);
printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word")\n", r->start, r->end);
/* Available regions must be sane */
if (r->start > r->end) {
@@ -911,7 +911,7 @@ BOOT_CODE static bool_t check_reserved_memory(word_t n_reserved,
/* Force ordering and exclusivity of reserved regions. */
for (word_t i = 0; i < n_reserved; i++) {
const region_t *r = &reserved[i];
printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word"]\n", r->start, r->end);
printf(" [%"SEL4_PRIx_word"..%"SEL4_PRIx_word")\n", r->start, r->end);
/* Reserved regions must be sane, the size is allowed to be zero. */
if (r->start > r->end) {