sel4 and compilation with/without optimisation

Alexander Tormasov a.tormasov at
Sun Jan 2 21:01:09 CET 2022

found «interesting» problem with compilation of genode:
compilation of sel4 failed due to optimisation flag.

I already reported this around 2 years ago [3]

in short, during compilation of sel4 library in the 
it generates «on the fly» file kernel_final.c which should generate kernel_final.s file.

what’s happens:
 kernel_final.c do contains something similar to below (take a look to x86_flush_rsb() in original code [2], simplify here):

typedef unsigned long word_t;
static inline void x86_flush_rsb(void)

    word_t iter = 32;
    __asm__ volatile(
        : [iter]"+r"(iter)
        : [stack_amount]"i"(sizeof(word_t) * iter)
        : "cc"


    if (1) {

code like this works perfectly ok
genode-x86-gcc -S  -O1  -o kernel_final.s t.c

while code
genode-x86-gcc -S  -o kernel_final.s t.c
genode-x86-gcc -S  -O0 -o kernel_final.s t.c
does not!
t.c: In function ‘x86_flush_rsb’:
t.c:7:5: warning: ‘asm’ operand 1 probably does not match constraints
    7 |     __asm__ volatile(
      |     ^~~~~~~
t.c:7:5: error: impossible constraint in ‘asm’

What’s happens:
asm code inside function do have this kind of input parameters
        : [stack_amount]"i"(sizeof(word_t) * iter)
IMHO (I am not sure for 100%) «i» mean immediate constant which
should be known in advance while «iter» above is a variable updated in output!
as stated in [1]:
 ‘i’ An immediate integer operand (one with constant value) is allowed. 
This includes symbolic constants whose values will be known only at assembly time or later.

Gcc with any optimisation level do drop this code because original function which 
call x86_flush_rsb (c_handle_vmexit) does not used at all and being removed 
during optimisation.

So, if you during debug add something like CFLAGS= as an env or make variable with -O0 - you are doomed!

this is true for current 10.3 and previous 9 gcc compilers…
This is not a part of genode code while problem happens in port sources [2]. I am not even sure how I can post an issue.

[2] contrib/sel4-9ab19376285d865052c2b5021560306306bf19a8/src/kernel/sel4/include/arch/x86/arch/machine.h


More information about the users mailing list