From 1c1e606205c8ea6373ec99e3e62462a93e2c1a91 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Tue, 24 May 2022 12:44:14 +0200 Subject: [PATCH] print more information and memory map Signed-off-by: Axel Heider --- libsel4debug/src/bootinfo.c | 99 ++++++++++++++++++++++++++----------- 1 file changed, 70 insertions(+), 29 deletions(-) diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index ea4b47e44..c657546e7 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c @@ -8,6 +8,7 @@ #include #include +#include #include #include @@ -24,38 +25,78 @@ static void print_slot_reg_info(char const *descr, seL4_SlotRegion *reg) void debug_print_bootinfo(seL4_BootInfo *info) { - printf("Node %"SEL4_PRIu_word" of %"SEL4_PRIu_word"\n", info->nodeID, info->numNodes); - printf("IOPT levels: %"SEL4_PRIu_word"\n", info->numIOPTLevels); - printf("IPC buffer: %p\n", info->ipcBuffer); - print_slot_reg_info("Empty slots: ", &info->empty); - print_slot_reg_info("sharedFrames: ", &info->sharedFrames); - print_slot_reg_info("userImageFrames: ", &info->userImageFrames); - print_slot_reg_info("extraBootInfo: ", &info->extraBIPages); - print_slot_reg_info("userImagePaging: ", &info->userImagePaging); - print_slot_reg_info("untypeds: ", &info->untyped); - printf("Initial thread domain: %"SEL4_PRIu_word"\n", + printf("Node: %"SEL4_PRIu_word" of %"SEL4_PRIu_word"\n", + info->nodeID, info->numNodes); + printf("Domain: %"SEL4_PRIu_word"\n", info->initThreadDomain); - printf("Initial thread cnode size: %"SEL4_PRIu_word"\n", - info->initThreadCNodeSizeBits); - printf("List of untypeds\n"); - printf("------------------\n"); - printf("Paddr | Size | Device\n"); - - int sizes[CONFIG_WORD_SIZE] = {0}; - for (int i = 0; i < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS && i < (info->untyped.end - info->untyped.start); i++) { - int index = info->untypedList[i].sizeBits; - assert(index < ARRAY_SIZE(sizes)); - sizes[index]++; - printf("0x%"SEL4_PRIx_word" | %zu | %d\n", - info->untypedList[i].paddr, - (size_t)info->untypedList[i].sizeBits, - (int)info->untypedList[i].isDevice); + printf("IPC buffer: %p\n", info->ipcBuffer); + printf("IO-MMU page table levels: %"SEL4_PRIu_word"\n", + info->numIOPTLevels); + printf("Root cnode size: 2^%"SEL4_PRIu_word" (%lu)\n", + info->initThreadCNodeSizeBits, + LIBSEL4_BIT(info->initThreadCNodeSizeBits)); + print_slot_reg_info("Shared pages: ", &info->sharedFrames); + print_slot_reg_info("User image MMU tables: ", &info->userImagePaging); + print_slot_reg_info("Extra boot info pages: ", &info->extraBIPages); + print_slot_reg_info("User image pages: ", &info->userImageFrames); + print_slot_reg_info("Untyped memory: ", &info->untyped); + print_slot_reg_info("Empty slots: ", &info->empty); + + printf("Extra boot info blobs:\n"); + seL4_Word offs = 0; + while (offs < info->extraLen) { + seL4_BootInfoHeader *h = (seL4_BootInfoHeader *)((seL4_Word)info + seL4_BootInfoFrameSize + offs); + printf(" type: %"SEL4_PRIu_word", offset: %"SEL4_PRIu_word", len: %"SEL4_PRIu_word"\n", + h->id, offs, h->len); + offs += h->len; } - printf("Untyped summary\n"); - for (int i = 0; i < ARRAY_SIZE(sizes); i++) { - if (sizes[i] != 0) { - printf("%d untypeds of size %d\n", sizes[i], i); + seL4_Word numUntypeds = info->untyped.end - info->untyped.start; + printf("Used bootinfo untyped descriptors: %"SEL4_PRIu_word" of %d\n", + numUntypeds, CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS); + /* Sanity check that the boot info is consistent. */ + assert(info->empty.end == LIBSEL4_BIT(info->initThreadCNodeSizeBits)); + assert(numUntypeds < CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS); + assert(info->extraLen <= (LIBSEL4_BIT(seL4_PageBits) * (info->extraBIPages.end - info->extraBIPages.start))); + + printf("Physical memory map with available untypeds:\n"); + printf("---------------------+------+----------+-------\n"); + printf(" Phys Addr | Size | Type | Slot\n"); + printf("---------------------+------+----------+-------\n"); + + for (seL4_Word pos = 0; pos < (seL4_Word)(-1); pos++) { + /* Find the next descriptor according to our current position. */ + seL4_UntypedDesc *d = NULL; + int idx = -1; + for (int i = 0; i < numUntypeds; i++) { + seL4_UntypedDesc *d_tmp = &info->untypedList[i]; + if (d_tmp->paddr < pos) { + continue; + } + if (d && (d_tmp->paddr >= d->paddr)) { + /* Two descriptors for the same region are not allowed. */ + assert(d_tmp->paddr != d->paddr); + continue; + } + d = d_tmp; /* Found a better match. */ + idx = i; + } + /* No adjacent descriptor found means there is reserved space. */ + if ((!d) || (pos < d->paddr)) { + printf(" %# *"SEL4_PRIx_word" | - | reserved | -\n", + 2 + (CONFIG_WORD_SIZE / 4), pos); + if (!d) { + break; /* No descriptors found at all means we are done. */ + } } + printf(" %# *"SEL4_PRIx_word" | 2^%-2u | %s | %"SEL4_PRIu_word"\n", + 2 + (CONFIG_WORD_SIZE / 4), + d->paddr, + d->sizeBits, + d->isDevice ? "device " : "free ", + info->untyped.start + idx); + seL4_Word pos_new = d->paddr + LIBSEL4_BIT(d->sizeBits) - 1; + assert(pos_new >= pos); /* Regions must not overflow. */ + pos = pos_new; } }