1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
4 *
5 * SPDX-License-Identifier: BSD-2-Clause
6 */
7
8#pragma once
9
10#include <autoconf.h>
11#include <sel4/functions.h>
12#include <sel4/sel4_arch/syscalls.h>
13#include <sel4/types.h>
14
15#ifdef CONFIG_KERNEL_MCS
16#define MCS_PARAM_DECL(r)    register seL4_Word reply_reg asm(r) = reply
17#define MCS_PARAM    , "r"(reply_reg)
18#define LIBSEL4_MCS_REPLY reply
19#else
20#define MCS_PARAM_DECL(r)
21#define MCS_PARAM
22#define LIBSEL4_MCS_REPLY 0
23#endif
24
25static inline void riscv_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1,
26                                  seL4_Word mr2, seL4_Word mr3)
27{
28    register seL4_Word destptr asm("a0") = dest;
29    register seL4_Word info asm("a1") = info_arg;
30
31    /* Load beginning of the message into registers. */
32    register seL4_Word msg0 asm("a2") = mr0;
33    register seL4_Word msg1 asm("a3") = mr1;
34    register seL4_Word msg2 asm("a4") = mr2;
35    register seL4_Word msg3 asm("a5") = mr3;
36
37    /* Perform the system call. */
38    register seL4_Word scno asm("a7") = sys;
39    asm volatile(
40        "ecall"
41        : "+r"(destptr), "+r"(msg0), "+r"(msg1), "+r"(msg2),
42        "+r"(msg3), "+r"(info)
43        : "r"(scno)
44    );
45}
46
47#ifndef CONFIG_KERNEL_MCS
48static inline void riscv_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2,
49                                   seL4_Word mr3)
50{
51    register seL4_Word info asm("a1") = info_arg;
52
53    /* Load beginning of the message into registers. */
54    register seL4_Word msg0 asm("a2") = mr0;
55    register seL4_Word msg1 asm("a3") = mr1;
56    register seL4_Word msg2 asm("a4") = mr2;
57    register seL4_Word msg3 asm("a5") = mr3;
58
59    /* Perform the system call. */
60    register seL4_Word scno asm("a7") = sys;
61    asm volatile(
62        "ecall"
63        : "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
64        "+r"(info)
65        : "r"(scno)
66    );
67}
68#endif
69
70static inline void riscv_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg)
71{
72    register seL4_Word destptr asm("a0") = src;
73    register seL4_Word info asm("a1") = info_arg;
74
75    /* Perform the system call. */
76    register seL4_Word scno asm("a7") = sys;
77    asm volatile(
78        "ecall"
79        : "+r"(destptr), "+r"(info)
80        : "r"(scno)
81    );
82}
83
84static inline void riscv_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word
85                                  *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3, LIBSEL4_UNUSED seL4_Word reply)
86{
87    register seL4_Word src_and_badge asm("a0") = src;
88    register seL4_Word info asm("a1");
89
90    /* Incoming message registers. */
91    register seL4_Word msg0 asm("a2");
92    register seL4_Word msg1 asm("a3");
93    register seL4_Word msg2 asm("a4");
94    register seL4_Word msg3 asm("a5");
95    MCS_PARAM_DECL("a6");
96
97    /* Perform the system call. */
98    register seL4_Word scno asm("a7") = sys;
99    asm volatile(
100        "ecall"
101        : "=r"(msg0), "=r"(msg1), "=r"(msg2), "=r"(msg3),
102        "=r"(info), "+r"(src_and_badge)
103        : "r"(scno) MCS_PARAM
104        : "memory"
105    );
106    *out_badge = src_and_badge;
107    *out_info = info;
108    *out_mr0 = msg0;
109    *out_mr1 = msg1;
110    *out_mr2 = msg2;
111    *out_mr3 = msg3;
112}
113
114static inline void riscv_sys_null(seL4_Word sys)
115{
116    register seL4_Word scno asm("a7") = sys;
117    asm volatile(
118        "ecall"
119        : /* no outputs */
120        : "r"(scno)
121    );
122}
123
124static inline void riscv_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info_arg,
125                                       seL4_Word
126                                       *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
127                                       seL4_Word
128                                       *in_out_mr3, LIBSEL4_UNUSED seL4_Word reply)
129{
130    register seL4_Word destptr asm("a0") = dest;
131    register seL4_Word info asm("a1") = info_arg;
132
133    /* Load beginning of the message into registers. */
134    register seL4_Word msg0 asm("a2") = *in_out_mr0;
135    register seL4_Word msg1 asm("a3") = *in_out_mr1;
136    register seL4_Word msg2 asm("a4") = *in_out_mr2;
137    register seL4_Word msg3 asm("a5") = *in_out_mr3;
138    MCS_PARAM_DECL("a6");
139
140    /* Perform the system call. */
141    register seL4_Word scno asm("a7") = sys;
142    asm volatile(
143        "ecall"
144        : "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
145        "+r"(info), "+r"(destptr)
146        : "r"(scno) MCS_PARAM
147        : "memory"
148    );
149    *out_info = info;
150    *out_badge = destptr;
151    *in_out_mr0 = msg0;
152    *in_out_mr1 = msg1;
153    *in_out_mr2 = msg2;
154    *in_out_mr3 = msg3;
155}
156
157#ifdef CONFIG_KERNEL_MCS
158static inline void riscv_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_badge,
159                                         seL4_Word info_arg,
160                                         seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
161                                         seL4_Word *in_out_mr3, seL4_Word reply)
162{
163    register seL4_Word src_and_badge asm("a0") = src;
164    register seL4_Word info asm("a1") = info_arg;
165
166    /* Load the beginning of the message info registers */
167    register seL4_Word msg0 asm("a2") = *in_out_mr0;
168    register seL4_Word msg1 asm("a3") = *in_out_mr1;
169    register seL4_Word msg2 asm("a4") = *in_out_mr2;
170    register seL4_Word msg3 asm("a5") = *in_out_mr3;
171
172    register seL4_Word reply_reg asm("a6") = reply;
173    register seL4_Word dest_reg asm("t0") = dest;
174
175    /* Perform the system call. */
176    register seL4_Word scno asm("a7") = sys;
177    asm volatile(
178        "ecall"
179        : "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
180        "+r"(src_and_badge), "+r"(info)
181        : "r"(scno), "r"(reply_reg), "r"(dest_reg)
182        : "memory"
183    );
184
185    *out_badge = src_and_badge;
186    *out_info = info;
187    *in_out_mr0 = msg0;
188    *in_out_mr1 = msg1;
189    *in_out_mr2 = msg2;
190    *in_out_mr3 = msg3;
191}
192#endif
193
194LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
195{
196    riscv_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1),
197                   seL4_GetMR(2), seL4_GetMR(3));
198}
199
200LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
201                                          seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
202{
203    riscv_sys_send(seL4_SysSend, dest, msgInfo.words[0],
204                   mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
205                   mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
206                   mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
207                   mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
208                  );
209
210}
211
212LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
213{
214    riscv_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1),
215                   seL4_GetMR(2), seL4_GetMR(3));
216
217}
218
219LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
220                                            seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
221{
222    riscv_sys_send(seL4_SysNBSend, dest, msgInfo.words[0],
223                   mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
224                   mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
225                   mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
226                   mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
227                  );
228
229}
230
231#ifndef CONFIG_KERNEL_MCS
232LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo)
233{
234    riscv_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2),
235                    seL4_GetMR(3));
236}
237
238LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
239                                           seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
240{
241    riscv_sys_reply(seL4_SysReply, msgInfo.words[0],
242                    mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
243                    mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
244                    mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
245                    mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
246                   );
247
248}
249#endif
250
251LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest)
252{
253    riscv_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
254}
255
256#ifdef CONFIG_KERNEL_MCS
257LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
258#else
259LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender)
260#endif
261{
262    seL4_MessageInfo_t info;
263    seL4_Word badge;
264    seL4_Word msg0;
265    seL4_Word msg1;
266    seL4_Word msg2;
267    seL4_Word msg3;
268
269    riscv_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
270
271    seL4_SetMR(0, msg0);
272    seL4_SetMR(1, msg1);
273    seL4_SetMR(2, msg2);
274    seL4_SetMR(3, msg3);
275
276    /* Return back sender and message information. */
277    if (sender) {
278        *sender = badge;
279    }
280    return info;
281
282}
283
284#ifdef CONFIG_KERNEL_MCS
285LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply,
286                                                        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
287#else
288LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
289                                                        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
290#endif
291{
292    seL4_MessageInfo_t info;
293    seL4_Word badge;
294    seL4_Word msg0 = 0;
295    seL4_Word msg1 = 0;
296    seL4_Word msg2 = 0;
297    seL4_Word msg3 = 0;
298
299    riscv_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
300
301    /* Write the message back out to memory. */
302    if (mr0 != seL4_Null) {
303        *mr0 = msg0;
304    }
305    if (mr1 != seL4_Null) {
306        *mr1 = msg1;
307    }
308    if (mr2 != seL4_Null) {
309        *mr2 = msg2;
310    }
311    if (mr3 != seL4_Null) {
312        *mr3 = msg3;
313    }
314
315    /* Return back sender and message information. */
316    if (sender) {
317        *sender = badge;
318    }
319    return info;
320}
321
322#ifdef CONFIG_KERNEL_MCS
323LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
324#else
325LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender)
326#endif
327{
328    seL4_MessageInfo_t info;
329    seL4_Word badge;
330    seL4_Word msg0;
331    seL4_Word msg1;
332    seL4_Word msg2;
333    seL4_Word msg3;
334
335    riscv_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
336
337    seL4_SetMR(0, msg0);
338    seL4_SetMR(1, msg1);
339    seL4_SetMR(2, msg2);
340    seL4_SetMR(3, msg3);
341
342    /* Return back sender and message information. */
343    if (sender) {
344        *sender = badge;
345    }
346    return info;
347
348}
349
350LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
351{
352    seL4_MessageInfo_t info;
353    seL4_Word msg0 = seL4_GetMR(0);
354    seL4_Word msg1 = seL4_GetMR(1);
355    seL4_Word msg2 = seL4_GetMR(2);
356    seL4_Word msg3 = seL4_GetMR(3);
357
358    riscv_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1,
359                        &msg2, &msg3, 0);
360
361    /* Write out the data back to memory. */
362    seL4_SetMR(0, msg0);
363    seL4_SetMR(1, msg1);
364    seL4_SetMR(2, msg2);
365    seL4_SetMR(3, msg3);
366
367    return info;
368}
369
370#ifndef CONFIG_KERNEL_MCS
371LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender)
372{
373    seL4_Recv(src, sender);
374}
375#endif
376
377LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender)
378{
379#ifdef CONFIG_KERNEL_MCS
380    return seL4_NBWait(src, sender);
381#else
382    return seL4_NBRecv(src, sender);
383#endif
384}
385
386LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
387                                                        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
388{
389    seL4_MessageInfo_t info;
390    seL4_Word msg0 = 0;
391    seL4_Word msg1 = 0;
392    seL4_Word msg2 = 0;
393    seL4_Word msg3 = 0;
394
395    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
396        msg0 = *mr0;
397    }
398    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
399        msg1 = *mr1;
400    }
401    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
402        msg2 = *mr2;
403    }
404    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
405        msg3 = *mr3;
406    }
407
408    riscv_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1,
409                        &msg2, &msg3, 0);
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    return info;
425}
426
427#ifdef CONFIG_KERNEL_MCS
428LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
429                                                      seL4_CPtr reply)
430#else
431LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
432#endif
433{
434    seL4_MessageInfo_t info;
435    seL4_Word badge;
436    seL4_Word msg0;
437    seL4_Word msg1;
438    seL4_Word msg2;
439    seL4_Word msg3;
440
441    /* Load beginning of the message into registers. */
442    msg0 = seL4_GetMR(0);
443    msg1 = seL4_GetMR(1);
444    msg2 = seL4_GetMR(2);
445    msg3 = seL4_GetMR(3);
446
447    riscv_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
448                        LIBSEL4_MCS_REPLY);
449
450    /* Write the message back out to memory. */
451    seL4_SetMR(0, msg0);
452    seL4_SetMR(1, msg1);
453    seL4_SetMR(2, msg2);
454    seL4_SetMR(3, msg3);
455
456    /* Return back sender and message information. */
457    if (sender) {
458        *sender = badge;
459    }
460
461    return info;
462
463}
464
465#ifdef CONFIG_KERNEL_MCS
466LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
467                                                             seL4_Word *sender,
468                                                             seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
469#else
470LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
471                                                             seL4_Word *sender,
472                                                             seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
473#endif
474{
475    seL4_MessageInfo_t info;
476    seL4_Word badge;
477    seL4_Word msg0 = 0;
478    seL4_Word msg1 = 0;
479    seL4_Word msg2 = 0;
480    seL4_Word msg3 = 0;
481
482    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
483        msg0 = *mr0;
484    }
485    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
486        msg1 = *mr1;
487    }
488    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
489        msg2 = *mr2;
490    }
491    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
492        msg3 = *mr3;
493    }
494
495    riscv_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
496                        LIBSEL4_MCS_REPLY);
497
498    /* Write out the data back to memory. */
499    if (mr0 != seL4_Null) {
500        *mr0 = msg0;
501    }
502    if (mr1 != seL4_Null) {
503        *mr1 = msg1;
504    }
505    if (mr2 != seL4_Null) {
506        *mr2 = msg2;
507    }
508    if (mr3 != seL4_Null) {
509        *mr3 = msg3;
510    }
511
512    /* Return back sender and message information. */
513    if (sender) {
514        *sender = badge;
515    }
516
517    return info;
518}
519
520#ifdef CONFIG_KERNEL_MCS
521LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
522                                                       seL4_Word *sender, seL4_CPtr reply)
523{
524    seL4_MessageInfo_t info;
525    seL4_Word badge;
526    seL4_Word msg0;
527    seL4_Word msg1;
528    seL4_Word msg2;
529    seL4_Word msg3;
530
531    /* Load beginning of the message into registers. */
532    msg0 = seL4_GetMR(0);
533    msg1 = seL4_GetMR(1);
534    msg2 = seL4_GetMR(2);
535    msg3 = seL4_GetMR(3);
536
537    riscv_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2,
538                          &msg3,
539                          reply);
540
541    /* Write the message back out to memory. */
542    seL4_SetMR(0, msg0);
543    seL4_SetMR(1, msg1);
544    seL4_SetMR(2, msg2);
545    seL4_SetMR(3, msg3);
546
547    /* Return back sender and message information. */
548    if (sender) {
549        *sender = badge;
550    }
551
552    return info;
553}
554
555LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
556                                                              seL4_Word *sender,
557                                                              seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
558{
559    seL4_MessageInfo_t info;
560    seL4_Word badge;
561    seL4_Word msg0 = 0;
562    seL4_Word msg1 = 0;
563    seL4_Word msg2 = 0;
564    seL4_Word msg3 = 0;
565
566    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
567        msg0 = *mr0;
568    }
569    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
570        msg1 = *mr1;
571    }
572    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
573        msg2 = *mr2;
574    }
575    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
576        msg3 = *mr3;
577    }
578
579    riscv_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2,
580                          &msg3,
581                          reply);
582
583    /* Write out the data back to memory. */
584    if (mr0 != seL4_Null) {
585        *mr0 = msg0;
586    }
587    if (mr1 != seL4_Null) {
588        *mr1 = msg1;
589    }
590    if (mr2 != seL4_Null) {
591        *mr2 = msg2;
592    }
593    if (mr3 != seL4_Null) {
594        *mr3 = msg3;
595    }
596
597    /* Return back sender and message information. */
598    if (sender) {
599        *sender = badge;
600    }
601
602    return info;
603}
604
605LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
606                                                       seL4_Word *sender)
607{
608    seL4_MessageInfo_t info;
609    seL4_Word badge;
610    seL4_Word msg0;
611    seL4_Word msg1;
612    seL4_Word msg2;
613    seL4_Word msg3;
614
615    /* Load beginning of the message into registers. */
616    msg0 = seL4_GetMR(0);
617    msg1 = seL4_GetMR(1);
618    msg2 = seL4_GetMR(2);
619    msg3 = seL4_GetMR(3);
620
621    riscv_sys_nbsend_recv(seL4_SysNBSendWait, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
622                          dest);
623
624    /* Write the message back out to memory. */
625    seL4_SetMR(0, msg0);
626    seL4_SetMR(1, msg1);
627    seL4_SetMR(2, msg2);
628    seL4_SetMR(3, msg3);
629
630    /* Return back sender and message information. */
631    if (sender) {
632        *sender = badge;
633    }
634
635    return info;
636}
637
638LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
639                                                              seL4_Word *sender,
640                                                              seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
641{
642    seL4_MessageInfo_t info;
643    seL4_Word badge;
644    seL4_Word msg0 = 0;
645    seL4_Word msg1 = 0;
646    seL4_Word msg2 = 0;
647    seL4_Word msg3 = 0;
648
649    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
650        msg0 = *mr0;
651    }
652    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
653        msg1 = *mr1;
654    }
655    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
656        msg2 = *mr2;
657    }
658    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
659        msg3 = *mr3;
660    }
661
662    riscv_sys_nbsend_recv(seL4_SysNBSendRecv, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
663                          dest);
664
665    /* Write out the data back to memory. */
666    if (mr0 != seL4_Null) {
667        *mr0 = msg0;
668    }
669    if (mr1 != seL4_Null) {
670        *mr1 = msg1;
671    }
672    if (mr2 != seL4_Null) {
673        *mr2 = msg2;
674    }
675    if (mr3 != seL4_Null) {
676        *mr3 = msg3;
677    }
678
679    /* Return back sender and message information. */
680    if (sender) {
681        *sender = badge;
682    }
683
684    return info;
685}
686#endif
687
688LIBSEL4_INLINE_FUNC void seL4_Yield(void)
689{
690    register seL4_Word scno asm("a7") = seL4_SysYield;
691    asm volatile("ecall" :: "r"(scno));
692}
693
694#ifdef CONFIG_KERNEL_MCS
695LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender)
696{
697    seL4_MessageInfo_t info;
698    seL4_Word badge;
699    seL4_Word msg0;
700    seL4_Word msg1;
701    seL4_Word msg2;
702    seL4_Word msg3;
703
704    riscv_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
705
706    seL4_SetMR(0, msg0);
707    seL4_SetMR(1, msg1);
708    seL4_SetMR(2, msg2);
709    seL4_SetMR(3, msg3);
710
711    /* Return back sender and message information. */
712    if (sender) {
713        *sender = badge;
714    }
715    return info;
716}
717
718LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender,
719                                                        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
720{
721    seL4_MessageInfo_t info;
722    seL4_Word badge;
723    seL4_Word msg0 = 0;
724    seL4_Word msg1 = 0;
725    seL4_Word msg2 = 0;
726    seL4_Word msg3 = 0;
727
728    riscv_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
729
730    /* Write the message back out to memory. */
731    if (mr0 != seL4_Null) {
732        *mr0 = msg0;
733    }
734    if (mr1 != seL4_Null) {
735        *mr1 = msg1;
736    }
737    if (mr2 != seL4_Null) {
738        *mr2 = msg2;
739    }
740    if (mr3 != seL4_Null) {
741        *mr3 = msg3;
742    }
743
744    /* Return back sender and message information. */
745    if (sender) {
746        *sender = badge;
747    }
748    return info;
749}
750
751LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender)
752{
753    seL4_MessageInfo_t info;
754    seL4_Word badge;
755    seL4_Word msg0;
756    seL4_Word msg1;
757    seL4_Word msg2;
758    seL4_Word msg3;
759
760    riscv_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
761
762    seL4_SetMR(0, msg0);
763    seL4_SetMR(1, msg1);
764    seL4_SetMR(2, msg2);
765    seL4_SetMR(3, msg3);
766
767    /* Return back sender and message information. */
768    if (sender) {
769        *sender = badge;
770    }
771    return info;
772}
773#endif
774
775#ifdef CONFIG_PRINTING
776LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
777{
778    seL4_Word unused0 = 0;
779    seL4_Word unused1 = 0;
780    seL4_Word unused2 = 0;
781    seL4_Word unused3 = 0;
782    seL4_Word unused4 = 0;
783    seL4_Word unused5 = 0;
784
785    riscv_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3,
786                        &unused4, &unused5, 0);
787}
788
789LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
790{
791    for (char *s = str; *s; s++) {
792        seL4_DebugPutChar(*s);
793    }
794    return;
795}
796
797LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
798{
799    seL4_Word unused0 = 0;
800    seL4_Word unused1 = 0;
801    seL4_Word unused2 = 0;
802    seL4_Word unused3 = 0;
803    seL4_Word unused4 = 0;
804    seL4_Word unused5 = 0;
805
806    riscv_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3,
807                        &unused4, &unused5, 0);
808}
809#endif
810
811#ifdef CONFIG_DEBUG_BUILD
812LIBSEL4_INLINE_FUNC void seL4_DebugHalt(void)
813{
814    register seL4_Word scno asm("a7") = seL4_SysDebugHalt;
815    asm volatile("ecall" :: "r"(scno) : "memory");
816}
817
818LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot(void)
819{
820    register seL4_Word scno asm("a7") = seL4_SysDebugSnapshot;
821    asm volatile("ecall" ::"r"(scno) : "memory");
822}
823
824LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
825{
826    seL4_Word unused0 = 0;
827    seL4_Word unused1 = 0;
828    seL4_Word unused2 = 0;
829    seL4_Word unused3 = 0;
830    seL4_Word unused4 = 0;
831
832    riscv_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2,
833                        &unused3, &unused4, 0);
834    return (seL4_Uint32)cap;
835}
836
837char *strcpy(char *, const char *);
838LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
839{
840    strcpy((char *)seL4_GetIPCBuffer()->msg, name);
841
842    seL4_Word unused0 = 0;
843    seL4_Word unused1 = 0;
844    seL4_Word unused2 = 0;
845    seL4_Word unused3 = 0;
846    seL4_Word unused4 = 0;
847    seL4_Word unused5 = 0;
848
849    riscv_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3,
850                        &unused4, &unused5, 0);
851}
852#endif
853
854#ifdef CONFIG_DANGEROUS_CODE_INJECTION
855LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (* userfn)(void *), void *userarg)
856{
857    register seL4_Word arg1 asm("a0") = (seL4_Word)userfn;
858    register seL4_Word arg2 asm("a1") = (seL4_Word)userarg;
859    register seL4_Word scno asm("a7") = seL4_SysDebugRun;
860    asm volatile("ecall" : "+r"(arg1) : "r"(arg2), "r"(scno));
861}
862#endif
863
864#ifdef CONFIG_ENABLE_BENCHMARKS
865/* set the log index back to 0 */
866LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void)
867{
868    seL4_Word unused0 = 0;
869    seL4_Word unused1 = 0;
870    seL4_Word unused2 = 0;
871    seL4_Word unused3 = 0;
872    seL4_Word unused4 = 0;
873
874    seL4_Word ret;
875    riscv_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
876
877    return (seL4_Error) ret;
878}
879
880LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void)
881{
882    seL4_Word unused0 = 0;
883    seL4_Word unused1 = 0;
884    seL4_Word unused2 = 0;
885    seL4_Word unused3 = 0;
886    seL4_Word unused4 = 0;
887
888    seL4_Word index_ret;
889    riscv_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4,
890                        0);
891
892    return (seL4_Word) index_ret;
893}
894
895LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
896{
897    seL4_Word unused0 = 0;
898    seL4_Word unused1 = 0;
899    seL4_Word unused2 = 0;
900    seL4_Word unused3 = 0;
901    seL4_Word unused4 = 0;
902
903    riscv_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3,
904                        &unused4, 0);
905
906    return (seL4_Error) frame_cptr;
907}
908
909LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall(void)
910{
911    riscv_sys_null(seL4_SysBenchmarkNullSyscall);
912    asm volatile("" ::: "memory");
913}
914
915LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches(void)
916{
917    riscv_sys_send_null(seL4_SysBenchmarkFlushCaches, 0, 0);
918    asm volatile("" ::: "memory");
919}
920
921LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushL1Caches(seL4_Word cache_type)
922{
923    riscv_sys_send_null(seL4_SysBenchmarkFlushCaches, 1, cache_type);
924    asm volatile("" ::: "memory");
925}
926
927#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
928LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
929{
930    seL4_Word unused0 = 0;
931    seL4_Word unused1 = 0;
932    seL4_Word unused2 = 0;
933    seL4_Word unused3 = 0;
934    seL4_Word unused4 = 0;
935    seL4_Word unused5 = 0;
936
937    riscv_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3,
938                        &unused4, &unused5, 0);
939}
940
941LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
942{
943    seL4_Word unused0 = 0;
944    seL4_Word unused1 = 0;
945    seL4_Word unused2 = 0;
946    seL4_Word unused3 = 0;
947    seL4_Word unused4 = 0;
948    seL4_Word unused5 = 0;
949
950    riscv_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3,
951                        &unused4, &unused5, 0);
952}
953#ifdef CONFIG_DEBUG_BUILD
954LIBSEL4_INLINE_FUNC void seL4_BenchmarkDumpAllThreadsUtilisation(void)
955{
956    seL4_Word unused0 = 0;
957    seL4_Word unused1 = 0;
958    seL4_Word unused2 = 0;
959    seL4_Word unused3 = 0;
960    seL4_Word unused4 = 0;
961    seL4_Word unused5 = 0;
962
963    riscv_sys_send_recv(seL4_SysBenchmarkDumpAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
964                        &unused5, 0);
965}
966
967LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetAllThreadsUtilisation(void)
968{
969    seL4_Word unused0 = 0;
970    seL4_Word unused1 = 0;
971    seL4_Word unused2 = 0;
972    seL4_Word unused3 = 0;
973    seL4_Word unused4 = 0;
974    seL4_Word unused5 = 0;
975
976    riscv_sys_send_recv(seL4_SysBenchmarkResetAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
977                        &unused5, 0);
978}
979#endif
980#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
981#endif /* CONFIG_ENABLE_BENCHMARKS */
982
983#ifdef CONFIG_SET_TLS_BASE_SELF
984LIBSEL4_INLINE_FUNC void seL4_SetTLSBase(seL4_Word tls_base)
985{
986    riscv_sys_send_null(seL4_SysSetTLSBase, tls_base, 0);
987    asm volatile("" ::: "memory");
988}
989#endif /* CONFIG_SET_TLS_BASE_SELF */
990