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