[seL4] Re: Port to a cartesi-machine (riscv:rv64ima)

On Fri, Aug 27, 2021 at 11:17 PM Kent Mcleod wrote:

Ah, I misunderstood what you meant by initialization functions.

The compilation error you get after rebuilding the docker container should be resolved with the patch associated with: https://github.com/seL4/seL4/issues/374#issuecomment-891737492. It does appear that the riscv compilers present in the current published version of the docker container don't have all of the different combinations of the compiler runtime binaries that you would expect with a multilib configuration. There are just versions for the abi combinations: ilp32, ilp32d, lp64, lp64d which implies arch combinations of at least rv*imac for all of them. Compare this with riscv64-unknown-elf-gcc in the debian repositories that has separate runtime binaries for almost every enumeration: rv32e rv32ea rv32eac rv32em rv32emac rv32i rv32ia rv32iac rv32iaf rv32iafd rv32if rv32ifd rv32im rv32imac rv32imafc rv32imafdc rv32imf rv32imfd rv64i rv64ia rv64iac rv64iaf rv64iafd rv64if rv64ifd rv64im rv64imac rv64imafc rv64imafdc rv64imf.

Patch worked, thanks.

If you turn on verbose mode for the linker, you should be able to see

which version of libgcc, crtbegin.o and crtend.o that the compiler uses (In some CMakeLists.txt: add_compile_options(-Wl,--verbose)).

I expect that your approach of rebuilding the compiler with the flags you want would work provided that you apply the patch from the top of my response to fix the seL4 build error. (Alternatively, you could build a gcc-10 version instead of gcc-11).

It worked, as in got sel4test to start at least, but I'm switching tasks for now. Hopefully I'll revisit this port in the future. Thanks for the help on this.

On Sat, Aug 28, 2021 at 3:07 AM Marcelo Politzer wrote:

...

The problem reported here happened after both of those changes, that is

what got me confused.

...

My suspicion is that these initialization functions get built as part of

...

I include `--with-arch=rv64ima --with-abi=lp64` to the toolchain "./configure" in riscv.Dockerfile:44. followed by a: `./build.sh -b camkes -s riscv` and then: `make -C sel4-docker/ user_camkes-riscv HOST_DIR=$PWD`

I tried to build the same project with: ``` ../init-build.sh -DPLATFORM=spike -DRISCV64=1 -DSIMULATION=TRUE -DElfloaderIncludeDtb=OFF ninja ```

But that got me this error: ``` [1/38] Generating circular_includes_valid FAILED: kernel/circular_includes_valid cd /host/cartesi/build2/kernel && /host/cartesi/kernel/tools/circular_includes.py --ignore kernel_all_copy.c < kernel_all.i && touch circular_includes_valid Traceback (most recent call last): File "/host/cartesi/kernel/tools/circular_includes.py", line 74, in <module> sys.exit(main(args)) File "/host/cartesi/kernel/tools/circular_includes.py", line 61, in

the GCC compilation stages, to try that out main

...

while file_stack[-1] != header: IndexError: list index out of range ninja: build stopped: subcommand failed. ```

The actual diffs for reference (some dirty, testing code)

``` diff --git a/CMakeLists.txt b/CMakeLists.txt index 57493960..f088648f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -79,7 +79,7 @@ if(KernelArchRiscV) string(APPEND common_flags " -march=rv64imafdc") string(APPEND common_flags " -mabi=lp64d") else() - string(APPEND common_flags " -march=rv64imac") + string(APPEND common_flags " -march=rv64ima") string(APPEND common_flags " -mabi=lp64") endif() else() ```

https://github.com/seL4/seL4_tools.git ``` diff --git a/cmake-tool/helpers/rootserver.cmake

...

index b0d8172..1af323e 100644 --- a/cmake-tool/helpers/rootserver.cmake +++ b/cmake-tool/helpers/rootserver.cmake @@ -98,35 +98,26 @@ function(DeclareRootserver rootservername) message(FATAL_ERROR "CROSS_COMPILER_PREFIX not set.") endif()

- if("${KernelOpenSBIPlatform}" STREQUAL "") - message(FATAL_ERROR "KernelOpenSBIPlatform not set.") - endif() - file(GLOB_RECURSE deps) set(OPENSBI_BINARY_DIR "${CMAKE_BINARY_DIR}/opensbi") set(OPENSBI_PLAYLOAD "${OPENSBI_BINARY_DIR}/payload") - if(Kernel32) - set(PLATFORM_RISCV_ISA "rv32imafdc") - set(PLATFORM_RISCV_ABI "ilp32d") - else() - set(PLATFORM_RISCV_ISA "rv64imafdc") - set(PLATFORM_RISCV_ABI "lp64d") - endif() + set(PLATFORM_RISCV_ISA "rv64ima") + set(PLATFORM_RISCV_ABI "lp64") set( OPENSBI_FW_PAYLOAD_ELF - "${OPENSBI_BINARY_DIR}/platform/${KernelOpenSBIPlatform}/firmware/fw_payload.elf" + "${OPENSBI_BINARY_DIR}/platform/cartesi/firmware/fw_payload.elf" ) add_custom_command( OUTPUT "${OPENSBI_FW_PAYLOAD_ELF}" COMMAND mkdir -p "${OPENSBI_BINARY_DIR}" COMMAND make -s -C "${OPENSBI_PATH}" O="${OPENSBI_BINARY_DIR}" - PLATFORM="${KernelOpenSBIPlatform}" clean + PLATFORM="cartesi" clean COMMAND ${CMAKE_OBJCOPY} -O binary "${elf_target_file}" "${OPENSBI_PLAYLOAD}" COMMAND make -C "${OPENSBI_PATH}" O="${OPENSBI_BINARY_DIR}" - CROSS_COMPILE=${CROSS_COMPILER_PREFIX} PLATFORM="${KernelOpenSBIPlatform}" + CROSS_COMPILE=${CROSS_COMPILER_PREFIX} PLATFORM="cartesi" PLATFORM_RISCV_XLEN=${KernelWordSize} FW_PAYLOAD_PATH="${OPENSBI_PLAYLOAD}" PLATFORM_RISCV_ISA=${PLATFORM_RISCV_ISA} PLATFORM_RISCV_ABI=${PLATFORM_RISCV_ABI} ```

https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles ``` diff --git a/dockerfiles/extras.Dockerfile b/dockerfiles/extras.Dockerfile index 4c0a052..9f025f5 100644 --- a/dockerfiles/extras.Dockerfile +++ b/dockerfiles/extras.Dockerfile @@ -18,6 +18,8 @@ FROM $USER_BASE_IMG # hadolint ignore=DL3008,DL3009 RUN apt-get update -q \ && apt-get install -y --no-install-recommends \ - # Add more dependencies here + flex \ + bison \ + libpixman-1-dev \ cowsay \ sudo diff --git a/dockerfiles/riscv.Dockerfile b/dockerfiles/riscv.Dockerfile index 44a3dbb..8e8ee3e 100644 --- a/dockerfiles/riscv.Dockerfile +++ b/dockerfiles/riscv.Dockerfile @@ -41,7 +41,7 @@ RUN cd qemu \ # Setup qemu targets RUN sed -i 's/--target-list=riscv64-linux-user,riscv32-linux-user/--target-list=riscv64-softmmu,riscv32-softmmu/g' ./Makefile.in

-RUN ./configure --prefix=$RISCV --enable-multilib \ +RUN ./configure --prefix=$RISCV --with-arch=rv64ima --with-abi=lp64 --enable-multilib \ && make linux \ && make build-qemu ```

On Thu, Aug 26, 2021 at 8:57 PM Kent Mcleod wrote:

...

Currently the kernel and build system only builds for the following RISC-V ISA combinations: rv64imafdc, rv64imac and rv32imac. If you want rv64ima then for now you would need to go through the CMake files and update the settings manually. Searching the tree for "rv64imafdc" should find the places where they're set. You will at least need to make a change in kernel/CMakeLists.txt and in tools/sel4/cmake-tool/helpers/rootserver.cmake but there may be other locations too.

On Fri, Aug 27, 2021 at 4:25 AM Marcelo Politzer via Devel wrote:

...

Found out the problem.

The initialization code is using the compression extension (it

shouldn't)

...

...

for this platform.

best, Marcelo

On Wed, Aug 25, 2021 at 2:46 PM Marcelo Politzer < marcelo.politzer@cartesi.io> wrote:

...

Thanks for the timely reply.

I swapped the application to a hello-world[1] to simplify debugging. Addresses have changed a little (faulting address is now: 0x101d0). `user exception 0x2 code 0 in thread 0xffffffc17fec8200 "rootserver" at address 0x101d0`[2]. Its address resolves to frame_dummy seems to be some gcc specific initialization code (that shouldn't run?)

Since it mentioned registers, I also checked the usage of float (unsupported in this CPU) but that's likely not it (build has emitted soft float functions).

[1] ```

#include

int main() { printf("hello world\n"); return 0; }

```

[2] ``` (gdb) disas 0x101d0 Dump of assembler code for function frame_dummy: 0x00000000000101d0 <+0>: j 0x10182 0x00000000000101d2 <+2>: unimp ```

On Wed, Aug 25, 2021 at 12:59 PM Axel Heider wrote:

...

Marcelo,

> I have a suspicion that the unsupported PMP may have something to do > with this but since I'm still pretty new to seL4 so I would like > advice on how to debug this further.

It can't be the PMP because seL4 starts in S-Mode. What code does

b/cmake-tool/helpers/rootserver.cmake the

...

...

...

...

...

sel4 root task have at the faulting address 0x101f0?

Axel

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems