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/* 14 * A general description of the x86_sys_ functions and what they do can be found in 15 * the ARM aarch32 syscalls.h file (substituting ARM for x86) 16 * 17 * Further there are two version of every function, one that supports Position 18 * Independent Code, and one that does not. The PIC variant works to preserve 19 * EBX, which is used by the compiler, and has to do additional work to save/restore 20 * and juggle the contents of EBX as the kernel ABI uses EBX 21 */ 22 23#ifdef CONFIG_KERNEL_MCS 24#define MCS_COND(a,b) a 25#else 26#define MCS_COND(a,b) b 27#endif 28 29 30#if defined(__pic__) 31 32/* mr2 doesn't get used on CONFIG_KERNEL_MCS */ 33static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, 34 LIBSEL4_UNUSED seL4_Word mr2) 35{ 36 asm volatile( 37 "pushl %%ebp \n" 38 "pushl %%ebx \n" 39 MCS_COND(, "movl %%ecx, %%ebp \n") 40 "movl %%esp, %%ecx \n" 41 "movl %%edx, %%ebx \n" 42 "leal 1f, %%edx \n" 43 "1: \n" 44 "sysenter \n" 45 "popl %%ebx \n" 46 "popl %%ebp \n" 47 : "+d"(dest) 48 : "a"(sys), 49 "S"(info), 50 "D"(mr1) 51#ifdef CONFIG_KERNEL_MCS 52 : "%ecx" 53#else 54 , "c"(mr2) 55#endif 56 ); 57} 58 59#ifndef CONFIG_KERNEL_MCS 60static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2) 61{ 62 asm volatile( 63 "pushl %%ebp \n" 64 "pushl %%ebx \n" 65 "movl %%ecx, %%ebp \n" 66 "movl %%esp, %%ecx \n" 67 "leal 1f, %%edx \n" 68 "1: \n" 69 "sysenter \n" 70 "popl %%ebx \n" 71 "popl %%ebp \n" 72 : 73 : "a"(sys), 74 "S"(info), 75 "D"(mr1), 76 "c"(mr2) 77 : "%edx" 78 ); 79} 80#endif /* !CONFIG_KERNEL_MCS */ 81 82static inline void x86_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info) 83{ 84 asm volatile( 85 "pushl %%ebp \n" 86 "pushl %%ebx \n" 87 "movl %%esp, %%ecx \n" 88 "movl %%edx, %%ebx \n" 89 "leal 1f, %%edx \n" 90 "1: \n" 91 "sysenter \n" 92 "popl %%ebx \n" 93 "popl %%ebp \n" 94 : "+d"(src) 95 : "a"(sys), 96 "S"(info) 97 : "%ecx" 98 ); 99} 100 101static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, 102 seL4_Word *out_mr1, MCS_COND(seL4_Word reply, seL4_Word *out_mr2)) 103{ 104 asm volatile( 105 "pushl %%ebp \n" 106 "pushl %%ebx \n" 107 MCS_COND("movl %%ecx, %%ebp \n",) 108 "movl %%esp, %%ecx \n" 109 "movl %%edx, %%ebx \n" 110 "leal 1f, %%edx \n" 111 "1: \n" 112 "sysenter \n" 113 "movl %%ebx, %%edx \n" 114 "popl %%ebx \n" 115 "movl %%ebp, %%ecx \n" 116 "popl %%ebp \n" 117 : 118 "=d"(*out_badge), 119 "=S"(*out_info), 120 "=D"(*out_mr1), 121 MCS_COND("+c"(reply), "=c"(*out_mr2)) 122 : "a"(sys), 123 "d"(src) 124 : "memory" 125 ); 126} 127 128static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info, 129 seL4_Word *out_info, seL4_Word *in_out_mr1, MCS_COND(seL4_Word reply, seL4_Word *in_out_mr2)) 130{ 131 asm volatile( 132 "pushl %%ebp \n" 133 "pushl %%ebx \n" 134 MCS_COND("movl %%ecx, %%ebp \n",) 135 "movl %%esp, %%ecx \n" 136 "movl %%edx, %%ebx \n" 137 "leal 1f, %%edx \n" 138 "1: \n" 139 "sysenter \n" 140 "movl %%ebx, %%edx \n" 141 "popl %%ebx \n" 142 "movl %%ebp, %%ecx \n" 143 "popl %%ebp \n" 144 : 145 "=S"(*out_info), 146 "=D"(*in_out_mr1), 147 "=d"(*out_badge) 148 MCS_COND("+c"(reply), "=c"(*in_out_mr2)) 149 : "a"(sys), 150 "S"(info), 151 "D"(*in_out_mr1), 152#ifndef CONFIG_KERNEL_MCS 153 "c"(*in_out_mr2), 154#endif 155 "d"(dest) 156 : "memory" 157 ); 158} 159 160#ifdef CONFIG_KERNEL_MCS 161static inline void x86_sys_nbsend_wait(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word info, 162 seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word reply) 163{ 164 asm volatile( 165 "pushl %%ebp \n" 166 "pushl %%ebx \n" 167 "movl %%ecx, %%ebp \n" 168 "movl %%esp, %%ecx \n" 169 "movl %%edx, %%ebx \n" 170 "leal 1f, %%edx \n" 171 "1: \n" 172 "sysenter \n" 173 "movl %%ebx, %%edx \n" 174 "popl %%ebx \n" 175 "movl %%ebp, %%ecx \n" 176 "popl %%ebp \n" 177 : 178 "=S"(*out_info), 179 "=D"(*in_out_mr1), 180 "=d"(*out_badge) 181 , "+c"(reply) 182 : "a"(sys), 183 "S"(info), 184 "D"(*in_out_mr1), 185 "d"(src) 186 : "memory" 187 ); 188} 189#endif /* CONFIG_KERNEL_MCS */ 190 191 192 193static inline void x86_sys_null(seL4_Word sys) 194{ 195 asm volatile( 196 "pushl %%ebp \n" 197 "pushl %%ebx \n" 198 "movl %%esp, %%ecx \n" 199 "leal 1f, %%edx \n" 200 "1: \n" 201 "sysenter \n" 202 "popl %%ebx \n" 203 "popl %%ebp \n" 204 : 205 : "a"(sys) 206 : "%ecx", "%edx" 207 ); 208} 209 210#else 211 212static inline void x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, seL4_Word mr2) 213{ 214 asm volatile( 215 "pushl %%ebp \n" 216#ifndef CONFIG_KERNEL_MCS 217 "movl %%ecx, %%ebp \n" 218#endif 219 "movl %%esp, %%ecx \n" 220 "leal 1f, %%edx \n" 221 "1: \n" 222 "sysenter \n" 223 "popl %%ebp \n" 224 : 225 : "a"(sys), 226 "b"(dest), 227 "S"(info), 228 "D"(mr1) 229#ifdef CONFIG_KERNEL_MCS 230 : "%ecx", 231#else 232 , "c"(mr2): 233#endif 234 "%edx" 235 ); 236} 237 238#ifndef CONFIG_KERNEL_MCS 239static inline void x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2) 240{ 241 asm volatile( 242 "pushl %%ebp \n" 243 "movl %%ecx, %%ebp \n" 244 "movl %%esp, %%ecx \n" 245 "leal 1f, %%edx \n" 246 "1: \n" 247 "sysenter \n" 248 "popl %%ebp \n" 249 : 250 : "a"(sys), 251 "S"(info), 252 "D"(mr1), 253 "c"(mr2) 254 : "%ebx", "%edx" 255 ); 256} 257#endif 258 259static inline void x86_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info) 260{ 261 asm volatile(\ 262 "pushl %%ebp \n" 263 "movl %%esp, %%ecx \n" 264 "leal 1f, %%edx \n" 265 "1: \n" 266 "sysenter \n" 267 "popl %%ebp \n" 268 : 269 : "a"(sys), 270 "b"(dest), 271 "S"(info) 272 : "%ecx", "edx" 273 ); 274} 275 276static inline void x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, 277 seL4_Word *out_mr1, MCS_COND(seL4_Word reply, seL4_Word *out_mr2)) 278{ 279 asm volatile(\ 280 "pushl %%ebp \n" 281 MCS_COND("movl %%ecx, %%ebp \n",) 282 "movl %%esp, %%ecx \n" 283 "leal 1f, %%edx \n" 284 "1: \n" 285 "sysenter \n" 286 "movl %%ebp, %%ecx \n" 287 "popl %%ebp \n" 288 : "=b"(*out_badge), 289 "=S"(*out_info), 290 "=D"(*out_mr1), 291 MCS_COND("+c"(reply), "=c"(*out_mr2)) 292 : "a"(sys), 293 "b"(src) 294 : "%edx", "memory" 295 ); 296} 297 298static inline void x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info, 299 seL4_Word *out_info, seL4_Word *in_out_mr1, MCS_COND(seL4_Word reply, seL4_Word *in_out_mr2)) 300{ 301 asm volatile( 302 "pushl %%ebp \n" 303 "movl %%ecx, %%ebp \n" 304 "movl %%esp, %%ecx \n" 305 "leal 1f, %%edx \n" 306 "1: \n" 307 "sysenter \n" 308 "movl %%ebp, %%ecx \n" 309 "popl %%ebp \n" 310 : "=S"(*out_info), 311 "=D"(*in_out_mr1), 312 "=b"(*out_badge), 313 MCS_COND("+c"(reply), "=c"(*in_out_mr2)) 314 : "a"(sys), 315 "S"(info), 316 "D"(*in_out_mr1), 317#ifndef CONFIG_KERNEL_MCS 318 "c"(*in_out_mr2), 319#endif 320 "b"(dest) 321 : "%edx", "memory" 322 ); 323} 324 325#ifdef CONFIG_KERNEL_MCS 326static inline void x86_sys_nbsend_wait(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word info, 327 seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word reply) 328{ 329 asm volatile( 330 "pushl %%ebp \n" 331 "movl %%ecx, %%ebp \n" 332 "movl %%esp, %%ecx \n" 333 "leal 1f, %%edx \n" 334 "1: \n" 335 "sysenter \n" 336 "movl %%ebp, %%ecx \n" 337 "popl %%ebp \n" 338 : "=S"(*out_info), 339 "=D"(*in_out_mr1), 340 "=b"(*out_badge), 341 "+c"(reply) 342 : "a"(sys), 343 "S"(info), 344 "D"(*in_out_mr1), 345 "b"(src) 346 : "%edx", "memory" 347 ); 348} 349#endif /* CONFIG_KERNEL_MCS */ 350 351static inline void x86_sys_null(seL4_Word sys) 352{ 353 asm volatile( 354 "pushl %%ebp \n" 355 "movl %%esp, %%ecx \n" 356 "leal 1f, %%edx \n" 357 "1: \n" 358 "sysenter \n" 359 "popl %%ebp \n" 360 : 361 : "a"(sys) 362 : "%ebx", "%ecx", "%edx" 363 ); 364} 365 366#endif /* defined(__pic__) */ 367#ifdef CONFIG_KERNEL_MCS 368#define GET_MRS seL4_GetMR(0), 0 369#define MAYBE_GET_MRS mr0 != seL4_Null ? *mr0 : 0 370#define MR_ARGS seL4_Word *mr0 371#define RECV_MRS &mr0 372#define REPLY &mr0 373#else 374#define MCS_MAYBE_GET_MR1 seL4_GetMR(1) 375#define MAYBE_GET_MRS mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0 376#define MR_ARGS 377#define RECV_MRS &mr0, &mr1 378#endif 379 380LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) 381{ 382 x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1))); 383} 384 385#ifdef CONFIG_KERNEL_MCS 386LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) 387#else 388LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) 389#endif 390{ 391 x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, MCS_COND(0, 392 mr1 != seL4_Null ? *mr1 : 0)); 393} 394 395LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) 396{ 397 x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), MCS_COND(0, seL4_GetMR(1))); 398} 399 400#ifdef CONFIG_KERNEL_MCS 401LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0) 402#else 403LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1) 404#endif 405{ 406 x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, MCS_COND(0, 407 mr1 != seL4_Null ? *mr1 : 0)); 408} 409 410#ifndef CONFIG_KERNEL_MCS 411LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo) 412{ 413 x86_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1)); 414} 415 416LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, 417 seL4_Word *mr0, seL4_Word *mr1) 418{ 419 x86_sys_reply(seL4_SysReply, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0); 420} 421#endif /* !CONFIG_KERNEL_MCS */ 422 423LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest) 424{ 425 x86_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]); 426} 427 428#ifdef CONFIG_KERNEL_MCS 429LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) 430#else 431LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender) 432#endif 433{ 434 seL4_MessageInfo_t info; 435 seL4_Word badge; 436 seL4_Word mr0; 437 LIBSEL4_UNUSED seL4_Word mr1; 438 439 x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1)); 440 441 seL4_SetMR(0, mr0); 442#ifndef CONFIG_KERNEL_MCS 443 seL4_SetMR(1, mr1); 444#endif 445 if (sender) { 446 *sender = badge; 447 } 448 449 return info; 450} 451 452#ifdef CONFIG_KERNEL_MCS 453LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, 454 seL4_Word *mr0, seL4_CPtr reply) 455#else 456LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, 457 seL4_Word *mr0, seL4_Word *mr1) 458#endif 459{ 460 seL4_MessageInfo_t info; 461 seL4_Word badge; 462 seL4_Word msg0 = 0; 463 LIBSEL4_UNUSED seL4_Word msg1 = 0; 464 465 x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, MCS_COND(reply, &msg1)); 466 467 if (mr0 != seL4_Null) { 468 *mr0 = msg0; 469 } 470 471#ifndef CONFIG_KERNEL_MCS 472 if (mr1 != seL4_Null) { 473 *mr1 = msg1; 474 } 475#endif 476 477 if (sender) { 478 *sender = badge; 479 } 480 481 return info; 482} 483 484#ifdef CONFIG_KERNEL_MCS 485LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) 486#else 487LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender) 488#endif 489{ 490 seL4_MessageInfo_t info; 491 seL4_Word badge; 492 seL4_Word mr0; 493 LIBSEL4_UNUSED seL4_Word mr1; 494 495 x86_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, MCS_COND(reply, &mr1)); 496 497 seL4_SetMR(0, mr0); 498#ifndef CONFIG_KERNEL_MCS 499 seL4_SetMR(1, mr1); 500#endif 501 502 if (sender) { 503 *sender = badge; 504 } 505 506 return info; 507} 508 509#ifdef CONFIG_KERNEL_MCS 510LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender) 511{ 512 seL4_MessageInfo_t info; 513 seL4_Word badge; 514 seL4_Word mr0; 515 516 x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &mr0, 0); 517 518 seL4_SetMR(0, mr0); 519 520 if (sender) { 521 *sender = badge; 522 } 523 524 return info; 525} 526 527LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender, 528 seL4_Word *mr0) 529{ 530 seL4_MessageInfo_t info; 531 seL4_Word badge; 532 seL4_Word msg0 = 0; 533 534 x86_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, 0); 535 536 if (mr0 != seL4_Null) { 537 *mr0 = msg0; 538 } 539 540 if (sender) { 541 *sender = badge; 542 } 543 544 return info; 545} 546 547LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender) 548{ 549 seL4_MessageInfo_t info; 550 seL4_Word badge; 551 seL4_Word mr0; 552 553 x86_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &mr0, 0); 554 555 seL4_SetMR(0, mr0); 556 557 if (sender) { 558 *sender = badge; 559 } 560 561 return info; 562} 563#endif /* CONFIG_KERNEL_MCS */ 564 565LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) 566{ 567 seL4_MessageInfo_t info; 568 seL4_Word mr0 = seL4_GetMR(0); 569 LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); 570 571 x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, MCS_COND(0, &mr1)); 572 573 seL4_SetMR(0, mr0); 574#ifndef CONFIG_KERNEL_MCS 575 seL4_SetMR(1, mr1); 576#endif 577 578 return info; 579} 580 581#ifdef CONFIG_KERNEL_MCS 582LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, 583 seL4_Word *mr0) 584#else 585LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, 586 seL4_Word *mr0, seL4_Word *mr1) 587#endif 588{ 589 seL4_MessageInfo_t info; 590 seL4_Word msg0 = 0; 591 LIBSEL4_UNUSED seL4_Word msg1 = 0; 592 593 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { 594 msg0 = *mr0; 595 } 596 597#ifndef CONFIG_KERNEL_MCS 598 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) { 599 msg1 = *mr1; 600 } 601#endif 602 603 x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, MCS_COND(0, &msg1)); 604 605 if (mr0 != seL4_Null) { 606 *mr0 = msg0; 607 } 608#ifndef CONFIG_KERNEL_MCS 609 if (mr1 != seL4_Null) { 610 *mr1 = msg1; 611 } 612#endif 613 614 return info; 615} 616 617#ifdef CONFIG_KERNEL_MCS 618LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, 619 seL4_CPtr reply) 620#else 621LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) 622#endif 623{ 624 seL4_MessageInfo_t info; 625 seL4_Word badge; 626 seL4_Word mr0 = seL4_GetMR(0); 627 LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); 628 629 x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0, 630 MCS_COND(reply, &mr1)); 631 632 seL4_SetMR(0, mr0); 633#ifndef CONFIG_KERNEL_MCS 634 seL4_SetMR(1, mr1); 635#endif 636 637 if (sender) { 638 *sender = badge; 639 } 640 641 return info; 642} 643 644#ifdef CONFIG_KERNEL_MCS 645LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, 646 seL4_Word *sender, 647 seL4_Word *mr0, seL4_CPtr reply) 648#else 649LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, 650 seL4_Word *sender, 651 seL4_Word *mr0, seL4_Word *mr1) 652#endif 653{ 654 seL4_MessageInfo_t info; 655 seL4_Word badge; 656 seL4_Word msg0 = 0; 657 LIBSEL4_UNUSED seL4_Word msg1 = 0; 658 659 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { 660 msg0 = *mr0; 661 } 662 663#ifndef CONFIG_KERNEL_MCS 664 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) { 665 msg1 = *mr1; 666 } 667#endif 668 x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, MCS_COND(0, &msg1)); 669 670 if (mr0 != seL4_Null) { 671 *mr0 = msg0; 672 } 673#ifndef CONFIG_KERNEL_MCS 674 if (mr1 != seL4_Null) { 675 *mr1 = msg1; 676 } 677#endif 678 679 if (sender) { 680 *sender = badge; 681 } 682 683 return info; 684} 685 686#ifdef CONFIG_KERNEL_MCS 687LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, 688 seL4_Word *sender, seL4_CPtr reply) 689{ 690 seL4_MessageInfo_t info; 691 seL4_Word badge; 692 seL4_Word mr0 = seL4_GetMR(0); 693 694 /* no spare registers on ia32 -> must use ipc buffer */ 695 seL4_SetUserData(dest); 696 697 x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &mr0, reply); 698 699 seL4_SetMR(0, mr0); 700 701 if (sender) { 702 *sender = badge; 703 } 704 705 return info; 706} 707 708LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, 709 seL4_Word *sender, 710 seL4_Word *mr0, seL4_CPtr reply) 711{ 712 seL4_MessageInfo_t info; 713 seL4_Word badge; 714 seL4_Word msg0 = 0; 715 716 /* no spare registers on ia32 -> must use ipc buffer */ 717 seL4_SetUserData(dest); 718 719 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { 720 msg0 = *mr0; 721 } 722 723 x86_sys_nbsend_wait(seL4_SysNBSendRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, reply); 724 725 if (mr0 != seL4_Null) { 726 *mr0 = msg0; 727 } 728 729 if (sender) { 730 *sender = badge; 731 } 732 733 return info; 734} 735 736LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, 737 seL4_Word *sender) 738{ 739 seL4_MessageInfo_t info; 740 seL4_Word badge; 741 seL4_Word mr0 = seL4_GetMR(0); 742 743 x86_sys_nbsend_wait(seL4_SysNBSendWait, src, &badge, msgInfo.words[0], &info.words[0], &mr0, dest); 744 745 seL4_SetMR(0, mr0); 746 747 if (sender) { 748 *sender = badge; 749 } 750 751 return info; 752} 753 754LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word src, 755 seL4_Word *sender, 756 seL4_Word *mr0) 757{ 758 seL4_MessageInfo_t info; 759 seL4_Word badge; 760 seL4_Word msg0 = 0; 761 762 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { 763 msg0 = *mr0; 764 } 765 766 x86_sys_nbsend_wait(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, dest); 767 768 if (mr0 != seL4_Null) { 769 *mr0 = msg0; 770 } 771 772 if (sender) { 773 *sender = badge; 774 } 775 776 return info; 777} 778#endif /* CONFIG_KERNEL_MCS */ 779 780LIBSEL4_INLINE_FUNC void seL4_Yield(void) 781{ 782 x86_sys_null(seL4_SysYield); 783 asm volatile("" :::"%esi", "%edi", "memory"); 784} 785 786#ifdef CONFIG_VTX 787LIBSEL4_INLINE_FUNC seL4_Word seL4_VMEnter(seL4_Word *sender) 788{ 789 seL4_Word fault; 790 seL4_Word badge; 791 seL4_Word mr0 = seL4_GetMR(0); 792 LIBSEL4_UNUSED seL4_Word mr1 = MCS_COND(0, seL4_GetMR(1)); 793 794 x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, MCS_COND(0, &mr1)); 795 796 seL4_SetMR(0, mr0); 797#ifndef CONFIG_KERNEL_MCS 798 seL4_SetMR(1, mr1); 799#endif 800 if (!fault && sender) { 801 *sender = badge; 802 } 803 return fault; 804} 805#endif 806 807#ifdef CONFIG_PRINTING 808LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c) 809{ 810 seL4_Word unused0 = 0; 811 seL4_Word unused1 = 0; 812 seL4_Word unused2 = 0; 813 LIBSEL4_UNUSED seL4_Word unused3 = 0; 814 815 x86_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); 816} 817 818LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) 819{ 820 for (char *s = str; *s; s++) { 821 seL4_DebugPutChar(*s); 822 } 823 return; 824} 825 826 827LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void) 828{ 829 seL4_Word unused0 = 0; 830 seL4_Word unused1 = 0; 831 seL4_Word unused2 = 0; 832 LIBSEL4_UNUSED seL4_Word unused3 = 0; 833 834 x86_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); 835} 836#endif 837 838#ifdef CONFIG_DEBUG_BUILD 839LIBSEL4_INLINE_FUNC void seL4_DebugHalt(void) 840{ 841 x86_sys_null(seL4_SysDebugHalt); 842 asm volatile("" :::"%esi", "%edi", "memory"); 843} 844#endif 845 846#if defined(CONFIG_DEBUG_BUILD) 847LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot(void) 848{ 849 x86_sys_null(seL4_SysDebugSnapshot); 850 asm volatile("" :::"%esi", "%edi", "memory"); 851} 852#endif 853 854#ifdef CONFIG_DEBUG_BUILD 855LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap) 856{ 857 seL4_Word unused0 = 0; 858 seL4_Word unused1 = 0; 859 LIBSEL4_UNUSED seL4_Word unused2 = 0; 860 861 x86_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, MCS_COND(0, &unused2)); 862 return (seL4_Uint32)cap; 863} 864 865char *strcpy(char *, const char *); 866LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name) 867{ 868 strcpy((char *)seL4_GetIPCBuffer()->msg, name); 869 870 seL4_Word unused0 = 0; 871 seL4_Word unused1 = 0; 872 seL4_Word unused2 = 0; 873 LIBSEL4_UNUSED seL4_Word unused3 = 0; 874 875 x86_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3)); 876} 877#endif 878 879#if defined(CONFIG_DANGEROUS_CODE_INJECTION) 880LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (*userfn)(void *), void *userarg) 881{ 882 x86_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg); 883 asm volatile("" ::: "%edi", "memory"); 884} 885#endif 886 887#if defined(CONFIG_KERNEL_X86_DANGEROUS_MSR) 888LIBSEL4_INLINE_FUNC void seL4_X86DangerousWRMSR(seL4_Uint32 msr, seL4_Uint64 value) 889{ 890 seL4_Uint32 value_low = value & 0xffffffff; 891 seL4_Uint32 value_high = value >> 32; 892#ifdef CONFIG_KERNEL_MCS 893 /* MR1 doesn't get passed through MRs on CONFIG_KERNEL_MCS */ 894 seL4_SetMR(1, value_high); 895#endif 896 x86_sys_send(seL4_SysX86DangerousWRMSR, msr, 0, value_low, value_high); 897} 898LIBSEL4_INLINE_FUNC seL4_Uint64 seL4_X86DangerousRDMSR(seL4_Word msr) 899{ 900 seL4_Word unused0 = 0; 901 seL4_Word unused1 = 0; 902 seL4_Word low, high; 903 x86_sys_recv(seL4_SysX86DangerousRDMSR, msr, &unused0, &unused1, &low, MCS_COND(0, &high)); 904#ifdef CONFIG_KERNEL_MCS 905 /* MR1 doesn't get passed through MRs on CONFIG_KERNEL_MCS */ 906 *high = seL4_GetMR(1); 907#endif 908 909 return ((seL4_Uint64)low) | ((seL4_Uint64)high << 32); 910} 911#endif 912 913#ifdef CONFIG_ENABLE_BENCHMARKS 914LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void) 915{ 916 seL4_Word unused0 = 0; 917 seL4_Word unused1 = 0; 918 LIBSEL4_UNUSED seL4_Word unused2 = 0; 919 920 seL4_Word ret; 921 922 x86_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, MCS_COND(0, &unused2)); 923 924 return (seL4_Error)ret; 925} 926 927LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void) 928{ 929 seL4_Word unused0 = 0; 930 seL4_Word unused1 = 0; 931 LIBSEL4_UNUSED seL4_Word unused2 = 0; 932 seL4_Word index_ret; 933 x86_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, MCS_COND(0, &unused2)); 934 935 return (seL4_Word)index_ret; 936} 937 938LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr) 939{ 940 seL4_Word unused0 = 0; 941 seL4_Word unused1 = 0; 942 LIBSEL4_UNUSED seL4_Word unused2 = 0; 943 944 x86_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, MCS_COND(0, &unused2)); 945 946 return (seL4_Error) frame_cptr; 947} 948 949 950LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall(void) 951{ 952 x86_sys_null(seL4_SysBenchmarkNullSyscall); 953 asm volatile("" :::"%esi", "%edi", "memory"); 954} 955 956LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches(void) 957{ 958 x86_sys_null(seL4_SysBenchmarkFlushCaches); 959 asm volatile("" :::"%esi", "%edi", "memory"); 960} 961 962#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION 963LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr) 964{ 965 seL4_Word unused0 = 0; 966 seL4_Word unused1 = 0; 967 seL4_Word unused2 = 0; 968 LIBSEL4_UNUSED seL4_Word unused3 = 0; 969 970 x86_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, MCS_COND(0, 971 &unused3)); 972} 973 974LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr) 975{ 976 seL4_Word unused0 = 0; 977 seL4_Word unused1 = 0; 978 seL4_Word unused2 = 0; 979 LIBSEL4_UNUSED seL4_Word unused3 = 0; 980 981 x86_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, MCS_COND(0, 982 &unused3)); 983} 984 985#ifdef CONFIG_DEBUG_BUILD 986LIBSEL4_INLINE_FUNC void seL4_BenchmarkDumpAllThreadsUtilisation(void) 987{ 988 seL4_Word unused0 = 0; 989 seL4_Word unused1 = 0; 990 seL4_Word unused2 = 0; 991 LIBSEL4_UNUSED seL4_Word unused3 = 0; 992 993 x86_sys_send_recv(seL4_SysBenchmarkDumpAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, MCS_COND(0, 994 &unused3)); 995} 996 997LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkResetAllThreadsUtilisation(void) 998{ 999 seL4_Word unused0 = 0; 1000 seL4_Word unused1 = 0; 1001 seL4_Word unused2 = 0; 1002 LIBSEL4_UNUSED seL4_Word unused3 = 0; 1003 1004 x86_sys_send_recv(seL4_SysBenchmarkResetAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, MCS_COND(0, 1005 &unused3)); 1006} 1007 1008#endif /* CONFIG_DEBUG_BUILD */ 1009#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */ 1010#endif /* CONFIG_ENABLE_BENCHMARKS */ 1011 1012#ifdef CONFIG_SET_TLS_BASE_SELF 1013LIBSEL4_INLINE_FUNC void seL4_SetTLSBase(seL4_Word tls_base) 1014{ 1015 x86_sys_send_null(seL4_SysSetTLSBase, tls_base, 0); 1016 asm volatile("" ::: "memory"); 1017} 1018#endif /* CONFIG_SET_TLS_BASE_SELF */ 1019