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/types.h>
12
13#ifdef CONFIG_KERNEL_MCS
14#define MCS_REPLY_DECL register seL4_Word reply_reg asm("r12") = reply
15#define MCS_REPLY ,"r"(reply_reg)
16#else
17#define MCS_REPLY_DECL
18#define MCS_REPLY
19#endif
20
21static inline void x64_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word msg0, seL4_Word msg1,
22                                seL4_Word msg2, seL4_Word msg3)
23{
24    register seL4_Word mr0 asm("r10") = msg0;
25    register seL4_Word mr1 asm("r8") = msg1;
26    register seL4_Word mr2 asm("r9") = msg2;
27    register seL4_Word mr3 asm("r15") = msg3;
28
29    asm volatile(
30        "movq   %%rsp, %%rbx        \n"
31        "syscall                    \n"
32        "movq   %%rbx, %%rsp        \n"
33        :
34        : "d"(sys),
35        "D"(dest),
36        "S"(info),
37        "r"(mr0),
38        "r"(mr1),
39        "r"(mr2),
40        "r"(mr3)
41        : "%rbx", "%rcx", "%r11"
42    );
43}
44
45#ifndef CONFIG_KERNEL_MCS
46static inline void x64_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word msg0, seL4_Word msg1, seL4_Word msg2,
47                                 seL4_Word msg3)
48{
49    register seL4_Word mr0 asm("r10") = msg0;
50    register seL4_Word mr1 asm("r8") = msg1;
51    register seL4_Word mr2 asm("r9") = msg2;
52    register seL4_Word mr3 asm("r15") = msg3;
53
54    asm volatile(
55        "movq   %%rsp, %%rbx        \n"
56        "syscall                    \n"
57        "movq   %%rbx, %%rsp        \n"
58        :
59        : "d"(sys),
60        "S"(info),
61        "r"(mr0),
62        "r"(mr1),
63        "r"(mr2),
64        "r"(mr3)
65        : "%rbx", "%rcx", "%r11"
66    );
67}
68#endif /* CONFIG_KERNEL_MCS */
69
70static inline void x64_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info)
71{
72    asm volatile(
73        "movq   %%rsp, %%rbx        \n"
74        "syscall                    \n"
75        "movq   %%rbx, %%rsp        \n"
76        :
77        : "d"(sys),
78        "D"(dest),
79        "S"(info)
80        : "%rcx", "%rbx", "%r11"
81    );
82}
83
84static inline void x64_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
85                                seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3,
86                                LIBSEL4_UNUSED seL4_Word reply)
87{
88    register seL4_Word mr0 asm("r10");
89    register seL4_Word mr1 asm("r8");
90    register seL4_Word mr2 asm("r9");
91    register seL4_Word mr3 asm("r15");
92    MCS_REPLY_DECL;
93
94    asm volatile(
95        "movq   %%rsp, %%rbx    \n"
96        "syscall                \n"
97        "movq   %%rbx, %%rsp    \n"
98        : "=D"(*out_badge),
99        "=S"(*out_info),
100        "=r"(mr0),
101        "=r"(mr1),
102        "=r"(mr2),
103        "=r"(mr3)
104        : "d"(sys),
105        "D"(src)
106        MCS_REPLY
107        : "%rcx", "%rbx", "r11", "memory"
108    );
109    *out_mr0 = mr0;
110    *out_mr1 = mr1;
111    *out_mr2 = mr2;
112    *out_mr3 = mr3;
113}
114
115static inline void x64_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_dest, seL4_Word info,
116                                     seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3,
117                                     LIBSEL4_UNUSED seL4_Word reply)
118{
119    register seL4_Word mr0 asm("r10") = *in_out_mr0;
120    register seL4_Word mr1 asm("r8") = *in_out_mr1;
121    register seL4_Word mr2 asm("r9") = *in_out_mr2;
122    register seL4_Word mr3 asm("r15") = *in_out_mr3;
123    MCS_REPLY_DECL;
124
125    asm volatile(
126        "movq   %%rsp, %%rbx    \n"
127        "syscall                \n"
128        "movq   %%rbx, %%rsp    \n"
129        : "=S"(*out_info),
130        "=r"(mr0),
131        "=r"(mr1),
132        "=r"(mr2),
133        "=r"(mr3),
134        "=D"(*out_dest)
135        : "d"(sys),
136        "D"(dest),
137        "S"(info),
138        "r"(mr0),
139        "r"(mr1),
140        "r"(mr2),
141        "r"(mr3)
142        MCS_REPLY
143        : "%rcx", "%rbx", "r11", "memory"
144    );
145    *in_out_mr0 = mr0;
146    *in_out_mr1 = mr1;
147    *in_out_mr2 = mr2;
148    *in_out_mr3 = mr3;
149}
150
151#ifdef CONFIG_KERNEL_MCS
152static inline void x64_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_dest,
153                                       seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
154                                       seL4_Word *in_out_mr3, seL4_Word reply)
155{
156    register seL4_Word mr0 asm("r10") = *in_out_mr0;
157    register seL4_Word mr1 asm("r8") = *in_out_mr1;
158    register seL4_Word mr2 asm("r9") = *in_out_mr2;
159    register seL4_Word mr3 asm("r15") = *in_out_mr3;
160    register seL4_Word reply_reg asm("r12") = reply;
161    register seL4_Word dest_reg asm("r13") = dest;
162
163    asm volatile(
164        "movq   %%rsp, %%rbx    \n"
165        "syscall                \n"
166        "movq   %%rbx, %%rsp    \n"
167        : "=S"(*out_info),
168        "=r"(mr0),
169        "=r"(mr1),
170        "=r"(mr2),
171        "=r"(mr3),
172        "=D"(*out_dest)
173        : "d"(sys),
174        "D"(src),
175        "S"(info),
176        "r"(mr0),
177        "r"(mr1),
178        "r"(mr2),
179        "r"(mr3),
180        "r"(reply_reg),
181        "r"(dest_reg)
182        : "%rcx", "%rbx", "r11", "memory"
183    );
184    *in_out_mr0 = mr0;
185    *in_out_mr1 = mr1;
186    *in_out_mr2 = mr2;
187    *in_out_mr3 = mr3;
188}
189#endif /* CONFIG_KERNEL_MCS */
190
191static inline void x64_sys_null(seL4_Word sys)
192{
193    asm volatile(
194        "movq   %%rsp, %%rbx    \n"
195        "syscall                \n"
196        "movq   %%rbx, %%rsp    \n"
197        :
198        : "d"(sys)
199        : "%rbx", "%rcx", "%rsi", "%rdi", "%r11"
200    );
201}
202