1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7#pragma once 8 9#include <autoconf.h> 10#include <sel4/functions.h> 11#include <sel4/types.h> 12 13#ifdef CONFIG_KERNEL_MCS 14#define MCS_REPLY_DECL register seL4_Word reply_reg asm("r12") = reply 15#define MCS_REPLY ,"r"(reply_reg) 16#else 17#define MCS_REPLY_DECL 18#define MCS_REPLY 19#endif 20 21static inline void x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word msg0, seL4_Word msg1, 22 seL4_Word msg2, seL4_Word msg3) 23{ 24 register seL4_Word mr0 asm("r10") = msg0; 25 register seL4_Word mr1 asm("r8") = msg1; 26 register seL4_Word mr2 asm("r9") = msg2; 27 register seL4_Word mr3 asm("r15") = msg3; 28 29 asm volatile( 30 "movq %%rsp, %%rbx \n" 31 "syscall \n" 32 "movq %%rbx, %%rsp \n" 33 : 34 : "d"(sys), 35 "D"(dest), 36 "S"(info), 37 "r"(mr0), 38 "r"(mr1), 39 "r"(mr2), 40 "r"(mr3) 41 : "%rbx", "%rcx", "%r11" 42 ); 43} 44 45#ifndef CONFIG_KERNEL_MCS 46static inline void x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0, seL4_Word msg1, seL4_Word msg2, 47 seL4_Word msg3) 48{ 49 register seL4_Word mr0 asm("r10") = msg0; 50 register seL4_Word mr1 asm("r8") = msg1; 51 register seL4_Word mr2 asm("r9") = msg2; 52 register seL4_Word mr3 asm("r15") = msg3; 53 54 asm volatile( 55 "movq %%rsp, %%rbx \n" 56 "syscall \n" 57 "movq %%rbx, %%rsp \n" 58 : 59 : "d"(sys), 60 "S"(info), 61 "r"(mr0), 62 "r"(mr1), 63 "r"(mr2), 64 "r"(mr3) 65 : "%rbx", "%rcx", "%r11" 66 ); 67} 68#endif /* CONFIG_KERNEL_MCS */ 69 70static inline void x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info) 71{ 72 asm volatile( 73 "movq %%rsp, %%rbx \n" 74 "syscall \n" 75 "movq %%rbx, %%rsp \n" 76 : 77 : "d"(sys), 78 "D"(dest), 79 "S"(info) 80 : "%rcx", "%rbx", "%r11" 81 ); 82} 83 84static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, 85 seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3, 86 LIBSEL4_UNUSED seL4_Word reply) 87{ 88 register seL4_Word mr0 asm("r10"); 89 register seL4_Word mr1 asm("r8"); 90 register seL4_Word mr2 asm("r9"); 91 register seL4_Word mr3 asm("r15"); 92 MCS_REPLY_DECL; 93 94 asm volatile( 95 "movq %%rsp, %%rbx \n" 96 "syscall \n" 97 "movq %%rbx, %%rsp \n" 98 : "=D"(*out_badge), 99 "=S"(*out_info), 100 "=r"(mr0), 101 "=r"(mr1), 102 "=r"(mr2), 103 "=r"(mr3) 104 : "d"(sys), 105 "D"(src) 106 MCS_REPLY 107 : "%rcx", "%rbx", "r11", "memory" 108 ); 109 *out_mr0 = mr0; 110 *out_mr1 = mr1; 111 *out_mr2 = mr2; 112 *out_mr3 = mr3; 113} 114 115static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_dest, seL4_Word info, 116 seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3, 117 LIBSEL4_UNUSED seL4_Word reply) 118{ 119 register seL4_Word mr0 asm("r10") = *in_out_mr0; 120 register seL4_Word mr1 asm("r8") = *in_out_mr1; 121 register seL4_Word mr2 asm("r9") = *in_out_mr2; 122 register seL4_Word mr3 asm("r15") = *in_out_mr3; 123 MCS_REPLY_DECL; 124 125 asm volatile( 126 "movq %%rsp, %%rbx \n" 127 "syscall \n" 128 "movq %%rbx, %%rsp \n" 129 : "=S"(*out_info), 130 "=r"(mr0), 131 "=r"(mr1), 132 "=r"(mr2), 133 "=r"(mr3), 134 "=D"(*out_dest) 135 : "d"(sys), 136 "D"(dest), 137 "S"(info), 138 "r"(mr0), 139 "r"(mr1), 140 "r"(mr2), 141 "r"(mr3) 142 MCS_REPLY 143 : "%rcx", "%rbx", "r11", "memory" 144 ); 145 *in_out_mr0 = mr0; 146 *in_out_mr1 = mr1; 147 *in_out_mr2 = mr2; 148 *in_out_mr3 = mr3; 149} 150 151#ifdef CONFIG_KERNEL_MCS 152static inline void x64_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_dest, 153 seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, 154 seL4_Word *in_out_mr3, seL4_Word reply) 155{ 156 register seL4_Word mr0 asm("r10") = *in_out_mr0; 157 register seL4_Word mr1 asm("r8") = *in_out_mr1; 158 register seL4_Word mr2 asm("r9") = *in_out_mr2; 159 register seL4_Word mr3 asm("r15") = *in_out_mr3; 160 register seL4_Word reply_reg asm("r12") = reply; 161 register seL4_Word dest_reg asm("r13") = dest; 162 163 asm volatile( 164 "movq %%rsp, %%rbx \n" 165 "syscall \n" 166 "movq %%rbx, %%rsp \n" 167 : "=S"(*out_info), 168 "=r"(mr0), 169 "=r"(mr1), 170 "=r"(mr2), 171 "=r"(mr3), 172 "=D"(*out_dest) 173 : "d"(sys), 174 "D"(src), 175 "S"(info), 176 "r"(mr0), 177 "r"(mr1), 178 "r"(mr2), 179 "r"(mr3), 180 "r"(reply_reg), 181 "r"(dest_reg) 182 : "%rcx", "%rbx", "r11", "memory" 183 ); 184 *in_out_mr0 = mr0; 185 *in_out_mr1 = mr1; 186 *in_out_mr2 = mr2; 187 *in_out_mr3 = mr3; 188} 189#endif /* CONFIG_KERNEL_MCS */ 190 191static inline void x64_sys_null(seL4_Word sys) 192{ 193 asm volatile( 194 "movq %%rsp, %%rbx \n" 195 "syscall \n" 196 "movq %%rbx, %%rsp \n" 197 : 198 : "d"(sys) 199 : "%rbx", "%rcx", "%rsi", "%rdi", "%r11" 200 ); 201} 202