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

x64/libsel4: Add x64 libsel4 implementation

Browse source
This commit is contained in:
Adrian Danis 2016-09-27 10:58:24 +10:00
parent 7f9970e5e2
commit 067b71cad4
20 changed files with 1143 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
include/arch/x86/arch/64/mode/api/constants.h Symbolic link
View file

@ -0,0 +1 @@
../../../../../../../libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h

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

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

1
include/arch/x86/arch/64/mode/api/shared_types.bf Symbolic link
View file

@ -0,0 +1 @@
../../../../../../../libsel4/include/sel4/shared_types_64.bf

4
libsel4/Makefile
View file

@ -22,8 +22,12 @@ endif
ifeq (${KERNEL_32}, y)
TYPE_SUFFIX:=32
else
ifeq (${KERNEL_64}, y)
TYPE_SUFFIX:=64
else
$(error Cannot determine TYPE_SUFFIX)
endif
endif
# Targets
PRIORITY_TARGETS := include/interfaces/sel4_client.h include/sel4/types_gen.h include/sel4/syscall.h \

30
libsel4/include/sel4/shared_types_64.bf Normal file
View file

@ -0,0 +1,30 @@
--
-- Copyright 2016, Data61
-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-- ABN 41 687 119 230.
--
-- 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(D61_BSD)
--
-- this file contains types shared between libsel4 and the kernel
base 64
block seL4_MessageInfo {
padding 32
field label 20
field capsUnwrapped 3
field extraCaps 2
field length 7
}
block seL4_PrioProps {
padding 32
padding 16
field mcp 8
field prio 8
}

39
libsel4/include/sel4/types_64.bf Normal file
View file

@ -0,0 +1,39 @@
--
-- Copyright 2016, Data61
-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-- ABN 41 687 119 230.
--
-- 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(D61_BSD)
--
base 64
block Guard {
padding 32
field CapDataType 1
padding 5
field GuardBits 18
field GuardSize 6
padding 2
}
block Badge {
padding 32
field CapDataType 1
padding 3
field Badge 28
}
-- The ordering of these tags is important. The padding bits in the guard
-- Can be set and will be ignored by the kernel, but the padding bits in Badge
-- must be 0
tagged_union seL4_CapData CapDataType {
tag Badge 0
tag Guard 1
}

45
libsel4/sel4_arch_include/x86_64/interfaces/sel4arch.xml Normal file
View file

@ -0,0 +1,45 @@
<?xml version="1.0" ?>
<!--
Copyright 2016, Data61
Commonwealth Scientific and Industrial Research Organisation (CSIRO)
ABN 41 687 119 230.
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(D61_BSD)
-->
<api>
<struct name="seL4_UserContext">
<member name="rip"/>
<member name="rsp"/>
<member name="rflags"/>
<member name="rax"/>
<member name="rbx"/>
<member name="rcx"/>
<member name="rdx"/>
<member name="rsi"/>
<member name="rdi"/>
<member name="rbp"/>
<member name="r8"/>
<member name="r9"/>
<member name="r10"/>
<member name="r11"/>
<member name="r12"/>
<member name="r13"/>
<member name="r14"/>
<member name="r15"/>
<member name="tls_base"/>
</struct>
<interface name="seL4_X86_PDPT">
<method id="X86PDPTMap" name="Map">
<param dir="in" name="pml4" type="seL4_X64_PML4"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
</method>
<method id="X86PDPTUnmap" name="Unmap">
</method>
</interface>
</api>

40
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h Normal file
View file

@ -0,0 +1,40 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#include <autoconf.h>
#define TLS_GDT_ENTRY 7
#define TLS_GDT_SELECTOR ((TLS_GDT_ENTRY << 3) | 3)
#define IPCBUF_GDT_ENTRY 8
#define IPCBUF_GDT_SELECTOR ((IPCBUF_GDT_ENTRY << 3) | 3)
#define seL4_DataFault 0
#define seL4_InstructionFault 1
/* for x86-64, the large page size is 2 MiB and huge page size is 1 GiB */
#define seL4_WordBits 64
#define seL4_PageBits 12
#define seL4_SlotBits 5
#define seL4_TCBBits 11
#define seL4_EndpointBits 4
#define seL4_NotificationBits 5
#define seL4_PageTableBits 12
#define seL4_PageDirBits 12
#define seL4_PDPTBits 12
#define seL4_PML4Bits 12
#define seL4_IOPageTableBits 12
#define seL4_LargePageBits 21
#define seL4_HugePageBits 30
#define seL4_ASIDPoolBits 12

17
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/deprecated.h Normal file
View file

@ -0,0 +1,17 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#include <autoconf.h>
#include <sel4/types.h>
#include <sel4/arch/syscalls.h>

117
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/exIPC.h Normal file
View file

@ -0,0 +1,117 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
/**
* 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_RSP,
EXCEPT_IPC_USER_MR_RFLAGS,
EXCEPT_IPC_USER_MR_NUMBER,
EXCEPT_IPC_USER_MR_CODE,
SEL4_USER_EXCEPT_IPC_LENGTH
} seL4_UserExceptIPCRegister;
typedef enum {
EXCEPT_IPC_SYS_MR_RAX,
EXCEPT_IPC_SYS_MR_RBX,
EXCEPT_IPC_SYS_MR_RCX,
EXCEPT_IPC_SYS_MR_RDX,
EXCEPT_IPC_SYS_MR_RSI,
EXCEPT_IPC_SYS_MR_RDI,
EXCEPT_IPC_SYS_MR_RBP,
EXCEPT_IPC_SYS_MR_R8,
EXCEPT_IPC_SYS_MR_R9,
EXCEPT_IPC_SYS_MR_R10,
EXCEPT_IPC_SYS_MR_R11,
EXCEPT_IPC_SYS_MR_R12,
EXCEPT_IPC_SYS_MR_R13,
EXCEPT_IPC_SYS_MR_R14,
EXCEPT_IPC_SYS_MR_R15,
EXCEPT_IPC_SYS_MR_RIP,
EXCEPT_IPC_SYS_MR_RSP,
EXCEPT_IPC_SYS_MR_RFLAGS,
EXCEPT_IPC_SYS_MR_SYSCALL,
SEL4_EXCEPT_IPC_LENGTH,
} seL4_ExceptIPCRegister;
typedef union {
struct {
seL4_Word fault_ip;
seL4_Word rsp;
seL4_Word rflags;
seL4_Word exception_number;
seL4_Word exception_code;
} regs;
seL4_Word raw[5];
} seL4_UserExceptionIpcRegisters;
typedef union {
struct {
seL4_Word rax;
seL4_Word rbx;
seL4_Word rcx;
seL4_Word rdx;
seL4_Word rsi;
seL4_Word rdi;
seL4_Word rbp;
seL4_Word r8;
seL4_Word r9;
seL4_Word r10;
seL4_Word r11;
seL4_Word r12;
seL4_Word r13;
seL4_Word r14;
seL4_Word r15;
seL4_Word rip;
seL4_Word rsp;
seL4_Word rflags;
seL4_Word syscall;
} regs;
seL4_Word raw[19];
} 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;
}

56
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/functions.h Normal file
View file

@ -0,0 +1,56 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#include <sel4/types.h>
/* the segment loaded into GS points directly to the IPC buffer */
#define SEL4_GET_IPCBUF_SCALE(field, i, res) \
do {\
asm volatile ("movq %%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 ("movq %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 ("movq %%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 ("movq %0, %%gs:%c1"\
: /* no outputs */\
: [value] "r" (val), /* inputs */\
[offset] "i" (SEL4_OFFSETOF(seL4_IPCBuffer, field))\
: "memory"); /* clobber */\
} while(0)

22
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/mapping.h Normal file
View file

@ -0,0 +1,22 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#define SEL4_MAPPING_LOOKUP_LEVEL 2
#define SEL4_MAPPING_LOOKUP_NO_PT 21
#define SEL4_MAPPING_LOOKUP_NO_PD 30
#define SEL4_MAPPING_LOOKUP_NO_PDPT 39
static inline seL4_Word seL4_MappingFailedLookupLevel() {
return seL4_GetMR(SEL4_MAPPING_LOOKUP_LEVEL);
}

33
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/objecttype.h Normal file
View file

@ -0,0 +1,33 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif /* HAVE_AUTOCONF */
typedef enum _mode_object {
seL4_X86_PDPTObject = seL4_NonArchObjectTypeCount,
seL4_X64_PML4Object,
#ifdef CONFIG_HUGE_PAGE
seL4_X64_HugePageObject,
#endif
seL4_ModeObjectTypeCount
} seL4_seL4ArchObjectType;
/* allow seL4_X86_PDPTObject and seL4_IA32_PDPTObject to be used interchangeable */
#define seL4_IA32_PDPTObject seL4_X86_PDPTObject
#ifndef CONFIG_HUGE_PAGE
#define seL4_X64_HugePageObject 0xfffffffe
#endif

13
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/pfIPC.h Normal file
View file

@ -0,0 +1,13 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once

23
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/simple_types.h Normal file
View file

@ -0,0 +1,23 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
typedef signed char seL4_Int8;
typedef signed short seL4_Int16;
typedef signed int seL4_Int32;
typedef signed long seL4_Int64;
typedef unsigned char seL4_Uint8;
typedef unsigned short seL4_Uint16;
typedef unsigned int seL4_Uint32;
typedef unsigned long seL4_Uint64;

380
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h Normal file
View file

@ -0,0 +1,380 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#include <autoconf.h>
#if defined(CONFIG_SYSENTER)
#include <sel4/sel4_arch/syscalls_sysenter.h>
#elif defined(CONFIG_SYSCALL)
#include <sel4/sel4_arch/syscalls_syscall.h>
#else
#error Unknown method for kernel syscalls
#endif
static inline void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
x64_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
}
static inline void
seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
x64_sys_send(seL4_SysSend, dest, msgInfo.words[0],
(mr0 != seL4_Null) ? *mr0 : 0,
(mr1 != seL4_Null) ? *mr1 : 0
);
}
static inline void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
x64_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
}
static inline void
seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
x64_sys_send(seL4_SysNBSend, dest, msgInfo.words[0],
(mr0 != seL4_Null) ? *mr0 : 0,
(mr1 != seL4_Null) ? *mr1 : 0
);
}
static inline void
seL4_Reply(seL4_MessageInfo_t msgInfo)
{
x64_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
}
static inline void
seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1)
{
x64_sys_reply(seL4_SysReply, msgInfo.words[0],
(mr0 != seL4_Null) ? *mr0 : 0,
(mr1 != seL4_Null) ? *mr1 : 0
);
}
static inline void
seL4_Signal(seL4_CPtr dest)
{
x64_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 1).words[0]);
}
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;
x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, &mr1);
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;
seL4_Word msg1;
x64_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1);
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;
x64_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, &mr1);
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);
x64_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, &mr1);
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;
}
x64_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1);
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);
x64_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0, &mr1);
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;
}
x64_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1);
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (sender) {
*sender = badge;
}
return info;
}
static inline void
seL4_Yield(void)
{
x64_sys_null(seL4_SysYield);
asm volatile("" ::: "memory");
}
#if defined(SEL4_DEBUG_KERNEL)
static inline void
seL4_DebugPutChar(char c)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
x64_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3);
}
#endif
#ifdef SEL4_DEBUG_KERNEL
static inline void
seL4_DebugHalt(void)
{
x64_sys_null(seL4_SysDebugHalt);
asm volatile("" :::"memory");
}
#endif
#if defined(SEL4_DEBUG_KERNEL)
static inline void
seL4_DebugSnapshot(void)
{
x64_sys_null(seL4_SysDebugSnapshot);
asm volatile("" :::"memory");
}
#endif
#ifdef SEL4_DEBUG_KERNEL
static inline seL4_Uint32
seL4_DebugCapIdentify(seL4_CPtr cap)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
x64_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2);
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);
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
x64_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3);
}
#endif
#if defined(SEL4_DANGEROUS_CODE_INJECTION_KERNEL)
static inline void
seL4_DebugRun(void (*userfn) (void *), void* userarg)
{
x64_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg);
asm volatile("" ::: "memory");
}
#endif
#if CONFIG_ENABLE_BENCHMARKS
static inline void
seL4_BenchmarkResetLog(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word ret;
x64_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2);
return (seL4_Error)ret;
}
static inline void
seL4_BenchmarkFinalizeLog(void)
{
x64_sys_null(seL4_SysBenchmarkFinalizeLog);
asm volatile("" ::: "memory");
}
static inline seL4_Error
seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
x64_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2);
return (seL4_Error) frame_cptr;
}
static inline void
seL4_BenchmarkNullSyscall(void)
{
x64_sys_null(seL4_SysBenchmarkNullSyscall);
asm volatile("" ::: "memory");
}
#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
static inline void
seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
x64_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3);
}
static inline void
seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
x64_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3);
}
#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
#endif /* CONFIG_ENABLE_BENCHMARKS */

131
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_syscall.h Normal file
View file

@ -0,0 +1,131 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#include <autoconf.h>
#include <sel4/arch/functions.h>
#include <sel4/types.h>
static inline void
x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word msg0, seL4_Word msg1)
{
register seL4_Word mr0 asm("r10") = msg0;
register seL4_Word mr1 asm("r8") = msg1;
asm volatile (
"movq %%rsp, %%rbx \n"
"syscall \n"
"movq %%rbx, %%rsp \n"
:
: "d" (sys),
"D" (dest),
"S" (info),
"r" (mr0),
"r" (mr1)
: "%rcx", "%rbx", "r11"
);
}
static inline void
x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0, seL4_Word msg1)
{
register seL4_Word mr0 asm("r10") = msg0;
register seL4_Word mr1 asm("r8") = msg1;
asm volatile (
"movq %%rsp, %%rbx \n"
"syscall \n"
"movq %%rbx, %%rsp \n"
:
: "d" (sys),
"S" (info),
"r" (mr0),
"r" (mr1)
: "%rbx", "%rcx", "%r11"
);
}
static inline void
x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info)
{
asm volatile (
"movq %%rsp, %%rbx \n"
"syscall \n"
"movq %%rbx, %%rsp \n"
:
: "d" (sys),
"D" (dest),
"S" (info)
: "%rcx", "%rbx", "%r11"
);
}
static inline void
x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr0, seL4_Word *out_mr1)
{
register seL4_Word mr0 asm("r10");
register seL4_Word mr1 asm("r8");
asm volatile (
"movq %%rsp, %%rbx \n"
"syscall \n"
"movq %%rbx, %%rsp \n"
: "=D" (*out_badge),
"=S" (*out_info),
"=r" (mr0),
"=r" (mr1)
: "d" (sys),
"D" (src)
: "%rcx", "%rbx", "r11", "memory"
);
*out_mr0 = mr0;
*out_mr1 = mr1;
}
static inline void
x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_dest, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1)
{
register seL4_Word mr0 asm("r10") = *in_out_mr0;
register seL4_Word mr1 asm("r8") = *in_out_mr1;
asm volatile (
"movq %%rsp, %%rbx \n"
"syscall \n"
"movq %%rbx, %%rsp \n"
: "=S" (*out_info),
"=r" (mr0),
"=r" (mr1),
"=D" (*out_dest)
: "d" (sys),
"D" (dest),
"S" (info),
"r" (mr0),
"r" (mr1)
: "%rcx", "%rbx", "r11", "memory"
);
*in_out_mr0 = mr0;
*in_out_mr1 = mr1;
}
static inline void
x64_sys_null(seL4_Word sys)
{
asm volatile (
"movq %%rsp, %%rbx \n"
"syscall \n"
"movq %%rbx, %%rsp \n"
:
: "d" (sys)
: "%rbx", "%rcx", "%rsi", "%rdi", "%r11"
);
}

139
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_sysenter.h Normal file
View file

@ -0,0 +1,139 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#include <autoconf.h>
#include <sel4/arch/functions.h>
#include <sel4/types.h>
static inline void
x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word msg0, seL4_Word msg1)
{
register seL4_Word mr0 asm("r10") = msg0;
register seL4_Word mr1 asm("r8") = msg1;
asm volatile (
"movq %%rsp, %%rcx \n"
"leaq 1f, %%rdx \n"
"1: \n"
"sysenter \n"
:
: "a" (sys),
"D" (dest),
"S" (info),
"r" (mr0),
"r" (mr1)
: "%rcx", "%rdx"
);
}
static inline void
x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0, seL4_Word msg1)
{
register seL4_Word mr0 asm("r10") = msg0;
register seL4_Word mr1 asm("r8") = msg1;
asm volatile (
"movq %%rsp, %%rcx \n"
"leaq 1f, %%rdx \n"
"1: \n"
"sysenter \n"
:
: "a" (sys),
"S" (info),
"r" (mr0),
"r" (mr1)
: "%rdx", "%rcx"
);
}
static inline void
x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info)
{
asm volatile (
"movq %%rsp, %%rcx \n"
"leaq 1f, %%rdx \n"
"1: \n"
"sysenter \n"
:
: "a" (sys),
"D" (dest),
"S" (info)
: "%rcx", "%rdx"
);
}
static inline void
x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr0, seL4_Word *out_mr1)
{
register seL4_Word mr0 asm("r10");
register seL4_Word mr1 asm("r8");
asm volatile (
"movq %%rsp, %%rcx \n"
"leaq 1f, %%rdx \n"
"1: \n"
"sysenter \n"
: "=D" (*out_badge),
"=S" (*out_info),
"=r" (mr0),
"=r" (mr1)
: "a" (sys),
"D" (src)
: "%rcx", "%rdx", "memory"
);
*out_mr0 = mr0;
*out_mr1 = mr1;
}
static inline void
x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_dest, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1)
{
register seL4_Word mr0 asm("r10") = *in_out_mr0;
register seL4_Word mr1 asm("r8") = *in_out_mr1;
asm volatile (
"movq %%rsp, %%rcx \n"
"leaq 1f, %%rdx \n"
"1: \n"
"sysenter \n"
: "=S" (*out_info),
"=r" (mr0),
"=r" (mr1),
"=D" (*out_dest)
: "a" (sys),
"D" (dest),
"S" (info),
"r" (mr0),
"r" (mr1)
: "%rcx", "%rdx", "memory"
);
*in_out_mr0 = mr0;
*in_out_mr1 = mr1;
}
static inline void
x64_sys_null(seL4_Word sys)
{
asm volatile (
"movq %%rsp, %%rcx \n"
"leaq 1f, %%rdx \n"
"1: \n"
"sysenter \n"
:
: "a" (sys)
: "%rbx", "%rcx", "%rdx", "%rsi", "%rdi", "memory"
);
}

33
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/types.h Normal file
View file

@ -0,0 +1,33 @@
/*
* Copyright 2016, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* 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(D61_BSD)
*/
#pragma once
#include <autoconf.h>
#include <sel4/simple_types.h>
typedef seL4_Uint64 seL4_Word;
typedef seL4_Word seL4_NodeId;
typedef seL4_Word seL4_PAddr;
typedef seL4_Word seL4_Domain;
typedef seL4_Word seL4_CPtr;
typedef seL4_CPtr seL4_X64_PML4;
/* User context as used by seL4_TCB_ReadRegisters / seL4_TCB_WriteRegisters */
typedef struct seL4_UserContext_ {
seL4_Word rip, rsp, rflags, rax, rbx, rcx, rdx, rsi, rdi, rbp,
r8, r9, r10, r11, r12, r13, r14, r15;
seL4_Word tls_base;
} seL4_UserContext;

20
libsel4/tools/syscall_stub_gen.py
View file

@ -207,7 +207,8 @@ class Parameter(object):
def init_data_types(wordsize):
types = [
# Simple Types
Type("int", wordsize, wordsize),
Type("int", 32, wordsize),
Type("long", wordsize, wordsize),
Type("seL4_Uint8", 8, wordsize),
Type("seL4_Uint16", 16, wordsize),
@ -272,6 +273,21 @@ def init_arch_types(wordsize):
CapType("seL4_X86_PageTable", wordsize),
CapType("seL4_X86_IOPageTable", wordsize),
StructType("seL4_UserContext", wordsize * 13, wordsize),
],
"x86_64" : [
Type("seL4_X86_VMAttributes", wordsize, wordsize),
CapType("seL4_X86_IOPort", wordsize),
CapType("seL4_X86_ASIDControl", wordsize),
CapType("seL4_X86_ASIDPool", wordsize),
CapType("seL4_X86_IOSpace", wordsize),
CapType("seL4_X86_Page", wordsize),
CapType("seL4_X64_PML4", wordsize),
CapType("seL4_X86_PDPT", wordsize),
CapType("seL4_X86_PageDirectory", wordsize),
CapType("seL4_X86_PageTable", wordsize),
CapType("seL4_X86_IOPageTable", wordsize),
StructType("seL4_UserContext", wordsize * 19, wordsize),
]
}
@ -509,7 +525,7 @@ def generate_stub(arch, wordsize, interface_name, method_name, method_id, input_
return_type = "%s_%s_t" % (interface_name, method_name)
returning_struct = True
else:
return_type = "int"
return_type = "long"
#
# Print function header.