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