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