Skip to content

Commit

Permalink
print more information and memory map
Browse files Browse the repository at this point in the history 
Signed-off-by: Axel Heider <[email protected]>
  • Loading branch information
@axel-h
axel-h committed Jan 3, 2022
1 parent e660ed1 commit 351fc8e
Showing 1 changed file with 94 additions and 35 deletions.
129 changes: 94 additions & 35 deletions libsel4debug/src/bootinfo.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,53 +8,112 @@
#include <sel4debug/gen_config.h>

#include <stdio.h>
#include <assert.h>

#include <sel4/sel4.h>
#include <utils/util.h>

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");
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^%u, %s memory, slot %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;
}
}

0 comments on commit 351fc8e

Please sign in to comment.