RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

userError string written to IPC buffer

Browse Source 
The format string in userError is now written to
the IPC buffer for debugging purposes.
This requires an snprintf which reuses vprintf with
a new structure for handling how output is done.

Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
This commit is contained in:
Saer Debel
2020-04-06 10:59:19 +10:00
parent 0548f8d7e9
commit 9dad7382e1
7 changed files with 120 additions and 30 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
include/api/failures.h
View File

@@ -8,6 +8,7 @@
#include <types.h>
#include <sel4/errors.h>
#include <sel4/constants.h>
/* These datatypes differ markedly from haskell, due to the
* different implementation of the various fault monads */
@@ -35,7 +36,13 @@ struct syscall_error {
};
typedef struct syscall_error syscall_error_t;
struct debug_syscall_error {
word_t errorMessage[DEBUG_MESSAGE_MAXLEN];
};
typedef struct debug_syscall_error debug_syscall_error_t;
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;

4
include/api/types.h
View File

@@ -110,6 +110,8 @@ static inline word_t CONST wordFromMessageInfo(seL4_MessageInfo_t mi)
#define THREAD_NAME ""
#endif
extern struct debug_syscall_error current_debug_error;
/*
* Print to serial a message helping userspace programmers to determine why the
* kernel is not performing their requested operation.
@@ -124,6 +126,8 @@ static inline word_t CONST wordFromMessageInfo(seL4_MessageInfo_t mi)
(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__); \
} while (0)
#else /* !CONFIG_PRINTING */
#define userError(...)

3
include/machine/io.h
View File

@@ -27,9 +27,10 @@ unsigned char getDebugChar(void);
void putchar(char c);
#define kernel_putchar(c) putchar(c)
word_t kprintf(const char *format, ...) VISIBLE FORMAT(printf, 1, 2);
word_t ksnprintf(char *str, word_t size, const char *format, ...);
word_t puts(const char *s) VISIBLE;
word_t print_unsigned_long(unsigned long x, word_t ui_base) VISIBLE;
#define printf(args...) kprintf(args)
#define snprintf(args...) ksnprintf(args)
#else /* CONFIG_PRINTING */
/* printf will NOT result in output */
#define kernel_putchar(c) ((void)(0))

3
libsel4/include/sel4/constants.h
View File

@@ -97,3 +97,6 @@ static inline seL4_Word seL4_MaxExtraRefills(seL4_Word size)
#endif /* !__ASSEMBLER__ */
#endif /* CONFIG_KERNEL_MCS */
#define DEBUG_MESSAGE_START 6
#define DEBUG_MESSAGE_MAXLEN 50

1
src/inlines.c
View File

@@ -10,3 +10,4 @@
lookup_fault_t current_lookup_fault;
seL4_Fault_t current_fault;
syscall_error_t current_syscall_error;
debug_syscall_error_t current_debug_error;

123
src/machine/io.c
View File

@@ -11,6 +11,35 @@
#include <stdarg.h>
/*
* a handle defining how to output a character
*/
typedef void (*out_fn)(char character, char *buf, word_t idx);
/*
* structure to allow a generic vprintf
* a out_fn handle and a buf to work on
*/
typedef struct {
out_fn putchar;
char *buf;
word_t idx;
word_t maxlen;
} out_wrap_t;
/*
* putchar would then just call the handle with its buf
* and current idx and then increment idx
*/
static void putchar_wrap(out_wrap_t *out, char c)
{
if (out->maxlen < 0 || out->idx < out->maxlen) {
out->putchar(c, out->buf, out->idx);
out->idx++;
}
}
void putchar(char c)
{
if (c == '\n') {
@@ -19,21 +48,21 @@ void putchar(char c)
putDebugChar(c);
}
static unsigned int print_spaces(int n)
static unsigned int print_spaces(out_wrap_t *out, int n)
{
for (int i = 0; i < n; i++) {
kernel_putchar(' ');
putchar_wrap(out, ' ');
}
return n;
}
static unsigned int print_string(const char *s)
static unsigned int print_string(out_wrap_t *out, const char *s)
{
unsigned int n;
for (n = 0; *s; s++, n++) {
kernel_putchar(*s);
putchar_wrap(out, *s);
}
return n;
@@ -63,7 +92,7 @@ static unsigned long xmod(unsigned long x, unsigned int denom)
}
}
word_t print_unsigned_long(unsigned long x, word_t ui_base)
static word_t print_unsigned_long(out_wrap_t *out_wrap, unsigned long x, word_t ui_base)
{
char out[sizeof(unsigned long) * 2 + 3];
word_t i, j;
@@ -78,7 +107,7 @@ word_t print_unsigned_long(unsigned long x, word_t ui_base)
}
if (x == 0) {
kernel_putchar('0');
putchar_wrap(out_wrap, '0');
return 1;
}
@@ -93,7 +122,7 @@ word_t print_unsigned_long(unsigned long x, word_t ui_base)
}
for (j = i; j > 0; j--) {
kernel_putchar(out[j - 1]);
putchar_wrap(out_wrap, out[j - 1]);
}
return i;
@@ -104,7 +133,7 @@ word_t print_unsigned_long(unsigned long x, word_t ui_base)
compile_assert(print_unsigned_long_long_sizes, sizeof(unsigned int) * 2 == sizeof(unsigned long long))
static unsigned int
print_unsigned_long_long(unsigned long long x, unsigned int ui_base)
print_unsigned_long_long(out_wrap_t *out, unsigned long long x, unsigned int ui_base)
{
unsigned int upper, lower;
unsigned int n = 0;
@@ -122,10 +151,10 @@ print_unsigned_long_long(unsigned long long x, unsigned int ui_base)
/* print first 32 bits if they exist */
if (upper > 0) {
n += print_unsigned_long(upper, ui_base);
n += print_unsigned_long(out, upper, ui_base);
/* print leading 0s */
while (!(mask & lower)) {
kernel_putchar('0');
putchar_wrap(out, '0');
n++;
mask = mask >> 4;
shifts++;
@@ -135,7 +164,7 @@ print_unsigned_long_long(unsigned long long x, unsigned int ui_base)
}
}
/* print last 32 bits */
n += print_unsigned_long(lower, ui_base);
n += print_unsigned_long(out, lower, ui_base);
return n;
}
@@ -151,7 +180,7 @@ static inline int atoi(char c)
return c - '0';
}
static int vprintf(const char *format, va_list ap)
static int vprintf(out_wrap_t *out, const char *format, va_list ap)
{
unsigned int n;
unsigned int formatting;
@@ -174,7 +203,7 @@ static int vprintf(const char *format, va_list ap)
}
switch (*format) {
case '%':
kernel_putchar('%');
putchar_wrap(out, '%');
n++;
format++;
break;
@@ -183,40 +212,40 @@ static int vprintf(const char *format, va_list ap)
int x = va_arg(ap, int);
if (x < 0) {
kernel_putchar('-');
putchar_wrap(out, '-');
n++;
x = -x;
}
n += print_unsigned_long(x, 10);
n += print_unsigned_long(out, x, 10);
format++;
break;
}
case 'u':
n += print_unsigned_long(va_arg(ap, unsigned int), 10);
n += print_unsigned_long(out, va_arg(ap, unsigned int), 10);
format++;
break;
case 'x':
n += print_unsigned_long(va_arg(ap, unsigned int), 16);
n += print_unsigned_long(out, va_arg(ap, unsigned int), 16);
format++;
break;
case 'p': {
unsigned long p = va_arg(ap, unsigned long);
if (p == 0) {
n += print_string("(nil)");
n += print_string(out, "(nil)");
} else {
n += print_string("0x");
n += print_unsigned_long(p, 16);
n += print_string(out, "0x");
n += print_unsigned_long(out, p, 16);
}
format++;
break;
}
case 's':
n += print_string(va_arg(ap, char *));
n += print_string(out, va_arg(ap, char *));
format++;
break;
@@ -227,27 +256,27 @@ static int vprintf(const char *format, va_list ap)
long x = va_arg(ap, long);
if (x < 0) {
kernel_putchar('-');
putchar_wrap(out, '-');
n++;
x = -x;
}
n += print_unsigned_long((unsigned long)x, 10);
n += print_unsigned_long(out, (unsigned long)x, 10);
format++;
}
break;
case 'l':
if (*(format + 1) == 'x') {
n += print_unsigned_long_long(va_arg(ap, unsigned long long), 16);
n += print_unsigned_long_long(out, va_arg(ap, unsigned long long), 16);
}
format += 2;
break;
case 'u':
n += print_unsigned_long(va_arg(ap, unsigned long), 10);
n += print_unsigned_long(out, va_arg(ap, unsigned long), 10);
format++;
break;
case 'x':
n += print_unsigned_long(va_arg(ap, unsigned long), 16);
n += print_unsigned_long(out, va_arg(ap, unsigned long), 16);
format++;
break;
@@ -261,7 +290,9 @@ static int vprintf(const char *format, va_list ap)
return -1;
}
n += print_spaces(nspaces - n);
if (nspaces > n) {
n += print_spaces(out, nspaces - n);
}
nspaces = 0;
formatting = 0;
} else {
@@ -272,7 +303,7 @@ static int vprintf(const char *format, va_list ap)
break;
default:
kernel_putchar(*format);
putchar_wrap(out, *format);
n++;
format++;
break;
@@ -283,6 +314,18 @@ static int vprintf(const char *format, va_list ap)
return n;
}
// sprintf fills its buf with the given character
static void buf_out_fn(char c, char *buf, word_t idx)
{
buf[idx] = c;
}
// printf only needs to call kernel_putchar
static void kernel_out_fn(char c, char *buf, word_t idx)
{
kernel_putchar(c);
}
word_t puts(const char *s)
{
for (; *s; s++) {
@@ -297,10 +340,32 @@ word_t kprintf(const char *format, ...)
va_list args;
word_t i;
out_wrap_t out = { kernel_out_fn, NULL, 0, -1 };
va_start(args, format);
i = vprintf(format, args);
i = vprintf(&out, format, args);
va_end(args);
return i;
}
word_t ksnprintf(char *str, word_t size, const char *format, ...)
{
va_list args;
word_t i;
out_wrap_t out = { buf_out_fn, str, 0, size };
va_start(args, format);
i = vprintf(&out, format, args);
va_end(args);
// make sure there is space for a 0 byte
if (i >= size) {
i = size - 1;
}
str[i] = 0;
return i;
}
#endif /* CONFIG_PRINTING */

9
src/object/endpoint.c
View File

@@ -5,6 +5,8 @@
*/
#include <types.h>
#include <string.h>
#include <sel4/constants.h>
#include <kernel/thread.h>
#include <kernel/vspace.h>
#include <machine/registerset.h>
@@ -259,6 +261,13 @@ void replyFromKernel_error(tcb_t *thread)
ipcBuffer = lookupIPCBuffer(true, thread);
setRegister(thread, badgeRegister, 0);
len = setMRs_syscall_error(thread, ipcBuffer);
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;
setRegister(thread, msgInfoRegister, wordFromMessageInfo(
seL4_MessageInfo_new(current_syscall_error.type, 0, 0, len)));
}