ehmry/genode
ehmry
/
genode
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

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
This commit is contained in:
Alexander Boettcher 2016-06-17 15:15:48 +02:00 committed by Christian Helmuth
parent 8b505306ed
commit af93f8d01b
22 changed files with 700 additions and 211 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
repos/base-sel4/include/sel4/autoconf.h
View File

@ -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_ */

28
repos/base-sel4/include/sel4/stdint.h
View File

@ -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 <base/fixed_stdint.h>
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_ */

17
repos/base-sel4/lib/import/import-syscall.mk
View File

@ -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

3
repos/base-sel4/lib/mk/spec/x86_32/kernel.mk
View File

@ -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

15
repos/base-sel4/lib/mk/spec/x86_32/platform.mk
View File

@ -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

31
repos/base-sel4/patches/bda.patch Normal file
View File

@ -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);
}

11
repos/base-sel4/patches/python.patch Normal file
View File

@ -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."

560
repos/base-sel4/patches/syscall.patch Normal file
View File

@ -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;

2
repos/base-sel4/ports/sel4.hash
View File

@ -1 +1 @@
994f493f94aea91a945653a057f025b8f29fda83
622f516efe02eb0b0d694d1c94b832aafa903105

6
repos/base-sel4/ports/sel4.port
View File

@ -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)

2
repos/base-sel4/src/core/capability_space.cc
View File

@ -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);

17
repos/base-sel4/src/core/include/initial_untyped_pool.h
View File

@ -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;
}

7
repos/base-sel4/src/core/include/kernel_object.h
View File

@ -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;
}

2
repos/base-sel4/src/core/include/platform_thread.h
View File

@ -170,7 +170,7 @@ class Genode::Platform_thread : public List<Platform_thread>::Element
/**
* Get thread name
*/
const char *name() const { return "noname"; }
const char *name() const { return _name.string(); }
/*****************************

2
repos/base-sel4/src/core/include/untyped_memory.h
View File

@ -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;

35
repos/base-sel4/src/core/include/vm_space.h
View File

@ -17,6 +17,7 @@
/* Genode includes */
#include <util/bit_allocator.h>
#include <util/volatile_object.h>
#include <base/log.h>
#include <base/thread.h>
/* 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 { };

40
repos/base-sel4/src/core/platform.cc
View File

@ -12,9 +12,9 @@
*/
/* Genode includes */
#include <base/printf.h>
#include <base/sleep.h>
#include <base/thread.h>
#include <base/log.h>
/* core includes */
#include <core_parent.h>
@ -24,6 +24,7 @@
#include <untyped_memory.h>
/* base-internal includes */
#include <base/internal/globals.h>
#include <base/internal/stack_area.h>
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();

9
repos/base-sel4/src/core/platform_pd.cc
View File

@ -12,7 +12,7 @@
*/
/* Genode includes */
#include <base/printf.h>
#include <base/log.h>
/* core includes */
#include <platform_pd.h>
@ -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<Page_directory_kobj>(*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;
}

8
repos/base-sel4/src/core/rpc_cap_factory.cc
View File

@ -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));
}

12
repos/base-sel4/src/lib/base/ipc.cc
View File

@ -12,9 +12,9 @@
*/
/* Genode includes */
#include <base/ipc.h>
#include <base/printf.h>
#include <base/blocking.h>
#include <base/ipc.h>
#include <base/log.h>
#include <base/thread.h>
#include <util/misc_math.h>
@ -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");
}

52
repos/base-sel4/src/lib/base/thread_sel4.cc
View File

@ -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 <base/thread.h>
#include <base/printf.h>
#include <base/sleep.h>
#include <base/env.h>
#include <base/rpc_client.h>
#include <session/session.h>
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");
}

25
tool/run/boot_dir/sel4
View File

@ -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