sel4 / sel4_tools

Basic tools for building seL4 projects

seL4_tools

Provides tools used to build seL4 projects. Also collects common config and tools for style checks.

• elfloader-tool: loads the arm kernel.
• cmake-tool: most of the build system.
• misc: miscellaneous extra tools, including code style checks.

Contributing

Contributions welcome!

See the CONTRIBUTING file for more.

sel4_tools's Issues

elf loader does not parse device tree passend on startup

Follow-up from

• seL4/seL4#373
• seL4/seL4#365 (comment)
• #103

There is no plan that the kerne will ever get device tree parsing support, as this is a huge effort for verification. A way to improve the situation is extending the ELF loader support for device tree parsing instead. Since it is usually created with the kernel, it has a certain understanding of the kernel's world-view and expectations. It can do some sanity checks easily before trying to load the kernel into memory regions that are not available of where booting will fails badly later anyway. If a device tree binary blob is compiled into the ELF Loder and a DTB is also passed by a bootloader, the ELF-Loader should try to match them and stop the boot process if there are serious differences. One example for such a sanity check is the the available memory areas on RISC-V, where OpenSBI carves out space for itself dynamically, where the ELF loader's compiled-in DTB contains a reserved area for this that is maintained manually.

build error for picoserver: pico_stack.h not found

When I try to build picoserver like this:

../init-build.sh -DPLATFORM=pc99 \
    -DCAMKES_APP=picoserver \
    -DPICOSERVER_IP_ADDR=10.0.2.15 \
    -DKernelExportPMCUser=ON

There is a build error:

projects/global-components/components/modules/picotcp-base/picotcp-init.c:14:10: \
fatal error: pico_stack.h: No such file or directory
 #include <pico_stack.h>
          ^~~~~~~~~~~~~~
compilation terminated.

This can be fixed by running init-bulid.sh for a second time; or, by adding another option to init-build.sh:

-DLibPicotcp=ON

It is unfortunate, because in picoserver's CMakeLists.txt, there's this line:

set(LibPicotcp ON CACHE BOOL "" FORCE)

but it's only evaluated after projects/util_libs/libpicotcp/CMakeLists.txt has used this option (typical error of variable used before being initialized).

set OpenSBI dependencies right

Follow-up from #117 concerning file(GLOB_RECURSE deps)

From @kent-mcleod: It looks like it's missing the other parts of it's implementation, actually specifying the path to the opensbi sources and then adding the sources to the depends line of add_custom_command. If you wanted to add a commit to this PR adding ${BBL_PATH} to the end of that statement, and also adding the deps arg to the ${CMAKE_BINARY_DIR}/bbl/bbl custom command [...]. Alternatively you could ignore it, or remove it if you think it's better to assume that the opensbi implementation isn't going to be edited by anyone between builds.

Cannot generate opensbi/platform/generic/firmware/fw_payload.elf

I'm trying to run sel4test on plat qemu-riscv-virt with commands:

mkdir build-riscv
cd build-riscv
../init-build.sh -DRISCV64=1 -DSIMULATION=TRUE -DPLATFORM=qemu-riscv-virt
ninja

The log shows the error:

Error: unrecognized opcode `fence.i', extension `zifencei' required

I find that the command generated in build.ninja builds opensbi with PLATFORM_RISCV_ISA=rv64imafdc PLATFORM_RISCV_ABI=lp64d. This env is generated by this line:

if(NOT OPENSBI_PLAT_ISA)
    set(OPENSBI_PLAT_ISA "rv${OPENSBI_PLAT_XLEN}imafdc")
endif()

Should it be set(OPENSBI_PLAT_ISA "rv${OPENSBI_PLAT_XLEN}imafdc_zifencei") instead?

make menuconfig does not detect ncurses correctly

make menuconfig will fail with an undefined symbol error if the system's ncurses was built with the --with-termlib option.

This was fixed in Linux in 3.10.rc1: torvalds/linux@fc9c6e0

ElfLoader CPU-ID display is incorrect

The function print_cpuid decodes the CPUID_PART using the following logic:

    if ((CPUID_PART(cpuid) & 0xf00) == 0xC00) {
        printf("Cortex-A%d ", CPUID_PART(cpuid) & 0xff);
    } else if ((CPUID_PART(cpuid) & 0xf00) == 0xD00) {
        printf("Cortex-A5%d ", CPUID_PART(cpuid) & 0xff);
    } else {
        printf("Part: 0x%03x ", CPUID_PART(cpuid));

The logic is incorrect for at least the Cortex A35. It has a part id of 0xD04. The current logic incorrectly reports this as Cortex-A54.

I think the only robust approach is to explicitly list the part identifies. A potential implementation is:

    switch (CPUID_PART(cpuid)) {
        case 0xD04:
            printf("Cortex-A35 ");
            break;
        default:
            printf("Part: 0x%03x ", CPUID_PART(cpuid));
     }

This is a partial regression though as there are probably other Cortex parts that the current logic happens to print correctly.

Ideally there would be a full list. I only have a Cortex A35 to test on.

ElfLoader should use monitor.S only if CONFIG_ARM_MONITOR_HOOK is set

The file monitor.S should only be compiled in (or it's content take into account), when CONFIG_ARM_MONITOR_HOOK is set. Otherwise the content should be ignored, so any accidental referenced make the build fail.

We ran into this issue when adding a new imx6 board platform, where we had to define something there to VECTOR_BASE even if this is not used anywhere because CONFIG_ARM_MONITOR_HOOK is not supported there.

elfloader-tool: MAIR attributes for aarch64 (question)

Does anyone remember why aarch64 code doesn't define memory region "type": "Normal memory, cacheable, write-through" in MAIR_EL1 ?

Memory refresher - this is what we have now:

/*
 * Memory types are defined in Memory Attribute Indirection Register.
 *  - nGnRnE Device non-Gathering, non-Reordering, No Early write acknowledgement
 *  - nGnRE Unused Device non-Gathering, non-Reordering, Early write acknowledgement
 *  - GRE Unused Device Gathering, Reordering, Early write acknowledgement
 *  - NORMAL_NC Normal Memory, Inner/Outer non-cacheable
 *  - NORMAL Normal Memory, Inner/Outer Write-back non-transient, Write-allocate, Read-allocate
 * Note: These should match with contents of MAIR_EL1 register!
 */
enum mair_types {
    DEVICE_nGnRnE = 0,
    DEVICE_nGnRE = 1,
    DEVICE_GRE = 2,
    NORMAL_NC = 3,
    NORMAL = 4
};

Elfloader crashes on ARMv7 platforms with external L2 Cache controller

The Elfloader doesn't currently implement any L2 cache flushing operations for ARMv7 platforms where the architectural flushing operations don't also flush external caches such as the PL310. This means that on platforms with an external cache controller if the previous bootloader has enabled caches and starts the Elfloader with them enabled, the Elfloader will crash when trying to enable the MMU.

The Elfloader assumes that when it is loaded and started that caches are already disabled which seemed to be generally true for older u-boot versions. Newer U-Boot versions tend to enable the caches and only disable them when loading a uImage that declares itself as a Linux kernel via bootm. In order to use alternative image file formats such as ELF, Raw binary or EFI, first the L2 Cache must be flushed and disabled before starting the elfloader if it was previously enabled.

Ideally the elfloader should be able to handle the case where it is started with caches enabled and be able to flush external caches when disabling them.

See seL4/seL4#631 for more context.

Use ENABLE_SMP_SUPPORT define

Follow-up from #95 (comment)

Since the kernel's one private config header are public now (see https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/config.h#L96), the define ENABLE_SMP_SUPPORT can be used in the ELF-Loder code also instead of checking CONFIG_MAX_NUM_NODES > 1. So we could replace this everywhere to align the code.

Bad hack to work around a CMake bug

As a result of #77, one of the issues preventing CI was fixed. However, this isn't an ideal solution and merely masks the error. It would be a good idea to go deeper and figure out what's going on that's causing CMake to omit the a platform_sift.py call.

macOS shell touch binary implement not support "@0" alias

Hi:
When I use macOS to build the seL4 project, will meet an error about touch

touch: out of range or illegal time specification: YYYY-MM-DDThh:mm:SS[.frac][tz]
[251/263] Building C object kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj

issue command is

 touch -d @0 `basename ${file}`

seL4_tools/cmake-tool/helpers/cpio.cmake

Line 51 in 6211394

"bash;-c;cpio ${cpio_reproducible_flag} --quiet --create -H newc --file=${CMAKE_CURRENT_BINARY_DIR}/archive.${output_name}.cpio;&&"

information of "@0"
https://unix.stackexchange.com/questions/154387/meaning-of-0-in-a-shell-script

macOS touch help

   -d      Change the access and modification times to the specified date time instead of the current time of day.  The argument is of the form
             “YYYY-MM-DDThh:mm:SS[.frac][tz]” where the letters represent the following:
                   YYYY    At least four decimal digits representing the year.
                   MM, DD, hh, mm, SS
                           As with -t time.
                   T       The letter T or a space is the time designator.
                   .frac   An optional fraction, consisting of a period or a comma followed by one or more digits.  The number of significant digits depends on
                           the kernel configuration and the filesystem, and may be zero.
                   tz      An optional letter Z indicating the time is in UTC.  Otherwise, the time is assumed to be in local time.  Local time is affected by
                           the value of the TZ environment variable.

There have some differences with GNU touch, so this command will error on macOS.

Thanks~

Add Arm spin-table SMP support

The raspberry pi 4b module uses spin table as SMP boot method which is not supported yet.
I find that there is a PR #153 to add the support but it seems to be already inactive.

elfloader: issues with Arm's linker script

The shared Arm's linker script includes some sections and directive that might not be necessary. For example, .interp and .hash here:

SECTIONS { .interp : { *(.interp) } } INSERT BEFORE .hash;

What's the reason this section exists in the elfloader, and why the INSERT BEFORE .hash? I am able to remove them and ELF linking works just fine. However, when building with LLVM/lld, they trigger a linking error as .hash and .interp don't exist.

aarch64-none-elf-ld.lld: error: unable to insert .interp before .hash aarch64-none-elf-ld.lld: error: unable to insert ._archive_cpio after .eh_frame

Similarly, INSERT AFTER .eh_frame;

I do have local fixes that remove them, I'd be happy to submit a PR if there's no good reason those sections/directives exist.

RISC-V linker issues for 32-bit simulation

As a result from #75, we discovered that having a contiguous blob of code + ro-data presents some problems for 32-bit RISC-V simulation on QEMU. The simulation in question manages to start up the elfloader only for it to freeze up near the beginning when it's printing information about the HART that it is running on.

IMAGE_START_ADDR vs actual start address on RISC-V

I am trying to understand some of the code for the ELF loader on RISC-V. I've come across an autogenerated define called IMAGE_START_ADDR. On the Spike platform for example (looking at the build for sel4test), this becomes 0x80a0c000. This define is then used in the linker script as the address of the _text section. However, since seL4 uses OpenSBI with FW_PAYLOAD, my understanding is that it will start the payload (in this case the ELF loader) at 0x8020000. This is confirmed by the following output using sel4test:

ELF-loader started on (HART 0) (NODES 1)
    paddr=[8020000...806a4037]

So if the IMAGE_START_ADDR is different to the actual address the image is started at, why are there no issues with the ELF loader? I'm sure I'm just misunderstanding something, so if anyone could point it out that would be great.

Thanks.

Core ID strings are only valid for CPUID_IMPL_ARM

Follow-up from #107 fixing #43
All the CoreID-to-String translation is only valid if CPUID_IMPL(cpuid) == CPUID_IMPL_ARM, otherwise we should just print the raw value.

asm code calls clear_bss without a valid stack pointer

In #82 we call clear_bss from asm code now when CONFIG_IMAGE_BINARY is enabled - but there is no stack set up. This is a bit dangerous, since C code always assumes there is stack. It may work if the function is simple enough so C does not create a stack frame.

RISC-V assembly startup code looks broken

RISC-V assembly startup code at

seL4_tools/elfloader-tool/src/arch-riscv/crt0.S

Line 52 in 53d5db6

blt x1, s1, _start1

looks broken, I can't figure out why we use x1 here. @wom-bat or @oliver-wm, could you clarify this? @yyshen any idea? This came in with #68

Make ElfLoader object usage the default build

This is a follow-up from #175 by
@kent-mcleod. Make the ElfLoader object usage the default build process and provide an option to use the old way as fall-back for users running into issues with that. That gets the new way, which is more flexible, a proper (implicit) test coverage them also.

elfloader, Arm: Issues with clearing .bss and stack regions during early init

The elfloader calls clear_bss early in its init process to zero the .bss section under some configurations to handle situations where the loader didn't zero any uninitialized memory. Because the elfloader's stack is declared in the .bss section this means that with correct operation of clear_bss the stack would be cleared in the middle. Consequences of this are crashing under high optimization levels (because under low optimization the stack doesn't get used in clear_bss) and erasing an arguments provided to the elfloader by an earlier stage that are stored on the stack.

This would have been detected much earlier if not for a separate issue involving the linker script:

    .bss : {
        _bss = .;
        *(.bss)
        _bss_end = .;
    }

This script means that zeroing from _bss to _bss_end will zero any symbol that had been matched by *(.bss). Before gcc-10, any global variables that are declared but uninitialized would be instead placed in the COMMON section until the final link stage. Because the linker script above is missing *(COMMON), any of these symbols would end up after _bss_end. This includes the stack and essentially every other global variable that would be in .bss in the elfloader.

With gcc-10 changing to default -fno-common, these variables stop being excluded from clear_bss however this means that now the stack gets zeroed while the stack is being used.

Fixing this should resolve a few stability issues found when using configurations that call clear_bss:

• CONFIG_IMAGE_BINARY on aarch64
• CONFIG_IMAGE_ELF, CONFIG_IMAGE_BINARY, CONFIG_IMAGE_UIMAGE on aarch32

print_cpuid display incorrect data for at least Cortex-A35

The function print_cpuid incorrectly calculates the CPU name associated with the part number.

The current code is:

    if ((CPUID_PART(cpuid) & 0xf00) == 0xC00) {
        printf("Cortex-A%d ", CPUID_PART(cpuid) & 0xff);
    } else if ((CPUID_PART(cpuid) & 0xf00) == 0xD00) {
        printf("Cortex-A5%d ", CPUID_PART(cpuid) & 0xff);
    } else {
        printf("Part: 0x%03x ", CPUID_PART(cpuid));

However, the Cortex-A35 part is 0xD04. The current logic prints that as Cortex-A54, which is obviously wrong.

I think the assumptions made in this printing is just incorrect. A switch-based look up table is probably most appropriate. Something like:

    switch (CPUID_PART(cpuid)) {
       case 0xD04:
           printf("Cortex-A35 ");
            break;
        default:
            printf("Part: 0x%03x ", CPUID_PART(cpuid));
     }

But, obviously, with additional switch statements for other, supported, CPUs.

Using -DKERNEL_PATH=<path/to/kernel> does not work

The find_file command on line 32 in cmake-tool/base.cmake searches explicitly for a directory named "kernel" and the result is stored in KERNEL_PATH. Renaming the kernel directory as stated in Incorporating into your project and defining KERNEL_PATH with the -D option will result in a bogus value for KERNEL_PATH resulting in cmake failing on line 40 (add_subdirectory). Also, the add_subdirectory command itself forces a fixed binary directory named "kernel", which seems unnecessary.

delete merged and stale branches

While I'm on it, here are a few more branches that look obsolete:

• already merged
  • gklein/github-ci
  • kent/fpu
• potentially stale branches to be considered for deletion
  • lsf37-patch-1
  • nomadeel/use-kernel-dtb
  • alyons-pr

Default branch for this repo is 2.0.x-compatible

Some punters might find that… confusing.

Setting `UseRiscVOpenSBI` has no affect

For example, running the following with seL4test:

../init-build.sh -DPLATFORM=hifive -DUseRiscVOpenSBI=OFF still produces an image with OpenSBI. The option is defined in rootserver.cmake with cmake_dependent_option. The CMake documentation (https://cmake.org/cmake/help/latest/module/CMakeDependentOption.html) says that the option should be available to the user, although I don't know what their definition of user is.

style-cmake.sh should not reset file mode

style-cmake.sh resets the file mode, using cmake-format with -i which always produces 644 files.

It'd be nice to keep the original file mode, since we have some cmake files that are intentionally 755.

This could be achieved in style-cmake.sh by processing files one by one, using stat to read the mode, then chmod to set it afterwards, or some such thing. Downside is that this probably will make it quite hard to deal with file names that have spaces in them.

Alternatively, we could do something similar in python inside style.py.

print_cpuid assumes implementer is ARM

The decoding of CPUID_PART(...) assumes that the implementer is ARM. The part namespace is implementer specific; the code should be updated to reflect this.

Note: This was identified in #107 and could be addressed there, however I think it is cleaner to have separate PRs for each issue.

On a risc-v build, the second argument received from OpenSBI seems to be getting clobbered

The value of bootloader_dtb in main, arch-riscv/boot.c:290 does not correspond to the arg1 from OpenSBI.
The patch below seems to fix the problem.

NOTE: tested with -DElfloaderIncludeDtb=OFF

diff --git a/elfloader-tool/src/arch-riscv/crt0.S b/elfloader-tool/src/arch-riscv/crt0.S
index 40ab09e..28a218c 100644
--- a/elfloader-tool/src/arch-riscv/crt0.S
+++ b/elfloader-tool/src/arch-riscv/crt0.S
@@ -32,6 +32,7 @@ _start:
 
 /* a0 should have hart id, store it in s0 so as not to clobber from HSM calls */
   mv s0, a0
+  mv s2, a1
 
 #ifdef CONFIG_IMAGE_BINARY
 /* Clear the BSS before we get to do anything more specific */
@@ -83,6 +84,7 @@ _start1:
 
   la sp, (elfloader_stack_alloc + BIT(12))
 
+  mv a1, s2
   la s0, main
   jr s0