diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index 8b56b9e92..0f9b26cdb 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c @@ -8,41 +8,95 @@ #include #include +#include #include #include +static void print_slot_reg_info(char const *descr, seL4_SlotRegion *reg) +{ + if (reg->end == reg->start) { + printf("%snone\n", descr); + } else { + printf("%s[%"SEL4_PRIu_word" --> %"SEL4_PRIu_word")\n", + descr, 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("Domain: %"SEL4_PRIu_word"\n", + info->initThreadDomain); + 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("Node %lu of %lu\n", (long)info->nodeID, (long)info->numNodes); - printf("IOPT levels: %u\n", (int)info->numIOPTLevels); - printf("IPC buffer: %p\n", info->ipcBuffer); - printf("Empty slots: [%lu --> %lu)\n", (long)info->empty.start, (long)info->empty.end); - printf("sharedFrames: [%lu --> %lu)\n", (long)info->sharedFrames.start, (long)info->sharedFrames.end); - printf("userImageFrames: [%lu --> %lu)\n", (long)info->userImageFrames.start, (long)info->userImageFrames.end); - printf("userImagePaging: [%lu --> %lu)\n", (long)info->userImagePaging.start, (long)info->userImagePaging.end); - printf("untypeds: [%lu --> %lu)\n", (long)info->untyped.start, (long)info->untyped.end); - printf("Initial thread domain: %u\n", (int)info->initThreadDomain); - printf("Initial thread cnode size: %u\n", (int)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("%p | %zu | %d\n", (void *)info->untypedList[i].paddr, (size_t)info->untypedList[i].sizeBits, - (int)info->untypedList[i].isDevice); + 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; } } - diff --git a/libsel4utils/arch_include/riscv/sel4utils/arch/util.h b/libsel4utils/arch_include/riscv/sel4utils/arch/util.h index 60544b1c0..603b06384 100644 --- a/libsel4utils/arch_include/riscv/sel4utils/arch/util.h +++ b/libsel4utils/arch_include/riscv/sel4utils/arch/util.h @@ -38,3 +38,8 @@ static inline void sel4utils_set_stack_pointer(seL4_UserContext *regs, { regs->sp = value; } + +static inline void sel4utils_set_arg0(seL4_UserContext *regs, seL4_Word value) +{ + regs->a0 = value; +} diff --git a/libsel4utils/include/sel4utils/benchmark.h b/libsel4utils/include/sel4utils/benchmark.h index 936090ee7..4f6814e87 100644 --- a/libsel4utils/include/sel4utils/benchmark.h +++ b/libsel4utils/include/sel4utils/benchmark.h @@ -26,11 +26,12 @@ static inline void seL4_BenchmarkTraceDumpFullLog(benchmark_tracepoint_log_entry while ((index * sizeof(benchmark_tracepoint_log_entry_t)) < logSize) { if (logBuffer[index].duration != 0) { - fprintf(fd, "tracepoint id = %u \tduration = %u\n", logBuffer[index].id, logBuffer[index].duration); + fprintf(fd, "tracepoint id = %"SEL4_PRIu_word" \tduration = %"SEL4_PRIu_word"\n", + logBuffer[index].id, logBuffer[index].duration); } index++; } - fprintf(fd, "Dumped entire log, size %" PRIu32 "\n", index); + fprintf(fd, "Dumped entire log, size %"SEL4_PRIu_word"\n", index); } #endif /* CONFIG_BENCHMARK_TRACEPOINTS */ diff --git a/libsel4utils/include/sel4utils/benchmark_track.h b/libsel4utils/include/sel4utils/benchmark_track.h index 8dd9bc806..3c8bffba6 100644 --- a/libsel4utils/include/sel4utils/benchmark_track.h +++ b/libsel4utils/include/sel4utils/benchmark_track.h @@ -39,10 +39,10 @@ static inline void seL4_BenchmarkTrackDumpSummary(benchmark_track_kernel_entry_t index++; } - fprintf(fd, "Number of system call invocations %d\n", syscall_entries); - fprintf(fd, "Number of interrupt invocations %d\n", interrupt_entries); - fprintf(fd, "Number of user-level faults %d\n", userlevelfault_entries); - fprintf(fd, "Number of VM faults %d\n", vmfault_entries); + fprintf(fd, "Number of system call invocations: %"SEL4_PRIu_word"\n", syscall_entries); + fprintf(fd, "Number of interrupt invocations: %"SEL4_PRIu_word"\n", interrupt_entries); + fprintf(fd, "Number of user-level faults: %"SEL4_PRIu_word"\n", userlevelfault_entries); + fprintf(fd, "Number of VM faults: %"SEL4_PRIu_word"\n", vmfault_entries); } /* Print out logged system call invocations */ @@ -54,22 +54,22 @@ static inline void seL4_BenchmarkTrackDumpFullSyscallLog(benchmark_track_kernel_ /* Get details of each system call invocation */ fprintf(fd, "-----------------------------------------------------------------------------------------------------------------------------\n"); - fprintf(fd, "| %-15s| %-15s| %-15s| %-15s| %-15s| %-15s| %-15s|\n", - "Log ID", "System Call ID", "Start Time", "Duration", "Capability Type", - "Invocation Tag", "Fastpath?"); + fprintf(fd, " %-10s | %-7s | %-20s | %-10s | %-3s | %-7s| %-8s\n", + "Log ID", "SysCall", "Start Time", "Duration", "Cap", + "Tag", "Fastpath?"); fprintf(fd, "-----------------------------------------------------------------------------------------------------------------------------\n"); while (logBuffer[index].start_time != 0 && (index * sizeof(benchmark_track_kernel_entry_t)) < logSize) { if (logBuffer[index].entry.path == Entry_Syscall) { - fprintf(fd, "| %-15d| %-15d| %-15llu| %-15d| %-15d| %-15d| %-15d|\n", + fprintf(fd, " %-10"SEL4_PRIu_word" | %-7u | %-20"PRIu64" | %-10u | %-3u | %-7u | %-9s\n", index, - logBuffer[index].entry.syscall_no, - (uint64_t) logBuffer[index].start_time, - logBuffer[index].duration, - logBuffer[index].entry.cap_type, - logBuffer[index].entry.invocation_tag, - logBuffer[index].entry.is_fastpath); + (unsigned int)logBuffer[index].entry.syscall_no, /* 4 bit */ + logBuffer[index].start_time, /* 64 bit */ + logBuffer[index].duration, /* 32 bit */ + (unsigned int)logBuffer[index].entry.cap_type, /* 5 bit */ + (unsigned int)logBuffer[index].entry.invocation_tag, /* 19 bit */ + logBuffer[index].entry.is_fastpath ? "yes" : "no"); } index++; } @@ -84,18 +84,18 @@ static inline void seL4_BenchmarkTrackDumpFullInterruptLog(benchmark_track_kerne /* Get details of each invocation */ fprintf(fd, "-----------------------------------------------------------------------------------------------------------------------------\n"); - fprintf(fd, "| %-15s| %-15s| %-15s| %-15s|\n", "Log ID", "IRQ", "Start Time", - "Duration"); + fprintf(fd, " %-10s | %-8s | %-20s | %-10s \n", + "Log ID", "IRQ", "Start Time", "Duration"); fprintf(fd, "-----------------------------------------------------------------------------------------------------------------------------\n"); while (logBuffer[index].start_time != 0 && (index * sizeof(benchmark_track_kernel_entry_t)) < logSize) { if (logBuffer[index].entry.path == Entry_Interrupt) { - fprintf(fd, "| %-15d| %-15d| %-15llu| %-15d|\n", \ + fprintf(fd, " %-10"SEL4_PRIu_word" | %-8u | %-20"PRIu64" | %-10u\n", \ index, - logBuffer[index].entry.word, - logBuffer[index].start_time, - logBuffer[index].duration); + (unsigned int)logBuffer[index].entry.word, /* 26 bits */ + logBuffer[index].start_time, /* 64 bit */ + logBuffer[index].duration); /* 32 bit */ } index++; }