1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#ifndef __LIBSEL4_ARCH_SYSCALLS_H 14#define __LIBSEL4_ARCH_SYSCALLS_H 15 16#include <autoconf.h> 17#include <sel4/arch/functions.h> 18#include <sel4/sel4_arch/syscalls.h> 19#include <sel4/types.h> 20 21LIBSEL4_INLINE_FUNC void 22seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) 23{ 24 arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3)); 25} 26 27LIBSEL4_INLINE_FUNC void 28seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, 29 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 30{ 31 arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], 32 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0, 33 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0, 34 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0, 35 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0 36 ); 37} 38 39LIBSEL4_INLINE_FUNC void 40seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) 41{ 42 arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3)); 43} 44 45LIBSEL4_INLINE_FUNC void 46seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, 47 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 48{ 49 arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], 50 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0, 51 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0, 52 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0, 53 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0 54 ); 55} 56 57LIBSEL4_INLINE_FUNC void 58seL4_Reply(seL4_MessageInfo_t msgInfo) 59{ 60 arm_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3)); 61} 62 63LIBSEL4_INLINE_FUNC void 64seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, 65 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 66{ 67 arm_sys_reply(seL4_SysReply, msgInfo.words[0], 68 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0, 69 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0, 70 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0, 71 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0 72 ); 73} 74 75LIBSEL4_INLINE_FUNC void 76seL4_Signal(seL4_CPtr dest) 77{ 78 arm_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]); 79} 80 81LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 82seL4_Recv(seL4_CPtr src, seL4_Word* sender) 83{ 84 seL4_MessageInfo_t info; 85 seL4_Word badge; 86 seL4_Word msg0; 87 seL4_Word msg1; 88 seL4_Word msg2; 89 seL4_Word msg3; 90 91 arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 92 93 seL4_SetMR(0, msg0); 94 seL4_SetMR(1, msg1); 95 seL4_SetMR(2, msg2); 96 seL4_SetMR(3, msg3); 97 98 /* Return back sender and message information. */ 99 if (sender) { 100 *sender = badge; 101 } 102 return info; 103} 104 105LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 106seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, 107 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 108{ 109 seL4_MessageInfo_t info; 110 seL4_Word badge; 111 seL4_Word msg0 = 0; 112 seL4_Word msg1 = 0; 113 seL4_Word msg2 = 0; 114 seL4_Word msg3 = 0; 115 116 arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 117 118 /* Write the message back out to memory. */ 119 if (mr0 != seL4_Null) { 120 *mr0 = msg0; 121 } 122 if (mr1 != seL4_Null) { 123 *mr1 = msg1; 124 } 125 if (mr2 != seL4_Null) { 126 *mr2 = msg2; 127 } 128 if (mr3 != seL4_Null) { 129 *mr3 = msg3; 130 } 131 132 /* Return back sender and message information. */ 133 if (sender) { 134 *sender = badge; 135 } 136 return info; 137} 138 139LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 140seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) 141{ 142 seL4_MessageInfo_t info; 143 seL4_Word badge; 144 seL4_Word msg0; 145 seL4_Word msg1; 146 seL4_Word msg2; 147 seL4_Word msg3; 148 149 arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 150 151 seL4_SetMR(0, msg0); 152 seL4_SetMR(1, msg1); 153 seL4_SetMR(2, msg2); 154 seL4_SetMR(3, msg3); 155 156 /* Return back sender and message information. */ 157 if (sender) { 158 *sender = badge; 159 } 160 return info; 161} 162 163LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 164seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) 165{ 166 seL4_MessageInfo_t info; 167 seL4_Word msg0 = seL4_GetMR(0); 168 seL4_Word msg1 = seL4_GetMR(1); 169 seL4_Word msg2 = seL4_GetMR(2); 170 seL4_Word msg3 = seL4_GetMR(3); 171 172 arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3); 173 174 /* Write out the data back to memory. */ 175 seL4_SetMR(0, msg0); 176 seL4_SetMR(1, msg1); 177 seL4_SetMR(2, msg2); 178 seL4_SetMR(3, msg3); 179 180 return info; 181} 182 183LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 184seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, 185 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 186{ 187 seL4_MessageInfo_t info; 188 seL4_Word msg0 = 0; 189 seL4_Word msg1 = 0; 190 seL4_Word msg2 = 0; 191 seL4_Word msg3 = 0; 192 193 /* Load beginning of the message into registers. */ 194 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { 195 msg0 = *mr0; 196 } 197 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) { 198 msg1 = *mr1; 199 } 200 if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) { 201 msg2 = *mr2; 202 } 203 if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) { 204 msg3 = *mr3; 205 } 206 207 arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3); 208 209 /* Write out the data back to memory. */ 210 if (mr0 != seL4_Null) { 211 *mr0 = msg0; 212 } 213 if (mr1 != seL4_Null) { 214 *mr1 = msg1; 215 } 216 if (mr2 != seL4_Null) { 217 *mr2 = msg2; 218 } 219 if (mr3 != seL4_Null) { 220 *mr3 = msg3; 221 } 222 223 return info; 224} 225 226LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 227seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) 228{ 229 seL4_MessageInfo_t info; 230 seL4_Word badge; 231 seL4_Word msg0; 232 seL4_Word msg1; 233 seL4_Word msg2; 234 seL4_Word msg3; 235 236 /* Load beginning of the message into registers. */ 237 msg0 = seL4_GetMR(0); 238 msg1 = seL4_GetMR(1); 239 msg2 = seL4_GetMR(2); 240 msg3 = seL4_GetMR(3); 241 242 arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3); 243 244 /* Write the message back out to memory. */ 245 seL4_SetMR(0, msg0); 246 seL4_SetMR(1, msg1); 247 seL4_SetMR(2, msg2); 248 seL4_SetMR(3, msg3); 249 250 /* Return back sender and message information. */ 251 if (sender) { 252 *sender = badge; 253 } 254 255 return info; 256} 257 258LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 259seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, 260 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) 261{ 262 seL4_MessageInfo_t info; 263 seL4_Word badge; 264 seL4_Word msg0 = 0; 265 seL4_Word msg1 = 0; 266 seL4_Word msg2 = 0; 267 seL4_Word msg3 = 0; 268 269 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { 270 msg0 = *mr0; 271 } 272 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) { 273 msg1 = *mr1; 274 } 275 if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) { 276 msg2 = *mr2; 277 } 278 if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) { 279 msg3 = *mr3; 280 } 281 282 arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3); 283 284 /* Write out the data back to memory. */ 285 if (mr0 != seL4_Null) { 286 *mr0 = msg0; 287 } 288 if (mr1 != seL4_Null) { 289 *mr1 = msg1; 290 } 291 if (mr2 != seL4_Null) { 292 *mr2 = msg2; 293 } 294 if (mr3 != seL4_Null) { 295 *mr3 = msg3; 296 } 297 298 /* Return back sender and message information. */ 299 if (sender) { 300 *sender = badge; 301 } 302 303 return info; 304} 305 306LIBSEL4_INLINE_FUNC void 307seL4_Yield(void) 308{ 309 arm_sys_null(seL4_SysYield); 310 asm volatile("" ::: "memory"); 311} 312 313#ifdef CONFIG_PRINTING 314LIBSEL4_INLINE_FUNC void 315seL4_DebugPutChar(char c) 316{ 317 seL4_Word unused0 = 0; 318 seL4_Word unused1 = 0; 319 seL4_Word unused2 = 0; 320 seL4_Word unused3 = 0; 321 seL4_Word unused4 = 0; 322 seL4_Word unused5 = 0; 323 324 arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5); 325} 326 327LIBSEL4_INLINE_FUNC void 328seL4_DebugDumpScheduler(void) 329{ 330 seL4_Word unused0 = 0; 331 seL4_Word unused1 = 0; 332 seL4_Word unused2 = 0; 333 seL4_Word unused3 = 0; 334 seL4_Word unused4 = 0; 335 seL4_Word unused5 = 0; 336 337 arm_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5); 338} 339#endif 340 341#if CONFIG_DEBUG_BUILD 342LIBSEL4_INLINE_FUNC void 343seL4_DebugHalt(void) 344{ 345 arm_sys_null(seL4_SysDebugHalt); 346} 347 348LIBSEL4_INLINE_FUNC void 349seL4_DebugSnapshot(void) 350{ 351 arm_sys_null(seL4_SysDebugSnapshot); 352 asm volatile("" ::: "memory"); 353} 354 355LIBSEL4_INLINE_FUNC seL4_Uint32 356seL4_DebugCapIdentify(seL4_CPtr cap) 357{ 358 seL4_Word unused0 = 0; 359 seL4_Word unused1 = 0; 360 seL4_Word unused2 = 0; 361 seL4_Word unused3 = 0; 362 seL4_Word unused4 = 0; 363 364 arm_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4); 365 return (seL4_Uint32)cap; 366} 367 368char *strcpy(char *, const char *); 369LIBSEL4_INLINE_FUNC void 370seL4_DebugNameThread(seL4_CPtr tcb, const char *name) 371{ 372 strcpy((char*)seL4_GetIPCBuffer()->msg, name); 373 374 seL4_Word unused0 = 0; 375 seL4_Word unused1 = 0; 376 seL4_Word unused2 = 0; 377 seL4_Word unused3 = 0; 378 seL4_Word unused4 = 0; 379 seL4_Word unused5 = 0; 380 381 arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5); 382} 383#endif 384 385#ifdef CONFIG_DANGEROUS_CODE_INJECTION 386LIBSEL4_INLINE_FUNC void 387seL4_DebugRun(void (* userfn) (void *), void* userarg) 388{ 389 arm_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg); 390 asm volatile("" ::: "memory"); 391} 392#endif 393 394#ifdef CONFIG_ENABLE_BENCHMARKS 395/* set the log index back to 0 */ 396LIBSEL4_INLINE_FUNC seL4_Error 397seL4_BenchmarkResetLog(void) 398{ 399 seL4_Word unused0 = 0; 400 seL4_Word unused1 = 0; 401 seL4_Word unused2 = 0; 402 seL4_Word unused3 = 0; 403 seL4_Word unused4 = 0; 404 405 seL4_Word ret; 406 arm_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4); 407 408 return (seL4_Error) ret; 409} 410 411LIBSEL4_INLINE_FUNC seL4_Word 412seL4_BenchmarkFinalizeLog(void) 413{ 414 seL4_Word unused0 = 0; 415 seL4_Word unused1 = 0; 416 seL4_Word unused2 = 0; 417 seL4_Word unused3 = 0; 418 seL4_Word unused4 = 0; 419 seL4_Word index_ret; 420 arm_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4); 421 422 return (seL4_Word)index_ret; 423} 424 425LIBSEL4_INLINE_FUNC seL4_Error 426seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr) 427{ 428 seL4_Word unused0 = 0; 429 seL4_Word unused1 = 0; 430 seL4_Word unused2 = 0; 431 seL4_Word unused3 = 0; 432 seL4_Word unused4 = 0; 433 434 arm_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3, &unused4); 435 436 return (seL4_Error) frame_cptr; 437} 438 439LIBSEL4_INLINE_FUNC void 440seL4_BenchmarkNullSyscall(void) 441{ 442 arm_sys_null(seL4_SysBenchmarkNullSyscall); 443 asm volatile("" ::: "memory"); 444} 445 446LIBSEL4_INLINE_FUNC void 447seL4_BenchmarkFlushCaches(void) 448{ 449 arm_sys_null(seL4_SysBenchmarkFlushCaches); 450 asm volatile("" ::: "memory"); 451} 452 453#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION 454LIBSEL4_INLINE_FUNC void 455seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr) 456{ 457 seL4_Word unused0 = 0; 458 seL4_Word unused1 = 0; 459 seL4_Word unused2 = 0; 460 seL4_Word unused3 = 0; 461 seL4_Word unused4 = 0; 462 seL4_Word unused5 = 0; 463 464 arm_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5); 465} 466 467LIBSEL4_INLINE_FUNC void 468seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr) 469{ 470 seL4_Word unused0 = 0; 471 seL4_Word unused1 = 0; 472 seL4_Word unused2 = 0; 473 seL4_Word unused3 = 0; 474 seL4_Word unused4 = 0; 475 seL4_Word unused5 = 0; 476 477 arm_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5); 478} 479#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */ 480#endif /* CONFIG_ENABLE_BENCHMARKS */ 481 482LIBSEL4_INLINE_FUNC void 483seL4_Wait(seL4_CPtr src, seL4_Word *sender) 484{ 485 seL4_Recv(src, sender); 486} 487 488LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 489seL4_Poll(seL4_CPtr src, seL4_Word *sender) 490{ 491 return seL4_NBRecv(src, sender); 492} 493 494#endif 495