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