[patch-axel-52]

include/api/debug.h

@@ -4,10 +4,11 @@
  * SPDX-License-Identifier: GPL-2.0-only
  */
 
+#pragma once
+
 #include <config.h>
 
 #ifdef CONFIG_DEBUG_BUILD
-#pragma once
 
 #include <benchmark/benchmark_track.h>
 #include <arch/api/syscall.h>

include/api/syscall.h

@@ -29,11 +29,11 @@
     }
 #endif
 
-exception_t handleSyscall(syscall_t syscall);
-exception_t handleInterruptEntry(void);
-exception_t handleUnknownSyscall(word_t w);
-exception_t handleUserLevelFault(word_t w_a, word_t w_b);
-exception_t handleVMFaultEvent(vm_fault_type_t vm_faultType);
+void handleSyscall(syscall_t syscall);
+void handleInterruptEntry(void);
+void handleUnknownSyscall(word_t w);
+void handleUserLevelFault(word_t w_a, word_t w_b);
+void handleVMFaultEvent(vm_fault_type_t vm_faultType);
 
 static inline word_t PURE getSyscallArg(word_t i, word_t *ipc_buffer)
 {

include/arch/arm/arch/machine.h

@@ -63,6 +63,17 @@ static inline void arch_pause(void)
 {
     /* TODO */
 }
+
+static inline void ipi_mem_barrier(void)
+{
+    /* For GICv2 systems a dmb() is sufficient, but it's not enough with GICv3
+     * due to the way IPIs is triggered (memory-mapped or MSR inst.). A dmb()
+     * does not prevent re-ordering to happen between memory accesses and
+     * instructions, this guarantee requires a dsb().
+     */
+    dsb_ishst();
+}
+
 #endif /* ENABLE_SMP_SUPPORT */
 
 /* Update the value of the actual regsiter to hold the expected value */

include/arch/arm/arch/machine/hardware.h

@@ -19,17 +19,7 @@ typedef word_t vm_fault_type_t;
 #define PAGE_BASE(_p, _s)        ((_p) & ~MASK(pageBitsForSize((_s))))
 #define PAGE_OFFSET(_p, _s)      ((_p) & MASK(pageBitsForSize((_s))))
 
-#define IPI_MEM_BARRIER \
-  do { \
-     /* This can be relaxed for GICv2 but for GICv3 dmb() no longer works */ \
-     /* since the way IPI is triggered is different (memory-mapped or MSR inst.) */ \
-     /* and dmb() is not able to avoid re-ordering between memory accesses and */ \
-     /* instructions. In order to support both GICv2 and v3 dsb() is required. */ \
-     dsb_ishst(); \
-  } while (0)
-
 #endif /* __ASSEMBLER__ */
 
 #define L1_CACHE_LINE_SIZE_BITS CONFIG_L1_CACHE_LINE_SIZE_BITS
 #define L1_CACHE_LINE_SIZE BIT(L1_CACHE_LINE_SIZE_BITS)
-

include/arch/riscv/arch/machine.h

@@ -71,6 +71,11 @@ static inline void fence_rw_rw(void)
     asm volatile("fence rw, rw" ::: "memory");
 }
 
+static inline void ipi_mem_barrier(void)
+{
+    fence_rw_rw();
+}
+
 static inline void fence_w_rw(void)
 {
     asm volatile("fence w, rw" ::: "memory");

include/arch/riscv/arch/machine/hardware.h

@@ -122,9 +122,3 @@ static inline void arch_clean_invalidate_caches(void)
 
 #define LOAD_S STRINGIFY(LOAD)
 #define STORE_S STRINGIFY(STORE)
-
-#define IPI_MEM_BARRIER \
-    do { \
-        asm volatile("fence rw,rw" ::: "memory"); \
-    } while (0)
-

include/arch/x86/arch/kernel/x2apic.h

@@ -65,6 +65,14 @@ static inline void apic_write_icr(word_t high, word_t low)
     x86_wrmsr(APIC_ICR, icr);
 }
 
-#define IPI_ICR_BARRIER  asm volatile("mfence" ::: "memory")
-#define IPI_MEM_BARRIER  IPI_ICR_BARRIER
+static inline void ipi_icr_barrier(void)
+{
+    asm volatile("mfence" ::: "memory");
+}
+
+static inline void ipi_mem_barrier(void)
+{
+    IPI_ICR_BARRIER;
+}
+
 #endif /* CONFIG_X2APIC */

include/arch/x86/arch/kernel/xapic.h

@@ -66,7 +66,14 @@ static inline void apic_write_icr(word_t high, word_t low)
     apic_write_reg(APIC_ICR1, low);
 }
 
-#define IPI_ICR_BARRIER  asm volatile("" ::: "memory")
-#define IPI_MEM_BARRIER IPI_ICR_BARRIER
-#endif  /* CONFIG_XAPIC */
+static inline void ipi_icr_barrier(void)
+{
+    asm volatile("" ::: "memory");
+}
 
+static inline void ipi_mem_barrier(void)
+{
+    ipi_icr_barrier();
+}
+
+#endif  /* CONFIG_XAPIC */

include/assert.h

@@ -12,13 +12,14 @@
 #ifdef CONFIG_DEBUG_BUILD
 
 void _fail(
-    const char  *str,
     const char  *file,
     unsigned int line,
-    const char  *function
+    const char  *function,
+    const char  *str,
+    ...
 ) NORETURN;
 
-#define fail(s) _fail(s, __FILE__, __LINE__, __func__)
+#define fail(...) _fail(__FILE__, __LINE__, __func__, __VA_ARGS__)
 
 void _assert_fail(
     const char  *assertion,
@@ -36,7 +37,7 @@ void _assert_fail(
 
 #else /* !DEBUG */
 
-#define fail(s) halt()
+#define fail(...) halt()
 
 #define assert(expr)
 

include/benchmark/benchmark.h

@@ -15,18 +15,18 @@
 #include <mode/hardware.h>
 
 #ifdef CONFIG_ENABLE_BENCHMARKS
-exception_t handle_SysBenchmarkFlushCaches(void);
-exception_t handle_SysBenchmarkResetLog(void);
-exception_t handle_SysBenchmarkFinalizeLog(void);
+void handle_SysBenchmarkFlushCaches(void);
+void handle_SysBenchmarkResetLog(void);
+void handle_SysBenchmarkFinalizeLog(void);
 #ifdef CONFIG_KERNEL_LOG_BUFFER
-exception_t handle_SysBenchmarkSetLogBuffer(void);
+void handle_SysBenchmarkSetLogBuffer(void);
 #endif /* CONFIG_KERNEL_LOG_BUFFER */
 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
-exception_t handle_SysBenchmarkGetThreadUtilisation(void);
-exception_t handle_SysBenchmarkResetThreadUtilisation(void);
+void handle_SysBenchmarkGetThreadUtilisation(void);
+void handle_SysBenchmarkResetThreadUtilisation(void);
 #ifdef CONFIG_DEBUG_BUILD
-exception_t handle_SysBenchmarkDumpAllThreadsUtilisation(void);
-exception_t handle_SysBenchmarkResetAllThreadsUtilisation(void);
+void handle_SysBenchmarkDumpAllThreadsUtilisation(void);
+void handle_SysBenchmarkResetAllThreadsUtilisation(void);
 #endif /* CONFIG_DEBUG_BUILD */
 #endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
 #endif /* CONFIG_ENABLE_BENCHMARKS */

include/smp/ipi.h

@@ -157,7 +157,7 @@ void doMaskReschedule(word_t mask);
 
 
 #ifdef CONFIG_DEBUG_BUILD
-exception_t handle_SysDebugSendIPI(void);
+void handle_SysDebugSendIPI(void);
 #endif
 
 #endif /* ENABLE_SMP_SUPPORT */

libsel4/arch_include/arm/sel4/arch/syscalls.h

@@ -629,10 +629,14 @@ LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
     return (seL4_Uint32)cap;
 }
 
-char *strcpy(char *, const char *);
+char *strncpy(char *, const char *, seL4_Word);
 LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
 {
-    strcpy((char *)seL4_GetIPCBuffer()->msg, name);
+    /* IPC buffer can be used directly, otherwise buffers must not overlap. */
+    char *ipc_buf = (char *)seL4_GetIPCBuffer()->msg;
+    if (name != ipc_buf) {
+        strncpy(ipc_buf, name, seL4_MsgMaxLength);
+    }
 
     seL4_Word unused0 = 0;
     seL4_Word unused1 = 0;

libsel4/arch_include/riscv/sel4/arch/syscalls.h

@@ -834,10 +834,14 @@ LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
     return (seL4_Uint32)cap;
 }
 
-char *strcpy(char *, const char *);
+char *strncpy(char *, const char *, seL4_Word);
 LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
 {
-    strcpy((char *)seL4_GetIPCBuffer()->msg, name);
+    /* IPC buffer can be used directly, otherwise buffers must not overlap. */
+    char *ipc_buf = (char *)seL4_GetIPCBuffer()->msg;
+    if (name != ipc_buf) {
+        strncpy(ipc_buf, name, seL4_MsgMaxLength);
+    }
 
     seL4_Word unused0 = 0;
     seL4_Word unused1 = 0;

libsel4/include/sel4/functions.h

@@ -103,3 +103,24 @@ LIBSEL4_INLINE_FUNC void seL4_SetCapReceivePath(seL4_CPtr receiveCNode, seL4_CPt
     ipcbuffer->receiveDepth = receiveDepth;
 }
 
+#if CONFIG_DEBUG_BUILD
+
+/* Making this a macro avoids requiring stdarg.h to get va_start() */
+#define seL4_DebugNameThreadFmt(tcb, fmt, ...) \
+    do { \
+        char *ipc_buf = (char *)seL4_GetIPCBuffer()->msg; \
+        snprintf(ipc_buf, seL4_MsgMaxLength, fmt, __VA_ARGS__); \
+        seL4_DebugNameThread(tcb, ipc_buf); \
+    } while(0)
+
+// LIBSEL4_INLINE_FUNC void seL4_DebugNameThreadFmt(seL4_CPtr tcb, const char *fmt, ...)
+// {
+//     char *ipc_buf = (char *)seL4_GetIPCBuffer()->msg;
+//     va_list args;
+//     va_start(args, fmt);
+//     vsnprintf(ipc_buf, seL4_MsgMaxLength, fmt, args)
+//     va_end(args);
+//     seL4_DebugNameThread(tcb, ipc_buf);
+// }
+
+#endif /* CONFIG_DEBUG_BUILD */

libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h

@@ -862,10 +862,14 @@ LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
     return (seL4_Uint32)cap;
 }
 
-char *strcpy(char *, const char *);
+char *strncpy(char *, const char *, seL4_Word);
 LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
 {
-    strcpy((char *)seL4_GetIPCBuffer()->msg, name);
+    /* IPC buffer can be used directly, otherwise buffers must not overlap. */
+    char *ipc_buf = (char *)seL4_GetIPCBuffer()->msg;
+    if (name != ipc_buf) {
+        strncpy(ipc_buf, name, seL4_MsgMaxLength);
+    }
 
     seL4_Word unused0 = 0;
     seL4_Word unused1 = 0;

libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h

@@ -658,11 +658,14 @@ LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
 #endif
 
 #ifdef CONFIG_DEBUG_BUILD
-char *strcpy(char *, const char *);
+char *strncpy(char *, const char *, seL4_Word);
 LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
 {
-
-    strcpy((char *)seL4_GetIPCBuffer()->msg, name);
+    /* IPC buffer can be used directly, otherwise buffers must not overlap. */
+    char *ipc_buf = (char *)seL4_GetIPCBuffer()->msg;
+    if (name != ipc_buf) {
+        strncpy(ipc_buf, name, seL4_MsgMaxLength);
+    }
 
     seL4_Word unused0 = 0;
     seL4_Word unused1 = 0;