sel4 build broken in 20.05?

Alexander Boettcher alexander.boettcher at genode-labs.com
Tue Aug 4 09:37:41 CEST 2020 

Hello,

On 04.08.20 01:54, Alexander Tormasov via users wrote:
> I am trying to compile sel4 demo for x86, and hit an error:
> during compilation of  [CC] kernel_final.s
> in the process which give
> /usr/local/genode/tool/current/bin/genode-x86-gcc  -S -o kernel_final.s kernel_final.c
> 
> it generates asm error
>  error: impossible constraint in ‘asm’!
> 
> Any suggestions?

according to our CI infrastructure and my manual try to build it, no it seems not to be broken.


You should check that you use the right genode-gcc version, e.g. what does
/usr/local/genode/tool/current/bin/genode-x86-gcc --version
tell you ?
Do you use the prebuilt toolchain as provided by Genode or do you have built it by your own ? In principle it should not matter.
Do you have any other changes, e.g. to the Genode build system or to the contrib sources of seL4 ?
When you use VERBOSE= during building, is indeed the genode-gcc toolchain taken, e.g.:

TOOLPREFIX=/usr/local/genode/tool/19.05/bin/genode-x86-


I attached as reference below the compilation of sel4 x86_32/x86_64 kernel with VERBOSE=.

alex at tmp:~/genode$ /usr/local/genode/tool/current/bin/genode-x86-gcc --version
genode-x86-gcc (GCC) 8.3.0
Copyright (C) 2018 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

alex at tmp:~/genode$ git clone git://github.com/genodelabs/genode.git tmp
Cloning into 'tmp'...
remote: Enumerating objects: 196, done.
remote: Counting objects: 100% (196/196), done.
remote: Compressing objects: 100% (139/139), done.
remote: Total 195911 (delta 97), reused 104 (delta 57), pack-reused 195715
Receiving objects: 100% (195911/195911), 47.22 MiB | 10.65 MiB/s, done.
Resolving deltas: 100% (106926/106926), done.

alex at tmp:~/genod$ cd tmp

alex at tmp:~/genode/tmp$ git checkout 20.05
HEAD is now at 5b87f68900 version: 20.05

alex at tmp:~/genode/tmp$ tool/ports/current sel4
/home/alex/genode/tmp/contrib/sel4-7935487f91a31c0cd8aaf09278f6312af56bb935

alex at tmp:~/genode/tmp$ tool/create_builddir x86_64
Successfully created build directory at /home/alex/genode/tmp/build/x86_64.
Please adjust /home/alex/genode/tmp/build/x86_64/etc/build.conf according to your needs.

alex at tmp:~/genode/tmp$ make -C build/x86_64 KERNEL=sel4 kernel
make: Entering directory '/home/alex/genode/tmp/build/x86_64'
checking library dependencies...

Error: Ports not prepared or outdated:
  sel4

You can prepare respectively update them as follows:
  /home/alex/genode/tmp/tool/ports/prepare_port sel4

var/libdeps:60: recipe for target 'check_ports' failed
make[1]: *** [check_ports] Error 1
Makefile:295: recipe for target 'gen_deps_and_build_targets' failed
make: *** [gen_deps_and_build_targets] Error 2
make: Leaving directory '/home/alex/genode/tmp/build/x86_64'

alex at tmp:~/genode/tmp$ tool/ports/prepare_port sel4
sel4  download https://github.com/seL4/seL4.git
sel4  git Cloning into 'src/kernel/sel4'...
sel4  update src/kernel/sel4
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/arm_cache.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/autoconf_32.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/autoconf_64.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/config.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/intel_efer.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/intel_ug.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/intel_vmcs.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/intel_vmx_disable_vpid.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/intel_vmx_full_state.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/intel_vtx_check.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/ioapic.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/noise.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/sched_bug_x86.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/sel4_tlb_x86_bug.patch
sel4  apply /home/alex/genode/tmp/repos/base-sel4/patches/vcpu_nullptr_bug.patch
sel4  generate sel4.hash
patching file src/kernel/sel4/configs/imx6/imx6q_sabrelite/autoconf.h
patching file src/kernel/sel4/configs/imx7/imx7d_sabre/autoconf.h

alex at tmp:~/genode/tmp$ make -C build/x86_64 KERNEL=sel4 kernel VERBOSE=
make: Entering directory '/home/alex/genode/tmp/build/x86_64'
make \
          TOOLPREFIX=/usr/local/genode/tool/19.05/bin/genode-x86- \
          BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 \
          SOURCE_ROOT=/home/alex/genode/tmp/contrib/sel4-7935487f91a31c0cd8aaf09278f6312af56bb935/src/kernel/sel4 -f/home/alex/genode/tmp/contrib/sel4-7935487f91a31c0cd8aaf09278f6312af56bb935/src/kernel/sel4/Makefile
checking library dependencies...
 [MKDIR] arch/object
 [PBF_GEN] arch/object/structures.pbf
 [PBF_GEN] plat/64/plat_mode/machine/hardware.pbf
 [PBF_GEN] 64/mode/api/shared_types.pbf
 [BF_GEN] arch/object/structures_gen.h
 [BF_GEN] plat/64/plat_mode/machine/hardware_gen.h
 [BF_GEN] 64/mode/api/shared_types_gen.h
 [CPP] src/arch/x86/64/machine_asm.s_pp
 [AS] src/arch/x86/64/machine_asm.o
 [CPP] src/arch/x86/64/traps.s_pp
 [AS] src/arch/x86/64/traps.o
 [CPP] src/arch/x86/64/head.s_pp
 [AS] src/arch/x86/64/head.o
 [CPP] src/arch/x86/multiboot.s_pp
 [AS] src/arch/x86/multiboot.o
 [TOUCH] sources_list_updated
 [CPP_GEN] kernel_all.c
 [CPP] kernel_all.c_pp
 [Circular includes] kernel_all.c_pp
 [CP] kernel_final.c
 [CC] kernel_final.s
 [AS] kernel.o
# Clear any .arch directive from the .s file in case we are assembling
# for a different architecture. This happens when the compiler supports
# a subset architecture compared to the assembler. For example where the
# compiler only supports armv7-a, where the assembler supports armv7ve
 [CPP] linker.lds_pp
 [LD] kernel.elf
 [STRIP] kernel.elf.strip
rm src/arch/x86/multiboot.s_pp plat/64/plat_mode/machine/hardware_gen.h arch/object/structures_gen.h src/arch/x86/64/machine_asm.s_pp src/arch/x86/64/head.s_pp 64/mode/api/shared_types_gen.h src/arch/x86/64/traps.s_pp
  Library kernel-sel4-pc
    MERGE    kernel-sel4-pc.lib.a
  Program kernel/sel4/sel4-pc
make: Leaving directory '/home/alex/genode/tmp/build/x86_64'

alex at tmp:~/genode/tmp$ tool/create_builddir x86_32
Successfully created build directory at /home/alex/genode/tmp/build/x86_32.
Please adjust /home/alex/genode/tmp/build/x86_32/etc/build.conf according to your needs.

alex at tmp:~/genode/tmp$ make -C build/x86_32 KERNEL=sel4 kernel VERBOSE=
make: Entering directory '/home/alex/genode/tmp/build/x86_32'
mkdir -p /home/alex/genode/tmp/build/x86_32/bin
mkdir -p /home/alex/genode/tmp/build/x86_32/debug
checking library dependencies...
make \
          TOOLPREFIX=/usr/local/genode/tool/19.05/bin/genode-x86- \
          BOARD=ia32 ARCH=x86 SEL4_ARCH=ia32 PLAT=pc99 DEBUG=1 \
          SOURCE_ROOT=/home/alex/genode/tmp/contrib/sel4-7935487f91a31c0cd8aaf09278f6312af56bb935/src/kernel/sel4 -f/home/alex/genode/tmp/contrib/sel4-7935487f91a31c0cd8aaf09278f6312af56bb935/src/kernel/sel4/Makefile
 [MKDIR] arch/object
 [PBF_GEN] arch/object/structures.pbf
 [PBF_GEN] plat/32/plat_mode/machine/hardware.pbf
 [PBF_GEN] 32/mode/api/shared_types.pbf
 [BF_GEN] arch/object/structures_gen.h
 [BF_GEN] plat/32/plat_mode/machine/hardware_gen.h
 [BF_GEN] 32/mode/api/shared_types_gen.h
 [CPP] src/arch/x86/32/machine_asm.s_pp
 [AS] src/arch/x86/32/machine_asm.o
 [CPP] src/arch/x86/32/traps.s_pp
 [AS] src/arch/x86/32/traps.o
 [CPP] src/arch/x86/32/head.s_pp
 [AS] src/arch/x86/32/head.o
 [CPP] src/arch/x86/multiboot.s_pp
 [AS] src/arch/x86/multiboot.o
 [TOUCH] sources_list_updated
 [CPP_GEN] kernel_all.c
 [CPP] kernel_all.c_pp
 [Circular includes] kernel_all.c_pp
 [CP] kernel_final.c
 [CC] kernel_final.s
 [AS] kernel.o
# Clear any .arch directive from the .s file in case we are assembling
# for a different architecture. This happens when the compiler supports
# a subset architecture compared to the assembler. For example where the
# compiler only supports armv7-a, where the assembler supports armv7ve
 [CPP] linker.lds_pp
 [LD] kernel.elf
 [STRIP] kernel.elf.strip
rm src/arch/x86/multiboot.s_pp src/arch/x86/32/traps.s_pp src/arch/x86/32/head.s_pp arch/object/structures_gen.h 32/mode/api/shared_types_gen.h src/arch/x86/32/machine_asm.s_pp plat/32/plat_mode/machine/hardware_gen.h
  Library kernel-sel4-pc
    MERGE    kernel-sel4-pc.lib.a
  Program kernel/sel4/sel4-pc
make: Leaving directory '/home/alex/genode/tmp/build/x86_32'
alex at tmp:~/genode/tmp$ 


alex at tmp:~/genode/tmp$ tool/depot/create genodelabs/bin/x86_32/base-sel4-x86
...
created genodelabs/bin/x86_32/base-sel4-x86/2020-05-26

alex at tmp:~/genode/tmp$ tool/depot/create genodelabs/bin/x86_64/base-sel4-x86
...
created genodelabs/bin/x86_32/base-sel4-x86/2020-05-26


-- 
Alexander Boettcher
Genode Labs

https://www.genode-labs.com - https://www.genode.org

Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

More information about the users mailing list