From 2d73fd0bacd22b7898ac1b4122554137de0b6f52 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Sat, 9 May 2020 17:57:24 +0200 Subject: [PATCH 1/6] libsel4utils: add sel4utils_set_arg0 for RISC-V Signed-off-by: Axel Heider --- libsel4utils/arch_include/riscv/sel4utils/arch/util.h | 5 +++++ 1 file changed, 5 insertions(+) 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; +} From a7d66135be9e51e7d8b9de2feea6918a3ec4f980 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 6 Apr 2023 14:31:35 +0200 Subject: [PATCH 2/6] style: remove empty line Signed-off-by: Axel Heider --- libsel4debug/src/bootinfo.c | 1 - 1 file changed, 1 deletion(-) diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index 8b56b9e92..9f90de119 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c @@ -45,4 +45,3 @@ void debug_print_bootinfo(seL4_BootInfo *info) } } } - From 3e78cd22f183eec0fdf300565248afe1d95014f6 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Sun, 2 Jan 2022 11:45:17 +0100 Subject: [PATCH 3/6] use proper printf format specifiers Also adds a helper function for printing the slot region. Signed-off-by: Axel Heider --- libsel4debug/src/bootinfo.c | 35 ++++++++++++++++++++++++----------- 1 file changed, 24 insertions(+), 11 deletions(-) diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index 9f90de119..945aa0a5e 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c @@ -12,19 +12,30 @@ #include #include -void debug_print_bootinfo(seL4_BootInfo *info) +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); + } +} - printf("Node %lu of %lu\n", (long)info->nodeID, (long)info->numNodes); - printf("IOPT levels: %u\n", (int)info->numIOPTLevels); +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); - 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); + 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("userImagePaging: ", &info->userImagePaging); + print_slot_reg_info("untypeds: ", &info->untyped); + 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"); @@ -34,7 +45,9 @@ void debug_print_bootinfo(seL4_BootInfo *info) 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, + printf("0x%"SEL4_PRIx_word" | %zu | %d\n", + info->untypedList[i].paddr, + (size_t)info->untypedList[i].sizeBits, (int)info->untypedList[i].isDevice); } From 52fb382e25721146f10e2c79f55d81265659d88e Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Tue, 24 May 2022 12:38:28 +0200 Subject: [PATCH 4/6] print slots for extra boot info pages Signed-off-by: Axel Heider --- libsel4debug/src/bootinfo.c | 1 + 1 file changed, 1 insertion(+) diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c index 945aa0a5e..ea4b47e44 100644 --- a/libsel4debug/src/bootinfo.c +++ b/libsel4debug/src/bootinfo.c @@ -30,6 +30,7 @@ void debug_print_bootinfo(seL4_BootInfo *info) 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", From 4c279fe914c8f8b1aca2efda8b7fcb58694c2752 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Tue, 24 May 2022 12:44:14 +0200 Subject: [PATCH 5/6] 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..0f9b26cdb 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; } } From 39bb11556c40be6755285e27dd6dada253bf2912 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 26 Nov 2021 07:22:55 +0100 Subject: [PATCH 6/6] libsel4utils: use proper types for printing Signed-off-by: Axel Heider --- libsel4utils/include/sel4utils/benchmark.h | 5 ++- .../include/sel4utils/benchmark_track.h | 40 +++++++++---------- 2 files changed, 23 insertions(+), 22 deletions(-) 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++; }