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