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
riscv_sys_send(seL4_Word sys,seL4_Word dest,seL4_Word info_arg,seL4_Word mr0,seL4_Word mr1,seL4_Word mr2,seL4_Word mr3)25 static 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
riscv_sys_reply(seL4_Word sys,seL4_Word info_arg,seL4_Word mr0,seL4_Word mr1,seL4_Word mr2,seL4_Word mr3)48 static 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
riscv_sys_send_null(seL4_Word sys,seL4_Word src,seL4_Word info_arg)70 static 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
riscv_sys_recv(seL4_Word sys,seL4_Word src,seL4_Word * out_badge,seL4_Word * out_info,seL4_Word * out_mr0,seL4_Word * out_mr1,seL4_Word * out_mr2,seL4_Word * out_mr3,LIBSEL4_UNUSED seL4_Word reply)84 static 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
riscv_sys_null(seL4_Word sys)114 static 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
riscv_sys_send_recv(seL4_Word sys,seL4_Word dest,seL4_Word * out_badge,seL4_Word info_arg,seL4_Word * out_info,seL4_Word * in_out_mr0,seL4_Word * in_out_mr1,seL4_Word * in_out_mr2,seL4_Word * in_out_mr3,LIBSEL4_UNUSED seL4_Word reply)124 static 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
riscv_sys_nbsend_recv(seL4_Word sys,seL4_Word dest,seL4_Word src,seL4_Word * out_badge,seL4_Word info_arg,seL4_Word * out_info,seL4_Word * in_out_mr0,seL4_Word * in_out_mr1,seL4_Word * in_out_mr2,seL4_Word * in_out_mr3,seL4_Word reply)158 static 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
seL4_Send(seL4_CPtr dest,seL4_MessageInfo_t msgInfo)194 LIBSEL4_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
seL4_SendWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)200 LIBSEL4_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
seL4_NBSend(seL4_CPtr dest,seL4_MessageInfo_t msgInfo)212 LIBSEL4_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
seL4_NBSendWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)219 LIBSEL4_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
seL4_Reply(seL4_MessageInfo_t msgInfo)232 LIBSEL4_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
seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)238 LIBSEL4_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
seL4_Signal(seL4_CPtr dest)251 LIBSEL4_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
seL4_Recv(seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply)257 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
258 #else
259 LIBSEL4_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
seL4_RecvWithMRs(seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)285 LIBSEL4_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
288 LIBSEL4_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
seL4_NBRecv(seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply)323 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
324 #else
325 LIBSEL4_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
seL4_Call(seL4_CPtr dest,seL4_MessageInfo_t msgInfo)350 LIBSEL4_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
seL4_Wait(seL4_CPtr src,seL4_Word * sender)371 LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender)
372 {
373 seL4_Recv(src, sender);
374 }
375 #endif
376
seL4_Poll(seL4_CPtr src,seL4_Word * sender)377 LIBSEL4_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
seL4_CallWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)386 LIBSEL4_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
seL4_ReplyRecv(seL4_CPtr src,seL4_MessageInfo_t msgInfo,seL4_Word * sender,seL4_CPtr reply)428 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
429 seL4_CPtr reply)
430 #else
431 LIBSEL4_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
seL4_ReplyRecvWithMRs(seL4_CPtr src,seL4_MessageInfo_t msgInfo,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3,seL4_CPtr reply)466 LIBSEL4_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
470 LIBSEL4_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
seL4_NBSendRecv(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply)521 LIBSEL4_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
seL4_NBSendRecvWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3,seL4_CPtr reply)555 LIBSEL4_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
seL4_NBSendWait(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender)605 LIBSEL4_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
seL4_NBSendWaitWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)638 LIBSEL4_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
seL4_Yield(void)688 LIBSEL4_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
seL4_Wait(seL4_CPtr src,seL4_Word * sender)695 LIBSEL4_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
seL4_WaitWithMRs(seL4_CPtr src,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)718 LIBSEL4_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
seL4_NBWait(seL4_CPtr src,seL4_Word * sender)751 LIBSEL4_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
seL4_DebugPutChar(char c)776 LIBSEL4_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
seL4_DebugPutString(char * str)789 LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
790 {
791 for (char *s = str; *s; s++) {
792 seL4_DebugPutChar(*s);
793 }
794 return;
795 }
796
seL4_DebugDumpScheduler(void)797 LIBSEL4_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
seL4_DebugHalt(void)812 LIBSEL4_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
seL4_DebugSnapshot(void)818 LIBSEL4_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
seL4_DebugCapIdentify(seL4_CPtr cap)824 LIBSEL4_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
837 char *strcpy(char *, const char *);
seL4_DebugNameThread(seL4_CPtr tcb,const char * name)838 LIBSEL4_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
seL4_DebugRun(void (* userfn)(void *),void * userarg)855 LIBSEL4_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 */
seL4_BenchmarkResetLog(void)866 LIBSEL4_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
seL4_BenchmarkFinalizeLog(void)880 LIBSEL4_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
seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)895 LIBSEL4_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
seL4_BenchmarkNullSyscall(void)909 LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall(void)
910 {
911 riscv_sys_null(seL4_SysBenchmarkNullSyscall);
912 asm volatile("" ::: "memory");
913 }
914
seL4_BenchmarkFlushCaches(void)915 LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches(void)
916 {
917 riscv_sys_send_null(seL4_SysBenchmarkFlushCaches, 0, 0);
918 asm volatile("" ::: "memory");
919 }
920
seL4_BenchmarkFlushL1Caches(seL4_Word cache_type)921 LIBSEL4_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
seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)928 LIBSEL4_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
seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)941 LIBSEL4_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
seL4_BenchmarkDumpAllThreadsUtilisation(void)954 LIBSEL4_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
seL4_BenchmarkResetAllThreadsUtilisation(void)967 LIBSEL4_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
seL4_SetTLSBase(seL4_Word tls_base)984 LIBSEL4_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