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 <sel4/sel4.h>
16#include <vka/object.h>
17
18#include "../test.h"
19#include "../helpers.h"
20#include <utils/util.h>
21
22#define READY_MAGIC 0x12374153
23#define SUCCESS_MAGIC 0x12374151
24
25static int ipc_caller(seL4_Word ep0, seL4_Word ep1, seL4_Word word_bits, seL4_Word arg4)
26{
27    /* Let our parent know we are ready. */
28    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1);
29    seL4_SetMR(0, READY_MAGIC);
30    seL4_Send(ep0, tag);
31    /*
32     * The parent has changed our cspace on us. Check that it makes sense.
33     *
34     * Basically the entire cspace should be empty except for the cap at ep0.
35     * We should still test that various points in the cspace resolve correctly.
36     */
37
38    /* Check that none of the typical endpoints are valid. */
39    for (unsigned long i = 0; i < word_bits; i++) {
40        seL4_MessageInfo_ptr_new(&tag, 0, 0, 0, 0);
41        tag = seL4_Call(i, tag);
42        test_assert(seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability);
43    }
44
45    /* Check that changing one bit still gives an invalid cap. */
46    for (unsigned long i = 0; i < word_bits; i++) {
47        seL4_MessageInfo_ptr_new(&tag, 0, 0, 0, 0);
48        tag = seL4_Call(ep1 ^ BIT(i), tag);
49        test_assert(seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability);
50    }
51
52    /* And we're done. This should be a valid cap and get us out of here! */
53    seL4_MessageInfo_ptr_new(&tag, 0, 0, 0, 1);
54    seL4_SetMR(0, SUCCESS_MAGIC);
55    seL4_Send(ep1, tag);
56
57    return sel4test_get_result();
58}
59
60static int test_full_cspace(env_t env)
61{
62    int error;
63    seL4_CPtr cnode[CONFIG_WORD_SIZE];
64    seL4_CPtr ep = vka_alloc_endpoint_leaky(&env->vka);
65    seL4_Word ep_pos = 1;
66
67    /* Create 32 or 64 cnodes, each resolving one bit. */
68    for (unsigned int i = 0; i < CONFIG_WORD_SIZE; i++) {
69        cnode[i] = vka_alloc_cnode_object_leaky(&env->vka, 1);
70        assert(cnode[i]);
71    }
72
73    /* Copy cnode i to alternating slots in cnode i-1. */
74    seL4_Word slot = 0;
75    for (unsigned int i = 1; i < CONFIG_WORD_SIZE; i++) {
76        error = seL4_CNode_Copy(
77                    cnode[i - 1], slot, 1,
78                    env->cspace_root, cnode[i], seL4_WordBits,
79                    seL4_AllRights);
80        test_error_eq(error, seL4_NoError);
81        ep_pos |= (slot << i);
82        slot ^= 1;
83    }
84    /* In the final cnode, put an IPC endpoint in slot 1. */
85    error = seL4_CNode_Copy(
86                cnode[CONFIG_WORD_SIZE - 1], slot, 1,
87                env->cspace_root, ep, seL4_WordBits,
88                seL4_AllRights);
89    test_error_eq(error, seL4_NoError);
90
91    /* Start a helper thread in our own cspace, to let it get set up. */
92    helper_thread_t t;
93
94    create_helper_thread(env, &t);
95    start_helper(env, &t, ipc_caller, ep, ep_pos, CONFIG_WORD_SIZE, 0);
96
97    /* Wait for it. */
98    seL4_MessageInfo_t tag;
99    seL4_Word sender_badge = 0;
100    tag = api_wait(ep, &sender_badge);
101    test_assert(seL4_MessageInfo_get_length(tag) == 1);
102    test_assert(seL4_GetMR(0) == READY_MAGIC);
103
104    /* Now switch its cspace. */
105    error = api_tcb_set_space(get_helper_tcb(&t), t.fault_endpoint,
106                              cnode[0], seL4_NilData, env->page_directory,
107                              seL4_NilData);
108
109    test_error_eq(error, seL4_NoError);
110
111    /* And now wait for it to do some tests and return to us. */
112    tag = api_wait(ep, &sender_badge);
113    test_assert(seL4_MessageInfo_get_length(tag) == 1);
114    test_assert(seL4_GetMR(0) == SUCCESS_MAGIC);
115
116    cleanup_helper(env, &t);
117    return sel4test_get_result();
118}
119DEFINE_TEST(CSPACE0001, "Test full cspace resolution", test_full_cspace, true)
120