Incorporating seL4 into your project, risc-v architecture
Dear seL4 devs and community.
I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0). I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this:
CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command):
Error evaluating generator expression:
$
On Fri, Dec 3, 2021 at 8:14 AM
Dear seL4 devs and community.
I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0). I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): Error evaluating generator expression:
$
Target "rootserver_image" not found. Call Stack (most recent call first): CMakeLists.txt:22 (GenerateSimulateScript) While going through Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. Project/ ├── kernel/ ├── projects/ │ ├── Hello/ │ ├── musllibc/ │ ├── utils_libs/ │ ├── seL4_libs/ ├── build/ ├── tools/ │ └── cmake-tool/ │ └── elfloader-tool/ ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── CMakeLists.txt ├── application_settings.cmake -> tools/cmake-tool/helpers/application_settings.cmake ├── settings.cmake
So I cannot tell where the issue lies. Any pointers would be appreciated.
If you are using https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt inside projects/Hello/ then you need to make sure that the top level CMakeLists inside Project/ is either a symlink to tools/cmake-tool/default-CMakeLists.txt or is similar to https://github.com/manu88/SeL4_101/blob/master/CMakeLists.txt. With this file layout, ../init-build.sh will end up calling the following CMake invocation: `cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DSEL4_CACHE_DIR=../.sel4_cache -C "../settings.cmake" "../"`. What is the contents of your settings.cmake file?
Kind regards, Sophia _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hello Kent, Thank you for your answer. And thank you for the point about the CMakeList.txt files. That was the thing I messed up. Bellow you can find the contents of my settings.cmake file: include_guard(GLOBAL) set(project_dir "${CMAKE_CURRENT_LIST_DIR}/../../") file(GLOB project_modules ${project_dir}/projects/*) list( APPEND CMAKE_MODULE_PATH ${project_dir}/kernel ${project_dir}/tools/cmake-tool/helpers/ ${project_dir}/tools/elfloader-tool/ ${project_modules} ) include(/host/application_settings.cmake) set(KernelArch "riscv") set(KernelPlatform "spike") set(KernelSel4Arch "riscv") include(/host/kernel/configs/seL4Config.cmake) set(CapDLLoaderMaxObjects 20000 CACHE STRING "" FORCE) set(KernelRootCNodeSizeBits 16 CACHE STRING "") # For the tutorials that do initialize the plat support serial printing they still # just want to use the kernel debug putchar if it exists set(LibSel4PlatSupportUseDebugPutChar true CACHE BOOL "" FORCE) # Just let the regular abort spin without calling DebugHalt to prevent needless # confusing output from the kernel for a tutorial set(LibSel4MuslcSysDebugHalt FALSE CACHE BOOL "" FORCE) # Only configure a single domain for the domain scheduler set(KernelNumDomains 1 CACHE STRING "" FORCE) # We must build the debug kernel because the tutorials rely on seL4_DebugPutChar # and they don't initialize a platsupport driver. ApplyCommonReleaseVerificationSettings(FALSE FALSE) # We will attempt to generate a simulation script, so try and generate a simulation # compatible configuration ApplyCommonSimulationSettings(${KernelSel4Arch}) if(FORCE_IOMMU) set(KernelIOMMU ON CACHE BOOL "" FORCE) endif() Kind regards, Sophia
On Wed, Dec 8, 2021 at 8:58 AM
Hello Kent, Thank you for your answer. And thank you for the point about the CMakeList.txt files. That was the thing I messed up.
Ok. Glad you got it working. It looks like your settings file originally came from an older version of the one in sel4-tutorials (https://github.com/seL4/sel4-tutorials/blob/master/settings.cmake) The options that come after `include(/host/kernel/configs/seL4Config.cmake)` aren't critical for your hello application and are mostly sel4-tutorial specific so should be safe to remove if you're trying to get down to a simple/minimal example.
Bellow you can find the contents of my settings.cmake file: include_guard(GLOBAL)
set(project_dir "${CMAKE_CURRENT_LIST_DIR}/../../") file(GLOB project_modules ${project_dir}/projects/*) list( APPEND CMAKE_MODULE_PATH ${project_dir}/kernel ${project_dir}/tools/cmake-tool/helpers/ ${project_dir}/tools/elfloader-tool/ ${project_modules} ) include(/host/application_settings.cmake)
set(KernelArch "riscv") set(KernelPlatform "spike") set(KernelSel4Arch "riscv")
include(/host/kernel/configs/seL4Config.cmake) set(CapDLLoaderMaxObjects 20000 CACHE STRING "" FORCE) set(KernelRootCNodeSizeBits 16 CACHE STRING "")
# For the tutorials that do initialize the plat support serial printing they still # just want to use the kernel debug putchar if it exists set(LibSel4PlatSupportUseDebugPutChar true CACHE BOOL "" FORCE)
# Just let the regular abort spin without calling DebugHalt to prevent needless # confusing output from the kernel for a tutorial set(LibSel4MuslcSysDebugHalt FALSE CACHE BOOL "" FORCE)
# Only configure a single domain for the domain scheduler set(KernelNumDomains 1 CACHE STRING "" FORCE)
# We must build the debug kernel because the tutorials rely on seL4_DebugPutChar # and they don't initialize a platsupport driver. ApplyCommonReleaseVerificationSettings(FALSE FALSE)
# We will attempt to generate a simulation script, so try and generate a simulation # compatible configuration ApplyCommonSimulationSettings(${KernelSel4Arch}) if(FORCE_IOMMU) set(KernelIOMMU ON CACHE BOOL "" FORCE) endif()
Kind regards, Sophia _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
participants (2)
-
Kent Mcleod -
so_s＠gmx.de