diff --git a/include/arch/x86/arch/64/mode/api/constants.h b/include/arch/x86/arch/64/mode/api/constants.h
new file mode 120000
index 000000000..14388a203
--- /dev/null
+++ b/include/arch/x86/arch/64/mode/api/constants.h
@@ -0,0 +1 @@
+../../../../../../../libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
\ No newline at end of file
diff --git a/include/arch/x86/arch/64/mode/api/objecttype.h b/include/arch/x86/arch/64/mode/api/objecttype.h
new file mode 120000
index 000000000..ef410dd0d
--- /dev/null
+++ b/include/arch/x86/arch/64/mode/api/objecttype.h
@@ -0,0 +1 @@
+../../../../../../../libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/objecttype.h
\ No newline at end of file
diff --git a/include/arch/x86/arch/64/mode/api/shared_types.bf b/include/arch/x86/arch/64/mode/api/shared_types.bf
new file mode 120000
index 000000000..ea54ec996
--- /dev/null
+++ b/include/arch/x86/arch/64/mode/api/shared_types.bf
@@ -0,0 +1 @@
+../../../../../../../libsel4/include/sel4/shared_types_64.bf
\ No newline at end of file
diff --git a/libsel4/Makefile b/libsel4/Makefile
index 4d97e1529..3a0e2d86e 100644
--- a/libsel4/Makefile
+++ b/libsel4/Makefile
@@ -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 \
diff --git a/libsel4/include/sel4/shared_types_64.bf b/libsel4/include/sel4/shared_types_64.bf
new file mode 100644
index 000000000..5f7571054
--- /dev/null
+++ b/libsel4/include/sel4/shared_types_64.bf
@@ -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
+}
diff --git a/libsel4/include/sel4/types_64.bf b/libsel4/include/sel4/types_64.bf
new file mode 100644
index 000000000..204c626a7
--- /dev/null
+++ b/libsel4/include/sel4/types_64.bf
@@ -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
+}
diff --git a/libsel4/sel4_arch_include/x86_64/interfaces/sel4arch.xml b/libsel4/sel4_arch_include/x86_64/interfaces/sel4arch.xml
new file mode 100644
index 000000000..9de8b5993
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/interfaces/sel4arch.xml
@@ -0,0 +1,45 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
new file mode 100644
index 000000000..938983548
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
@@ -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
+
+#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
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/deprecated.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/deprecated.h
new file mode 100644
index 000000000..e4a1b8fac
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/deprecated.h
@@ -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
+#include
+#include
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/exIPC.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/exIPC.h
new file mode 100644
index 000000000..b2715a196
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/exIPC.h
@@ -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;
+}
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/functions.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/functions.h
new file mode 100644
index 000000000..28d4aa726
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/functions.h
@@ -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
+
+/* 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)
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/mapping.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/mapping.h
new file mode 100644
index 000000000..48b16f987
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/mapping.h
@@ -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);
+}
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/objecttype.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/objecttype.h
new file mode 100644
index 000000000..a219307fa
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/objecttype.h
@@ -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
+#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
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/pfIPC.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/pfIPC.h
new file mode 100644
index 000000000..08ee658a7
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/pfIPC.h
@@ -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
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/simple_types.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/simple_types.h
new file mode 100644
index 000000000..240759d74
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/simple_types.h
@@ -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;
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
new file mode 100644
index 000000000..ecadb461d
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
@@ -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
+
+#if defined(CONFIG_SYSENTER)
+#include
+#elif defined(CONFIG_SYSCALL)
+#include
+#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 */
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_syscall.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_syscall.h
new file mode 100644
index 000000000..a287b1af0
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_syscall.h
@@ -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
+#include
+#include
+
+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"
+ );
+}
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_sysenter.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_sysenter.h
new file mode 100644
index 000000000..a7b4e5b02
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls_sysenter.h
@@ -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
+#include
+#include
+
+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"
+ );
+}
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/types.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/types.h
new file mode 100644
index 000000000..e99d84648
--- /dev/null
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/types.h
@@ -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
+#include
+
+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;
diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py
index 77ab2b744..e2394f74e 100644
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -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.