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