From af93f8d01ba2089f05c801d8b745dc4c3990682a Mon Sep 17 00:00:00 2001 From: Alexander Boettcher Date: Fri, 17 Jun 2016 15:15:48 +0200 Subject: [PATCH] sel4: update to 3.1.0 - adjust syscall bindings to support -fPIC - read serial i/o ports from BIOS data area - use autoconf.h provided by sel4 -- to avoid ambiguity between sel4 kernel and user libraries -- remove manual set defines - remove debug messages - increase user virtual area to 3GB Issue #1720 Issue #2044 --- repos/base-sel4/include/sel4/autoconf.h | 27 - repos/base-sel4/include/sel4/stdint.h | 28 - repos/base-sel4/lib/import/import-syscall.mk | 17 +- repos/base-sel4/lib/mk/spec/x86_32/kernel.mk | 3 +- .../base-sel4/lib/mk/spec/x86_32/platform.mk | 15 +- repos/base-sel4/patches/bda.patch | 31 + repos/base-sel4/patches/python.patch | 11 + repos/base-sel4/patches/syscall.patch | 560 ++++++++++++++++++ repos/base-sel4/ports/sel4.hash | 2 +- repos/base-sel4/ports/sel4.port | 6 +- repos/base-sel4/src/core/capability_space.cc | 2 +- .../src/core/include/initial_untyped_pool.h | 17 - .../src/core/include/kernel_object.h | 7 +- .../src/core/include/platform_thread.h | 2 +- .../src/core/include/untyped_memory.h | 2 +- repos/base-sel4/src/core/include/vm_space.h | 35 +- repos/base-sel4/src/core/platform.cc | 40 +- repos/base-sel4/src/core/platform_pd.cc | 9 +- repos/base-sel4/src/core/rpc_cap_factory.cc | 8 +- repos/base-sel4/src/lib/base/ipc.cc | 12 +- repos/base-sel4/src/lib/base/thread_sel4.cc | 52 -- tool/run/boot_dir/sel4 | 25 +- 22 files changed, 700 insertions(+), 211 deletions(-) delete mode 100644 repos/base-sel4/include/sel4/autoconf.h delete mode 100644 repos/base-sel4/include/sel4/stdint.h create mode 100644 repos/base-sel4/patches/bda.patch create mode 100644 repos/base-sel4/patches/python.patch create mode 100644 repos/base-sel4/patches/syscall.patch delete mode 100644 repos/base-sel4/src/lib/base/thread_sel4.cc diff --git a/repos/base-sel4/include/sel4/autoconf.h b/repos/base-sel4/include/sel4/autoconf.h deleted file mode 100644 index c8cb3069a..000000000 --- a/repos/base-sel4/include/sel4/autoconf.h +++ /dev/null @@ -1,27 +0,0 @@ -/* - * \brief Configuration values expected by seL4's kernel-interface headers - * \author Norman Feske - * \date 2014-10-15 - */ - -/* - * Copyright (C) 2014 Genode Labs GmbH - * - * This file is part of the Genode OS framework, which is distributed - * under the terms of the GNU General Public License version 2. - */ - -#ifndef _INCLUDE__SEL4__AUTOCONF_H_ -#define _INCLUDE__SEL4__AUTOCONF_H_ - -#define SEL4_DEBUG_KERNEL 1 - -#define DEBUG 1 - -#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 - -#define CONFIG_NUM_PRIORITIES 256 - -#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 - -#endif /* _INCLUDE__SEL4__AUTOCONF_H_ */ diff --git a/repos/base-sel4/include/sel4/stdint.h b/repos/base-sel4/include/sel4/stdint.h deleted file mode 100644 index efbc1b3d4..000000000 --- a/repos/base-sel4/include/sel4/stdint.h +++ /dev/null @@ -1,28 +0,0 @@ -/* - * \brief Basic type definitions expected by seL4's kernel-interface headers - * \author Norman Feske - * \date 2014-10-15 - */ - -/* - * Copyright (C) 2014 Genode Labs GmbH - * - * This file is part of the Genode OS framework, which is distributed - * under the terms of the GNU General Public License version 2. - */ - -#ifndef _INCLUDE__SEL4__STDINT_H_ -#define _INCLUDE__SEL4__STDINT_H_ - -#include - -typedef genode_uint8_t uint8_t; -typedef genode_uint16_t uint16_t; -typedef genode_uint32_t uint32_t; -typedef genode_uint64_t uint64_t; - -#ifndef NULL -#define NULL ((void *)0) -#endif - -#endif /* _INCLUDE__SEL4__STDINT_H_ */ diff --git a/repos/base-sel4/lib/import/import-syscall.mk b/repos/base-sel4/lib/import/import-syscall.mk index e3407c6c2..f86cdb385 100644 --- a/repos/base-sel4/lib/import/import-syscall.mk +++ b/repos/base-sel4/lib/import/import-syscall.mk @@ -7,18 +7,7 @@ INC_DIR += $(BUILD_BASE_DIR)/include # # Access to other sel4-specific headers such as 'autoconf.h'. # -REP_INC_DIR += include/sel4 +INC_DIR += $(BUILD_BASE_DIR)/include/sel4 -# -# Compile code that uses the system-call bindings without -fPIC. Otherwise, -# the compiler would complain with the following error: -# -# error: inconsistent operand constraints in an ‘asm’ -# -# XXX avoid mixing PIC with non-PIC code -# -# The lack of PIC support in the seL4 system bindings ultimately results in -# a mix of PIC and non-PIC code within a single binary. This may become a -# problem when using shared libraries. -# -CC_OPT_PIC = +# required for seL4_DebugPutChar +CC_OPT += -DSEL4_DEBUG_KERNEL -DDEBUG diff --git a/repos/base-sel4/lib/mk/spec/x86_32/kernel.mk b/repos/base-sel4/lib/mk/spec/x86_32/kernel.mk index 6bf0ef667..26a995494 100644 --- a/repos/base-sel4/lib/mk/spec/x86_32/kernel.mk +++ b/repos/base-sel4/lib/mk/spec/x86_32/kernel.mk @@ -17,11 +17,10 @@ build_kernel: $(VERBOSE)$(MAKE) \ TOOLPREFIX=$(CROSS_DEV_PREFIX) \ ARCH=x86 SEL4_ARCH=ia32 PLAT=pc99 DEBUG=1 \ + CONFIG_KERNEL_EXTRA_CPPFLAGS="-DCONFIG_PRINTING=y -DCONFIG_USER_STACK_TRACE_LENGTH=16" \ LDFLAGS+=-nostdlib LDFLAGS+=-Wl,-nostdlib \ $(addprefix LDFLAGS+=$(LINKER_OPT_PREFIX),$(LD_MARCH)) \ CFLAGS+="-fno-builtin-printf -O3" \ $(addprefix CFLAGS+=,$(CC_MARCH)) \ - CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_MAX_NUM_IOAPIC=1 \ - CONFIG_KERNEL_EXTRA_CPPFLAGS+=-DCONFIG_IRQ_IOAPIC=1 \ SOURCE_ROOT=$(SEL4_DIR) -f$(SEL4_DIR)/Makefile diff --git a/repos/base-sel4/lib/mk/spec/x86_32/platform.mk b/repos/base-sel4/lib/mk/spec/x86_32/platform.mk index de121b64b..d112d64fe 100644 --- a/repos/base-sel4/lib/mk/spec/x86_32/platform.mk +++ b/repos/base-sel4/lib/mk/spec/x86_32/platform.mk @@ -10,6 +10,7 @@ # port, if missing, is added to the missing-ports list of this stage. # LIBSEL4_DIR := $(call select_from_ports,sel4)/src/kernel/sel4/libsel4 +LIBSEL4_AUTO:= $(call select_from_ports,sel4)/src/kernel/sel4/include/plat/pc99 # # Execute the rules in this file only at the second build stage when we know @@ -30,10 +31,10 @@ SEL4_ARCH_INCLUDES := simple_types.h types.h constants.h objecttype.h \ ARCH_INCLUDES := objecttype.h types.h constants.h functions.h deprecated.h \ pfIPC.h syscalls.h exIPC.h invocation.h simple_types.h -INCLUDES := objecttype.h types.h bootinfo.h errors.h constants.h \ +INCLUDES := objecttype.h types.h bootinfo.h bootinfo_types.h errors.h constants.h \ messages.h sel4.h macros.h simple_types.h types_gen.h syscall.h \ invocation.h shared_types_gen.h debug_assert.h shared_types.h \ - sel4.h deprecated.h + sel4.h deprecated.h autoconf.h INCLUDE_SYMLINKS += $(addprefix $(BUILD_BASE_DIR)/include/sel4/, $(INCLUDES)) INCLUDE_SYMLINKS += $(addprefix $(BUILD_BASE_DIR)/include/sel4/arch/, $(ARCH_INCLUDES)) @@ -53,6 +54,10 @@ $(BUILD_BASE_DIR)/include/sel4/arch/%.h: $(LIBSEL4_DIR)/arch_include/x86/sel4/ar $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)ln -sf $< $@ +$(BUILD_BASE_DIR)/include/sel4/autoconf.h: $(LIBSEL4_AUTO)/autoconf.h + $(VERBOSE)mkdir -p $(dir $@) + $(VERBOSE)ln -sf $< $@ + $(BUILD_BASE_DIR)/include/sel4/%.h: $(LIBSEL4_DIR)/include/sel4/%.h $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)ln -sf $< $@ @@ -60,13 +65,13 @@ $(BUILD_BASE_DIR)/include/sel4/%.h: $(LIBSEL4_DIR)/include/sel4/%.h # # Generated headers # -$(BUILD_BASE_DIR)/include/sel4/types_gen.h: $(LIBSEL4_DIR)/include/sel4/types.bf +$(BUILD_BASE_DIR)/include/sel4/types_gen.h: $(LIBSEL4_DIR)/include/sel4/types_32.bf $(MSG_CONVERT)$(notdir $@) $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \ --environment libsel4 "$<" $@ -$(BUILD_BASE_DIR)/include/sel4/shared_types_gen.h: $(LIBSEL4_DIR)/include/sel4/shared_types.bf +$(BUILD_BASE_DIR)/include/sel4/shared_types_gen.h: $(LIBSEL4_DIR)/include/sel4/shared_types_32.bf $(MSG_CONVERT)$(notdir $@) $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)python $(LIBSEL4_DIR)/tools/bitfield_gen.py \ @@ -105,6 +110,6 @@ $(BUILD_BASE_DIR)/include/interfaces/sel4_client.h: $(SEL4_CLIENT_H_SRC) $(MSG_CONVERT)$(notdir $@) $(VERBOSE)mkdir -p $(dir $@) $(VERBOSE)python $(LIBSEL4_DIR)/tools/syscall_stub_gen.py \ - --buffer -a ia32 -o $@ $(SEL4_CLIENT_H_SRC) + --buffer -a ia32 --word-size 32 -o $@ $(SEL4_CLIENT_H_SRC) endif diff --git a/repos/base-sel4/patches/bda.patch b/repos/base-sel4/patches/bda.patch new file mode 100644 index 000000000..abb724fb8 --- /dev/null +++ b/repos/base-sel4/patches/bda.patch @@ -0,0 +1,31 @@ +--- src/kernel/sel4/src/arch/x86/kernel/cmdline.c ++++ src/kernel/sel4/src/arch/x86/kernel/cmdline.c +@@ -107,9 +107,16 @@ static void UNUSED parse_uint16_array(char* str, uint16_t* array, int array_size + + void cmdline_parse(const char *cmdline, cmdline_opt_t* cmdline_opt) + { ++#if defined(CONFIG_PRINTING) || defined(CONFIG_DEBUG_BUILD) ++ /* use BIOS data area to read serial configuration */ ++ const unsigned short * bda_port = (unsigned short *)0x400; ++ const unsigned short * bda_equi = (unsigned short *)0x410; ++ int const bda_ports_count = (*bda_equi >> 9) & 0x7; ++#endif ++ + #ifdef CONFIG_PRINTING +- /* initialise to default */ +- cmdline_opt->console_port = 0x3f8; ++ /* initialise to default or use BDA if available */ ++ cmdline_opt->console_port = bda_ports_count && *bda_port ? *bda_port : 0x3f8; + + if (parse_opt(cmdline, "console_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) { + parse_uint16_array(cmdline_val, &cmdline_opt->console_port, 1); +@@ -129,7 +136,8 @@ void cmdline_parse(const char *cmdline, cmdline_opt_t* cmdline_opt) + #endif + + #ifdef CONFIG_DEBUG_BUILD +- cmdline_opt->debug_port = 0x3f8; ++ /* initialise to default or use BDA if available */ ++ cmdline_opt->debug_port = bda_ports_count && *bda_port ? *bda_port : 0x3f8; + if (parse_opt(cmdline, "debug_port", cmdline_val, MAX_CMDLINE_VAL_LEN) != -1) { + parse_uint16_array(cmdline_val, &cmdline_opt->debug_port, 1); + } diff --git a/repos/base-sel4/patches/python.patch b/repos/base-sel4/patches/python.patch new file mode 100644 index 000000000..febe14772 --- /dev/null +++ b/repos/base-sel4/patches/python.patch @@ -0,0 +1,11 @@ +--- src/kernel/sel4/libsel4/tools/syscall_stub_gen.py ++++ src/kernel/sel4/libsel4/tools/syscall_stub_gen.py +@@ -807,7 +807,7 @@ def main(): + print "Invalid word size in configuration file." + sys.exit(2) + else: +- wordsize = args.wsize ++ wordsize = int(args.wsize) + + if wordsize is -1: + print "Invalid word size." diff --git a/repos/base-sel4/patches/syscall.patch b/repos/base-sel4/patches/syscall.patch new file mode 100644 index 000000000..bdb534e47 --- /dev/null +++ b/repos/base-sel4/patches/syscall.patch @@ -0,0 +1,560 @@ +--- src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h ++++ src/kernel/sel4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h +@@ -20,19 +20,21 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : ++ : "+d" (dest) + : "a" (seL4_SysSend), +- "b" (dest), + "S" (msgInfo.words[0]), + "D" (seL4_GetMR(0)), + "c" (seL4_GetMR(1)) +- : "%edx" ++ : + ); + } + +@@ -42,19 +44,21 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : ++ : "+d" (dest) + : "a" (seL4_SysSend), +- "b" (dest), + "S" (msgInfo.words[0]), + "D" (mr0 != seL4_Null ? *mr0 : 0), + "c" (mr1 != seL4_Null ? *mr1 : 0) +- : "%edx" ++ : + ); + } + +@@ -63,19 +67,21 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : ++ : "+d" (dest) + : "a" (seL4_SysNBSend), +- "b" (dest), + "S" (msgInfo.words[0]), + "D" (seL4_GetMR(0)), + "c" (seL4_GetMR(1)) +- : "%edx" ++ : + ); + } + +@@ -85,19 +91,21 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : ++ : "+d" (dest) + : "a" (seL4_SysNBSend), +- "b" (dest), + "S" (msgInfo.words[0]), + "D" (mr0 != seL4_Null ? *mr0 : 0), + "c" (mr1 != seL4_Null ? *mr1 : 0) +- : "%edx" ++ : + ); + } + +@@ -106,18 +114,20 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" + : + : "a" (seL4_SysReply), + "S" (msgInfo.words[0]), + "D" (seL4_GetMR(0)), + "c" (seL4_GetMR(1)) +- : "%ebx", "%edx" ++ : "%edx" + ); + } + +@@ -127,18 +137,20 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" + : + : "a" (seL4_SysReply), + "S" (msgInfo.words[0]), + "D" (mr0 != seL4_Null ? *mr0 : 0), + "c" (mr1 != seL4_Null ? *mr1 : 0) +- : "%ebx", "%edx" ++ : "%edx" + ); + } + +@@ -147,16 +159,18 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : ++ : "+d" (dest) + : "a" (seL4_SysSend), +- "b" (dest), + "S" (seL4_MessageInfo_new(0, 0, 0, 0).words[0]) +- : "%ecx", "%edx" ++ : "%ecx" + ); + } + +@@ -170,20 +184,24 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : +- "=b" (badge), ++ "=d" (badge), + "=S" (info.words[0]), + "=D" (mr0), + "=c" (mr1) + : "a" (seL4_SysRecv), +- "b" (src) +- : "%edx", "memory" ++ "d" (src) ++ : "memory" + ); + + seL4_SetMR(0, mr0); +@@ -207,20 +225,24 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : +- "=b" (badge), ++ "=d" (badge), + "=S" (info.words[0]), + "=D" (msg0), + "=c" (msg1) + : "a" (seL4_SysRecv), +- "b" (src) +- : "%edx", "memory" ++ "d" (src) ++ : "memory" + ); + + if (mr0 != seL4_Null) { +@@ -247,20 +269,23 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : +- "=b" (badge), ++ "=d" (badge), + "=S" (info.words[0]), + "=D" (mr0), + "=c" (mr1) + : "a" (seL4_SysNBRecv), +- "b" (src) +- : "%edx", "memory" ++ "d" (src) ++ : "memory" + ); + + seL4_SetMR(0, mr0); +@@ -282,24 +307,27 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : + "=S" (info.words[0]), + "=D" (mr0), + "=c" (mr1), +- "=b" (dest) /* dummy, tells GCC that ebx is clobbered */ ++ "+d" (dest) + : "a" (seL4_SysCall), +- "b" (dest), + "S" (msgInfo.words[0]), + "D" (mr0), + "c" (mr1) +- : "%edx", "memory" ++ : "memory" + ); + + seL4_SetMR(0, mr0); +@@ -325,24 +353,27 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : + "=S" (info.words[0]), + "=D" (msg0), + "=c" (msg1), +- "=b" (dest) /* dummy, tells GCC that ebx is clobbered */ ++ "+d" (dest) + : "a" (seL4_SysCall), +- "b" (dest), + "S" (msgInfo.words[0]), + "D" (msg0), + "c" (msg1) +- : "%edx", "memory" ++ : "memory" + ); + + if (mr0 != seL4_Null) { +@@ -365,24 +396,28 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : +- "=b" (badge), ++ "=d" (badge), + "=S" (info.words[0]), + "=D" (mr0), + "=c" (mr1) + : "a" (seL4_SysReplyRecv), +- "b" (dest), ++ "d" (dest), + "S" (msgInfo.words[0]), + "D" (mr0), + "c" (mr1) +- : "%edx", "memory" ++ : "memory" + ); + + seL4_SetMR(0, mr0); +@@ -413,24 +448,27 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%ecx, %%ebp \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : +- "=b" (badge), ++ "+d" (badge), + "=S" (info.words[0]), + "=D" (msg0), + "=c" (msg1) + : "a" (seL4_SysReplyRecv), +- "b" (dest), + "S" (msgInfo.words[0]), + "D" (msg0), + "c" (msg1) +- : "%edx", "memory" ++ : "memory" + ); + + if (mr0 != seL4_Null) { +@@ -452,14 +490,16 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" + : + : "a" (seL4_SysYield) +- : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory" ++ : "%ecx", "%edx", "%esi", "%edi", "memory" + ); + } + +@@ -469,15 +509,17 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : +- : "a" (seL4_SysDebugPutChar), +- "b" (c) +- : "%ecx", "%edx", "%esi", "%edi", "memory" ++ : "+d" (c) ++ : "a" (seL4_SysDebugPutChar) ++ : "%ecx", "%esi", "%edi", "memory" + ); + } + #endif +@@ -488,14 +530,16 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" + : + : "a" (seL4_SysDebugHalt) +- : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory" ++ : "%ecx", "%edx", "%esi", "%edi", "memory" + ); + } + #endif +@@ -506,14 +550,16 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" + : + : "a" (seL4_SysDebugSnapshot) +- : "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory" ++ : "%ecx", "%edx", "%esi", "%edi", "memory" + ); + } + #endif +@@ -524,14 +570,18 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : "=b"(cap) +- : "a"(seL4_SysDebugCapIdentify), "b"(cap) +- : "%ecx", "%edx", "%esi", "%edi", "memory" ++ : "+d"(cap) ++ : "a"(seL4_SysDebugCapIdentify) ++ : "%ecx", "%esi", "%edi", "memory" + ); + return (seL4_Uint32)cap; + } +@@ -546,14 +596,17 @@ + + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : +- : "a"(seL4_SysDebugNameThread), "b"(tcb) +- : "%ecx", "%edx", "%esi", "%edi", "memory" ++ : "+d" (tcb) ++ : "a"(seL4_SysDebugNameThread) ++ : "%ecx", "%esi", "%edi", "memory" + ); + } + #endif +@@ -564,16 +617,18 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : ++ : "+d" (userfn) + : "a" (seL4_SysDebugRun), +- "b" (userfn), + "S" (userarg) +- : "%ecx", "%edx", "%edi", "memory" ++ : "%ecx", "%edi", "memory" + ); + } + #endif +@@ -600,16 +655,19 @@ + { + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" ++ "movl %%edx, %%ebx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : "=b" (start) ++ : "+d" (start) + : "a" (seL4_SysBenchmarkDumpLog), +- "b" (start), + "S" (size) +- : "%ecx", "%edx", "%edi", "memory" ++ : "%ecx", "%edi", "memory" + ); + + return (seL4_Uint32) start; +@@ -622,14 +680,17 @@ + seL4_Uint32 ret = 0; + asm volatile ( + "pushl %%ebp \n" ++ "pushl %%ebx \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" ++ "movl %%ebx, %%edx \n" ++ "popl %%ebx \n" + "popl %%ebp \n" +- : "=b" (ret) ++ : "=d" (ret) + : "a" (seL4_SysBenchmarkLogSize) +- : "%ecx", "%edx", "%edi", "memory" ++ : "%ecx", "%edi", "memory" + ); + + return ret; diff --git a/repos/base-sel4/ports/sel4.hash b/repos/base-sel4/ports/sel4.hash index 7c20310bc..da4bc27e6 100644 --- a/repos/base-sel4/ports/sel4.hash +++ b/repos/base-sel4/ports/sel4.hash @@ -1 +1 @@ -994f493f94aea91a945653a057f025b8f29fda83 +622f516efe02eb0b0d694d1c94b832aafa903105 diff --git a/repos/base-sel4/ports/sel4.port b/repos/base-sel4/ports/sel4.port index 579579ad4..d311e1696 100644 --- a/repos/base-sel4/ports/sel4.port +++ b/repos/base-sel4/ports/sel4.port @@ -3,6 +3,8 @@ VERSION := git DOWNLOADS := sel4.git URL(sel4) := https://github.com/seL4/seL4.git -# master branch, version 2.1 -REV(sel4) := 0115ad1d0d7a871d637f8ceb79e37b46f9981249 +# master branch, version 3.1 +REV(sel4) := 8150e914c377bb2d94796c6857d08f64973a7295 DIR(sel4) := src/kernel/sel4 + +PATCHES := $(wildcard $(REP_DIR)/patches/*.patch) diff --git a/repos/base-sel4/src/core/capability_space.cc b/repos/base-sel4/src/core/capability_space.cc index ac7f97945..e27685189 100644 --- a/repos/base-sel4/src/core/capability_space.cc +++ b/repos/base-sel4/src/core/capability_space.cc @@ -111,7 +111,7 @@ Capability_space::create_rpc_obj_cap(Native_capability ep_cap, src_depth, rights, badge); - ASSERT(ret == 0); + ASSERT(ret == seL4_NoError); } return Native_capability(data); diff --git a/repos/base-sel4/src/core/include/initial_untyped_pool.h b/repos/base-sel4/src/core/include/initial_untyped_pool.h index b006677d2..9a020898c 100644 --- a/repos/base-sel4/src/core/include/initial_untyped_pool.h +++ b/repos/base-sel4/src/core/include/initial_untyped_pool.h @@ -65,20 +65,6 @@ class Genode::Initial_untyped_pool { } }; - Initial_untyped_pool() - { - size_t total_bytes = 0; - - PINF("initial untyped pool:"); - for_each_range([&] (Range const &range) { - total_bytes += range.size; - PINF(" [%u] phys=0x%lx size=0x%zx", - range.sel, range.phys, range.size); - }); - - PINF(" total: %zd bytes", total_bytes); - } - /** * Apply functor to each untyped memory range * @@ -142,9 +128,6 @@ class Genode::Initial_untyped_pool */ range.free_offset = new_free_offset; - PDBG("alloc 0x%lx bytes from %u -> free index 0x%lx", - 1UL << size_log2, range.sel, range.free_offset); - /* return selector is matching range */ sel = range.sel; } diff --git a/repos/base-sel4/src/core/include/kernel_object.h b/repos/base-sel4/src/core/include/kernel_object.h index 68f5234b0..9eb22fb3f 100644 --- a/repos/base-sel4/src/core/include/kernel_object.h +++ b/repos/base-sel4/src/core/include/kernel_object.h @@ -57,14 +57,14 @@ namespace Genode { struct Page_table_kobj { - enum { SEL4_TYPE = seL4_IA32_PageTableObject, SIZE_LOG2 = 12 }; + enum { SEL4_TYPE = seL4_X86_PageTableObject, SIZE_LOG2 = 12 }; static char const *name() { return "page table"; } }; struct Page_directory_kobj { - enum { SEL4_TYPE = seL4_IA32_PageDirectoryObject, SIZE_LOG2 = 12 }; + enum { SEL4_TYPE = seL4_X86_PageDirectoryObject, SIZE_LOG2 = 12 }; static char const *name() { return "page directory"; } }; @@ -127,9 +127,6 @@ namespace Genode { throw Retype_untyped_failed(); } - PLOG("created kernel object '%s' at 0x%lx -> root=%lu index=%lu", - KOBJ::name(), phys_addr, dst_cnode_sel.value(), dst_idx.value()); - return phys_addr; } diff --git a/repos/base-sel4/src/core/include/platform_thread.h b/repos/base-sel4/src/core/include/platform_thread.h index d671875f4..d6ffdd1e3 100644 --- a/repos/base-sel4/src/core/include/platform_thread.h +++ b/repos/base-sel4/src/core/include/platform_thread.h @@ -170,7 +170,7 @@ class Genode::Platform_thread : public List::Element /** * Get thread name */ - const char *name() const { return "noname"; } + const char *name() const { return _name.string(); } /***************************** diff --git a/repos/base-sel4/src/core/include/untyped_memory.h b/repos/base-sel4/src/core/include/untyped_memory.h index 50825dc3c..fc01f0531 100644 --- a/repos/base-sel4/src/core/include/untyped_memory.h +++ b/repos/base-sel4/src/core/include/untyped_memory.h @@ -93,7 +93,7 @@ struct Genode::Untyped_memory for (size_t i = 0; i < num_pages; i++, phys_addr += get_page_size()) { seL4_Untyped const service = untyped_sel(phys_addr).value(); - int const type = seL4_IA32_4K; + int const type = seL4_X86_4K; int const size_bits = 0; seL4_CNode const root = Core_cspace::TOP_CNODE_SEL; int const node_index = Core_cspace::TOP_CNODE_PHYS_IDX; diff --git a/repos/base-sel4/src/core/include/vm_space.h b/repos/base-sel4/src/core/include/vm_space.h index da069a038..b0c57d82f 100644 --- a/repos/base-sel4/src/core/include/vm_space.h +++ b/repos/base-sel4/src/core/include/vm_space.h @@ -17,6 +17,7 @@ /* Genode includes */ #include #include +#include #include /* core includes */ @@ -169,17 +170,16 @@ class Genode::Vm_space * Insert copy of page-frame selector into page table */ { - seL4_IA32_Page const service = _idx_to_sel(pte_idx); - seL4_IA32_PageDirectory const pd = _pd_sel.value(); - seL4_Word const vaddr = to_virt; - seL4_CapRights const rights = seL4_AllRights; - seL4_IA32_VMAttributes const attr = seL4_IA32_Default_VMAttributes; + seL4_X86_Page const service = _idx_to_sel(pte_idx); + seL4_X86_PageDirectory const pd = _pd_sel.value(); + seL4_Word const vaddr = to_virt; + seL4_CapRights const rights = seL4_AllRights; + seL4_X86_VMAttributes const attr = seL4_X86_Default_VMAttributes; - int const ret = seL4_IA32_Page_Map(service, pd, vaddr, rights, attr); + int const ret = seL4_X86_Page_Map(service, pd, vaddr, rights, attr); - if (ret != 0) - PERR("seL4_IA32_Page_Map to 0x%lx returned %d", - (unsigned long)vaddr, ret); + if (ret != seL4_NoError) + error("seL4_X86_Page_Map to ", Hex(vaddr), " returned ", ret); } } @@ -199,17 +199,14 @@ class Genode::Vm_space void _map_page_table(Cap_sel pt_sel, addr_t to_virt) { - seL4_IA32_PageTable const service = pt_sel.value(); - seL4_IA32_PageDirectory const pd = _pd_sel.value(); - seL4_Word const vaddr = to_virt; - seL4_IA32_VMAttributes const attr = seL4_IA32_Default_VMAttributes; + seL4_X86_PageTable const service = pt_sel.value(); + seL4_X86_PageDirectory const pd = _pd_sel.value(); + seL4_Word const vaddr = to_virt; + seL4_X86_VMAttributes const attr = seL4_X86_Default_VMAttributes; - PDBG("map page table 0x%lx to virt 0x%lx, pdir sel %lu", - pt_sel.value(), to_virt, _pd_sel.value()); - - int const ret = seL4_IA32_PageTable_Map(service, pd, vaddr, attr); - if (ret != 0) - PDBG("seL4_IA32_PageTable_Map returned %d", ret); + int const ret = seL4_X86_PageTable_Map(service, pd, vaddr, attr); + if (ret != seL4_NoError) + error("seL4_X86_PageTable_Map returned ", ret); } class Alloc_page_table_failed : Exception { }; diff --git a/repos/base-sel4/src/core/platform.cc b/repos/base-sel4/src/core/platform.cc index 21a4f3f77..7583411e1 100644 --- a/repos/base-sel4/src/core/platform.cc +++ b/repos/base-sel4/src/core/platform.cc @@ -12,9 +12,9 @@ */ /* Genode includes */ -#include #include #include +#include /* core includes */ #include @@ -24,6 +24,7 @@ #include /* base-internal includes */ +#include #include using namespace Genode; @@ -83,6 +84,9 @@ bool Mapped_mem_allocator::_unmap_local(addr_t virt_addr, unsigned size) void Platform::_init_unused_phys_alloc() { + /* enable log support early */ + init_log(); + _unused_phys_alloc.add_range(0, ~0UL); } @@ -114,8 +118,6 @@ void Platform::_init_allocators() addr_t const base = range.phys + page_aligned_offset; size_t const size = range.size - page_aligned_offset; - PDBG("register phys mem range 0x%lx size=0x%zx", base, size); - _core_mem_alloc.phys_alloc()->add_range(base, size); _unused_phys_alloc.remove_range(base, size); }; @@ -153,9 +155,11 @@ void Platform::_init_allocators() _core_mem_alloc.virt_alloc()->remove_range(core_virt_beg, core_size); if (verbose_boot_info) { - printf("core image:\n"); - printf(" virtual address range [%08lx,%08lx) size=0x%zx\n", - core_virt_beg, core_virt_end, core_size); + log("core image:"); + log(" virtual address range [", + Hex(core_virt_beg, Hex::OMIT_PREFIX, Hex::PAD), ",", + Hex(core_virt_end, Hex::OMIT_PREFIX, Hex::PAD), ") size=", + Hex(core_size)); } /* preserve stack area in core's virtual address space */ @@ -238,9 +242,8 @@ void Platform::_switch_to_core_cspace() Core_cspace::TOP_CNODE_SEL, null_data, seL4_CapInitThreadPD, null_data); - if (ret != 0) { - PERR("%s: seL4_TCB_SetSpace returned %d", __FUNCTION__, ret); - } + if (ret != seL4_NoError) + error(__FUNCTION__, ": seL4_TCB_SetSpace returned ", ret); } } @@ -259,7 +262,7 @@ void Platform::_init_core_page_table_registry() * Register initial page tables */ addr_t virt_addr = (addr_t)(&_prog_img_beg); - for (unsigned sel = bi.userImagePTs.start; sel < bi.userImagePTs.end; sel++) { + for (unsigned sel = bi.userImagePaging.start; sel < bi.userImagePaging.end; sel++) { _core_page_table_registry.insert_page_table(virt_addr, Cap_sel(sel)); @@ -303,7 +306,7 @@ void Platform::_init_rom_modules() _unused_phys_alloc.alloc_aligned(modules_size, &out_ptr, get_page_size_log2()); if (alloc_ret.error()) { - PERR("could not reserve phys CNode space for boot modules"); + error("could not reserve phys CNode space for boot modules"); struct Init_rom_modules_failed { }; throw Init_rom_modules_failed(); } @@ -366,7 +369,7 @@ Platform::Platform() _unused_phys_alloc(core_mem_alloc()), _init_unused_phys_alloc_done((_init_unused_phys_alloc(), true)), _vm_base(0x2000), /* 2nd page is used as IPC buffer of main thread */ - _vm_size(2*1024*1024*1024UL - _vm_base), /* use the lower 2GiB */ + _vm_size(3*1024*1024*1024UL - _vm_base), /* use the lower 3GiB */ _init_sel4_ipc_buffer_done((init_sel4_ipc_buffer(), true)), _switch_to_core_cspace_done((_switch_to_core_cspace(), true)), _core_page_table_registry(*core_mem_alloc()), @@ -382,15 +385,16 @@ Platform::Platform() _core_page_table_registry) { /* - * Print statistics about allocator initialization + * Log statistics about allocator initialization */ - printf("VM area at [%08lx,%08lx)\n", _vm_base, _vm_base + _vm_size); + log("VM area at [", Hex(_vm_base, Hex::OMIT_PREFIX, Hex::PAD), ",", + Hex(_vm_base + _vm_size, Hex::OMIT_PREFIX, Hex::PAD), ")"); if (verbose_boot_info) { - printf(":phys_alloc: "); (*_core_mem_alloc.phys_alloc())()->dump_addr_tree(); - printf(":unused_phys_alloc:"); _unused_phys_alloc()->dump_addr_tree(); - printf(":virt_alloc: "); (*_core_mem_alloc.virt_alloc())()->dump_addr_tree(); - printf(":io_mem_alloc: "); _io_mem_alloc()->dump_addr_tree(); + log(":phys_alloc: "); (*_core_mem_alloc.phys_alloc())()->dump_addr_tree(); + log(":unused_phys_alloc:"); _unused_phys_alloc()->dump_addr_tree(); + log(":virt_alloc: "); (*_core_mem_alloc.virt_alloc())()->dump_addr_tree(); + log(":io_mem_alloc: "); _io_mem_alloc()->dump_addr_tree(); } _init_rom_modules(); diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc index e5b24b74f..18fe3ab90 100644 --- a/repos/base-sel4/src/core/platform_pd.cc +++ b/repos/base-sel4/src/core/platform_pd.cc @@ -12,7 +12,7 @@ */ /* Genode includes */ -#include +#include /* core includes */ #include @@ -102,17 +102,16 @@ void Platform_pd::assign_parent(Native_capability parent) addr_t Platform_pd::_init_page_directory() { - PDBG("_init_page_directory at sel %lu", _page_directory_sel.value()); addr_t const phys = create(*platform()->ram_alloc(), platform_specific()->core_cnode().sel(), _page_directory_sel); - int const ret = seL4_IA32_ASIDPool_Assign(platform_specific()->asid_pool().value(), + int const ret = seL4_X86_ASIDPool_Assign(platform_specific()->asid_pool().value(), _page_directory_sel.value()); - if (ret != 0) - PERR("seL4_IA32_ASIDPool_Assign returned %d", ret); + if (ret != seL4_NoError) + error("seL4_X86_ASIDPool_Assign returned ", ret); return phys; } diff --git a/repos/base-sel4/src/core/rpc_cap_factory.cc b/repos/base-sel4/src/core/rpc_cap_factory.cc index 7f0bc9c25..67fb611c6 100644 --- a/repos/base-sel4/src/core/rpc_cap_factory.cc +++ b/repos/base-sel4/src/core/rpc_cap_factory.cc @@ -55,10 +55,14 @@ void Rpc_cap_factory::free(Native_capability cap) if (!cap.valid()) return; - PDBG("not implemented"); - /* * XXX check whether this CAP session has created the capability to delete. */ + + static uint64_t leakage = 0; + + leakage ++; + if (1ULL << log2(leakage) == leakage) + warning(__PRETTY_FUNCTION__, " not implemented - resources leaked: ", Hex(leakage)); } diff --git a/repos/base-sel4/src/lib/base/ipc.cc b/repos/base-sel4/src/lib/base/ipc.cc index 71e110577..af896f30c 100644 --- a/repos/base-sel4/src/lib/base/ipc.cc +++ b/repos/base-sel4/src/lib/base/ipc.cc @@ -12,9 +12,9 @@ */ /* Genode includes */ -#include -#include #include +#include +#include #include #include @@ -173,12 +173,12 @@ static void decode_seL4_message(seL4_MessageInfo_t const &msg_info, * So it is already present within the capability space. */ - unsigned const arg_badge = + unsigned long const arg_badge = seL4_CapData_Badge_get_Badge(seL4_GetBadge(curr_sel4_cap_idx)); if (arg_badge != rpc_obj_key.value()) { - PWRN("argument badge (%d) != RPC object key (%d)", - arg_badge, rpc_obj_key.value()); + warning("argument badge (", arg_badge, ") != RPC object key (", + rpc_obj_key.value(), ")"); } Native_capability arg_cap = Capability_space::lookup(rpc_obj_key); @@ -272,7 +272,7 @@ Rpc_exception_code Genode::ipc_call(Native_capability dst, size_t) { if (!dst.valid()) { - PERR("Trying to invoke an invalid capability, stop."); + error("Trying to invoke an invalid capability, stop."); kernel_debugger_panic("IPC destination is invalid"); } diff --git a/repos/base-sel4/src/lib/base/thread_sel4.cc b/repos/base-sel4/src/lib/base/thread_sel4.cc deleted file mode 100644 index 54fc59cdc..000000000 --- a/repos/base-sel4/src/lib/base/thread_sel4.cc +++ /dev/null @@ -1,52 +0,0 @@ -/* - * \brief seL4-specific implementation of the Thread API - * \author Norman Feske - * \date 2014-10-14 - */ - -/* - * Copyright (C) 2014 Genode Labs GmbH - * - * This file is part of the Genode OS framework, which is distributed - * under the terms of the GNU General Public License version 2. - */ - -/* Genode includes */ -#include -#include -#include -#include - -#include -#include - - -using namespace Genode; - - -/************ - ** Thread ** - ************/ - -void Thread::_init_platform_thread(size_t, Type type) -{ - PDBG("not implemented"); -} - - -void Thread::_deinit_platform_thread() -{ - PDBG("not implemented"); -} - - -void Thread::start() -{ - PDBG("not implemented"); -} - - -void Thread::cancel_blocking() -{ - PDBG("not implemented"); -} diff --git a/tool/run/boot_dir/sel4 b/tool/run/boot_dir/sel4 index ca5209097..3343979b3 100644 --- a/tool/run/boot_dir/sel4 +++ b/tool/run/boot_dir/sel4 @@ -181,13 +181,28 @@ proc run_boot_dir {binaries} { run_image $elf_img - # set symbolic link to image.elf file in TFTP directory for PXE boot if {[have_include "load/tftp"]} { - exec ln -sf [pwd]/$elf_img [load_tftp_base_dir][load_tftp_offset_dir] + # + # Install PXE bootloader pulsar + # + install_pxe_bootloader_to_run_dir - if {[have_include "image/uboot"]} { - exec ln -sf [pwd]/[run_dir]/uImage [load_tftp_base_dir][load_tftp_offset_dir] - } + # + # Generate pulsar config file + # + set fh [open "[run_dir]/config-52-54-00-12-34-56" "WRONLY CREAT TRUNC"] + puts $fh " exec /boot/bender" + puts $fh " load /sel4" + puts $fh " load /image.elf" + close $fh + + generate_tftp_config + } + + if {[have_include "load/ipxe"]} { + create_ipxe_iso_config + update_ipxe_boot_dir + create_symlink_for_iso } # retrieve stand-alone core