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 <stdio.h>
14#include <sel4/sel4.h>
15#include <vka/object.h>
16#include <vka/capops.h>
17
18#include "../test.h"
19#include "../helpers.h"
20
21static int send_func(seL4_CPtr ep, seL4_Word msg, UNUSED seL4_Word arg4, UNUSED seL4_Word arg3)
22{
23    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
24
25    /* Send the given message once. */
26    seL4_SetMR(0, msg);
27    seL4_Send(ep, tag);
28
29    return sel4test_get_result();
30}
31
32static int test_nbwait(env_t env)
33{
34
35    vka_object_t notification = {0};
36    vka_object_t endpoint = {0};
37    vka_object_t reply = {0};
38    int error;
39    seL4_MessageInfo_t info = {{0}};
40    seL4_Word badge = 0;
41
42    /* allocate an endpoint and a notification */
43    error = vka_alloc_endpoint(&env->vka, &endpoint);
44    test_eq(error, 0);
45
46    error = vka_alloc_notification(&env->vka, &notification);
47    test_eq(error, 0);
48
49    if (config_set(CONFIG_KERNEL_MCS)) {
50        error = vka_alloc_reply(&env->vka, &reply);
51        test_eq(error, 0);
52    }
53
54    /* bind the notification to the current thread */
55    error = seL4_TCB_BindNotification(env->tcb, notification.cptr);
56    test_eq(error, 0);
57
58    /* create cspace paths for both objects */
59    cspacepath_t notification_path, endpoint_path;
60    vka_cspace_make_path(&env->vka, notification.cptr, &notification_path);
61    vka_cspace_make_path(&env->vka, endpoint.cptr, &endpoint_path);
62
63    /* badge both caps */
64    cspacepath_t badged_notification, badged_endpoint;
65    error = vka_cspace_alloc_path(&env->vka, &badged_notification);
66    test_eq(error, 0);
67    vka_cspace_alloc_path(&env->vka, &badged_endpoint);
68    test_eq(error, 0);
69
70    error = vka_cnode_mint(&badged_endpoint, &endpoint_path, seL4_AllRights, 1);
71    test_eq(error, 0);
72
73    error = vka_cnode_mint(&badged_notification, &notification_path, seL4_AllRights, 2);
74    test_eq(error, 0);
75
76    /* NBRecv on endpoint with no messages should return 0 immediately */
77    info = api_nbrecv(endpoint.cptr, &badge, reply.cptr);
78    test_eq(badge, (seL4_Word)0);
79
80    /* Poll on a notification with no messages should return 0 immediately */
81    info = seL4_Poll(notification.cptr, &badge);
82    test_eq(badge, (seL4_Word)0);
83
84    /* send a signal to the notification */
85    seL4_Signal(badged_notification.capPtr);
86
87    /* Polling should return the badge from the signal we just sent */
88    info = seL4_Poll(notification.cptr, &badge);
89    test_eq(badge, (seL4_Word)2);
90
91    /* Polling again should return nothign */
92    info = seL4_Poll(notification.cptr, &badge);
93    test_eq(badge, (seL4_Word)0);
94
95    /* send a signal to the notification */
96    seL4_Signal(badged_notification.capPtr);
97
98    /* This time NBRecv the endpoint - since we are bound, we should get the badge from the signal again */
99    info = api_nbrecv(endpoint.cptr, &badge, reply.cptr);
100    test_eq(badge, (seL4_Word)2);
101
102    /* NBRecving again should return nothign */
103    info = api_nbrecv(endpoint.cptr, &badge, reply.cptr);
104    test_eq(badge, (seL4_Word)0);
105
106    /* now start a helper to send a message on the badged endpoint */
107    helper_thread_t thread;
108    create_helper_thread(env, &thread);
109    start_helper(env, &thread, send_func, badged_endpoint.capPtr, 0xdeadbeef, 0, 0);
110    set_helper_priority(env, &thread, env->priority);
111    /* let helper run */
112    seL4_TCB_SetPriority(env->tcb, env->tcb, env->priority - 1);
113
114    /* NBRecving should return helpers message */
115    info = api_nbrecv(endpoint.cptr, &badge, reply.cptr);
116    test_eq(badge, (seL4_Word)1);
117    test_eq(seL4_MessageInfo_get_length(info), (seL4_Word)1);
118    test_eq(seL4_GetMR(0), (seL4_Word)0xdeadbeef);
119
120    /* NBRecving again should return nothign */
121    info = api_nbrecv(endpoint.cptr, &badge, reply.cptr);
122    test_eq(badge, (seL4_Word)0);
123
124    /* clean up */
125    wait_for_helper(&thread);
126    cleanup_helper(env, &thread);
127    seL4_TCB_UnbindNotification(env->tcb);
128    vka_cnode_delete(&badged_notification);
129    vka_cnode_delete(&badged_endpoint);
130    vka_cspace_free(&env->vka, badged_endpoint.capPtr);
131    vka_cspace_free(&env->vka, badged_notification.capPtr);
132    vka_free_object(&env->vka, &endpoint);
133    vka_free_object(&env->vka, &notification);
134
135    return sel4test_get_result();
136}
137DEFINE_TEST(NBWAIT0001, "Test seL4_NBRecv", test_nbwait, true)
138