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