search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

zcu102 hello example build with SEL4CP_CONFIG=release fails #35

Open alain-lclark opened 1 year ago

alain-lclark commented 1 year ago

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).

Ivan-Velickovic commented 1 year ago

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.

Ivan-Velickovic commented 1 year ago

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.

alain-lclark commented 1 year ago

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.

Ivan-Velickovic commented 1 year ago

No worries, thanks for reporting it!