From c35e9ce0d1682f27dead51c35104f00ad49e9412 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Mon, 3 Jan 2022 19:01:02 +0100 Subject: [PATCH] print more information and memory map Signed-off-by: Axel Heider --- libsel4debug/src/bootinfo.c | 132 ++++++++++++++++++++++++++---------- 1 file changed, 97 insertions(+), 35 deletions(-) diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index d3489b04e..dacacdb29 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c @@ -8,53 +8,115 @@ #include #include +#include #include #include -void debug_print_bootinfo(seL4_BootInfo *info) +static void print_slot_reg_info(seL4_SlotRegion *reg) { + if (reg->end == reg->start) { + printf("none "); + } + printf("[%"SEL4_PRIu_word" --> %"SEL4_PRIu_word"]", + reg->start, reg->end); +} +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", + + printf("IO-MMU PT levels: %"SEL4_PRIu_word"\n", info->numIOPTLevels); - printf("IPC buffer: %p\n", - info->ipcBuffer); - printf("Empty slots: [%"SEL4_PRIu_word"--> %"SEL4_PRIu_word"]\n", - info->empty.start, info->empty.end); - printf("sharedFrames: [%"SEL4_PRIu_word" --> %"SEL4_PRIu_word"]\n", - info->sharedFrames.start, info->sharedFrames.end); - printf("userImageFrames: [%"SEL4_PRIu_word" --> %"SEL4_PRIu_word"]\n", - info->userImageFrames.start, info->userImageFrames.end); - printf("userImagePaging: [%"SEL4_PRIu_word" --> %"SEL4_PRIu_word"]\n", - info->userImagePaging.start, info->userImagePaging.end); - printf("untypeds: [%"SEL4_PRIu_word" --> %]\n", - info->untyped.start, info->untyped.end); - printf("Initial thread domain: %"SEL4_PRIu_word"\n", + + printf("initial thread 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("root cnode size: 2^%"SEL4_PRIu_word" (%"SEL4_PRIu_word")\n", + info->initThreadCNodeSizeBits, + LIBSEL4_BIT(info->initThreadCNodeSizeBits)); + + printf("IPC buffer: %p\n", info->ipcBuffer); + + printf("shared pages: "); + print_slot_reg_info(&info->sharedFrames); + printf("\n"); + + printf("user image MMU tables: "); + print_slot_reg_info(&info->userImagePaging); + printf("\n"); + + printf("user image pages: "); + print_slot_reg_info(&info->userImageFrames); + printf("\n"); + + printf("extra boot info pages: "); + print_slot_reg_info(&info->extraBIPages); + printf(" (extraLen: %"SEL4_PRIu_word")\n", info->extraLen); + + printf("untyped memory: "); + print_slot_reg_info(&info->untyped); + seL4_Word numUntypeds = info->untyped.end - info->untyped.start; + printf(" (%"SEL4_PRIu_word"/%d descriptors used)\n", + numUntypeds, CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS); + + printf("empty slots: "); + print_slot_reg_info(&info->empty); + seL4_Word numEmpty = info->empty.end - info->empty.start; + printf(" (%"SEL4_PRIu_word")\n", numEmpty); + + /* 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("extra boot info blobs:\n"); + seL4_Word offs = 0; + while (offs < info->extraLen) { + seL4_BootInfoHeader *h = (seL4_BootInfoHeader *)((seL4_Word)info + 4096 + 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); + 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 | %u\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; } } -