From a221ee1ca8dde0b9683887746524893abf0c79b8 Mon Sep 17 00:00:00 2001 From: Saer Debel Date: Mon, 6 Apr 2020 10:59:34 +1000 Subject: [PATCH] Enabled IPC debug features under new config Introduced a new config flag to enable userError format strings to be written to the IPC buffer. Another config bool has been introduced to toggle printing the error out and this can also be set at runtime. Signed-off-by: Saer Debel --- config.cmake | 9 ++++++++ include/api/failures.h | 4 +++- include/api/types.h | 21 ++++++++++++------- libsel4/CMakeLists.txt | 8 +++++++ libsel4/arch_include/arm/sel4/arch/syscalls.h | 8 +++++++ .../arch_include/riscv/sel4/arch/syscalls.h | 8 +++++++ libsel4/include/sel4/constants.h | 3 ++- libsel4/include/sel4/functions.h | 20 ++++++++++++++++++ .../ia32/sel4/sel4_arch/syscalls.h | 9 ++++++++ .../x86_64/sel4/sel4_arch/syscalls.h | 8 +++++++ libsel4/src/sel4_bootinfo.c | 4 ++++ libsel4/tools/syscall_stub_gen.py | 5 +++++ src/inlines.c | 3 +++ src/object/endpoint.c | 2 ++ 14 files changed, 102 insertions(+), 10 deletions(-) diff --git a/config.cmake b/config.cmake index 48023e8f8..a61812c9f 100644 --- a/config.cmake +++ b/config.cmake @@ -330,6 +330,15 @@ config_option( DEPENDS "NOT KernelVerificationBuild" DEFAULT_DISABLED OFF ) + +config_option( + KernelInvocationReportErrorIPC KERNEL_INVOCATION_REPORT_ERROR_IPC + "Allows the kernel to write the userError to the IPC buffer" + DEFAULT OFF + DEPENDS "KernelPrinting" + DEFAULT_DISABLED OFF +) + config_choice( KernelBenchmarks KERNEL_BENCHMARK diff --git a/include/api/failures.h b/include/api/failures.h index bbd0f8046..b84de75bc 100644 --- a/include/api/failures.h +++ b/include/api/failures.h @@ -36,13 +36,15 @@ struct syscall_error { }; typedef struct syscall_error syscall_error_t; +#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC struct debug_syscall_error { word_t errorMessage[DEBUG_MESSAGE_MAXLEN]; }; typedef struct debug_syscall_error debug_syscall_error_t; +extern debug_syscall_error_t current_debug_error; +#endif extern lookup_fault_t current_lookup_fault; extern seL4_Fault_t current_fault; extern syscall_error_t current_syscall_error; -extern debug_syscall_error_t current_debug_error; diff --git a/include/api/types.h b/include/api/types.h index 05e97ad2c..df01660b4 100644 --- a/include/api/types.h +++ b/include/api/types.h @@ -110,24 +110,29 @@ static inline word_t CONST wordFromMessageInfo(seL4_MessageInfo_t mi) #define THREAD_NAME "" #endif +#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC extern struct debug_syscall_error current_debug_error; +#define out_error(...) \ + snprintf((char *)current_debug_error.errorMessage, \ + DEBUG_MESSAGE_MAXLEN * sizeof(word_t), __VA_ARGS__); +#else +#define out_error printf +#endif + /* * Print to serial a message helping userspace programmers to determine why the * kernel is not performing their requested operation. */ -#define userError(...) \ +#define userError(M, ...) \ do { \ - printf(ANSI_DARK "<<" ANSI_GREEN "seL4(CPU %lu)" ANSI_DARK \ - " [%s/%d T%p \"%s\" @%lx]: ", \ + out_error(ANSI_DARK "<<" ANSI_GREEN "seL4(CPU %lu)" ANSI_DARK \ + " [%s/%d T%p \"%s\" @%lx]: " M ">>" ANSI_RESET "\n", \ SMP_TERNARY(getCurrentCPUIndex(), 0lu), \ __func__, __LINE__, NODE_STATE(ksCurThread), \ THREAD_NAME, \ - (word_t)getRestartPC(NODE_STATE(ksCurThread))); \ - printf(__VA_ARGS__); \ - printf(">>" ANSI_RESET "\n"); \ - snprintf((char *)current_debug_error.errorMessage, \ - DEBUG_MESSAGE_MAXLEN * sizeof(word_t), __VA_ARGS__); \ + (word_t)getRestartPC(NODE_STATE(ksCurThread)), \ + ## __VA_ARGS__); \ } while (0) #else /* !CONFIG_PRINTING */ #define userError(...) diff --git a/libsel4/CMakeLists.txt b/libsel4/CMakeLists.txt index 665d7bd10..d6ca94801 100644 --- a/libsel4/CMakeLists.txt +++ b/libsel4/CMakeLists.txt @@ -35,6 +35,14 @@ config_option( DEFAULT OFF ) +config_string( + LibSel4PrintInvocationErrors LIB_SEL4_PRINT_INVOCATION_ERRORS + "Generated stubs on error will print the message contained in the IPC buffer" + DEFAULT 1 + DEPENDS "KernelInvocationReportErrorIPC" DEFAULT_DISABLED 0 + UNQUOTE +) + if(LibSel4StubsUseIPCBufferOnly) set(buffer "--buffer") endif() diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h index 45b9bfc57..eb31dc8a6 100644 --- a/libsel4/arch_include/arm/sel4/arch/syscalls.h +++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h @@ -584,6 +584,14 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c) arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0); } +LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) +{ + for (char *s = str; *s; s++) { + seL4_DebugPutChar(*s); + } + return; +} + LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void) { seL4_Word unused0 = 0; diff --git a/libsel4/arch_include/riscv/sel4/arch/syscalls.h b/libsel4/arch_include/riscv/sel4/arch/syscalls.h index 58c84ba8c..00f393e36 100644 --- a/libsel4/arch_include/riscv/sel4/arch/syscalls.h +++ b/libsel4/arch_include/riscv/sel4/arch/syscalls.h @@ -786,6 +786,14 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c) &unused4, &unused5, 0); } +LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) +{ + for (char *s = str; *s; s++) { + seL4_DebugPutChar(*s); + } + return; +} + LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void) { seL4_Word unused0 = 0; diff --git a/libsel4/include/sel4/constants.h b/libsel4/include/sel4/constants.h index a68f7a68f..dbeb557e7 100644 --- a/libsel4/include/sel4/constants.h +++ b/libsel4/include/sel4/constants.h @@ -97,6 +97,7 @@ static inline seL4_Word seL4_MaxExtraRefills(seL4_Word size) #endif /* !__ASSEMBLER__ */ #endif /* CONFIG_KERNEL_MCS */ +#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC #define DEBUG_MESSAGE_START 6 #define DEBUG_MESSAGE_MAXLEN 50 - +#endif diff --git a/libsel4/include/sel4/functions.h b/libsel4/include/sel4/functions.h index 0bceb5654..e66b439f3 100644 --- a/libsel4/include/sel4/functions.h +++ b/libsel4/include/sel4/functions.h @@ -13,6 +13,26 @@ extern __thread seL4_IPCBuffer *__sel4_ipc_buffer; __thread __attribute__((weak)) seL4_IPCBuffer *__sel4_ipc_buffer; +#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC +extern __thread char __sel4_print_error; + +LIBSEL4_INLINE_FUNC char *seL4_GetDebugError(void) +{ + return (char *)(__sel4_ipc_buffer->msg + DEBUG_MESSAGE_START); +} + +LIBSEL4_INLINE_FUNC void seL4_SetPrintError(char print_error) +{ + __sel4_print_error = print_error; + return; +} + +LIBSEL4_INLINE_FUNC char seL4_CanPrintError(void) +{ + return __sel4_print_error; +} +#endif + LIBSEL4_INLINE_FUNC void seL4_SetIPCBuffer(seL4_IPCBuffer *ipc_buffer) { __sel4_ipc_buffer = ipc_buffer; diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h index f2f807cc4..0ba7aa949 100644 --- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h +++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h @@ -815,6 +815,15 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c) x86_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } +LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) +{ + for (char *s = str; *s; s++) { + seL4_DebugPutChar(*s); + } + return; +} + + LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void) { seL4_Word unused0 = 0; diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h index c254c2c54..516f413c3 100644 --- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h +++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h @@ -588,6 +588,14 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c) x64_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0); } +LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) +{ + for (char *s = str; *s; s++) { + seL4_DebugPutChar(*s); + } + return; +} + LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void) { seL4_Word unused0 = 0; diff --git a/libsel4/src/sel4_bootinfo.c b/libsel4/src/sel4_bootinfo.c index 03e3e94e2..afee42729 100644 --- a/libsel4/src/sel4_bootinfo.c +++ b/libsel4/src/sel4_bootinfo.c @@ -6,6 +6,10 @@ #include +#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC +__thread char __sel4_print_error = CONFIG_LIB_SEL4_PRINT_INVOCATION_ERRORS; +#endif + /** Userland per-thread IPC buffer address **/ __thread seL4_IPCBuffer *__sel4_ipc_buffer; diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py index a2b6ced17..0ca4ed5d6 100644 --- a/libsel4/tools/syscall_stub_gen.py +++ b/libsel4/tools/syscall_stub_gen.py @@ -715,6 +715,11 @@ def generate_stub(arch, wordsize, interface_name, method_name, method_id, input_ result.append("\tif (%s != seL4_NoError) {" % label) for i in range(num_mrs): result.append("\t\tseL4_SetMR(%d, mr%d);" % (i, i)) + result.append("#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC") + result.append("\t\tif (seL4_CanPrintError()) {") + result.append("\t\t\tseL4_DebugPutString(seL4_GetDebugError());") + result.append("\t\t}") + result.append("#endif") if returning_struct: result.append("\t\treturn result;") result.append("\t}") diff --git a/src/inlines.c b/src/inlines.c index 42b61af5b..a93984a0c 100644 --- a/src/inlines.c +++ b/src/inlines.c @@ -10,4 +10,7 @@ lookup_fault_t current_lookup_fault; seL4_Fault_t current_fault; syscall_error_t current_syscall_error; +#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC debug_syscall_error_t current_debug_error; +#endif + diff --git a/src/object/endpoint.c b/src/object/endpoint.c index 9b126ba92..308deabf1 100644 --- a/src/object/endpoint.c +++ b/src/object/endpoint.c @@ -262,11 +262,13 @@ void replyFromKernel_error(tcb_t *thread) setRegister(thread, badgeRegister, 0); len = setMRs_syscall_error(thread, ipcBuffer); +#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC char *debugBuffer = (char *)(ipcBuffer + DEBUG_MESSAGE_START + 1); word_t add = strlcpy(debugBuffer, (char *)current_debug_error.errorMessage, DEBUG_MESSAGE_MAXLEN * sizeof(word_t)); len += (add / sizeof(word_t)) + 1; +#endif setRegister(thread, msgInfoRegister, wordFromMessageInfo( seL4_MessageInfo_new(current_syscall_error.type, 0, 0, len)));