From 50976837c79178cbb71472bec713908d36ade314 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:57:48 +0100 Subject: [PATCH 1/9] 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 a1f130e55..d3f569853 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 2b73861114a2eaf67eee469d508d6cad214ad74c Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:58:03 +0100 Subject: [PATCH 2/9] 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 d3f569853..355abaa2f 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 d785a2202a46f0594a24b72ed628e063acaa2d41 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:55:51 +0100 Subject: [PATCH 3/9] 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 355abaa2f..d354f5795 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 58d56a14a280521b5a0e4f27bc7d385b671256b7 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:56:01 +0100 Subject: [PATCH 4/9] 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 d354f5795..b499a759b 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 723b6fa9769aa660380e9a0ce0474093af903340 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 12 Jan 2024 12:57:00 +0100 Subject: [PATCH 5/9] 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 b499a759b..7fa76333d 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 335cecee0c63d2d557a9e8729bf41450f872a3d9 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 22:24:26 +0100 Subject: [PATCH 6/9] 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 7fa76333d..ad0ffc961 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 f56797b1d2ba89e1958b34ba99f77e3aea17ac00 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 23:12:29 +0100 Subject: [PATCH 7/9] 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 ad0ffc961..7eac97ef1 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 9cf8949afe549ee95f5309a510f44b7e0dda16e4 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 22:04:12 +0100 Subject: [PATCH 8/9] 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 7eac97ef1..d0fccd972 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 f8a55267ec2413d076aadbd4c050db4151708387 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 22 Feb 2024 23:12:51 +0100 Subject: [PATCH 9/9] 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 d0fccd972..9fcf9b8ca 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_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; }