[seL4] Re: Bug when compling in release mode

June 2, 2021 9:08 AM, "Kent Mcleod" wrote:

On Thu, May 20, 2021 at 6:13 AM Ben Fiedler wrote:

...

Hello everyone,

I've recently found an interesting bug that only occurs when compiling in release mode.

Use of the ZF_LOG library (for normal log output) leads to syscalls being made when the capdl-loader runs. These are invoked via musllibc's __stdio_write, which relies on __sysinfo being set correctly for syscalls to work. When compiling with RELEASE=OFF this works fine, however when compiling with RELEASE=ON, __sysinfo is not set (yet?), and subsequently leads to an illegal prefetch exception when __stdio_write tries to invoke a syscall.

Setting __sysinfo to sel4_vsyscall using gdb during runtime fixes this. I don't really know the correct place to fix this in the code, but I hope that you can provide some hints on where to fix this bug.

If you look in the CMake file capdl-loader-app/helpers.cmake you will see that libsel4muslcsys is only linked into the capdl-loader-app under debug builds. This library implements the registration of a set of syscalls under __sysinfo and any printing would need to go through that. Thus, the capdl-loader-app doesn't support log output via ZF_LOG while RELEASE=ON.

RELEASE=ON essentially does 2 things currently: Turn off kernel debug syscalls, and turn up optimization levels for the compiler. The printing in the capdl-loader-app needs the seL4_DebugPutChar syscall, so you would still need that syscall to turn on printing.

Ah that makes sense. I've worked around this issue by selectively enabling printing only in the files I need to (using #define ZF_LOG_LEVEL).

If you wanted to add printing when RELEASE=ON then you would need to link libsel4muslcsys unconditionally, and edit main.c to call init_bootinfo also, and you would need to also set KernelPrinting=ON.

I'll keep this in mind for further debugging, thanks!