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#include <assert.h>
14#include <stdio.h>
15#include <stdlib.h>
16#include <sel4/sel4.h>
17#include <vka/object.h>
18
19#include "../helpers.h"
20
21
22#define MAGIC1 42
23#define MAGIC2 0xDEADBEEF
24#define MAGIC3 666
25
26static int check_recv(seL4_CPtr ep, seL4_Word val, seL4_CPtr reply)
27{
28    api_recv(ep, NULL, reply);
29    test_check(val == seL4_GetMR(0));
30    // This one is just for Rendez-vous
31    api_recv(ep, NULL, reply);
32    return sel4test_get_result();
33}
34
35static int test_send_needs_write(env_t env)
36{
37    vka_t *vka = &env->vka;
38    seL4_CPtr ep = vka_alloc_endpoint_leaky(vka);
39    seL4_CPtr reply = vka_alloc_reply_leaky(vka);
40    seL4_CPtr epMint;
41    vka_cspace_alloc(vka, &epMint);
42    helper_thread_t t;
43    seL4_CapRights_t rights;
44    for (seL4_Word i = 0 ; i < BIT(seL4_MsgExtraCapBits) ; i++) {
45        rights.words[0] = i;
46        create_helper_thread(env, &t);
47        start_helper(env, &t, (helper_fn_t)check_recv, ep, MAGIC1, reply, 0);
48        cnode_mint(env, ep, epMint, rights, 0);
49
50        seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
51        if (!seL4_CapRights_get_capAllowWrite(rights)) {
52            seL4_SetMR(0, MAGIC2);
53            seL4_Send(epMint, tag);
54        }
55        seL4_SetMR(0, MAGIC1);
56        seL4_Send(ep, tag);
57        // This one is just for Rendez-vous
58        seL4_Send(ep, tag);
59        cleanup_helper(env, &t);
60        cnode_delete(env, epMint);
61
62    }
63    return sel4test_get_result();
64}
65
66DEFINE_TEST(IPCRIGHTS0001, "seL4_Send needs write", test_send_needs_write, true)
67
68
69static int
70test_recv_needs_read(env_t env)
71{
72    vka_t *vka = &env->vka;
73    seL4_CPtr ep = vka_alloc_endpoint_leaky(vka);
74    seL4_CPtr reply = vka_alloc_reply_leaky(vka);
75    seL4_CPtr fault_ep = vka_alloc_endpoint_leaky(vka);
76    seL4_CPtr fault_reply = vka_alloc_reply_leaky(vka);
77    seL4_CPtr epMint;
78    vka_cspace_alloc(vka, &epMint);
79    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
80    for (seL4_Word i = 0 ; i < BIT(seL4_MsgExtraCapBits) ; i++) {
81        seL4_CapRights_t rights;
82        rights.words[0] = i;
83        cnode_mint(env, ep, epMint, rights, 0);
84        helper_thread_t t;
85        create_helper_thread(env, &t);
86        int error;
87        error = api_tcb_set_space(get_helper_tcb(&t),
88                                  fault_ep,
89                                  env->cspace_root,
90                                  seL4_NilData,
91                                  env->page_directory, seL4_NilData);
92        test_error_eq(error, seL4_NoError);
93        start_helper(env, &t, (helper_fn_t)check_recv, epMint, MAGIC1, reply, 0);
94
95        if (seL4_CapRights_get_capAllowRead(rights)) {
96            seL4_SetMR(0, MAGIC1);
97            seL4_Send(ep, tag);
98            seL4_Send(ep, tag);
99        } else {
100            api_recv(fault_ep, NULL, fault_reply);
101        }
102        cleanup_helper(env, &t);
103        cnode_delete(env, epMint);
104    }
105
106    return sel4test_get_result();
107}
108
109DEFINE_TEST(IPCRIGHTS0002, "seL4_Recv needs read", test_recv_needs_read, true)
110
111static int
112check_recv_cap(env_t env, seL4_CPtr ep, bool should_recv_cap, seL4_CPtr reply)
113{
114    vka_t *vka = &env->vka;
115
116    seL4_CPtr recvSlot;
117    int vka_error = vka_cspace_alloc(vka, &recvSlot);
118    test_error_eq(vka_error, seL4_NoError);
119    set_cap_receive_path(env, recvSlot);
120    api_recv(ep, NULL, reply);
121
122    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
123
124    test_assert(seL4_GetMR(0) == MAGIC1);
125
126    if (should_recv_cap) {
127        test_assert(!is_slot_empty(env, recvSlot));
128        seL4_SetMR(0, MAGIC2);
129        seL4_Send(recvSlot, tag);
130        int error = cnode_delete(env, recvSlot);
131        test_check(!error);
132    }
133    test_assert(is_slot_empty(env, recvSlot));
134    vka_cspace_free(vka, recvSlot);
135    seL4_SetMR(0, MAGIC3);
136    seL4_Send(ep, tag);
137
138    return sel4test_get_result();
139}
140
141static int test_send_cap_needs_grant(env_t env)
142{
143    vka_t *vka = &env->vka;
144    seL4_CPtr ep = vka_alloc_endpoint_leaky(vka);
145    seL4_CPtr reply = vka_alloc_reply_leaky(vka);
146    seL4_CPtr return_ep = vka_alloc_endpoint_leaky(vka);
147    seL4_CPtr return_reply = vka_alloc_reply_leaky(vka);
148    seL4_CPtr epMint;
149    vka_cspace_alloc(vka, &epMint);
150    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 1, 1);
151
152    for (seL4_Word i = 0; i < BIT(seL4_MsgExtraCapBits); i++) {
153        seL4_CapRights_t rights;
154        rights.words[0] = i;
155        if (!seL4_CapRights_get_capAllowWrite(rights)) {
156            continue;
157        }
158        bool grant = seL4_CapRights_get_capAllowGrant(rights);
159
160        cnode_mint(env, ep, epMint, rights, 0);
161
162        helper_thread_t t;
163        create_helper_thread(env, &t);
164        start_helper(env, &t, (helper_fn_t)check_recv_cap, (seL4_Word)env, ep, grant, reply);
165
166        seL4_SetMR(0, MAGIC1);
167        seL4_SetCap(0, return_ep);
168        seL4_Send(epMint, tag);
169
170        if (grant) {
171            api_recv(return_ep, NULL, return_reply);
172            test_check(seL4_GetMR(0) == MAGIC2);
173        }
174        api_recv(ep, NULL, reply);
175        test_check(seL4_GetMR(0) == MAGIC3);
176        cleanup_helper(env, &t);
177        cnode_delete(env, epMint);
178    }
179
180    /* test_check(seL4_GetMR(0) == 42); */
181    return sel4test_get_result();
182}
183
184DEFINE_TEST(IPCRIGHTS0003, "seL4_Send with caps needs grant", test_send_cap_needs_grant, true)
185
186#ifndef CONFIG_KERNEL_MCS
187
188static int
189check_call(env_t env, seL4_CPtr ep, bool should_call, bool reply_recv)
190{
191    vka_t *vka = &env->vka;
192
193
194    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
195    seL4_SetMR(0, MAGIC1);
196    seL4_Call(ep, tag);
197    if (reply_recv) {
198        seL4_Call(ep, tag);
199    }
200
201
202    /* if we are here, the call should have worked (or else we would have been inactive) */
203    test_assert(should_call);
204    test_assert(seL4_GetMR(0) == MAGIC2);
205    seL4_Send(ep, tag);
206
207    return sel4test_get_result();
208}
209
210
211
212static int test_call_needs_grant_or_grant_reply(env_t env)
213{
214    vka_t *vka = &env->vka;
215    seL4_CPtr ep = vka_alloc_endpoint_leaky(vka);
216    seL4_CPtr return_ep = vka_alloc_endpoint_leaky(vka);
217    seL4_CPtr reply = get_free_slot(env);
218    seL4_CPtr epMint = get_free_slot(env);
219    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
220
221    enum {
222        nothing,
223        save_caller,
224        reply_recv
225    };
226
227    for (int mode = nothing; mode <= reply_recv; mode++) {
228        for (seL4_Word i = 0; i < BIT(seL4_MsgExtraCapBits); i++) {
229            seL4_CapRights_t rights;
230            rights.words[0] = i;
231            if (!seL4_CapRights_get_capAllowWrite(rights)) {
232                continue;
233            }
234            bool grant = seL4_CapRights_get_capAllowGrant(rights);
235            bool grant_reply = seL4_CapRights_get_capAllowGrantReply(rights);
236
237            cnode_copy(env, ep, epMint, rights);
238
239            helper_thread_t t;
240            create_helper_thread(env, &t);
241            start_helper(env, &t, (helper_fn_t)check_call, (seL4_Word)env, epMint,
242                         grant || grant_reply, mode == reply_recv);
243
244
245            seL4_Recv(ep, NULL);
246            if (grant || grant_reply) {
247                test_check(seL4_GetMR(0) == MAGIC1);
248                switch (mode) {
249                case nothing:
250                    seL4_SetMR(0, MAGIC2);
251                    seL4_Reply(tag);
252                    cnode_savecaller(env, reply);
253                    test_assert(is_slot_empty(env, reply));
254                    break;
255                case save_caller:
256                    cnode_savecaller(env, reply);
257                    test_assert(!is_slot_empty(env, reply));
258                    seL4_SetMR(0, MAGIC2);
259                    seL4_Send(reply, tag);
260                    test_assert(is_slot_empty(env, reply));
261                    break;
262                case reply_recv:
263                    seL4_ReplyRecv(ep, tag, NULL);
264                    seL4_SetMR(0, MAGIC2);
265                    seL4_Reply(tag);
266                    cnode_savecaller(env, reply);
267                    test_assert(is_slot_empty(env, reply));
268                    break;
269                }
270                seL4_Recv(ep, NULL);
271                test_check(seL4_GetMR(0) == MAGIC2);
272            } else {
273                cnode_savecaller(env, reply);
274                test_assert(is_slot_empty(env, reply));
275                cnode_delete(env, epMint);
276                cnode_copy(env, ep, epMint, seL4_AllRights);
277                seL4_TCB_Resume(get_helper_tcb(&t));
278                seL4_Recv(ep, NULL);
279                cnode_savecaller(env, reply);
280                test_assert(!is_slot_empty(env, reply));
281                seL4_TCB_Suspend(get_helper_tcb(&t));
282                test_assert(is_slot_empty(env, reply));
283            }
284            cleanup_helper(env, &t);
285            cnode_delete(env, epMint);
286        }
287    }
288
289    return sel4test_get_result();
290}
291
292DEFINE_TEST(IPCRIGHTS0004, "seL4_Call needs grant or grant-reply",
293            test_call_needs_grant_or_grant_reply, true)
294
295static int
296check_call_return_cap(env_t env, seL4_CPtr ep,
297                      bool should_recv_cap, bool reply_recv)
298{
299    vka_t *vka = &env->vka;
300
301    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
302    seL4_CPtr recvSlot = get_free_slot(env);
303    set_cap_receive_path(env, recvSlot);
304    seL4_SetMR(0, MAGIC1);
305    seL4_Call(ep, tag);
306    if (reply_recv) {
307        seL4_Call(ep, tag);
308    }
309
310    test_check(seL4_GetMR(0) == MAGIC2);
311
312    if (should_recv_cap) {
313        test_assert(!is_slot_empty(env, recvSlot));
314        seL4_SetMR(0, MAGIC3);
315        seL4_Send(recvSlot, tag);
316        int error = cnode_delete(env, recvSlot);
317        test_check(!error);
318    }
319    test_assert(is_slot_empty(env, recvSlot));
320    vka_cspace_free(vka, recvSlot);
321    seL4_SetMR(0, MAGIC3);
322    seL4_Send(ep, tag);
323    return sel4test_get_result();
324}
325
326static int test_reply_grant_receiver(env_t env)
327{
328    vka_t *vka = &env->vka;
329    seL4_CPtr ep = vka_alloc_endpoint_leaky(vka);
330    seL4_CPtr return_ep = vka_alloc_endpoint_leaky(vka);
331    seL4_CPtr reply = get_free_slot(env);
332    seL4_CPtr epMint = get_free_slot(env);
333    seL4_MessageInfo_t tag_no_cap = seL4_MessageInfo_new(0, 0, 0, 1);
334    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 1, 1);
335
336    enum {
337        nothing,
338        save_caller,
339        reply_recv
340    };
341
342    for (int mode = nothing; mode <= reply_recv; mode++) {
343        for (seL4_Word i = 0; i < BIT(seL4_MsgExtraCapBits); i++) {
344            seL4_CapRights_t rights;
345            rights.words[0] = i;
346            if (!seL4_CapRights_get_capAllowRead(rights)) {
347                continue;
348            }
349            bool grant = seL4_CapRights_get_capAllowGrant(rights);
350
351            cnode_copy(env, ep, epMint, rights);
352
353            helper_thread_t t;
354            create_helper_thread(env, &t);
355            start_helper(env, &t, (helper_fn_t)check_call_return_cap,
356                         (seL4_Word)env, ep, grant, mode == reply_recv);
357
358            seL4_Recv(epMint, NULL);
359            seL4_Word callmsg = seL4_GetMR(0);
360            test_check(callmsg == MAGIC1);
361            if (mode == save_caller) {
362                cnode_savecaller(env, reply);
363                test_assert(!is_slot_empty(env, reply));
364                seL4_SetMR(0, MAGIC2);
365                seL4_SetCap(0, return_ep);
366                seL4_Send(reply, tag);
367                test_assert(is_slot_empty(env, reply));
368            } else {
369                if (mode == reply_recv) {
370                    seL4_ReplyRecv(epMint, tag_no_cap, NULL);
371                }
372                seL4_SetMR(0, MAGIC2);
373                seL4_SetCap(0, return_ep);
374                seL4_Reply(tag);
375            }
376
377            if (grant) {
378                seL4_Recv(return_ep, NULL);
379                test_check(seL4_GetMR(0) == MAGIC3);
380            }
381            seL4_Recv(ep, NULL);
382            test_check(seL4_GetMR(0) == MAGIC3);
383            cleanup_helper(env, &t);
384            cnode_delete(env, epMint);
385        }
386    }
387
388    return sel4test_get_result();
389}
390
391DEFINE_TEST(IPCRIGHTS0005, "seL4_Reply grant depends of the grant of previous seL4_Recv",
392            test_reply_grant_receiver, true)
393
394
395
396
397#endif /* CONFIG_KERNEL_MCS */
398
399