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

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 the GCC compilation stages, to try that out 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 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 b/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 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