seL4
zcu102 hello example build with SEL4CP_CONFIG=release fails
I'm trying to build the zcu102 hello example with SEL4CP_CONFIG set to "release" but it fails with the error message:
Traceback (most recent call last):
File "runpy", line 197, in _run_module_as_main
File "runpy", line 87, in _run_code
File "sel4coreplat.__main__", line 1781, in <module>
File "sel4coreplat.__main__", line 1632, in main
File "sel4coreplat.__main__", line 674, in build_system
File "sel4coreplat.sel4", line 819, in emulate_kernel_boot_partial
File "sel4coreplat.sel4", line 791, in _kernel_partial_boot
File "sel4coreplat.sel4", line 718, in _kernel_device_addrs
File "sel4coreplat.elf", line 442, in find_symbol
KeyError: 'No symbol named kernel_device_frames found'
I can build a "debug" binary w/o any issue.
I'm using Nataliya Korovkina's docker file. I'm using the latest sel4cp sources (commit 192c223).
The command I'm using:
PATH=$PATH:/usr/local/musl/aarch64/bin:/usr/local/gcc-x86_64-aarch64-none-elf/bin make BUILD_DIR=./release SEL4CP_SDK=/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6 SEL4CP_BOARD=zcu102 SEL4CP_CONFIG=release
The output prior to the error message:
aarch64-none-elf-gcc -c -mcpu=cortex-a53 -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall -Wno-unused-function -Werror -I/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6/board/zcu102/release/include hello.c -o release/hello.o
aarch64-none-elf-ld -L/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6/board/zcu102/release/lib release/hello.o -lsel4cp -Tsel4cp.ld -o release/hello.elf
/host/sandbox/tmp/sel4cp/release/sel4cp-sdk-1.2.6/bin/sel4cp hello.system --search-path ./release --board zcu102 --config release -o ./release/loader.img -r ./release/report.txt
I'm getting a similar error message for other platforms (e.g., Odroid-C2).
Hi Alain, I've recently discovered this issue as well. What's happening is that the seL4CP tool uses the kernel_device_frames array in the kernel ELF to know which device untypeds are not available to the user. Now what's happening with a release build of the kernel is that the compiler is doing optimisations and has decided to instead remove the array all together and I assume inline the accesses. This means that the symbol is gone by the time seL4CP reads the final kernel ELF.
So, how do we fix this? Fortunately there is instead a configuration file outputted by the kernel that contains the same data essentially and we can instead read from this instead of inspecting the kernel ELF. I'm waiting for https://github.com/seL4/seL4/pull/1061 to go through first, and then should be able to make a PR here with the fix.
I'm going to be on leave soon for a couple weeks and so if you need an urgent solution, this one line change to the kernel will also work: https://github.com/Ivan-Velickovic/seL4/commit/4542369ef353d325482ced8ddca235a750f2e35b.
Hi Ivan. It's not urgent. Just wanted to log the error. For now, I'm happy with debug builds. Thanks for the quick reply.