portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

libsel4: Generate libsel4 definitions from the current ARCH as well as the SEL4_ARCH

Browse source
This commit is contained in:
Adrian Danis 2015-08-19 14:35:56 +10:00
parent a7c7ba2ef8
commit 44a522dce2
43 changed files with 1355 additions and 953 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
Makefile
View file

@ -457,7 +457,7 @@ ASM_SOURCES += $(patsubst %, src/plat/${PLAT}/%, ${PLAT_ASM_SOURCES})
GENHEADERS = $(patsubst %.bf, %.pbf, ${BF_SOURCES}) \
$(patsubst %.bf, %_gen.h, ${BF_SOURCES})
GENHEADERS += arch/api/invocation.h api/invocation.h arch/api/syscall.h
GENHEADERS += arch/api/invocation.h arch/api/sel4_invocation.h api/invocation.h arch/api/syscall.h
DEFTHEORIES = $(patsubst %.bf, %_defs.thy, ${BF_SOURCES})
PROOFTHEORIES = $(patsubst %.bf, %_proofs.thy, ${BF_SOURCES})
@ -570,6 +570,11 @@ arch/api/invocation.h: ${SOURCE_ROOT}/libsel4/arch_include/${ARCH}/interfaces/se
$(Q)${INVOCATION_ID_GEN_PATH} --arch --xml $< \
--dest $@
arch/api/sel4_invocation.h: ${SOURCE_ROOT}/libsel4/sel4_arch_include/${SEL4_ARCH}/interfaces/sel4arch.xml | ${DIRECTORIES}
$(Q)rm -f ${SOURCE_ROOT}/include/arch/${ARCH}/arch/api/sel4_invocation.h
$(Q)${INVOCATION_ID_GEN_PATH} --sel4_arch --xml $< \
--dest $@
api/invocation.h: ${SOURCE_ROOT}/libsel4/include/interfaces/sel4.xml | ${DIRECTORIES}
$(Q)rm -f ${SOURCE_ROOT}/include/api/invocation.h

1
include/arch/x86/arch/32/mode/api/objecttype.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../../../libsel4/sel4_arch_include/ia32/sel4/sel4_arch/objecttype.h

1
include/arch/x86/arch/api/types.h
View file

@ -13,6 +13,7 @@
#include <api/objecttype.h>
#include <config.h>
#include <mode/api/objecttype.h>
#include <arch/api/objecttype.h>
#define pageType PageObject4K

17
libsel4/Makefile
View file

@ -17,7 +17,8 @@ CHANGED_PATH := ${SOURCE_DIR}/tools/changed.sh
# Targets
PRIORITY_TARGETS := include/interfaces/sel4_client.h include/sel4/types_gen.h include/sel4/syscall.h \
include/sel4/invocation.h arch_include/${ARCH}/sel4/arch/invocation.h
include/sel4/invocation.h arch_include/${ARCH}/sel4/arch/invocation.h \
sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/invocation.h
TARGETS := libsel4.a
# Source files required to build the target
@ -29,6 +30,7 @@ CFILES := \
HDRFILES := \
$(wildcard $(SOURCE_DIR)/include/*) \
$(wildcard $(SOURCE_DIR)/arch_include/$(ARCH)/*) \
$(wildcard $(SOURCE_DIR)/sel4_arch_include/$(SEL4_ARCH)/*) \
$(BUILD_DIR)/include/sel4 \
$(BUILD_DIR)/include/interfaces #TODO proper prefix instruction
@ -53,6 +55,12 @@ include/sel4/invocation.h: ${SOURCE_DIR}/include/interfaces/sel4.xml
@${CHANGED_PATH} $@ python ${INVOCATION_ID_GEN_PATH} \
--xml $< --libsel4 --dest $@
sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/invocation.h: ${SOURCE_DIR}/sel4_arch_include/${SEL4_ARCH}/interfaces/sel4arch.xml
@echo " [GEN] $@"
@mkdir -p $(dir $@)
@${CHANGED_PATH} ${SOURCE_DIR}/$@ python ${INVOCATION_ID_GEN_PATH} \
--xml $< --libsel4 --sel4_arch --dest ${SOURCE_DIR}/$@
arch_include/${ARCH}/sel4/arch/invocation.h: ${SOURCE_DIR}/arch_include/${ARCH}/interfaces/sel4arch.xml
@echo " [GEN] $@"
@mkdir -p $(dir $@)
@ -77,13 +85,16 @@ include/sel4/types_gen.h: \
@mkdir -p $(dir $@)
@${CHANGED_PATH} $@ python ${BF_GEN_PATH} --environment libsel4 "${SOURCE_DIR}/include/sel4/types.bf" include/sel4/types_gen.h
# Stub generator
include/interfaces/sel4_client.h: \
${SOURCE_DIR}/arch_include/${ARCH}/interfaces/sel4arch.xml \
${SOURCE_DIR}/sel4_arch_include/${SEL4_ARCH}/interfaces/sel4arch.xml \
${SOURCE_DIR}/arch_include/${ARCH}/interfaces/sel4arch.xml \
${SOURCE_DIR}/include/interfaces/sel4.xml
@echo " [GEN] $@"
@mkdir -p $(dir $@)
@${CHANGED_PATH} $@ \
python ${SOURCE_DIR}/tools/syscall_stub_gen.py \
--buffer \
-a $(ARCH) -o $@ $^
-a $(SEL4_ARCH) -o $@ $^

195
libsel4/arch_include/x86/interfaces/sel4arch.xml
View file

@ -9,109 +9,100 @@
@TAG(NICTA_BSD)
-->
<api>
<struct name="seL4_UserContext">
<member name="eip"/>
<member name="esp"/>
<member name="eflags"/>
<member name="eax"/>
<member name="ebx"/>
<member name="ecx"/>
<member name="edx"/>
<member name="esi"/>
<member name="edi"/>
<member name="ebp"/>
<member name="tls_base"/>
<member name="fs"/>
<member name="gs"/>
</struct>
<interface name="seL4_IA32_PageDirectory">
<method id="IA32PageDirectoryMap" name="Map">
<param dir="in" name="pdpt" type="seL4_IA32_PageDirectory"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<method id="IA32PageDirectoryUnmap" name="Unmap">
</method>
</interface>
<interface name="seL4_IA32_PageTable">
<method id="IA32PageTableMap" name="Map">
<param dir="in" name="pd" type="seL4_IA32_PageDirectory"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<interface name="seL4_IA32_PageDirectory">
<method id="IA32PageDirectoryMap" name="Map">
<param dir="in" name="vroot" type="seL4_CPtr"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<method id="IA32PageDirectoryUnmap" name="Unmap">
</method>
</interface>
<interface name="seL4_IA32_PageTable">
<method id="IA32PageTableMap" name="Map">
<param dir="in" name="vroot" type="seL4_CPtr"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<method id="IA32PageTableUnmap" name="Unmap">
</method>
</interface>
<interface name="seL4_IA32_IOPageTable">
<method id="IA32IOPageTableMap" name="Map">
<param dir="in" name="iospace" type="seL4_IA32_IOSpace"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
</method>
<method id="IA32IOPageTableUnmap" name="Unmap">
</method>
</interface>
<interface name="seL4_IA32_Page">
<method id="IA32PageMap" name="Map">
<param dir="in" name="pd" type="seL4_IA32_PageDirectory"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="rights" type="seL4_CapRights"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<method id="IA32PageRemap" name="Remap">
<param dir="in" name="pd" type="seL4_IA32_PageDirectory"/>
<param dir="in" name="rights" type="seL4_CapRights"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<method id="IA32PageUnmap" name="Unmap"/>
<method id="IA32PageMapIO" name="MapIO">
<param dir="in" name="iospace" type="seL4_IA32_IOSpace"/>
<param dir="in" name="rights" type="seL4_CapRights"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
</method>
<method id="IA32PageGetAddress" name="GetAddress">
<param dir="out" name="paddr" type="seL4_Word"/>
</method>
</interface>
<interface name="seL4_IA32_ASIDControl">
<method id="IA32ASIDControlMakePool" name="MakePool">
<param dir="in" name="untyped" type="seL4_Untyped"/>
<param dir="in" name="root" type="seL4_CNode"/>
<param dir="in" name="index" type="seL4_Word"/>
<param dir="in" name="depth" type="seL4_Uint8"/>
</method>
</interface>
<interface name="seL4_IA32_ASIDPool">
<method id="IA32ASIDPoolAssign" name="Assign">
<param dir="in" name="vroot" type="seL4_IA32_PageDirectory"/>
</method>
</interface>
<interface name="seL4_IA32_IOPort">
<method id="IA32IOPortIn8" name="In8">
<param dir="out" name="result" type="seL4_Uint8"/>
<param dir="in" name="port" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortIn16" name="In16">
<param dir="out" name="result" type="seL4_Uint16"/>
<param dir="in" name="port" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortIn32" name="In32">
<param dir="out" name="result" type="seL4_Uint32"/>
<param dir="in" name="port" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortOut8" name="Out8">
<param dir="in" name="port" type="seL4_Uint16"/>
<param dir="in" name="data" type="seL4_Uint8"/>
</method>
<method id="IA32IOPortOut16" name="Out16">
<param dir="in" name="port" type="seL4_Uint16"/>
<param dir="in" name="data" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortOut32" name="Out32">
<param dir="in" name="port" type="seL4_Uint16"/>
<param dir="in" name="data" type="seL4_Uint32"/>
</method>
</interface>
<interface name="seL4_IA32_IOSpace">
<method id="IA32IOSpaceRemovePassthrough" name="RemovePassthrough"/>
</interface>
<interface name="seL4_IA32_IOPageTable">
<method id="IA32IOPageTableMap" name="Map">
<param dir="in" name="iospace" type="seL4_IA32_IOSpace"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
</method>
<method id="IA32IOPageTableUnmap" name="Unmap">
</method>
</interface>
<interface name="seL4_IA32_Page">
<method id="IA32PageMap" name="Map">
<param dir="in" name="vroot" type="seL4_CPtr"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="rights" type="seL4_CapRights"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<method id="IA32PageRemap" name="Remap">
<param dir="in" name="vroot" type="seL4_CPtr"/>
<param dir="in" name="rights" type="seL4_CapRights"/>
<param dir="in" name="attr" type="seL4_IA32_VMAttributes"/>
</method>
<method id="IA32PageUnmap" name="Unmap"/>
<method id="IA32PageMapIO" name="MapIO">
<param dir="in" name="iospace" type="seL4_IA32_IOSpace"/>
<param dir="in" name="rights" type="seL4_CapRights"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
</method>
<method id="IA32PageGetAddress" name="GetAddress">
<param dir="out" name="paddr" type="seL4_Word"/>
</method>
</interface>
<interface name="seL4_IA32_ASIDControl">
<method id="IA32ASIDControlMakePool" name="MakePool">
<param dir="in" name="untyped" type="seL4_Untyped"/>
<param dir="in" name="root" type="seL4_CNode"/>
<param dir="in" name="index" type="seL4_Word"/>
<param dir="in" name="depth" type="seL4_Uint8"/>
</method>
</interface>
<interface name="seL4_IA32_ASIDPool">
<method id="IA32ASIDPoolAssign" name="Assign">
<param dir="in" name="vroot" type="seL4_CPtr"/>
</method>
</interface>
<interface name="seL4_IA32_IOPort">
<method id="IA32IOPortIn8" name="In8">
<param dir="out" name="result" type="seL4_Uint8"/>
<param dir="in" name="port" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortIn16" name="In16">
<param dir="out" name="result" type="seL4_Uint16"/>
<param dir="in" name="port" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortIn32" name="In32">
<param dir="out" name="result" type="seL4_Uint32"/>
<param dir="in" name="port" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortOut8" name="Out8">
<param dir="in" name="port" type="seL4_Uint16"/>
<param dir="in" name="data" type="seL4_Uint8"/>
</method>
<method id="IA32IOPortOut16" name="Out16">
<param dir="in" name="port" type="seL4_Uint16"/>
<param dir="in" name="data" type="seL4_Uint16"/>
</method>
<method id="IA32IOPortOut32" name="Out32">
<param dir="in" name="port" type="seL4_Uint16"/>
<param dir="in" name="data" type="seL4_Uint32"/>
</method>
</interface>
<interface name="seL4_IA32_IOSpace">
<method id="IA32IOSpaceRemovePassthrough" name="RemovePassthrough"/>
</interface>
</api>

7
libsel4/arch_include/x86/sel4/arch/constants.h
View file

@ -13,13 +13,10 @@
#include <autoconf.h>
#define TLS_GDT_ENTRY 6
#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3)
#define IPCBUF_GDT_ENTRY 7
#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3)
#include <sel4/sel4_arch/constants.h>
#ifndef __ASM__
#include <sel4/sel4_arch/objecttype.h>
#include <sel4/arch/objecttype.h>
#endif

3
libsel4/arch_include/x86/sel4/arch/deprecated.h
View file

@ -23,4 +23,5 @@ seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *send
return seL4_ReplyRecvWithMRs(src, msgInfo, sender, mr0, mr1);
}
#endif /* CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS */
#endif /* __ARCH_DEPRECATED_H__ */
#endif /* __SEL4_ARCH_DEPRECATED_H__ */

88
libsel4/arch_include/x86/sel4/arch/exIPC.h
View file

@ -11,92 +11,6 @@
#ifndef __LIBSEL4_ARCH_EXCEPTION_IPC
#define __LIBSEL4_ARCH_EXCEPTION_IPC
/**
* NOT A STANDALONE INCLUDE
*/
/* Unknown syscall exception message. */
#define SEL4_EXCEPT_IPC_LABEL 3
/* User exception (such as divide by zero) message. */
#define SEL4_USER_EXCEPTION_LABEL 4
#define SEL4_USER_EXCEPTION_LENGTH 5
typedef enum {
EXCEPT_IPC_USER_MR_FAULT_IP,
EXCEPT_IPC_USER_MR_ESP,
EXCEPT_IPC_USER_MR_EFLAGS,
EXCEPT_IPC_USER_MR_NUMBER,
EXCEPT_IPC_USER_MR_CODE,
SEL4_USER_EXCEPT_IPC_LENGTH
} seL4_UserExceptIPCRegister;
typedef enum {
EXCEPT_IPC_SYS_MR_EAX,
EXCEPT_IPC_SYS_MR_EBX,
EXCEPT_IPC_SYS_MR_ECX,
EXCEPT_IPC_SYS_MR_EDX,
EXCEPT_IPC_SYS_MR_ESI,
EXCEPT_IPC_SYS_MR_EDI,
EXCEPT_IPC_SYS_MR_EBP,
EXCEPT_IPC_SYS_MR_EIP,
EXCEPT_IPC_SYS_MR_ESP,
EXCEPT_IPC_SYS_MR_EFLAGS,
EXCEPT_IPC_SYS_MR_SYSCALL,
SEL4_EXCEPT_IPC_LENGTH,
} seL4_ExceptIPCRegister;
typedef union {
struct {
seL4_Word fault_ip;
seL4_Word esp;
seL4_Word eflags;
seL4_Word exception_number;
seL4_Word exception_code;
} regs;
seL4_Word raw[5];
} seL4_UserExceptionIpcRegisters;
typedef union {
struct {
seL4_Word eax;
seL4_Word ebx;
seL4_Word ecx;
seL4_Word edx;
seL4_Word esi;
seL4_Word edi;
seL4_Word ebp;
seL4_Word eip;
seL4_Word esp;
seL4_Word eflags;
seL4_Word syscall;
} regs;
seL4_Word raw[11];
} seL4_ExceptionIpcRegisters;
static inline seL4_Word seL4_isExceptIPC_Tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == SEL4_EXCEPT_IPC_LABEL;
}
static inline seL4_Word seL4_ExceptIPC_Get(seL4_Word mr)
{
return seL4_GetMR(mr);
}
static inline void seL4_ExceptIPC_Set(seL4_Word index, seL4_Word val)
{
seL4_SetMR(index, val);
}
static inline seL4_Word seL4_IsArchSyscallFrom(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_length(tag) == SEL4_EXCEPT_IPC_LENGTH;
}
static inline seL4_Word seL4_IsArchExceptionFrom(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_length(tag) == SEL4_USER_EXCEPTION_LENGTH;
}
#include <sel4/sel4_arch/exIPC.h>
#endif

44
libsel4/arch_include/x86/sel4/arch/functions.h
View file

@ -12,49 +12,7 @@
#define __LIBSEL4_ARCH_FUNCTIONS_H
#include <sel4/types.h>
#include <sel4/macros.h>
/* the segment loaded into GS points directly to the IPC buffer */
#define SEL4_GET_IPCBUF_SCALE(field, i, res) \
do {\
asm volatile ("movl %%gs:%c2(,%1,%c3), %0"\
: [result] "=r" (res) /* outputs */\
: [scale] "r" (i), /* inputs */\
[offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)),\
[scale_factor] "i" (sizeof(seL4_Word))\
/* no clobber */);\
} while(0)
#define SEL4_SET_IPCBUF_SCALE(field, i, val) \
do {\
asm volatile ("movl %0, %%gs:%c2(,%1,%c3)"\
: /* no outputs */\
: [value] "r" (val), /* inputs */\
[scale] "r" (i),\
[offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)),\
[scale_factor] "i" (sizeof(seL4_Word))\
: "memory"); /* clobber */\
} while(0)
#define SEL4_GET_IPCBUF(field, res) \
do {\
asm volatile ("movl %%gs:%c1, %0"\
: [result] "=r" (res) /* inputs */\
: [offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)) /* outputs */\
/* no clobber */);\
} while(0)
#define SEL4_SET_IPCBUF(field, val) \
do {\
asm volatile ("movl %0, %%gs:%c1"\
: /* no outputs */\
: [value] "r" (val), /* inputs */\
[offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field))\
: "memory"); /* clobber */\
} while(0)
#include <sel4/sel4_arch/functions.h>
static inline seL4_MessageInfo_t
seL4_GetTag(void)

15
libsel4/arch_include/x86/sel4/arch/mapping.h
View file

@ -11,19 +11,6 @@
#ifndef __LIBSEL4_ARCH_MAPPING
#define __LIBSEL4_ARCH_MAPPING
#include <autoconf.h>
#define SEL4_MAPPING_LOOKUP_LEVEL 2
#ifdef CONFIG_PAE_PAGING
#define SEL4_MAPPING_LOOKUP_NO_PT 21
#define SEL4_MAPPING_LOOKUP_NO_PD 30
#else
#define SEL4_MAPPING_LOOKUP_NO_PT 22
#endif
static inline seL4_Word seL4_MappingFailedLookupLevel()
{
return seL4_GetMR(SEL4_MAPPING_LOOKUP_LEVEL);
}
#include <sel4/sel4_arch/mapping.h>
#endif

11
libsel4/arch_include/x86/sel4/arch/objecttype.h
View file

@ -16,20 +16,23 @@
#endif /* HAVE_AUTOCONF */
typedef enum _object {
seL4_IA32_4K = seL4_NonArchObjectTypeCount,
seL4_IA32_4K = seL4_ModeObjectTypeCount,
seL4_IA32_LargePage,
seL4_IA32_PageTableObject,
seL4_IA32_PageDirectoryObject,
seL4_IA32_PDPTObject,
#ifdef CONFIG_IOMMU
seL4_IA32_IOPageTableObject,
#endif
seL4_ObjectTypeCount
} seL4_ArchObjectType;
typedef seL4_Word object_t;
/* Previously frame types were explcitly 4K and 4M. If not PAE
* we assume legacy environment and emulate old definitions */
#ifndef CONFIG_PAE_PAGING
#define seL4_IA32_4M seL4_IA32_LargePage
#endif
#ifndef CONFIG_IOMMU
#define seL4_IA32_IOPageTableObject 0xffffff
#endif
#endif

16
libsel4/arch_include/x86/sel4/arch/simple_types.h
View file

@ -8,19 +8,3 @@
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_ARCH_SIMPLE_TYPES_H_
#define __LIBSEL4_ARCH_SIMPLE_TYPES_H_
typedef signed char seL4_Int8;
typedef signed short seL4_Int16;
typedef signed int seL4_Int32;
typedef signed long long seL4_Int64;
typedef unsigned char seL4_Uint8;
typedef unsigned short seL4_Uint16;
typedef unsigned int seL4_Uint32;
typedef unsigned long long seL4_Uint64;
#endif // __LIBSEL4_ARCH_SIMPLE_TYPES_H_

638
libsel4/arch_include/x86/sel4/arch/syscalls.h
View file

@ -13,655 +13,19 @@
#include <autoconf.h>
#include <sel4/arch/functions.h>
#include <sel4/sel4_arch/syscalls.h>
#include <sel4/types.h>
static inline void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (seL4_GetMR(0)),
"c" (seL4_GetMR(1))
: "%edx"
);
}
static inline void
seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0 != seL4_Null ? *mr0 : 0),
"c" (mr1 != seL4_Null ? *mr1 : 0)
: "%edx"
);
}
static inline void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysNBSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (seL4_GetMR(0)),
"c" (seL4_GetMR(1))
: "%edx"
);
}
static inline void
seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysNBSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0 != seL4_Null ? *mr0 : 0),
"c" (mr1 != seL4_Null ? *mr1 : 0)
: "%edx"
);
}
static inline void
seL4_Reply(seL4_MessageInfo_t msgInfo)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysReply),
"S" (msgInfo.words[0]),
"D" (seL4_GetMR(0)),
"c" (seL4_GetMR(1))
: "%ebx", "%edx"
);
}
static inline void
seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \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"
);
}
static inline void
seL4_Signal(seL4_CPtr dest)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysSend),
"b" (dest),
"S" (seL4_MessageInfo_new(0, 0, 0, 1).words[0])
: "%ecx", "%edx"
);
}
static inline seL4_MessageInfo_t
seL4_Recv(seL4_CPtr src, seL4_Word* sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (mr0),
"=c" (mr1)
: "a" (seL4_SysRecv),
"b" (src)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
if (sender) {
*sender = badge;
}
return info;
}
static inline void
seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_Recv(src, sender);
}
static inline seL4_MessageInfo_t
seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender,
seL4_Word *mr0, seL4_Word *mr1)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (msg0),
"=c" (msg1)
: "a" (seL4_SysRecv),
"b" (src)
: "%edx", "memory"
);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_NBRecv(seL4_CPtr src, seL4_Word* sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (mr0),
"=c" (mr1)
: "a" (seL4_SysNBRecv),
"b" (src)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_Poll(seL4_CPtr src, seL4_Word *sender)
{
return seL4_NBRecv(src, sender);
}
static inline seL4_MessageInfo_t
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
seL4_MessageInfo_t info;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \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 */
: "a" (seL4_SysCall),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0),
"c" (mr1)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
return info;
}
static inline seL4_MessageInfo_t
seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
seL4_MessageInfo_t info;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \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 */
: "a" (seL4_SysCall),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (msg0),
"c" (msg1)
: "%edx", "memory"
);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (mr0),
"=c" (mr1)
: "a" (seL4_SysReplyRecv),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0),
"c" (mr1)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (msg0),
"=c" (msg1)
: "a" (seL4_SysReplyRecv),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (msg0),
"c" (msg1)
: "%edx", "memory"
);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (sender) {
*sender = badge;
}
return info;
}
static inline void
seL4_Yield(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysYield)
: "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#if defined(SEL4_DEBUG_KERNEL)
static inline void
seL4_DebugPutChar(char c)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugPutChar),
"b" (c)
: "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#ifdef SEL4_DEBUG_KERNEL
static inline void
seL4_DebugHalt(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugHalt)
: "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#if defined(SEL4_DEBUG_KERNEL)
static inline void
seL4_DebugSnapshot(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugSnapshot)
: "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#ifdef SEL4_DEBUG_KERNEL
static inline seL4_Uint32
seL4_DebugCapIdentify(seL4_CPtr cap)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
: "=b"(cap)
: "a"(seL4_SysDebugCapIdentify), "b"(cap)
: "%ecx", "%edx", "%esi", "%edi", "memory"
);
return (seL4_Uint32)cap;
}
#endif
#ifdef SEL4_DEBUG_KERNEL
char *strcpy(char *, const char *);
static inline void
seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
{
strcpy((char*)seL4_GetIPCBuffer()->msg, name);
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a"(seL4_SysDebugNameThread), "b"(tcb)
: "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#if defined(SEL4_DANGEROUS_CODE_INJECTION_KERNEL)
static inline void
seL4_DebugRun(void (*userfn) (void *), void* userarg)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugRun),
"b" (userfn),
"S" (userarg)
: "%ecx", "%edx", "%edi", "memory"
);
}
#endif
#if CONFIG_MAX_NUM_TRACE_POINTS > 0
static inline void
seL4_BenchmarkResetLog(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysBenchmarkResetLog)
: "%ecx", "%edx", "%edi", "memory"
);
}
static inline seL4_Uint32
seL4_BenchmarkDumpLog(seL4_Word start, seL4_Word size)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
: "=b" (start)
: "a" (seL4_SysBenchmarkDumpLog),
"b" (start),
"S" (size)
: "%ecx", "%edx", "%edi", "memory"
);
return (seL4_Uint32) start;
}
static inline seL4_Uint32
seL4_BenchmarkLogSize(void)
{
seL4_Uint32 ret = 0;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
: "=b" (ret)
: "a" (seL4_SysBenchmarkLogSize)
: "%ecx", "%edx", "%edi", "memory"
);
return ret;
}
static inline void
seL4_BenchmarkFinalizeLog(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysBenchmarkFinalizeLog)
: "%ecx", "%edx", "%edi", "memory"
);
}
#endif /* CONFIG_MAX_NUM_TRACE_POINTS > 0 */
#endif

37
libsel4/arch_include/x86/sel4/arch/types.h
View file

@ -13,51 +13,18 @@
#include <autoconf.h>
#include <sel4/simple_types.h>
#define seL4_WordBits 32
#define seL4_PageBits 12
#define seL4_SlotBits 4
#define seL4_TCBBits 10
#define seL4_EndpointBits 4
#define seL4_NotificationBits 4
#define seL4_PageTableBits 12
#define seL4_PageDirBits 12
#define seL4_IOPageTableBits 12
#ifdef CONFIG_PAE_PAGING
#define seL4_PDPTBits 5
#define seL4_LargePageBits 21
#else
#define seL4_LargePageBits 22
#endif
/* Previously large frames were explicitly assumed to be 4M. If not using
* PAE assuming a legacy environment and leave the old definition */
#ifndef CONFIG_PAE_PAGING
#define seL4_4MBits seL4_LargePageBits
#endif
typedef seL4_Uint32 seL4_Word;
typedef seL4_Word seL4_CPtr;
#include <sel4/sel4_arch/types.h>
typedef seL4_CPtr seL4_IA32_ASIDControl;
typedef seL4_CPtr seL4_IA32_ASIDPool;
typedef seL4_CPtr seL4_IA32_IOSpace;
typedef seL4_CPtr seL4_IA32_IOPort;
typedef seL4_CPtr seL4_IA32_Page;
typedef seL4_CPtr seL4_IA32_PDPT;
typedef seL4_CPtr seL4_IA32_PageDirectory;
typedef seL4_CPtr seL4_IA32_PageTable;
typedef seL4_CPtr seL4_IA32_IOPageTable;
/* User context as used by seL4_TCB_ReadRegisters / seL4_TCB_WriteRegisters */
typedef struct seL4_UserContext_ {
/* frameRegisters */
seL4_Word eip, esp, eflags, eax, ebx, ecx, edx, esi, edi, ebp;
/* gpRegisters */
seL4_Word tls_base, fs, gs;
} seL4_UserContext;
typedef enum {
seL4_IA32_Default_VMAttributes = 0,
seL4_IA32_WriteBack = 0,

1
libsel4/include/sel4/deprecated.h
View file

@ -12,6 +12,7 @@
#define __LIBSEL4_DEPRECATED_H
#include <sel4/arch/deprecated.h>
#include <sel4/sel4_arch/deprecated.h>
static inline int __attribute__((deprecated("use seL4_IRQHandler_SetNotification")))
seL4_IRQHandler_SetEndpoint(seL4_CPtr irq_handler, seL4_CPtr endpoint)

3
libsel4/include/sel4/messages.h
View file

@ -14,5 +14,8 @@
#include <sel4/arch/pfIPC.h> /* format of pagefault ipc */
#include <sel4/arch/exIPC.h> /* format of exception ipc */
#include <sel4/arch/mapping.h> /* format and meaning of errors for mapping invocations */
#include <sel4/sel4_arch/pfIPC.h> /* format of pagefault ipc */
#include <sel4/sel4_arch/exIPC.h> /* format of exception ipc */
#include <sel4/sel4_arch/mapping.h> /* format and meaning of errors for mapping invocations */
#endif

1
libsel4/include/sel4/sel4.h
View file

@ -14,6 +14,7 @@
#include <sel4/types.h>
#include <sel4/arch/syscalls.h>
#include <sel4/sel4_arch/syscalls.h>
#include <sel4/invocation.h>
#include <interfaces/sel4_client.h>

1
libsel4/include/sel4/simple_types.h
View file

@ -13,6 +13,7 @@
/* Get the architectural types seL4_{u}int{N} */
#include <sel4/arch/simple_types.h>
#include <sel4/sel4_arch/simple_types.h>
/* Define boolean type and true/false */
#define seL4_True 1

1
libsel4/include/sel4/types.h
View file

@ -14,6 +14,7 @@
#include <sel4/simple_types.h>
#include <sel4/macros.h>
#include <sel4/arch/types.h>
#include <sel4/sel4_arch/types.h>
#include <sel4/types_gen.h>
#include <sel4/syscall.h>
#include <sel4/objecttype.h>

12
libsel4/sel4_arch_include/arm/interfaces/sel4arch.xml Normal file
View file

@ -0,0 +1,12 @@
<?xml version="1.0" ?>
<!--
Copyright 2014, NICTA
This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
@TAG(NICTA_BSD)
-->
<api>
</api>

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/constants.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_CONSTANTS_H
#define __LIBSEL4_SEL4_ARCH_CONSTANTS_H
#endif

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/deprecated.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_DEPRECATED_H
#define __LIBSEL4_SEL4_ARCH_DEPRECATED_H
#endif /* __ARCH_DEPRECATED_H__ */

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/exIPC.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_EXCEPTION_IPC
#define __LIBSEL4_SEL4_ARCH_EXCEPTION_IPC
#endif

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/functions.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_FUNCTIONS_H
#define __LIBSEL4_SEL4_ARCH_FUNCTIONS_H
#endif

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/mapping.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_MAPPING
#define __LIBSEL4_SEL4_ARCH_MAPPING
#endif

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/objecttype.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __SEL4_ARCH_OBJECT_TYPE_H
#define __SEL4_ARCH_OBJECT_TYPE_H
#endif

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/pfIPC.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_PAGEFAULT_IPC
#define __LIBSEL4_SEL4_ARCH_PAGEFAULT_IPC
#endif

15
libsel4/sel4_arch_include/arm/sel4/sel4_arch/simple_types.h Normal file
View file

@ -0,0 +1,15 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_SIMPLE_TYPES_H_
#define __LIBSEL4_SEL4_ARCH_SIMPLE_TYPES_H_
#endif // __LIBSEL4_SEL4_ARCH_SIMPLE_TYPES_H_

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/syscalls.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_SYSCALLS_H
#define __LIBSEL4_SEL4_ARCH_SYSCALLS_H
#endif

14
libsel4/sel4_arch_include/arm/sel4/sel4_arch/types.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_TYPES_H
#define __LIBSEL4_SEL4_ARCH_TYPES_H
#endif

27
libsel4/sel4_arch_include/ia32/interfaces/sel4arch.xml Normal file
View file

@ -0,0 +1,27 @@
<?xml version="1.0" ?>
<!--
Copyright 2014, NICTA
This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
@TAG(NICTA_BSD)
-->
<api>
<struct name="seL4_UserContext">
<member name="eip"/>
<member name="esp"/>
<member name="eflags"/>
<member name="eax"/>
<member name="ebx"/>
<member name="ecx"/>
<member name="edx"/>
<member name="esi"/>
<member name="edi"/>
<member name="ebp"/>
<member name="tls_base"/>
<member name="fs"/>
<member name="gs"/>
</struct>
</api>

22
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h Normal file
View file

@ -0,0 +1,22 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_CONSTANTS_H
#define __LIBSEL4_SEL4_ARCH_CONSTANTS_H
#include <autoconf.h>
#define TLS_GDT_ENTRY 6
#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3)
#define IPCBUF_GDT_ENTRY 7
#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3)
#endif

18
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/deprecated.h Normal file
View file

@ -0,0 +1,18 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_DEPRECATED_H
#define __LIBSEL4_SEL4_ARCH_DEPRECATED_H
#include <autoconf.h>
#include <sel4/types.h>
#include <sel4/arch/syscalls.h>
#endif /* __ARCH_DEPRECATED_H__ */

102
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/exIPC.h Normal file
View file

@ -0,0 +1,102 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_EXCEPTION_IPC
#define __LIBSEL4_SEL4_ARCH_EXCEPTION_IPC
/**
* NOT A STANDALONE INCLUDE
*/
/* Unknown syscall exception message. */
#define SEL4_EXCEPT_IPC_LABEL 3
/* User exception (such as divide by zero) message. */
#define SEL4_USER_EXCEPTION_LABEL 4
#define SEL4_USER_EXCEPTION_LENGTH 5
typedef enum {
EXCEPT_IPC_USER_MR_FAULT_IP,
EXCEPT_IPC_USER_MR_ESP,
EXCEPT_IPC_USER_MR_EFLAGS,
EXCEPT_IPC_USER_MR_NUMBER,
EXCEPT_IPC_USER_MR_CODE,
SEL4_USER_EXCEPT_IPC_LENGTH
} seL4_UserExceptIPCRegister;
typedef enum {
EXCEPT_IPC_SYS_MR_EAX,
EXCEPT_IPC_SYS_MR_EBX,
EXCEPT_IPC_SYS_MR_ECX,
EXCEPT_IPC_SYS_MR_EDX,
EXCEPT_IPC_SYS_MR_ESI,
EXCEPT_IPC_SYS_MR_EDI,
EXCEPT_IPC_SYS_MR_EBP,
EXCEPT_IPC_SYS_MR_EIP,
EXCEPT_IPC_SYS_MR_ESP,
EXCEPT_IPC_SYS_MR_EFLAGS,
EXCEPT_IPC_SYS_MR_SYSCALL,
SEL4_EXCEPT_IPC_LENGTH,
} seL4_ExceptIPCRegister;
typedef union {
struct {
seL4_Word fault_ip;
seL4_Word esp;
seL4_Word eflags;
seL4_Word exception_number;
seL4_Word exception_code;
} regs;
seL4_Word raw[5];
} seL4_UserExceptionIpcRegisters;
typedef union {
struct {
seL4_Word eax;
seL4_Word ebx;
seL4_Word ecx;
seL4_Word edx;
seL4_Word esi;
seL4_Word edi;
seL4_Word ebp;
seL4_Word eip;
seL4_Word esp;
seL4_Word eflags;
seL4_Word syscall;
} regs;
seL4_Word raw[11];
} seL4_ExceptionIpcRegisters;
static inline seL4_Word seL4_isExceptIPC_Tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == SEL4_EXCEPT_IPC_LABEL;
}
static inline seL4_Word seL4_ExceptIPC_Get(seL4_Word mr)
{
return seL4_GetMR(mr);
}
static inline void seL4_ExceptIPC_Set(seL4_Word index, seL4_Word val)
{
seL4_SetMR(index, val);
}
static inline seL4_Word seL4_IsArchSyscallFrom(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_length(tag) == SEL4_EXCEPT_IPC_LENGTH;
}
static inline seL4_Word seL4_IsArchExceptionFrom(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_length(tag) == SEL4_USER_EXCEPTION_LENGTH;
}
#endif

59
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/functions.h Normal file
View file

@ -0,0 +1,59 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_FUNCTIONS_H
#define __LIBSEL4_SEL4_ARCH_FUNCTIONS_H
#include <sel4/types.h>
#include <sel4/macros.h>
/* the segment loaded into GS points directly to the IPC buffer */
#define SEL4_GET_IPCBUF_SCALE(field, i, res) \
do {\
asm volatile ("movl %%gs:%c2(,%1,%c3), %0"\
: [result] "=r" (res) /* outputs */\
: [scale] "r" (i), /* inputs */\
[offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)),\
[scale_factor] "i" (sizeof(seL4_Word))\
/* no clobber */);\
} while(0)
#define SEL4_SET_IPCBUF_SCALE(field, i, val) \
do {\
asm volatile ("movl %0, %%gs:%c2(,%1,%c3)"\
: /* no outputs */\
: [value] "r" (val), /* inputs */\
[scale] "r" (i),\
[offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)),\
[scale_factor] "i" (sizeof(seL4_Word))\
: "memory"); /* clobber */\
} while(0)
#define SEL4_GET_IPCBUF(field, res) \
do {\
asm volatile ("movl %%gs:%c1, %0"\
: [result] "=r" (res) /* inputs */\
: [offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field)) /* outputs */\
/* no clobber */);\
} while(0)
#define SEL4_SET_IPCBUF(field, val) \
do {\
asm volatile ("movl %0, %%gs:%c1"\
: /* no outputs */\
: [value] "r" (val), /* inputs */\
[offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field))\
: "memory"); /* clobber */\
} while(0)
#endif

29
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/mapping.h Normal file
View file

@ -0,0 +1,29 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_MAPPING
#define __LIBSEL4_SEL4_ARCH_MAPPING
#include <autoconf.h>
#define SEL4_MAPPING_LOOKUP_LEVEL 2
#ifdef CONFIG_PAE_PAGING
#define SEL4_MAPPING_LOOKUP_NO_PT 21
#define SEL4_MAPPING_LOOKUP_NO_PD 30
#else
#define SEL4_MAPPING_LOOKUP_NO_PT 22
#endif
static inline seL4_Word seL4_MappingFailedLookupLevel()
{
return seL4_GetMR(SEL4_MAPPING_LOOKUP_LEVEL);
}
#endif

31
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/objecttype.h Normal file
View file

@ -0,0 +1,31 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __SEL4_ARCH_OBJECT_TYPE_H
#define __SEL4_ARCH_OBJECT_TYPE_H
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif /* HAVE_AUTOCONF */
typedef enum _mode_object {
#ifdef CONFIG_PAE_PAGING
seL4_IA32_PDPTObject = seL4_NonArchObjectTypeCount,
seL4_ModeObjectTypeCount
#else
seL4_ModeObjectTypeCount = seL4_NonArchObjectTypeCount,
#endif
} seL4_ModeObjectType;
#ifndef CONFIG_PAE_PAGING
#define seL4_IA32_PDPTObject 0xffffffff
#endif
#endif

14
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/pfIPC.h Normal file
View file

@ -0,0 +1,14 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_PAGEFAULT_IPC
#define __LIBSEL4_SEL4_ARCH_PAGEFAULT_IPC
#endif

26
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/simple_types.h Normal file
View file

@ -0,0 +1,26 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_SIMPLE_TYPES_H_
#define __LIBSEL4_SEL4_ARCH_SIMPLE_TYPES_H_
typedef signed char seL4_Int8;
typedef signed short seL4_Int16;
typedef signed int seL4_Int32;
typedef signed long long seL4_Int64;
typedef unsigned char seL4_Uint8;
typedef unsigned short seL4_Uint16;
typedef unsigned int seL4_Uint32;
typedef unsigned long long seL4_Uint64;
#endif // __LIBSEL4_SEL4_ARCH_SIMPLE_TYPES_H_

655
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h Normal file
View file

@ -0,0 +1,655 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_SYSCALLS_H
#define __LIBSEL4_SEL4_ARCH_SYSCALLS_H
#include <autoconf.h>
#include <sel4/arch/functions.h>
#include <sel4/types.h>
static inline void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (seL4_GetMR(0)),
"c" (seL4_GetMR(1))
: "%edx"
);
}
static inline void
seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0 != seL4_Null ? *mr0 : 0),
"c" (mr1 != seL4_Null ? *mr1 : 0)
: "%edx"
);
}
static inline void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysNBSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (seL4_GetMR(0)),
"c" (seL4_GetMR(1))
: "%edx"
);
}
static inline void
seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysNBSend),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0 != seL4_Null ? *mr0 : 0),
"c" (mr1 != seL4_Null ? *mr1 : 0)
: "%edx"
);
}
static inline void
seL4_Reply(seL4_MessageInfo_t msgInfo)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysReply),
"S" (msgInfo.words[0]),
"D" (seL4_GetMR(0)),
"c" (seL4_GetMR(1))
: "%ebx", "%edx"
);
}
static inline void
seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \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"
);
}
static inline void
seL4_Signal(seL4_CPtr dest)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysSend),
"b" (dest),
"S" (seL4_MessageInfo_new(0, 0, 0, 1).words[0])
: "%ecx", "%edx"
);
}
static inline seL4_MessageInfo_t
seL4_Recv(seL4_CPtr src, seL4_Word* sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (mr0),
"=c" (mr1)
: "a" (seL4_SysRecv),
"b" (src)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender,
seL4_Word *mr0, seL4_Word *mr1)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (msg0),
"=c" (msg1)
: "a" (seL4_SysRecv),
"b" (src)
: "%edx", "memory"
);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_NBRecv(seL4_CPtr src, seL4_Word* sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0;
seL4_Word mr1;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (mr0),
"=c" (mr1)
: "a" (seL4_SysNBRecv),
"b" (src)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
seL4_MessageInfo_t info;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \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 */
: "a" (seL4_SysCall),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0),
"c" (mr1)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
return info;
}
static inline seL4_MessageInfo_t
seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
seL4_MessageInfo_t info;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \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 */
: "a" (seL4_SysCall),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (msg0),
"c" (msg1)
: "%edx", "memory"
);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (mr0),
"=c" (mr1)
: "a" (seL4_SysReplyRecv),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (mr0),
"c" (mr1)
: "%edx", "memory"
);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);
if (sender) {
*sender = badge;
}
return info;
}
static inline seL4_MessageInfo_t
seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
asm volatile (
"pushl %%ebp \n"
"movl %%ecx, %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"movl %%ebp, %%ecx \n"
"popl %%ebp \n"
:
"=b" (badge),
"=S" (info.words[0]),
"=D" (msg0),
"=c" (msg1)
: "a" (seL4_SysReplyRecv),
"b" (dest),
"S" (msgInfo.words[0]),
"D" (msg0),
"c" (msg1)
: "%edx", "memory"
);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (sender) {
*sender = badge;
}
return info;
}
static inline void
seL4_Yield(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysYield)
: "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#if defined(SEL4_DEBUG_KERNEL)
static inline void
seL4_DebugPutChar(char c)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugPutChar),
"b" (c)
: "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#ifdef SEL4_DEBUG_KERNEL
static inline void
seL4_DebugHalt(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugHalt)
: "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#if defined(SEL4_DEBUG_KERNEL)
static inline void
seL4_DebugSnapshot(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugSnapshot)
: "%ebx", "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#ifdef SEL4_DEBUG_KERNEL
static inline seL4_Uint32
seL4_DebugCapIdentify(seL4_CPtr cap)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
: "=b"(cap)
: "a"(seL4_SysDebugCapIdentify), "b"(cap)
: "%ecx", "%edx", "%esi", "%edi", "memory"
);
return (seL4_Uint32)cap;
}
#endif
#ifdef SEL4_DEBUG_KERNEL
char *strcpy(char *, const char *);
static inline void
seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
{
strcpy((char*)seL4_GetIPCBuffer()->msg, name);
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a"(seL4_SysDebugNameThread), "b"(tcb)
: "%ecx", "%edx", "%esi", "%edi", "memory"
);
}
#endif
#if defined(SEL4_DANGEROUS_CODE_INJECTION_KERNEL)
static inline void
seL4_DebugRun(void (*userfn) (void *), void* userarg)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysDebugRun),
"b" (userfn),
"S" (userarg)
: "%ecx", "%edx", "%edi", "memory"
);
}
#endif
#if CONFIG_MAX_NUM_TRACE_POINTS > 0
static inline void
seL4_BenchmarkResetLog(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysBenchmarkResetLog)
: "%ecx", "%edx", "%edi", "memory"
);
}
static inline seL4_Uint32
seL4_BenchmarkDumpLog(seL4_Word start, seL4_Word size)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
: "=b" (start)
: "a" (seL4_SysBenchmarkDumpLog),
"b" (start),
"S" (size)
: "%ecx", "%edx", "%edi", "memory"
);
return (seL4_Uint32) start;
}
static inline seL4_Uint32
seL4_BenchmarkLogSize(void)
{
seL4_Uint32 ret = 0;
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
: "=b" (ret)
: "a" (seL4_SysBenchmarkLogSize)
: "%ecx", "%edx", "%edi", "memory"
);
return ret;
}
static inline void
seL4_BenchmarkFinalizeLog(void)
{
asm volatile (
"pushl %%ebp \n"
"movl %%esp, %%ecx \n"
"leal 1f, %%edx \n"
"1: \n"
"sysenter \n"
"popl %%ebp \n"
:
: "a" (seL4_SysBenchmarkFinalizeLog)
: "%ecx", "%edx", "%edi", "memory"
);
}
#endif /* CONFIG_MAX_NUM_TRACE_POINTS > 0 */
#endif

52
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/types.h Normal file
View file

@ -0,0 +1,52 @@
/*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*/
#ifndef __LIBSEL4_SEL4_ARCH_TYPES_H
#define __LIBSEL4_SEL4_ARCH_TYPES_H
#include <autoconf.h>
#include <sel4/simple_types.h>
#define seL4_WordBits 32
#define seL4_PageBits 12
#define seL4_SlotBits 4
#define seL4_TCBBits 10
#define seL4_EndpointBits 4
#define seL4_NotificationBits 4
#define seL4_PageTableBits 12
#define seL4_PageDirBits 12
#define seL4_IOPageTableBits 12
#ifdef CONFIG_PAE_PAGING
#define seL4_PDPTBits 5
#define seL4_LargePageBits 21
#else
#define seL4_LargePageBits 22
#endif
/* Previously large frames were explicitly assumed to be 4M. If not using
* PAE assuming a legacy environment and leave the old definition */
#ifndef CONFIG_PAE_PAGING
#define seL4_4MBits seL4_LargePageBits
#endif
typedef seL4_Uint32 seL4_Word;
typedef seL4_Word seL4_CPtr;
/* User context as used by seL4_TCB_ReadRegisters / seL4_TCB_WriteRegisters */
typedef struct seL4_UserContext_ {
/* frameRegisters */
seL4_Word eip, esp, eflags, eax, ebx, ecx, edx, esi, edi, ebp;
/* gpRegisters */
seL4_Word tls_base, fs, gs;
} seL4_UserContext;
#endif

4
libsel4/tools/syscall_stub_gen.py
View file

@ -58,7 +58,7 @@ MAX_MESSAGE_LENGTH = 32
MESSAGE_REGISTERS_FOR_ARCH = {
"arm": 4,
"x86": 2,
"ia32": 2,
}
# Headers to include
@ -233,7 +233,7 @@ arch_types = {
StructType("seL4_UserContext", WORD_SIZE_BITS * 17),
],
"x86" : [
"ia32" : [
Type("seL4_IA32_VMAttributes", WORD_SIZE_BITS),
CapType("seL4_IA32_ASIDControl"),
CapType("seL4_IA32_ASIDPool"),

29
tools/invocation_header_gen.py
View file

@ -44,24 +44,42 @@ enum invocation_label {
};
{{if libsel4}}
#include <sel4/sel4_arch/invocation.h>
#include <sel4/arch/invocation.h>
{{endif}}
#endif /* __{{header_title}}_INVOCATION_H */
"""
SEL4_ARCH_INVOCATION_TEMPLATE = COMMON_HEADER + """
#ifndef __{{header_title}}_SEL4_ARCH_INVOCATION_H
#define __{{header_title}}_SEL4_ARCH_INVOCATION_H
{{if not libsel4}}
#include <api/invocation.h>
{{endif}}
enum sel4_arch_invocation_label {
{{for loop, label in looper(invocations)}}
{{label}} = nInvocationLabels + {{loop.index}},
{{endfor}}
nSeL4ArchInvocationLabels
};
#endif /* __{{header_title}}_SEL4_ARCH_INVOCATION_H */
"""
ARCH_INVOCATION_TEMPLATE = COMMON_HEADER + """
#ifndef __{{header_title}}_ARCH_INVOCATION_H
#define __{{header_title}}_ARCH_INVOCATION_H
{{if not libsel4}}
#include <api/invocation.h>
#include <arch/api/sel4_invocation.h>
{{endif}}
enum arch_invocation_label {
{{for loop, label in looper(invocations)}}
{{label}} = nInvocationLabels + {{loop.index}},
{{label}} = nSeL4ArchInvocationLabels + {{loop.index}},
{{endfor}}
nArchInvocationLabels
};
@ -78,8 +96,11 @@ def parse_args():
help='Name of file to create', required=True)
parser.add_argument('--libsel4', action='store_true',
help='Is this being generated for libsel4?')
parser.add_argument('--arch', action='store_true',
group = parser.add_mutually_exclusive_group()
group.add_argument('--arch', action='store_true',
help='Is this being generated for the arch layer?')
group.add_argument('--sel4_arch', action='store_true',
help='Is this being generated for the seL4 arch layer?')
return parser.parse_args()
@ -104,6 +125,8 @@ def generate(args, invocations):
if args.arch:
template = tempita.Template(ARCH_INVOCATION_TEMPLATE)
elif args.sel4_arch:
template = tempita.Template(SEL4_ARCH_INVOCATION_TEMPLATE)
else:
template = tempita.Template(INVOCATION_TEMPLATE)