Re: sel4 build broken in 20.05?

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@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@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@tmp:~/genod$ cd tmp

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

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

alex@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@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@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@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@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@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@tmp:~/genode/tmp$

alex@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@tmp:~/genode/tmp$ tool/depot/create genodelabs/bin/x86_64/base-sel4-x86 ... created genodelabs/bin/x86_32/base-sel4-x86/2020-05-26