/* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause */ #pragma once #include #include #include /* * A general description of the x86_sys_ functions and what they do can be found in * the ARM aarch32 syscalls.h file (substituting ARM for x86) * * Further there are two version of every function, one that supports Position * Independent Code, and one that does not. The PIC variant works to preserve * EBX, which is used by the compiler, and has to do additional work to save/restore * and juggle the contents of EBX as the kernel ABI uses EBX */ #ifdef CONFIG_KERNEL_MCS #define MCS_COND(a,b) a #else #define MCS_COND(a,b) b #endif #if defined(__pic__) /* mr2 doesn't get used on CONFIG_KERNEL_MCS */ static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, LIBSEL4_UNUSED seL4_Word mr2) { asm volatile( "pushl %%ebp \n" "pushl %%ebx \n" MCS_COND(, "movl %%ecx, %%ebp \n") "movl %%esp, %%ecx \n" "movl %%edx, %%ebx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebx \n" "popl %%ebp \n" : "+d"(dest) : "a"(sys), "S"(info), "D"(mr1) #ifdef CONFIG_KERNEL_MCS : "%ecx" #else , "c"(mr2) #endif ); } #ifndef CONFIG_KERNEL_MCS static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2) { asm volatile( "pushl %%ebp \n" "pushl %%ebx \n" "movl %%ecx, %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebx \n" "popl %%ebp \n" : : "a"(sys), "S"(info), "D"(mr1), "c"(mr2) : "%edx" ); } #endif /* !CONFIG_KERNEL_MCS */ static inline void x86_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info) { asm volatile( "pushl %%ebp \n" "pushl %%ebx \n" "movl %%esp, %%ecx \n" "movl %%edx, %%ebx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebx \n" "popl %%ebp \n" : "+d"(src) : "a"(sys), "S"(info) : "%ecx" ); } static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr1, MCS_COND(seL4_Word reply, seL4_Word *out_mr2)) { asm volatile( "pushl %%ebp \n" "pushl %%ebx \n" MCS_COND("movl %%ecx, %%ebp \n",) "movl %%esp, %%ecx \n" "movl %%edx, %%ebx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "movl %%ebx, %%edx \n" "popl %%ebx \n" "movl %%ebp, %%ecx \n" "popl %%ebp \n" : "=d"(*out_badge), "=S"(*out_info), "=D"(*out_mr1), MCS_COND("+c"(reply), "=c"(*out_mr2)) : "a"(sys), "d"(src) : "memory" ); } static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr1, MCS_COND(seL4_Word reply, seL4_Word *in_out_mr2)) { asm volatile( "pushl %%ebp \n" "pushl %%ebx \n" MCS_COND("movl %%ecx, %%ebp \n",) "movl %%esp, %%ecx \n" "movl %%edx, %%ebx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "movl %%ebx, %%edx \n" "popl %%ebx \n" "movl %%ebp, %%ecx \n" "popl %%ebp \n" : "=S"(*out_info), "=D"(*in_out_mr1), "=d"(*out_badge) MCS_COND("+c"(reply), "=c"(*in_out_mr2)) : "a"(sys), "S"(info), "D"(*in_out_mr1), #ifndef CONFIG_KERNEL_MCS "c"(*in_out_mr2), #endif "d"(dest) : "memory" ); } #ifdef CONFIG_KERNEL_MCS static inline void x86_sys_nbsend_wait(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word reply) { asm volatile( "pushl %%ebp \n" "pushl %%ebx \n" "movl %%ecx, %%ebp \n" "movl %%esp, %%ecx \n" "movl %%edx, %%ebx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "movl %%ebx, %%edx \n" "popl %%ebx \n" "movl %%ebp, %%ecx \n" "popl %%ebp \n" : "=S"(*out_info), "=D"(*in_out_mr1), "=d"(*out_badge) , "+c"(reply) : "a"(sys), "S"(info), "D"(*in_out_mr1), "d"(src) : "memory" ); } #endif /* CONFIG_KERNEL_MCS */ static inline void x86_sys_null(seL4_Word sys) { asm volatile( "pushl %%ebp \n" "pushl %%ebx \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebx \n" "popl %%ebp \n" : : "a"(sys) : "%ecx", "%edx" ); } #else static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, seL4_Word mr2) { asm volatile( "pushl %%ebp \n" #ifndef CONFIG_KERNEL_MCS "movl %%ecx, %%ebp \n" #endif "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a"(sys), "b"(dest), "S"(info), "D"(mr1) #ifdef CONFIG_KERNEL_MCS : "%ecx", #else , "c"(mr2): #endif "%edx" ); } #ifndef CONFIG_KERNEL_MCS static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2) { 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"(sys), "S"(info), "D"(mr1), "c"(mr2) : "%ebx", "%edx" ); } #endif static inline void x86_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info) { asm volatile(\ "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a"(sys), "b"(dest), "S"(info) : "%ecx", "edx" ); } static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr1, MCS_COND(seL4_Word reply, seL4_Word *out_mr2)) { asm volatile(\ "pushl %%ebp \n" MCS_COND("movl %%ecx, %%ebp \n",) "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "movl %%ebp, %%ecx \n" "popl %%ebp \n" : "=b"(*out_badge), "=S"(*out_info), "=D"(*out_mr1), MCS_COND("+c"(reply), "=c"(*out_mr2)) : "a"(sys), "b"(src) : "%edx", "memory" ); } static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr1, MCS_COND(seL4_Word reply, seL4_Word *in_out_mr2)) { 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"(*out_info), "=D"(*in_out_mr1), "=b"(*out_badge), MCS_COND("+c"(reply), "=c"(*in_out_mr2)) : "a"(sys), "S"(info), "D"(*in_out_mr1), #ifndef CONFIG_KERNEL_MCS "c"(*in_out_mr2), #endif "b"(dest) : "%edx", "memory" ); } #ifdef CONFIG_KERNEL_MCS static inline void x86_sys_nbsend_wait(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word reply) { 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"(*out_info), "=D"(*in_out_mr1), "=b"(*out_badge), "+c"(reply) : "a"(sys), "S"(info), "D"(*in_out_mr1), "b"(src) : "%edx", "memory" ); } #endif /* CONFIG_KERNEL_MCS */ static inline void x86_sys_null(seL4_Word sys) { asm volatile( "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a"(sys) : "%ebx", "%ecx", "%edx" ); } #endif /* defined(__pic__) */ #ifdef CONFIG_KERNEL_MCS #define GET_MRS seL4_GetMR(0), 0 #define MAYBE_GET_MRS mr0 != seL4_Null ? *mr0 : 0 #define MR_ARGS seL4_Word *mr0 #define RECV_MRS &mr0 #define REPLY &mr0 #else #define MCS_MAYBE_GET_MR1 seL4_GetMR(1) #define MAYBE_GET_MRS mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0 #define MR_ARGS #define RECV_MRS &mr0, &mr1 #endif LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1))); } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) #else LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) #endif { x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, MCS_COND(0, mr1 != seL4_Null ? *mr1 : 0)); } LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1))); } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) #else LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) #endif { x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, MCS_COND(0, mr1 != seL4_Null ? *mr1 : 0)); } #ifndef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo) { x86_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1)); } LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) { x86_sys_reply(seL4_SysReply, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0); } #endif /* !CONFIG_KERNEL_MCS */ LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest) { x86_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]); } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) #else LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender) #endif { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word mr0; LIBSEL4_UNUSED seL4_Word mr1; x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1)); seL4_SetMR(0, mr0); #ifndef CONFIG_KERNEL_MCS seL4_SetMR(1, mr1); #endif if (sender) { *sender = badge; } return info; } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_CPtr reply) #else LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1) #endif { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word msg0 = 0; LIBSEL4_UNUSED seL4_Word msg1 = 0; x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, MCS_COND(reply, &msg1)); if (mr0 != seL4_Null) { *mr0 = msg0; } #ifndef CONFIG_KERNEL_MCS if (mr1 != seL4_Null) { *mr1 = msg1; } #endif if (sender) { *sender = badge; } return info; } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) #else LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender) #endif { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word mr0; LIBSEL4_UNUSED seL4_Word mr1; x86_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1)); seL4_SetMR(0, mr0); #ifndef CONFIG_KERNEL_MCS seL4_SetMR(1, mr1); #endif if (sender) { *sender = badge; } return info; } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender) { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word mr0; x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &mr0, 0); seL4_SetMR(0, mr0); if (sender) { *sender = badge; } return info; } LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_Word *mr0) { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word msg0 = 0; x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, 0); if (mr0 != seL4_Null) { *mr0 = msg0; } if (sender) { *sender = badge; } return info; } LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender) { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word mr0; x86_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &mr0, 0); seL4_SetMR(0, mr0); if (sender) { *sender = badge; } return info; } #endif /* CONFIG_KERNEL_MCS */ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { seL4_MessageInfo_t info; seL4_Word mr0 = seL4_GetMR(0); LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, MCS_COND(0, &mr1)); seL4_SetMR(0, mr0); #ifndef CONFIG_KERNEL_MCS seL4_SetMR(1, mr1); #endif return info; } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) #else LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) #endif { seL4_MessageInfo_t info; seL4_Word msg0 = 0; LIBSEL4_UNUSED seL4_Word msg1 = 0; if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { msg0 = *mr0; } #ifndef CONFIG_KERNEL_MCS if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) { msg1 = *mr1; } #endif x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, MCS_COND(0, &msg1)); if (mr0 != seL4_Null) { *mr0 = msg0; } #ifndef CONFIG_KERNEL_MCS if (mr1 != seL4_Null) { *mr1 = msg1; } #endif return info; } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply) #else LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) #endif { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word mr0 = seL4_GetMR(0); LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0, MCS_COND(reply, &mr1)); seL4_SetMR(0, mr0); #ifndef CONFIG_KERNEL_MCS seL4_SetMR(1, mr1); #endif if (sender) { *sender = badge; } return info; } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_CPtr reply) #else LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1) #endif { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word msg0 = 0; LIBSEL4_UNUSED seL4_Word msg1 = 0; if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { msg0 = *mr0; } #ifndef CONFIG_KERNEL_MCS if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) { msg1 = *mr1; } #endif x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, MCS_COND(0, &msg1)); if (mr0 != seL4_Null) { *mr0 = msg0; } #ifndef CONFIG_KERNEL_MCS if (mr1 != seL4_Null) { *mr1 = msg1; } #endif if (sender) { *sender = badge; } return info; } #ifdef CONFIG_KERNEL_MCS LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender, seL4_CPtr reply) { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word mr0 = seL4_GetMR(0); /* no spare registers on ia32 -> must use ipc buffer */ seL4_SetUserData(dest); x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &mr0, reply); seL4_SetMR(0, mr0); if (sender) { *sender = badge; } return info; } LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender, seL4_Word *mr0, seL4_CPtr reply) { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word msg0 = 0; /* no spare registers on ia32 -> must use ipc buffer */ seL4_SetUserData(dest); if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { msg0 = *mr0; } x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, reply); if (mr0 != seL4_Null) { *mr0 = msg0; } if (sender) { *sender = badge; } return info; } LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender) { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word mr0 = seL4_GetMR(0); x86_sys_nbsend_wait(seL4_SysNBSendWait, src, &badge, msgInfo.words[0], &info.words[0], &mr0, dest); seL4_SetMR(0, mr0); if (sender) { *sender = badge; } return info; } LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, seL4_Word *sender, seL4_Word *mr0) { seL4_MessageInfo_t info; seL4_Word badge; seL4_Word msg0 = 0; if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { msg0 = *mr0; } x86_sys_nbsend_wait(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, dest); if (mr0 != seL4_Null) { *mr0 = msg0; } if (sender) { *sender = badge; } return info; } #endif /* CONFIG_KERNEL_MCS */ LIBSEL4_INLINE_FUNC void seL4_Yield(void) { x86_sys_null(seL4_SysYield); asm volatile("" :::"%esi", "%edi", "memory"); } #ifdef CONFIG_VTX LIBSEL4_INLINE_FUNC seL4_Word seL4_VMEnter(seL4_Word *sender) { seL4_Word fault; seL4_Word badge; seL4_Word mr0 = seL4_GetMR(0); LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, MCS_COND(0, &mr1)); seL4_SetMR(0, mr0); #ifndef CONFIG_KERNEL_MCS seL4_SetMR(1, mr1); #endif if (!fault && sender) { *sender = badge; } return fault; } #endif #ifdef CONFIG_PRINTING LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; seL4_Word unused2 = 0; LIBSEL4_UNUSED seL4_Word unused3 = 0; x86_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) { for (char *s = str; *s; s++) { seL4_DebugPutChar(*s); } return; } LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; seL4_Word unused2 = 0; LIBSEL4_UNUSED seL4_Word unused3 = 0; x86_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } #endif #ifdef CONFIG_DEBUG_BUILD LIBSEL4_INLINE_FUNC void seL4_DebugHalt(void) { x86_sys_null(seL4_SysDebugHalt); asm volatile("" :::"%esi", "%edi", "memory"); } #endif #if defined(CONFIG_DEBUG_BUILD) LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot(void) { x86_sys_null(seL4_SysDebugSnapshot); asm volatile("" :::"%esi", "%edi", "memory"); } #endif #ifdef CONFIG_DEBUG_BUILD LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; LIBSEL4_UNUSED seL4_Word unused2 = 0; x86_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, MCS_COND(0, &unused2)); return (seL4_Uint32)cap; } char *strcpy(char *, const char *); LIBSEL4_INLINE_FUNC 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; LIBSEL4_UNUSED seL4_Word unused3 = 0; x86_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } #endif #if defined(CONFIG_DANGEROUS_CODE_INJECTION) LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (*userfn)(void *), void *userarg) { x86_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg); asm volatile("" ::: "%edi", "memory"); } #endif #if defined(CONFIG_KERNEL_X86_DANGEROUS_MSR) LIBSEL4_INLINE_FUNC void seL4_X86DangerousWRMSR(seL4_Uint32 msr, seL4_Uint64 value) { seL4_Uint32 value_low = value & 0xffffffff; seL4_Uint32 value_high = value >> 32; #ifdef CONFIG_KERNEL_MCS /* MR1 doesn't get passed through MRs on CONFIG_KERNEL_MCS */ seL4_SetMR(1, value_high); #endif x86_sys_send(seL4_SysX86DangerousWRMSR, msr, 0, value_low, value_high); } LIBSEL4_INLINE_FUNC seL4_Uint64 seL4_X86DangerousRDMSR(seL4_Word msr) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; seL4_Word low, high; x86_sys_recv(seL4_SysX86DangerousRDMSR, msr, &unused0, &unused1, &low, MCS_COND(0, &high)); #ifdef CONFIG_KERNEL_MCS /* MR1 doesn't get passed through MRs on CONFIG_KERNEL_MCS */ *high = seL4_GetMR(1); #endif return ((seL4_Uint64)low) | ((seL4_Uint64)high << 32); } #endif #ifdef CONFIG_ENABLE_BENCHMARKS LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; LIBSEL4_UNUSED seL4_Word unused2 = 0; seL4_Word ret; x86_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, MCS_COND(0, &unused2)); return (seL4_Error)ret; } LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; LIBSEL4_UNUSED seL4_Word unused2 = 0; seL4_Word index_ret; x86_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, MCS_COND(0, &unused2)); return (seL4_Word)index_ret; } LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; LIBSEL4_UNUSED seL4_Word unused2 = 0; x86_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, MCS_COND(0, &unused2)); return (seL4_Error) frame_cptr; } LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall(void) { x86_sys_null(seL4_SysBenchmarkNullSyscall); asm volatile("" :::"%esi", "%edi", "memory"); } LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches(void) { x86_sys_null(seL4_SysBenchmarkFlushCaches); asm volatile("" :::"%esi", "%edi", "memory"); } #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; seL4_Word unused2 = 0; LIBSEL4_UNUSED seL4_Word unused3 = 0; x86_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; seL4_Word unused2 = 0; LIBSEL4_UNUSED seL4_Word unused3 = 0; x86_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } #ifdef CONFIG_DEBUG_BUILD LIBSEL4_INLINE_FUNC void seL4_BenchmarkDumpAllThreadsUtilisation(void) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; seL4_Word unused2 = 0; LIBSEL4_UNUSED seL4_Word unused3 = 0; x86_sys_send_recv(seL4_SysBenchmarkDumpAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkResetAllThreadsUtilisation(void) { seL4_Word unused0 = 0; seL4_Word unused1 = 0; seL4_Word unused2 = 0; LIBSEL4_UNUSED seL4_Word unused3 = 0; x86_sys_send_recv(seL4_SysBenchmarkResetAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); } #endif /* CONFIG_DEBUG_BUILD */ #endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */ #endif /* CONFIG_ENABLE_BENCHMARKS */ #ifdef CONFIG_SET_TLS_BASE_SELF LIBSEL4_INLINE_FUNC void seL4_SetTLSBase(seL4_Word tls_base) { x86_sys_send_null(seL4_SysSetTLSBase, tls_base, 0); asm volatile("" ::: "memory"); } #endif /* CONFIG_SET_TLS_BASE_SELF */