From fcabdef37016cd568a40c82e0d97a264b86ee6d4 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 4 Apr 2024 20:12:48 +0200 Subject: [PATCH 01/21] CI: use proper step name Signed-off-by: Axel Heider --- .github/workflows/sel4test-sim.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/sel4test-sim.yml b/.github/workflows/sel4test-sim.yml index 33436c89..38969fbf 100644 --- a/.github/workflows/sel4test-sim.yml +++ b/.github/workflows/sel4test-sim.yml @@ -22,7 +22,7 @@ concurrency: cancel-in-progress: ${{ github.event_name == 'pull_request' }} jobs: - cparser: + simulation: name: Simulation runs-on: ubuntu-latest strategy: From cf1982c1f9e544648141af1e8416b86f0d773c7d Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Tue, 28 Jun 2022 19:12:42 +0200 Subject: [PATCH 02/21] WIP libsel4platsupport: debug log --- libsel4muslcsys/src/sys_morecore.c | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/libsel4muslcsys/src/sys_morecore.c b/libsel4muslcsys/src/sys_morecore.c index c5240f63..3d83bb62 100644 --- a/libsel4muslcsys/src/sys_morecore.c +++ b/libsel4muslcsys/src/sys_morecore.c @@ -68,6 +68,11 @@ long sys_mmap_impl(void *addr, size_t length, int prot, int flags, int fd, off_t if (length > morecore_top - morecore_base) { return -ENOMEM; } + + ZF_LOGI( + "morecore %p - %p, len %#x, return address: 0x%"PRIxPTR, + morecore_base, morecore_top, length, morecore_top-length); + /* Steal from the top */ morecore_top -= length; return morecore_top; @@ -116,6 +121,8 @@ static void init_morecore_region(void) morecore_base = (uintptr_t) morecore_area; morecore_top = (uintptr_t) &morecore_area[morecore_size]; } + + ZF_LOGI("morecore %p - %p (%#zd)", morecore_base, morecore_top, morecore_size); } static long sys_brk_static(va_list ap) @@ -199,8 +206,16 @@ static long sys_mmap_impl_static(void *addr, size_t length, int prot, int flags, if (base < morecore_base) { return -ENOMEM; } + ZF_LOGF_IF( + (base % 0x1000) != 0, + "morecore %p - %p, len %#zx, return address: %p (not 4 KiB aligned)", + (void*)morecore_base, (void*)morecore_top, length, (void*)base); + + ZF_LOGI( + "morecore %p - %p, len %#zx, return address: %p", + (void*)morecore_base, (void*)morecore_top, length, (void*)base); + morecore_top = base; - ZF_LOGF_IF((base % 0x1000) != 0, "return address: 0x%"PRIxPTR" requires alignment: 0x%x ", base, 0x1000); return base; } assert(!"not implemented"); From 2d73fd0bacd22b7898ac1b4122554137de0b6f52 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Sat, 9 May 2020 17:57:24 +0200 Subject: [PATCH 03/21] 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 60544b1c..603b0638 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 04/21] 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 8b56b9e9..9f90de11 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 05/21] 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 9f90de11..945aa0a5 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 06/21] 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 945aa0a5..ea4b47e4 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 07/21] 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 ea4b47e4..0f9b26cd 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 08/21] 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 936090ee..4f6814e8 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 8dd9bc80..3c8bffba 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++; } From d3ed8cabe6d7fa5e59720e24bdbaa7a8502274d0 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:57:48 +0100 Subject: [PATCH 09/21] libsel4platsupport: use ZF_LOGE() instead of printf() Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index a1f130e5..d3f56985 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -228,7 +228,7 @@ int platsupport_serial_setup_simple( return 0; } if (setup_status != NOT_INITIALIZED) { - printf("Trying to initialise a partially initialised serial. Current setup status is %d\n", setup_status); + ZF_LOGE("Trying to initialise a partially initialised serial. Current setup status is %d\n", setup_status); assert(!"You cannot recover"); return -1; } From 15bdb1186c313c99a6003932fe346750c950cb52 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:58:03 +0100 Subject: [PATCH 10/21] libsel4platsupport: define USE_DEBUG_PUTCHAR Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index d3f56985..355abaa2 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -32,6 +32,10 @@ #include #include +#if defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_DEBUG_BUILD) +#define USE_DEBUG_PUTCHAR +#endif + enum serial_setup_status { NOT_INITIALIZED = 0, START_REGULAR_SETUP, @@ -56,7 +60,7 @@ static vka_t _vka_mem; static seL4_CPtr device_cap = 0; extern char __executable_start[]; -#if !(defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_DEBUG_BUILD)) +#ifndef USE_DEBUG_PUTCHAR static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, int cached, ps_mem_flags_t flags); @@ -66,8 +70,7 @@ static ps_io_ops_t io_ops = { .io_unmap_fn = NULL, }, }; - -#endif +#endif /* !USE_DEBUG_PUTCHAR */ /* completely hacky way of getting a virtual address. This is used a last ditch attempt to * get serial device going so we can print out an error */ @@ -201,10 +204,10 @@ int platsupport_serial_setup_bootinfo_failsafe(void) } memset(&_simple_mem, 0, sizeof(simple_t)); memset(&_vka_mem, 0, sizeof(vka_t)); -#if defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_DEBUG_BUILD) +#ifdef USE_DEBUG_PUTCHAR /* only support putchar on a debug kernel */ setup_status = SETUP_COMPLETE; -#else +#else /* not USE_DEBUG_PUTCHAR */ setup_status = START_FAILSAFE_SETUP; simple_default_init_bootinfo(&_simple_mem, platsupport_get_bootinfo()); simple = &_simple_mem; @@ -214,7 +217,7 @@ int platsupport_serial_setup_bootinfo_failsafe(void) sel4platsupport_get_io_port_ops(&io_ops.io_port_ops, simple, vka); #endif err = platsupport_serial_setup_io_ops(&io_ops); -#endif +#endif /* [not] USE_DEBUG_PUTCHAR */ return err; } @@ -232,10 +235,10 @@ int platsupport_serial_setup_simple( assert(!"You cannot recover"); return -1; } -#if defined(CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR) && defined(CONFIG_DEBUG_BUILD) +#ifdef USE_DEBUG_PUTCHAR /* only support putchar on a debug kernel */ setup_status = SETUP_COMPLETE; -#else +#else /* not USE_DEBUG_PUTCHAR */ /* start setup */ setup_status = START_REGULAR_SETUP; vspace = _vspace; @@ -249,7 +252,7 @@ int platsupport_serial_setup_simple( vspace = NULL; simple = NULL; /* Don't reset vka here */ -#endif +#endif /* [not] USE_DEBUG_PUTCHAR */ return err; } From 218e3d81a7884a710576e379b20e5e26da96c745 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:55:51 +0100 Subject: [PATCH 11/21] libsel4platsupport: cleanup __serial_setup() Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 86 ++++++++++++++++++--------------- 1 file changed, 47 insertions(+), 39 deletions(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index 355abaa2..d354f579 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -256,59 +256,64 @@ int platsupport_serial_setup_simple( return err; } -static void __serial_setup() +/* This function is called if an attempt for serial I/O is done before it has + * been set up. Try to do some best-guess seetup. + */ +static int fallback_serial_setup() { - int started_regular __attribute__((unused)) = 0; - /* this function is called if we attempt to do serial and it isn't setup. - * we now need to handle this somehow */ switch (setup_status) { - case START_FAILSAFE_SETUP: - /* we're stuck. */ - abort(); - break; - case START_REGULAR_SETUP: - started_regular = 1; + + case SETUP_COMPLETE: + return 0; /* we don't except to be called in thi state */ + case NOT_INITIALIZED: + case START_REGULAR_SETUP: + break; /* continue below fir failsafe setup */ + + default: /* includes START_FAILSAFE_SETUP */ + return -1; + } + #ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR - setup_status = SETUP_COMPLETE; - printf("\nWarning: using printf before serial is set up. This only works as your\n"); - printf("printf is backed by seL4_Debug_PutChar()\n"); - started_regular = 1; -#else - /* attempt failsafe initialization and print something out */ - platsupport_serial_setup_bootinfo_failsafe(); - if (started_regular) { - printf("Regular serial setup failed.\n" - "This message coming to you courtesy of failsafe serial\n" - "Your vspace has been clobbered but we will keep running to get any more error output\n"); - } else { - printf("You attempted to print before initialising the libsel4platsupport serial device!\n"); - while (1); - } -#endif /* CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR */ - break; - case SETUP_COMPLETE: - break; + setup_status = SETUP_COMPLETE; + ZF_LOGI("using kernel syscalls for char I/O"); +#else /* not CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR */ + /* Attempt failsafe initialization to be able to print something. */ + int err = platsupport_serial_setup_bootinfo_failsafe(); + if (err || (START_REGULAR_SETUP != setup_status)) { + /* Setup failed, so printing an error may not output anything. */ + ZF_LOGE("You attempted to print before initialising the" + " libsel4platsupport serial device!"); + return -1; } + + /* Setup worked, so this warning will show up. */ + ZF_LOGW("Regular serial setup failed.\n" + "This message coming to you courtesy of failsafe serial.\n" + "Your vspace has been clobbered but we will keep running" + " to get any more error output"); +#endif /* [not] CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR */ + return 0; } -void NO_INLINE #ifdef CONFIG_LIB_SEL4_MUSLC_SYS_ARCH_PUTCHAR_WEAK -WEAK +#define LIBSEL4_IO NO_INLINE WEAK +#else +#define LIBSEL4_IO NO_INLINE #endif -__arch_putchar(int c) + +void LIBSEL4_IO __arch_putchar(int c) { if (setup_status != SETUP_COMPLETE) { - __serial_setup(); + if (0 != fallback_serial_setup()) { + abort(); /* ToDo: hopefully this does not print anything */ + UNREACHABLE(); + } } __plat_putchar(c); } -size_t NO_INLINE -#ifdef CONFIG_LIB_SEL4_MUSLC_SYS_ARCH_PUTCHAR_WEAK -WEAK -#endif -__arch_write(char *data, size_t count) +size_t LIBSEL4_IO __arch_write(char *data, size_t count) { for (size_t i = 0; i < count; i++) { __arch_putchar(data[i]); @@ -319,7 +324,10 @@ __arch_write(char *data, size_t count) int __arch_getchar(void) { if (setup_status != SETUP_COMPLETE) { - __serial_setup(); + if (0 != fallback_serial_setup()) { + abort(); /* ToDo: hopefully this does not print anything */ + UNREACHABLE(); + } } return __plat_getchar(); } From 7fdbec266210e5fc21b8299732f92e45355cfc5e Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:56:01 +0100 Subject: [PATCH 12/21] libsel4platsupport: inline things into __map_device_page() Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 128 +++++++++++--------------------- 1 file changed, 43 insertions(+), 85 deletions(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index d354f579..b499a759 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -54,110 +54,68 @@ static vka_t *vka = NULL; /* To keep failsafe setup we need actual memory for a simple and a vka */ static simple_t _simple_mem; static vka_t _vka_mem; - -/* Hacky constants / data structures for a failsafe mapping */ -#define DITE_HEADER_START ((seL4_Word)__executable_start - 0x1000) static seL4_CPtr device_cap = 0; extern char __executable_start[]; #ifndef USE_DEBUG_PUTCHAR -static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, - int cached, ps_mem_flags_t flags); -static ps_io_ops_t io_ops = { - .io_mapper = { - .io_map_fn = &__map_device_page, - .io_unmap_fn = NULL, - }, -}; -#endif /* !USE_DEBUG_PUTCHAR */ - -/* completely hacky way of getting a virtual address. This is used a last ditch attempt to - * get serial device going so we can print out an error */ -static seL4_Word platsupport_alloc_device_vaddr(seL4_Word bits) +static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, + int cached, ps_mem_flags_t flags) { - seL4_Word va; + seL4_Error err; - va = DITE_HEADER_START - (BIT(bits)); - - /* Ensure we are aligned to bits. If not, round down. */ - va = va & ~((BIT(bits)) - 1); - - return va; -} + if (0 != device_cap) { + /* we only support a single page for the serial device. */ + abort(); + } -static void *__map_device_page_failsafe(void *cookie UNUSED, uintptr_t paddr, size_t size, - int cached UNUSED, ps_mem_flags_t flags UNUSED) -{ - int bits = CTZ(size); - int error; - seL4_Word vaddr = 0; vka_object_t dest; - - if (device_cap != 0) { - /* we only support a single page for the serial */ - for (;;); + int bits = CTZ(size); + err = sel4platsupport_alloc_frame_at(vka, paddr, bits, &dest); + if (err) { + ZF_LOGE("Failed to get cap for serial device frame"); + abort(); } - error = sel4platsupport_alloc_frame_at(vka, paddr, bits, &dest); - if (error != seL4_NoError) { - goto error; - } device_cap = dest.cptr; - vaddr = platsupport_alloc_device_vaddr(bits); - error = - seL4_ARCH_Page_Map( - device_cap, - seL4_CapInitThreadPD, - vaddr, - seL4_AllRights, - 0 - ); - -error: - if (error) - for (;;); - - assert(!error); - - return (void *)vaddr; -} - -static void *__map_device_page_regular(void *cookie UNUSED, uintptr_t paddr, size_t size, - int cached UNUSED, ps_mem_flags_t flags UNUSED) -{ - int bits = CTZ(size); - void *vaddr; - int error; - vka_object_t dest; - - error = sel4platsupport_alloc_frame_at(vka, paddr, bits, &dest); - if (error) { - ZF_LOGF("Failed to get cap for serial device frame"); + if ((setup_status == START_REGULAR_SETUP) && vspace) { + /* map device page regularly */ + void *vaddr = vspace_map_pages(vspace, &dest.cptr, NULL, seL4_AllRights, 1, bits, 0); + if (!vaddr) { + ZF_LOGE("Failed to map serial device"); + abort(); + } + return vaddr; } - vaddr = vspace_map_pages(vspace, &dest.cptr, NULL, seL4_AllRights, 1, bits, 0); - if (!vaddr) { - ZF_LOGF("Failed to map serial device :(\n"); - for (;;); + /* Try a last ditch attempt to get serial device going, so we can print out + * an error. Find a properly aligned virtual address and try to map the + * device cap there. + */ + if ((setup_status == START_FAILSAFE_SETUP) || !vspace) { + seL4_Word header_start = (seL4_Word)__executable_start - PAGE_SIZE_4K; + seL4_Word vaddr = (header_start - BIT(bits)) & ~(BIT(bits) - 1); + err = seL4_ARCH_Page_Map(device_cap, seL4_CapInitThreadPD, vaddr, seL4_AllRights, 0); + if (err) { + ZF_LOGE("Failed to map serial device in failsafe mode"); + abort(); + } + return (void *)vaddr; } - device_cap = dest.cptr; - return (void *)vaddr; + ZF_LOGE("invalid setup state %d", setup_status); + abort(); } -void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, - int cached, ps_mem_flags_t flags) -{ - if (setup_status == START_REGULAR_SETUP && vspace) { - return __map_device_page_regular(cookie, paddr, size, cached, flags); - } else if (setup_status == START_FAILSAFE_SETUP || !vspace) { - return __map_device_page_failsafe(cookie, paddr, size, cached, flags); - } - printf("Unknown setup status!\n"); - for (;;); -} +static ps_io_ops_t io_ops = { + .io_mapper = { + .io_map_fn = &__map_device_page, + .io_unmap_fn = NULL, + }, +}; + +#endif /* !USE_DEBUG_PUTCHAR */ /* * This function is designed to be called when creating a new cspace/vspace, From 6e14884c33f835be8be552f1e328e6d74ef35ada Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:57:00 +0100 Subject: [PATCH 13/21] libsel4platsupport: add unrechable marker Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index b499a759..7fa76333 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -67,6 +67,7 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, if (0 != device_cap) { /* we only support a single page for the serial device. */ abort(); + UNREACHABLE(); } vka_object_t dest; @@ -75,6 +76,7 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, if (err) { ZF_LOGE("Failed to get cap for serial device frame"); abort(); + UNREACHABLE(); } device_cap = dest.cptr; @@ -85,6 +87,7 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, if (!vaddr) { ZF_LOGE("Failed to map serial device"); abort(); + UNREACHABLE(); } return vaddr; } @@ -100,6 +103,7 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, if (err) { ZF_LOGE("Failed to map serial device in failsafe mode"); abort(); + UNREACHABLE(); } return (void *)vaddr; } From a7a1351332e62a32a23207827824addec702d832 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 22:24:26 +0100 Subject: [PATCH 14/21] libsel4platsupport: always clear vka Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index 7fa76333..ad0ffc96 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -136,8 +136,8 @@ void platsupport_undo_serial_setup(void) vka_cnode_delete(&path); vka_cspace_free(vka, device_cap); device_cap = 0; - vka = NULL; } + vka = NULL; } /* Initialise serial input interrupt. */ From 1844f3f56e1934ed3afcfbfdc426400346e384ef Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 23:12:29 +0100 Subject: [PATCH 15/21] libsel4platsupport: use switch/case Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index ad0ffc96..7eac97ef 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -189,14 +189,17 @@ int platsupport_serial_setup_simple( vka_t *_vka __attribute__((unused))) { int err = 0; - if (setup_status == SETUP_COMPLETE) { + switch (setup_status) { + case SETUP_COMPLETE: return 0; - } - if (setup_status != NOT_INITIALIZED) { + case NOT_INITIALIZED: + break; /* continue below */ + default: ZF_LOGE("Trying to initialise a partially initialised serial. Current setup status is %d\n", setup_status); assert(!"You cannot recover"); return -1; } + #ifdef USE_DEBUG_PUTCHAR /* only support putchar on a debug kernel */ setup_status = SETUP_COMPLETE; From 30de680a0d8bf0e9d29c89b2d40f843db521f6e1 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 22:04:12 +0100 Subject: [PATCH 16/21] libsel4platsupport: add global context Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 109 ++++++++++++++++++-------------- 1 file changed, 60 insertions(+), 49 deletions(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index 7eac97ef..d0fccd97 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -42,19 +42,28 @@ enum serial_setup_status { START_FAILSAFE_SETUP, SETUP_COMPLETE }; -static enum serial_setup_status setup_status = NOT_INITIALIZED; + +typedef struct { + enum serial_setup_status setup_status; +#ifndef USE_DEBUG_PUTCHAR + seL4_CPtr device_cap; + vspace_t *vspace; + simple_t *simple; + vka_t *vka; +#endif /* not USE_DEBUG_PUTCHAR */ +} ctx_t; /* Some globals for tracking initialisation variables. This is currently just to avoid * passing parameters down to the platform code for backwards compatibility reasons. This * is strictly to avoid refactoring all existing platform code */ -static vspace_t *vspace = NULL; -static UNUSED simple_t *simple = NULL; -static vka_t *vka = NULL; +static ctx_t ctx = { + .setup_status = NOT_INITIALIZED +}; /* To keep failsafe setup we need actual memory for a simple and a vka */ static simple_t _simple_mem; static vka_t _vka_mem; -static seL4_CPtr device_cap = 0; + extern char __executable_start[]; #ifndef USE_DEBUG_PUTCHAR @@ -64,7 +73,7 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, { seL4_Error err; - if (0 != device_cap) { + if (0 != ctx.device_cap) { /* we only support a single page for the serial device. */ abort(); UNREACHABLE(); @@ -72,18 +81,18 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, vka_object_t dest; int bits = CTZ(size); - err = sel4platsupport_alloc_frame_at(vka, paddr, bits, &dest); + err = sel4platsupport_alloc_frame_at(ctx.vka, paddr, bits, &dest); if (err) { ZF_LOGE("Failed to get cap for serial device frame"); abort(); UNREACHABLE(); } - device_cap = dest.cptr; + ctx.device_cap = dest.cptr; - if ((setup_status == START_REGULAR_SETUP) && vspace) { + if ((ctx.setup_status == START_REGULAR_SETUP) && ctx.vspace) { /* map device page regularly */ - void *vaddr = vspace_map_pages(vspace, &dest.cptr, NULL, seL4_AllRights, 1, bits, 0); + void *vaddr = vspace_map_pages(ctx.vspace, &dest.cptr, NULL, seL4_AllRights, 1, bits, 0); if (!vaddr) { ZF_LOGE("Failed to map serial device"); abort(); @@ -96,10 +105,10 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, * an error. Find a properly aligned virtual address and try to map the * device cap there. */ - if ((setup_status == START_FAILSAFE_SETUP) || !vspace) { + if ((ctx.setup_status == START_FAILSAFE_SETUP) || !ctx.vspace) { seL4_Word header_start = (seL4_Word)__executable_start - PAGE_SIZE_4K; seL4_Word vaddr = (header_start - BIT(bits)) & ~(BIT(bits) - 1); - err = seL4_ARCH_Page_Map(device_cap, seL4_CapInitThreadPD, vaddr, seL4_AllRights, 0); + err = seL4_ARCH_Page_Map(ctx.device_cap, seL4_CapInitThreadPD, vaddr, seL4_AllRights, 0); if (err) { ZF_LOGE("Failed to map serial device in failsafe mode"); abort(); @@ -108,7 +117,7 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, return (void *)vaddr; } - ZF_LOGE("invalid setup state %d", setup_status); + ZF_LOGE("invalid setup state %d", ctx.setup_status); abort(); } @@ -128,16 +137,18 @@ static ps_io_ops_t io_ops = { void platsupport_undo_serial_setup(void) { /* Re-initialise some structures. */ - setup_status = NOT_INITIALIZED; - if (device_cap) { + ctx.setup_status = NOT_INITIALIZED; +#ifndef USE_DEBUG_PUTCHAR + if (ctx.device_cap) { cspacepath_t path; - seL4_ARCH_Page_Unmap(device_cap); - vka_cspace_make_path(vka, device_cap, &path); + seL4_ARCH_Page_Unmap(ctx.device_cap); + vka_cspace_make_path(ctx.vka, ctx.device_cap, &path); vka_cnode_delete(&path); - vka_cspace_free(vka, device_cap); - device_cap = 0; + vka_cspace_free(ctx.vka, ctx.device_cap); + ctx.device_cap = 0; } - vka = NULL; + ctx.vka = NULL; +#endif /* not USE_DEBUG_PUTCHAR */ } /* Initialise serial input interrupt. */ @@ -148,12 +159,12 @@ void platsupport_serial_input_init_IRQ(void) int platsupport_serial_setup_io_ops(ps_io_ops_t *io_ops) { int err = 0; - if (setup_status == SETUP_COMPLETE) { + if (ctx.setup_status == SETUP_COMPLETE) { return 0; } err = __plat_serial_init(io_ops); if (!err) { - setup_status = SETUP_COMPLETE; + ctx.setup_status = SETUP_COMPLETE; } return err; } @@ -161,22 +172,21 @@ int platsupport_serial_setup_io_ops(ps_io_ops_t *io_ops) int platsupport_serial_setup_bootinfo_failsafe(void) { int err = 0; - if (setup_status == SETUP_COMPLETE) { + if (ctx.setup_status == SETUP_COMPLETE) { return 0; } memset(&_simple_mem, 0, sizeof(simple_t)); memset(&_vka_mem, 0, sizeof(vka_t)); #ifdef USE_DEBUG_PUTCHAR /* only support putchar on a debug kernel */ - setup_status = SETUP_COMPLETE; + ctx.setup_status = SETUP_COMPLETE; #else /* not USE_DEBUG_PUTCHAR */ - setup_status = START_FAILSAFE_SETUP; + ctx.setup_status = START_FAILSAFE_SETUP; simple_default_init_bootinfo(&_simple_mem, platsupport_get_bootinfo()); - simple = &_simple_mem; - vka = &_vka_mem; - simple_make_vka(simple, vka); + ctx.vka = &_vka_mem; + simple_make_vka(&_simple_mem, ctx.vka); #ifdef CONFIG_ARCH_X86 - sel4platsupport_get_io_port_ops(&io_ops.io_port_ops, simple, vka); + sel4platsupport_get_io_port_ops(&io_ops.io_port_ops, &_simple_mem, ctx.vka); #endif err = platsupport_serial_setup_io_ops(&io_ops); #endif /* [not] USE_DEBUG_PUTCHAR */ @@ -184,39 +194,40 @@ int platsupport_serial_setup_bootinfo_failsafe(void) } int platsupport_serial_setup_simple( - vspace_t *_vspace __attribute__((unused)), - simple_t *_simple __attribute__((unused)), - vka_t *_vka __attribute__((unused))) + vspace_t *vspace __attribute__((unused)), + simple_t *simple __attribute__((unused)), + vka_t *vka __attribute__((unused))) { int err = 0; - switch (setup_status) { + switch (ctx.setup_status) { case SETUP_COMPLETE: return 0; case NOT_INITIALIZED: break; /* continue below */ default: - ZF_LOGE("Trying to initialise a partially initialised serial. Current setup status is %d\n", setup_status); + ZF_LOGE("Trying to initialise a partially initialised serial. Current setup status is %d\n", ctx.setup_status); assert(!"You cannot recover"); return -1; } #ifdef USE_DEBUG_PUTCHAR /* only support putchar on a debug kernel */ - setup_status = SETUP_COMPLETE; + ctx.setup_status = SETUP_COMPLETE; #else /* not USE_DEBUG_PUTCHAR */ /* start setup */ - setup_status = START_REGULAR_SETUP; - vspace = _vspace; - simple = _simple; - vka = _vka; + ctx.setup_status = START_REGULAR_SETUP; + ctx.vspace = vspace; + ctx.simple = simple; + ctx.vka = vka; #ifdef CONFIG_ARCH_X86 - sel4platsupport_get_io_port_ops(&io_ops.io_port_ops, simple, vka); + sel4platsupport_get_io_port_ops(&io_ops.io_port_ops, ctx.simple, ctx.vka); #endif err = platsupport_serial_setup_io_ops(&io_ops); - /* done */ - vspace = NULL; - simple = NULL; - /* Don't reset vka here */ + /* setup done. We still need vka in platsupport_undo_serial_setup(), the + * rest can be cleared + */ + ctx.vspace = NULL; + ctx.simple = NULL; #endif /* [not] USE_DEBUG_PUTCHAR */ return err; } @@ -226,7 +237,7 @@ int platsupport_serial_setup_simple( */ static int fallback_serial_setup() { - switch (setup_status) { + switch (ctx.setup_status) { case SETUP_COMPLETE: return 0; /* we don't except to be called in thi state */ @@ -240,12 +251,12 @@ static int fallback_serial_setup() } #ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR - setup_status = SETUP_COMPLETE; + ctx.setup_status = SETUP_COMPLETE; ZF_LOGI("using kernel syscalls for char I/O"); #else /* not CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR */ /* Attempt failsafe initialization to be able to print something. */ int err = platsupport_serial_setup_bootinfo_failsafe(); - if (err || (START_REGULAR_SETUP != setup_status)) { + if (err || (START_REGULAR_SETUP != ctx.setup_status)) { /* Setup failed, so printing an error may not output anything. */ ZF_LOGE("You attempted to print before initialising the" " libsel4platsupport serial device!"); @@ -269,7 +280,7 @@ static int fallback_serial_setup() void LIBSEL4_IO __arch_putchar(int c) { - if (setup_status != SETUP_COMPLETE) { + if (ctx.setup_status != SETUP_COMPLETE) { if (0 != fallback_serial_setup()) { abort(); /* ToDo: hopefully this does not print anything */ UNREACHABLE(); @@ -288,7 +299,7 @@ size_t LIBSEL4_IO __arch_write(char *data, size_t count) int __arch_getchar(void) { - if (setup_status != SETUP_COMPLETE) { + if (ctx.setup_status != SETUP_COMPLETE) { if (0 != fallback_serial_setup()) { abort(); /* ToDo: hopefully this does not print anything */ UNREACHABLE(); From 5a6850f24f67c349c009d6e0972102dda6073896 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 23:12:51 +0100 Subject: [PATCH 17/21] libsel4platsupport: inline io_ops Signed-off-by: Axel Heider --- libsel4platsupport/src/common.c | 63 +++++++++++++++++---------------- 1 file changed, 32 insertions(+), 31 deletions(-) diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index d0fccd97..e4f72720 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -47,9 +47,12 @@ typedef struct { enum serial_setup_status setup_status; #ifndef USE_DEBUG_PUTCHAR seL4_CPtr device_cap; + ps_io_ops_t io_ops; vspace_t *vspace; - simple_t *simple; vka_t *vka; + /* To keep failsafe setup we need actual memory for a simple and a vka */ + simple_t simple_mem; + vka_t vka_mem; #endif /* not USE_DEBUG_PUTCHAR */ } ctx_t; @@ -60,10 +63,6 @@ static ctx_t ctx = { .setup_status = NOT_INITIALIZED }; -/* To keep failsafe setup we need actual memory for a simple and a vka */ -static simple_t _simple_mem; -static vka_t _vka_mem; - extern char __executable_start[]; #ifndef USE_DEBUG_PUTCHAR @@ -121,14 +120,19 @@ static void *__map_device_page(void *cookie, uintptr_t paddr, size_t size, abort(); } -static ps_io_ops_t io_ops = { - .io_mapper = { - .io_map_fn = &__map_device_page, - .io_unmap_fn = NULL, - }, -}; +static int setup_io_ops( + simple_t *simple __attribute__((unused)), + vka_t *vka __attribute__((unused))) +{ + ctx.io_ops.io_mapper.io_map_fn = &__map_device_page; + +#ifdef CONFIG_ARCH_X86 + sel4platsupport_get_io_port_ops(&ctx.io_ops.io_port_ops, simple, vka); +#endif + return platsupport_serial_setup_io_ops(&ctx.io_ops); +} -#endif /* !USE_DEBUG_PUTCHAR */ +#endif /* not USE_DEBUG_PUTCHAR */ /* * This function is designed to be called when creating a new cspace/vspace, @@ -175,20 +179,26 @@ int platsupport_serial_setup_bootinfo_failsafe(void) if (ctx.setup_status == SETUP_COMPLETE) { return 0; } - memset(&_simple_mem, 0, sizeof(simple_t)); - memset(&_vka_mem, 0, sizeof(vka_t)); + #ifdef USE_DEBUG_PUTCHAR /* only support putchar on a debug kernel */ ctx.setup_status = SETUP_COMPLETE; #else /* not USE_DEBUG_PUTCHAR */ ctx.setup_status = START_FAILSAFE_SETUP; - simple_default_init_bootinfo(&_simple_mem, platsupport_get_bootinfo()); - ctx.vka = &_vka_mem; - simple_make_vka(&_simple_mem, ctx.vka); -#ifdef CONFIG_ARCH_X86 - sel4platsupport_get_io_port_ops(&io_ops.io_port_ops, &_simple_mem, ctx.vka); -#endif - err = platsupport_serial_setup_io_ops(&io_ops); + + simple_t *simple = &(ctx.simple_mem); + memset(simple, 0, sizeof(*simple)); + + simple_default_init_bootinfo(simple, platsupport_get_bootinfo()); + + vka_t *vka = &(ctx.vka_mem); + memset(vka, 0, sizeof(*vka)); + simple_make_vka(simple, vka); + + ctx.vspace = NULL; + ctx.vka = vka; + + err = setup_io_ops(simple, vka); #endif /* [not] USE_DEBUG_PUTCHAR */ return err; } @@ -217,17 +227,8 @@ int platsupport_serial_setup_simple( /* start setup */ ctx.setup_status = START_REGULAR_SETUP; ctx.vspace = vspace; - ctx.simple = simple; ctx.vka = vka; -#ifdef CONFIG_ARCH_X86 - sel4platsupport_get_io_port_ops(&io_ops.io_port_ops, ctx.simple, ctx.vka); -#endif - err = platsupport_serial_setup_io_ops(&io_ops); - /* setup done. We still need vka in platsupport_undo_serial_setup(), the - * rest can be cleared - */ - ctx.vspace = NULL; - ctx.simple = NULL; + err = setup_io_ops(simple, vka); /* uses ctx.vka */ #endif /* [not] USE_DEBUG_PUTCHAR */ return err; } From 99ed01e3a92f3075ea221a0fcbba6d2c140d4120 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Apr 2024 17:13:34 +0200 Subject: [PATCH 18/21] libsel4allocman: simplify code Signed-off-by: Axel Heider --- libsel4allocman/src/bootstrap.c | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/libsel4allocman/src/bootstrap.c b/libsel4allocman/src/bootstrap.c index e78fed9e..2d16611e 100644 --- a/libsel4allocman/src/bootstrap.c +++ b/libsel4allocman/src/bootstrap.c @@ -1119,15 +1119,14 @@ int allocman_add_simple_untypeds_with_regions(allocman_t *alloc, simple_t *simpl uintptr_t paddr; bool device; cspacepath_t path = allocman_cspace_make_path(alloc, simple_get_nth_untyped(simple, i, &size_bits, &paddr, &device)); - int dev_type = device ? ALLOCMAN_UT_DEV : ALLOCMAN_UT_KERNEL; - // If it is regular UT memory, then we add cap and move on. - if (dev_type == ALLOCMAN_UT_KERNEL) { - error = allocman_utspace_add_uts(alloc, 1, &path, &size_bits, &paddr, dev_type); - ZF_LOGF_IF(error, "Could not add kernel untyped."); - } else { - // Otherwise we are Device untyped. + if (device) { + // Separates device RAM memory into separate untyped caps error = handle_device_untyped_cap(state, paddr, size_bits, &path, alloc); - ZF_LOGF_IF(error, "bootstrap_arch_handle_device_untyped_cap failed."); + ZF_LOGF_IF(error, "handle_device_untyped_cap failed (%d).", error); + } else { + // for regular UT memory we add cap + error = allocman_utspace_add_uts(alloc, 1, &path, &size_bits, &paddr, ALLOCMAN_UT_KERNEL); + ZF_LOGF_IF(error, "Could not add kernel untyped (%d).", error); } } if (state) { From 55b4963e3d495cd94e3fdbbd8b3ffd33b5627ec3 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Apr 2024 17:20:29 +0200 Subject: [PATCH 19/21] libsel4allocman: add error check The signature allows returning an error, so this must be checked. Signed-off-by: Axel Heider --- libsel4allocman/src/bootstrap.c | 15 +++++++++++++-- libsel4simple/src/simple.c | 7 ++++++- 2 files changed, 19 insertions(+), 3 deletions(-) diff --git a/libsel4allocman/src/bootstrap.c b/libsel4allocman/src/bootstrap.c index 2d16611e..d4dbc465 100644 --- a/libsel4allocman/src/bootstrap.c +++ b/libsel4allocman/src/bootstrap.c @@ -233,7 +233,14 @@ static int bootstrap_add_untypeds_from_simple(bootstrap_info_t *bs, simple_t *si if (!bs->have_boot_cspace || (bs->uts && !bs->uts_in_current_cspace)) { return 1; } - for (i = 0; i < simple_get_untyped_count(simple); i++) { + + int cnt = simple_get_untyped_count(simple); + if (cnt < 0) { + ZF_LOGW("Could not get untyped count (%d)", cnt); + return 1; + } + + for (i = 0; i < cnt; i++) { size_t size_bits; uintptr_t paddr; bool device; @@ -1112,7 +1119,11 @@ int allocman_add_simple_untypeds_with_regions(allocman_t *alloc, simple_t *simpl ZF_LOGF_IF(error, "bootstrap_prepare_handle_device_untyped_cap Failed"); size_t i; - size_t total_untyped = simple_get_untyped_count(simple); + int total_untyped = simple_get_untyped_count(simple); + if (total_untyped < 0) { + ZF_LOGW("Could not get untyped count (%d)", total_untyped); + return 0; /* don't report an error, just do nothing */ + } for(i = 0; i < total_untyped; i++) { size_t size_bits; diff --git a/libsel4simple/src/simple.c b/libsel4simple/src/simple.c index d280e6e4..34f08720 100644 --- a/libsel4simple/src/simple.c +++ b/libsel4simple/src/simple.c @@ -9,8 +9,13 @@ bool simple_is_untyped_cap(simple_t *simple, seL4_CPtr pos) { int i; + int cnt = simple_get_untyped_count(simple); + if (cnt < 0) { + ZF_LOGW("Could not get untyped count (%d)", cnt); + return false; + } - for (i = 0; i < simple_get_untyped_count(simple); i++) { + for (i = 0; i < cnt; i++) { seL4_CPtr ut_pos = simple_get_nth_untyped(simple, i, NULL, NULL, NULL); if (ut_pos == pos) { return true; From 96cb46f1bb4e091e110648cc78457c4e95581ac6 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 3 Nov 2023 16:15:35 +0100 Subject: [PATCH 20/21] libsel4allocman: inline loop variable Signed-off-by: Axel Heider --- libsel4allocman/src/bootstrap.c | 6 ++---- libsel4simple/src/simple.c | 3 +-- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/libsel4allocman/src/bootstrap.c b/libsel4allocman/src/bootstrap.c index d4dbc465..81bcf547 100644 --- a/libsel4allocman/src/bootstrap.c +++ b/libsel4allocman/src/bootstrap.c @@ -227,7 +227,6 @@ int bootstrap_add_untypeds_from_bootinfo(bootstrap_info_t *bs, seL4_BootInfo *bi static int bootstrap_add_untypeds_from_simple(bootstrap_info_t *bs, simple_t *simple) { int error; - int i; /* if we do not have a boot cspace, or we have added some uts that aren't in the * current space then just bail */ if (!bs->have_boot_cspace || (bs->uts && !bs->uts_in_current_cspace)) { @@ -240,7 +239,7 @@ static int bootstrap_add_untypeds_from_simple(bootstrap_info_t *bs, simple_t *si return 1; } - for (i = 0; i < cnt; i++) { + for (int i = 0; i < cnt; i++) { size_t size_bits; uintptr_t paddr; bool device; @@ -1118,14 +1117,13 @@ int allocman_add_simple_untypeds_with_regions(allocman_t *alloc, simple_t *simpl int error = prepare_handle_device_untyped_cap(alloc, simple, &state, num_regions, region_list); ZF_LOGF_IF(error, "bootstrap_prepare_handle_device_untyped_cap Failed"); - size_t i; int total_untyped = simple_get_untyped_count(simple); if (total_untyped < 0) { ZF_LOGW("Could not get untyped count (%d)", total_untyped); return 0; /* don't report an error, just do nothing */ } - for(i = 0; i < total_untyped; i++) { + for(int i = 0; i < total_untyped; i++) { size_t size_bits; uintptr_t paddr; bool device; diff --git a/libsel4simple/src/simple.c b/libsel4simple/src/simple.c index 34f08720..886db733 100644 --- a/libsel4simple/src/simple.c +++ b/libsel4simple/src/simple.c @@ -8,14 +8,13 @@ bool simple_is_untyped_cap(simple_t *simple, seL4_CPtr pos) { - int i; int cnt = simple_get_untyped_count(simple); if (cnt < 0) { ZF_LOGW("Could not get untyped count (%d)", cnt); return false; } - for (i = 0; i < cnt; i++) { + for (int i = 0; i < cnt; i++) { seL4_CPtr ut_pos = simple_get_nth_untyped(simple, i, NULL, NULL, NULL); if (ut_pos == pos) { return true; From 070911a2412bf641bb2933c1d2ae9c31754029c5 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Apr 2024 17:13:46 +0200 Subject: [PATCH 21/21] libsel4allocman: cleanup Signed-off-by: Axel Heider --- libsel4allocman/src/bootstrap.c | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/libsel4allocman/src/bootstrap.c b/libsel4allocman/src/bootstrap.c index 81bcf547..bde6a206 100644 --- a/libsel4allocman/src/bootstrap.c +++ b/libsel4allocman/src/bootstrap.c @@ -1011,10 +1011,7 @@ static int handle_device_untyped_cap(add_untypeds_state_t *state, uintptr_t padd bool cap_tainted = false; int error; uintptr_t ut_end = paddr + BIT(size_bits); - int num_regions = 0; - if (state != NULL) { - num_regions = state->num_regions; - } + int num_regions = state ? state->num_regions : 0; for (int i = 0; i < num_regions; i++) { pmem_region_t *region = &state->regions[i]; uint64_t region_end = region->base_addr + region->length;