1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13#ifndef __LIBSEL4_ARCH_SYSCALLS_H
14#define __LIBSEL4_ARCH_SYSCALLS_H
15
16#include <autoconf.h>
17#include <sel4/arch/functions.h>
18#include <sel4/sel4_arch/syscalls.h>
19#include <sel4/types.h>
20
21LIBSEL4_INLINE_FUNC void
22seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
23{
24    arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
25}
26
27LIBSEL4_INLINE_FUNC void
28seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
29                 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
30{
31    arm_sys_send(seL4_SysSend, dest, msgInfo.words[0],
32                 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
33                 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
34                 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
35                 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
36                );
37}
38
39LIBSEL4_INLINE_FUNC void
40seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
41{
42    arm_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
46seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
47                   seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
48{
49    arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0],
50                 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
51                 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
52                 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
53                 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
54                );
55}
56
57LIBSEL4_INLINE_FUNC void
58seL4_Reply(seL4_MessageInfo_t msgInfo)
59{
60    arm_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
61}
62
63LIBSEL4_INLINE_FUNC void
64seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
65                  seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
66{
67    arm_sys_reply(seL4_SysReply, msgInfo.words[0],
68                  mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
69                  mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
70                  mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
71                  mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
72                 );
73}
74
75LIBSEL4_INLINE_FUNC void
76seL4_Signal(seL4_CPtr dest)
77{
78    arm_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
79}
80
81LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
82seL4_Recv(seL4_CPtr src, seL4_Word* sender)
83{
84    seL4_MessageInfo_t info;
85    seL4_Word badge;
86    seL4_Word msg0;
87    seL4_Word msg1;
88    seL4_Word msg2;
89    seL4_Word msg3;
90
91    arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
92
93    seL4_SetMR(0, msg0);
94    seL4_SetMR(1, msg1);
95    seL4_SetMR(2, msg2);
96    seL4_SetMR(3, msg3);
97
98    /* Return back sender and message information. */
99    if (sender) {
100        *sender = badge;
101    }
102    return info;
103}
104
105LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
106seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender,
107                 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
108{
109    seL4_MessageInfo_t info;
110    seL4_Word badge;
111    seL4_Word msg0 = 0;
112    seL4_Word msg1 = 0;
113    seL4_Word msg2 = 0;
114    seL4_Word msg3 = 0;
115
116    arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
117
118    /* Write the message back out to memory. */
119    if (mr0 != seL4_Null) {
120        *mr0 = msg0;
121    }
122    if (mr1 != seL4_Null) {
123        *mr1 = msg1;
124    }
125    if (mr2 != seL4_Null) {
126        *mr2 = msg2;
127    }
128    if (mr3 != seL4_Null) {
129        *mr3 = msg3;
130    }
131
132    /* Return back sender and message information. */
133    if (sender) {
134        *sender = badge;
135    }
136    return info;
137}
138
139LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
140seL4_NBRecv(seL4_CPtr src, seL4_Word* sender)
141{
142    seL4_MessageInfo_t info;
143    seL4_Word badge;
144    seL4_Word msg0;
145    seL4_Word msg1;
146    seL4_Word msg2;
147    seL4_Word msg3;
148
149    arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3);
150
151    seL4_SetMR(0, msg0);
152    seL4_SetMR(1, msg1);
153    seL4_SetMR(2, msg2);
154    seL4_SetMR(3, msg3);
155
156    /* Return back sender and message information. */
157    if (sender) {
158        *sender = badge;
159    }
160    return info;
161}
162
163LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
164seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
165{
166    seL4_MessageInfo_t info;
167    seL4_Word msg0 = seL4_GetMR(0);
168    seL4_Word msg1 = seL4_GetMR(1);
169    seL4_Word msg2 = seL4_GetMR(2);
170    seL4_Word msg3 = seL4_GetMR(3);
171
172    arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
173
174    /* Write out the data back to memory. */
175    seL4_SetMR(0, msg0);
176    seL4_SetMR(1, msg1);
177    seL4_SetMR(2, msg2);
178    seL4_SetMR(3, msg3);
179
180    return info;
181}
182
183LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
184seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
185                 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
186{
187    seL4_MessageInfo_t info;
188    seL4_Word msg0 = 0;
189    seL4_Word msg1 = 0;
190    seL4_Word msg2 = 0;
191    seL4_Word msg3 = 0;
192
193    /* Load beginning of the message into registers. */
194    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
195        msg0 = *mr0;
196    }
197    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
198        msg1 = *mr1;
199    }
200    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
201        msg2 = *mr2;
202    }
203    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
204        msg3 = *mr3;
205    }
206
207    arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
208
209    /* Write out the data back to memory. */
210    if (mr0 != seL4_Null) {
211        *mr0 = msg0;
212    }
213    if (mr1 != seL4_Null) {
214        *mr1 = msg1;
215    }
216    if (mr2 != seL4_Null) {
217        *mr2 = msg2;
218    }
219    if (mr3 != seL4_Null) {
220        *mr3 = msg3;
221    }
222
223    return info;
224}
225
226LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
227seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
228{
229    seL4_MessageInfo_t info;
230    seL4_Word badge;
231    seL4_Word msg0;
232    seL4_Word msg1;
233    seL4_Word msg2;
234    seL4_Word msg3;
235
236    /* Load beginning of the message into registers. */
237    msg0 = seL4_GetMR(0);
238    msg1 = seL4_GetMR(1);
239    msg2 = seL4_GetMR(2);
240    msg3 = seL4_GetMR(3);
241
242    arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
243
244    /* Write the message back out to memory. */
245    seL4_SetMR(0, msg0);
246    seL4_SetMR(1, msg1);
247    seL4_SetMR(2, msg2);
248    seL4_SetMR(3, msg3);
249
250    /* Return back sender and message information. */
251    if (sender) {
252        *sender = badge;
253    }
254
255    return info;
256}
257
258LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
259seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
260                      seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
261{
262    seL4_MessageInfo_t info;
263    seL4_Word badge;
264    seL4_Word msg0 = 0;
265    seL4_Word msg1 = 0;
266    seL4_Word msg2 = 0;
267    seL4_Word msg3 = 0;
268
269    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
270        msg0 = *mr0;
271    }
272    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
273        msg1 = *mr1;
274    }
275    if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
276        msg2 = *mr2;
277    }
278    if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
279        msg3 = *mr3;
280    }
281
282    arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3);
283
284    /* Write out the data back to memory. */
285    if (mr0 != seL4_Null) {
286        *mr0 = msg0;
287    }
288    if (mr1 != seL4_Null) {
289        *mr1 = msg1;
290    }
291    if (mr2 != seL4_Null) {
292        *mr2 = msg2;
293    }
294    if (mr3 != seL4_Null) {
295        *mr3 = msg3;
296    }
297
298    /* Return back sender and message information. */
299    if (sender) {
300        *sender = badge;
301    }
302
303    return info;
304}
305
306LIBSEL4_INLINE_FUNC void
307seL4_Yield(void)
308{
309    arm_sys_null(seL4_SysYield);
310    asm volatile("" ::: "memory");
311}
312
313#ifdef CONFIG_PRINTING
314LIBSEL4_INLINE_FUNC void
315seL4_DebugPutChar(char c)
316{
317    seL4_Word unused0 = 0;
318    seL4_Word unused1 = 0;
319    seL4_Word unused2 = 0;
320    seL4_Word unused3 = 0;
321    seL4_Word unused4 = 0;
322    seL4_Word unused5 = 0;
323
324    arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
325}
326
327LIBSEL4_INLINE_FUNC void
328seL4_DebugDumpScheduler(void)
329{
330    seL4_Word unused0 = 0;
331    seL4_Word unused1 = 0;
332    seL4_Word unused2 = 0;
333    seL4_Word unused3 = 0;
334    seL4_Word unused4 = 0;
335    seL4_Word unused5 = 0;
336
337    arm_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
338}
339#endif
340
341#if CONFIG_DEBUG_BUILD
342LIBSEL4_INLINE_FUNC void
343seL4_DebugHalt(void)
344{
345    arm_sys_null(seL4_SysDebugHalt);
346}
347
348LIBSEL4_INLINE_FUNC void
349seL4_DebugSnapshot(void)
350{
351    arm_sys_null(seL4_SysDebugSnapshot);
352    asm volatile("" ::: "memory");
353}
354
355LIBSEL4_INLINE_FUNC seL4_Uint32
356seL4_DebugCapIdentify(seL4_CPtr cap)
357{
358    seL4_Word unused0 = 0;
359    seL4_Word unused1 = 0;
360    seL4_Word unused2 = 0;
361    seL4_Word unused3 = 0;
362    seL4_Word unused4 = 0;
363
364    arm_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
365    return (seL4_Uint32)cap;
366}
367
368char *strcpy(char *, const char *);
369LIBSEL4_INLINE_FUNC void
370seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
371{
372    strcpy((char*)seL4_GetIPCBuffer()->msg, name);
373
374    seL4_Word unused0 = 0;
375    seL4_Word unused1 = 0;
376    seL4_Word unused2 = 0;
377    seL4_Word unused3 = 0;
378    seL4_Word unused4 = 0;
379    seL4_Word unused5 = 0;
380
381    arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
382}
383#endif
384
385#ifdef CONFIG_DANGEROUS_CODE_INJECTION
386LIBSEL4_INLINE_FUNC void
387seL4_DebugRun(void (* userfn) (void *), void* userarg)
388{
389    arm_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg);
390    asm volatile("" ::: "memory");
391}
392#endif
393
394#ifdef CONFIG_ENABLE_BENCHMARKS
395/* set the log index back to 0 */
396LIBSEL4_INLINE_FUNC seL4_Error
397seL4_BenchmarkResetLog(void)
398{
399    seL4_Word unused0 = 0;
400    seL4_Word unused1 = 0;
401    seL4_Word unused2 = 0;
402    seL4_Word unused3 = 0;
403    seL4_Word unused4 = 0;
404
405    seL4_Word ret;
406    arm_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
407
408    return (seL4_Error) ret;
409}
410
411LIBSEL4_INLINE_FUNC seL4_Word
412seL4_BenchmarkFinalizeLog(void)
413{
414    seL4_Word unused0 = 0;
415    seL4_Word unused1 = 0;
416    seL4_Word unused2 = 0;
417    seL4_Word unused3 = 0;
418    seL4_Word unused4 = 0;
419    seL4_Word index_ret;
420    arm_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
421
422    return (seL4_Word)index_ret;
423}
424
425LIBSEL4_INLINE_FUNC seL4_Error
426seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
427{
428    seL4_Word unused0 = 0;
429    seL4_Word unused1 = 0;
430    seL4_Word unused2 = 0;
431    seL4_Word unused3 = 0;
432    seL4_Word unused4 = 0;
433
434    arm_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3, &unused4);
435
436    return (seL4_Error) frame_cptr;
437}
438
439LIBSEL4_INLINE_FUNC void
440seL4_BenchmarkNullSyscall(void)
441{
442    arm_sys_null(seL4_SysBenchmarkNullSyscall);
443    asm volatile("" ::: "memory");
444}
445
446LIBSEL4_INLINE_FUNC void
447seL4_BenchmarkFlushCaches(void)
448{
449    arm_sys_null(seL4_SysBenchmarkFlushCaches);
450    asm volatile("" ::: "memory");
451}
452
453#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
454LIBSEL4_INLINE_FUNC void
455seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
456{
457    seL4_Word unused0 = 0;
458    seL4_Word unused1 = 0;
459    seL4_Word unused2 = 0;
460    seL4_Word unused3 = 0;
461    seL4_Word unused4 = 0;
462    seL4_Word unused5 = 0;
463
464    arm_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
465}
466
467LIBSEL4_INLINE_FUNC void
468seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
469{
470    seL4_Word unused0 = 0;
471    seL4_Word unused1 = 0;
472    seL4_Word unused2 = 0;
473    seL4_Word unused3 = 0;
474    seL4_Word unused4 = 0;
475    seL4_Word unused5 = 0;
476
477    arm_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5);
478}
479#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
480#endif /* CONFIG_ENABLE_BENCHMARKS */
481
482LIBSEL4_INLINE_FUNC void
483seL4_Wait(seL4_CPtr src, seL4_Word *sender)
484{
485    seL4_Recv(src, sender);
486}
487
488LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
489seL4_Poll(seL4_CPtr src, seL4_Word *sender)
490{
491    return seL4_NBRecv(src, sender);
492}
493
494#endif
495