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 <sel4/sel4.h> 15#include <vka/vka.h> 16#include <vka/object.h> 17#include <vka/capops.h> 18 19#include "../test.h" 20#include "../helpers.h" 21 22/* Get a cap that we can move/copy/delete/etc and compare without causing chaos. 23 */ 24static seL4_CPtr get_cap(vka_t *vka) 25{ 26 return vka_alloc_tcb_leaky(vka); 27} 28static int test_cnode_copy(env_t env) 29{ 30 int error; 31 seL4_Word src, dest; 32 33 /* A call that should succeed. */ 34 src = get_cap(&env->vka); 35 dest = get_free_slot(env); 36 test_assert(is_slot_empty(env, dest)); 37 error = cnode_copy(env, src, dest, seL4_AllRights); 38 test_error_eq(error, seL4_NoError); 39 test_assert(are_tcbs_distinct(src, dest) == 0); 40 41 /* Copy to an occupied slot (should fail). */ 42 src = get_cap(&env->vka); 43 dest = get_cap(&env->vka); 44 error = cnode_copy(env, src, dest, seL4_AllRights); 45 test_error_eq(error, seL4_DeleteFirst); 46 47 /* Copy from a free slot to an occupied slot (should fail). */ 48 src = get_free_slot(env); 49 test_assert(is_slot_empty(env, src)); 50 dest = get_cap(&env->vka); 51 error = cnode_copy(env, src, dest, seL4_AllRights); 52 test_error_eq(error, seL4_DeleteFirst); 53 54 /* Copy from a free slot to a free slot (should fail). */ 55 src = get_free_slot(env); 56 test_assert(is_slot_empty(env, src)); 57 dest = get_free_slot(env); 58 test_assert(is_slot_empty(env, dest)); 59 error = cnode_copy(env, src, dest, seL4_AllRights); 60 test_error_eq(error, seL4_FailedLookup); 61 62 return sel4test_get_result(); 63} 64DEFINE_TEST(CNODEOP0001, "Basic seL4_CNode_Copy() testing", test_cnode_copy, true) 65 66static int 67test_cnode_delete(env_t env) 68{ 69 int error; 70 seL4_Word slot; 71 72 /* A call that should succeed. */ 73 slot = get_cap(&env->vka); 74 error = cnode_delete(env, slot); 75 test_error_eq(error, seL4_NoError); 76 test_assert(is_slot_empty(env, slot)); 77 78 /* Deleting a free slot (should succeed). */ 79 slot = get_free_slot(env); 80 error = cnode_delete(env, slot); 81 test_error_eq(error, seL4_NoError); 82 test_assert(is_slot_empty(env, slot)); 83 84 return sel4test_get_result(); 85} 86DEFINE_TEST(CNODEOP0002, "Basic seL4_CNode_Delete() testing", test_cnode_delete, true) 87 88static int 89test_cnode_mint(env_t env) 90{ 91 int error; 92 seL4_Word src, dest; 93 94 /* A call that should succeed. */ 95 src = get_cap(&env->vka); 96 dest = get_free_slot(env); 97 error = cnode_mint(env, src, dest, seL4_AllRights, seL4_NilData); 98 test_error_eq(error, seL4_NoError); 99 test_assert(are_tcbs_distinct(src, dest) == 0); 100 101 /* Mint to an occupied slot (should fail). */ 102 src = get_cap(&env->vka); 103 dest = get_cap(&env->vka); 104 error = cnode_mint(env, src, dest, seL4_AllRights, seL4_NilData); 105 test_error_eq(error, seL4_DeleteFirst); 106 107 /* Mint from an empty slot (should fail). */ 108 src = get_free_slot(env); 109 dest = get_free_slot(env); 110 error = cnode_mint(env, src, dest, seL4_AllRights, seL4_NilData); 111 test_error_eq(error, seL4_FailedLookup); 112 113 return sel4test_get_result(); 114} 115DEFINE_TEST(CNODEOP0003, "Basic seL4_CNode_Mint() testing", test_cnode_mint, true) 116 117static int 118test_cnode_move(env_t env) 119{ 120 int error; 121 seL4_Word src, dest; 122 123 /* A call that should succeed. */ 124 src = get_cap(&env->vka); 125 dest = get_free_slot(env); 126 error = cnode_move(env, src, dest); 127 test_error_eq(error, seL4_NoError); 128 test_assert(is_slot_empty(env, src)); 129 test_assert(!is_slot_empty(env, dest)); 130 131 /* Move from an empty slot (should fail). */ 132 src = get_free_slot(env); 133 dest = get_free_slot(env); 134 error = cnode_move(env, src, dest); 135 test_error_eq(error, seL4_FailedLookup); 136 test_assert(is_slot_empty(env, dest)); 137 138 /* Move to an occupied slot (should fail). */ 139 src = get_cap(&env->vka); 140 dest = get_cap(&env->vka); 141 error = cnode_move(env, src, dest); 142 test_error_eq(error, seL4_DeleteFirst); 143 test_assert(!is_slot_empty(env, src)); 144 test_assert(!is_slot_empty(env, dest)); 145 146 return sel4test_get_result(); 147} 148DEFINE_TEST(CNODEOP0004, "Basic seL4_CNode_Move() testing", test_cnode_move, true) 149 150static int 151test_cnode_mutate(env_t env) 152{ 153 int error; 154 seL4_Word src, dest; 155 156 /* A call that should succeed. */ 157 src = get_cap(&env->vka); 158 dest = get_free_slot(env); 159 error = cnode_mutate(env, src, dest); 160 test_error_eq(error, seL4_NoError); 161 test_assert(is_slot_empty(env, src)); 162 test_assert(!is_slot_empty(env, dest)); 163 164 /* Mutating to an occupied slot (should fail). */ 165 src = get_cap(&env->vka); 166 dest = get_cap(&env->vka); 167 error = cnode_mutate(env, src, dest); 168 test_error_eq(error, seL4_DeleteFirst); 169 test_assert(!is_slot_empty(env, src)); 170 test_assert(!is_slot_empty(env, dest)); 171 172 /* Mutating an empty slot (should fail). */ 173 src = get_free_slot(env); 174 dest = get_free_slot(env); 175 error = cnode_mutate(env, src, dest); 176 test_error_eq(error, seL4_FailedLookup); 177 test_assert(is_slot_empty(env, src)); 178 test_assert(is_slot_empty(env, dest)); 179 180 return sel4test_get_result(); 181} 182DEFINE_TEST(CNODEOP0005, "Basic seL4_CNode_Mutate() testing", test_cnode_mutate, true) 183 184static int 185test_cnode_cancelBadgedSends(env_t env) 186{ 187 int error; 188 seL4_Word slot; 189 190 /* A call that should succeed. */ 191 seL4_CPtr ep = vka_alloc_endpoint_leaky(&env->vka); 192 error = cnode_cancelBadgedSends(env, ep); 193 test_error_eq(error, seL4_NoError); 194 test_assert(!is_slot_empty(env, ep)); 195 196 /* Recycling an empty slot (should fail). */ 197 slot = get_free_slot(env); 198 error = cnode_cancelBadgedSends(env, slot); 199 test_error_eq(error, seL4_IllegalOperation); 200 test_assert(is_slot_empty(env, slot)); 201 202 return sel4test_get_result(); 203} 204DEFINE_TEST(CNODEOP0006, "Basic seL4_CNode_CancelBadgedSends() testing", test_cnode_cancelBadgedSends, true) 205 206static int 207test_cnode_revoke(env_t env) 208{ 209 int error; 210 seL4_Word slot; 211 212 /* A call that should succeed. */ 213 slot = get_cap(&env->vka); 214 error = cnode_revoke(env, slot); 215 test_error_eq(error, seL4_NoError); 216 test_assert(!is_slot_empty(env, slot)); 217 218 /* Revoking a null cap (should fail). */ 219 slot = get_free_slot(env); 220 error = cnode_revoke(env, slot); 221 test_error_eq(error, seL4_NoError); 222 test_assert(is_slot_empty(env, slot)); 223 224 return sel4test_get_result(); 225} 226DEFINE_TEST(CNODEOP0007, "Basic seL4_CNode_Revoke() testing", test_cnode_revoke, true) 227 228static int 229test_cnode_rotate(env_t env) 230{ 231 int error; 232 seL4_Word src, pivot, dest; 233 234 /* A call that should succeed. */ 235 src = get_cap(&env->vka); 236 pivot = get_cap(&env->vka); 237 dest = get_free_slot(env); 238 error = cnode_rotate(env, src, pivot, dest); 239 test_error_eq(error, seL4_NoError); 240 test_assert(is_slot_empty(env, src)); 241 test_assert(!is_slot_empty(env, pivot)); 242 test_assert(!is_slot_empty(env, dest)); 243 244 /* Destination occupied (should fail). */ 245 src = get_cap(&env->vka); 246 pivot = get_cap(&env->vka); 247 dest = get_cap(&env->vka); 248 error = cnode_rotate(env, src, pivot, dest); 249 test_error_eq(error, seL4_DeleteFirst); 250 test_assert(!is_slot_empty(env, src)); 251 test_assert(!is_slot_empty(env, pivot)); 252 test_assert(!is_slot_empty(env, dest)); 253 254 /* Swapping two caps (should succeed). */ 255 src = get_cap(&env->vka); 256 pivot = get_cap(&env->vka); 257 dest = src; 258 error = cnode_rotate(env, src, pivot, dest); 259 test_error_eq(error, seL4_NoError); 260 test_assert(are_tcbs_distinct(src, dest) == 0); 261 test_assert(!is_slot_empty(env, pivot)); 262 263 /* Moving a cap onto itself (should fail). */ 264 src = get_cap(&env->vka); 265 pivot = src; 266 dest = get_free_slot(env); 267 error = cnode_rotate(env, src, pivot, dest); 268 test_error_eq(error, seL4_IllegalOperation); 269 test_assert(!is_slot_empty(env, src)); 270 test_assert(is_slot_empty(env, dest)); 271 272 /* Moving empty slots (should fail). */ 273 src = get_free_slot(env); 274 pivot = get_free_slot(env); 275 dest = get_free_slot(env); 276 error = cnode_rotate(env, src, pivot, dest); 277 test_error_eq(error, seL4_FailedLookup); 278 test_assert(is_slot_empty(env, src)); 279 test_assert(is_slot_empty(env, pivot)); 280 test_assert(is_slot_empty(env, dest)); 281 282 return sel4test_get_result(); 283} 284DEFINE_TEST(CNODEOP0008, "Basic seL4_CNode_Rotate() testing", test_cnode_rotate, true) 285 286 287static int 288test_cnode_savecaller(env_t env) 289{ 290 int error; 291 seL4_Word slot; 292 293 /* A call that should succeed. */ 294 slot = get_free_slot(env); 295 error = cnode_savecaller(env, slot); 296 test_error_eq(error, seL4_NoError); 297 298 /* Save to an occupied slot (should fail). */ 299 slot = get_cap(&env->vka); 300 error = cnode_savecaller(env, slot); 301 test_error_eq(error, seL4_DeleteFirst); 302 test_assert(!is_slot_empty(env, slot)); 303 304 /* TODO: Test saving an actual reply capability. */ 305 306 return sel4test_get_result(); 307} 308DEFINE_TEST(CNODEOP0009, "Basic seL4_CNode_SaveCaller() testing", test_cnode_savecaller, !config_set(CONFIG_KERNEL_MCS)) 309