1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 */ 10 11#include <assert.h> 12#include <config.h> 13#include <types.h> 14#include <api/failures.h> 15#include <api/syscall.h> 16#include <arch/object/objecttype.h> 17#include <machine/io.h> 18#include <object/objecttype.h> 19#include <object/structures.h> 20#include <object/notification.h> 21#include <object/endpoint.h> 22#include <object/cnode.h> 23#include <object/interrupt.h> 24#include <object/tcb.h> 25#include <object/untyped.h> 26#include <model/statedata.h> 27#include <kernel/thread.h> 28#include <kernel/vspace.h> 29#include <machine.h> 30#include <util.h> 31#include <string.h> 32 33word_t getObjectSize(word_t t, word_t userObjSize) 34{ 35 if (t >= seL4_NonArchObjectTypeCount) { 36 return Arch_getObjectSize(t); 37 } else { 38 switch (t) { 39 case seL4_TCBObject: 40 return seL4_TCBBits; 41 case seL4_EndpointObject: 42 return seL4_EndpointBits; 43 case seL4_NotificationObject: 44 return seL4_NotificationBits; 45 case seL4_CapTableObject: 46 return seL4_SlotBits + userObjSize; 47 case seL4_UntypedObject: 48 return userObjSize; 49 default: 50 fail("Invalid object type"); 51 return 0; 52 } 53 } 54} 55 56deriveCap_ret_t 57deriveCap(cte_t *slot, cap_t cap) 58{ 59 deriveCap_ret_t ret; 60 61 if (isArchCap(cap)) { 62 return Arch_deriveCap(slot, cap); 63 } 64 65 switch (cap_get_capType(cap)) { 66 case cap_zombie_cap: 67 ret.status = EXCEPTION_NONE; 68 ret.cap = cap_null_cap_new(); 69 break; 70 71 case cap_irq_control_cap: 72 ret.status = EXCEPTION_NONE; 73 ret.cap = cap_null_cap_new(); 74 break; 75 76 case cap_untyped_cap: 77 ret.status = ensureNoChildren(slot); 78 if (ret.status != EXCEPTION_NONE) { 79 ret.cap = cap_null_cap_new(); 80 } else { 81 ret.cap = cap; 82 } 83 break; 84 85 case cap_reply_cap: 86 ret.status = EXCEPTION_NONE; 87 ret.cap = cap_null_cap_new(); 88 break; 89 90 default: 91 ret.status = EXCEPTION_NONE; 92 ret.cap = cap; 93 } 94 95 return ret; 96} 97 98finaliseCap_ret_t 99finaliseCap(cap_t cap, bool_t final, bool_t exposed) 100{ 101 finaliseCap_ret_t fc_ret; 102 103 if (isArchCap(cap)) { 104 return Arch_finaliseCap(cap, final); 105 } 106 107 switch (cap_get_capType(cap)) { 108 case cap_endpoint_cap: 109 if (final) { 110 cancelAllIPC(EP_PTR(cap_endpoint_cap_get_capEPPtr(cap))); 111 } 112 113 fc_ret.remainder = cap_null_cap_new(); 114 fc_ret.cleanupInfo = cap_null_cap_new(); 115 return fc_ret; 116 117 case cap_notification_cap: 118 if (final) { 119 notification_t *ntfn = NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)); 120 121 unbindMaybeNotification(ntfn); 122 cancelAllSignals(ntfn); 123 } 124 fc_ret.remainder = cap_null_cap_new(); 125 fc_ret.cleanupInfo = cap_null_cap_new(); 126 return fc_ret; 127 128 case cap_reply_cap: 129 case cap_null_cap: 130 case cap_domain_cap: 131 fc_ret.remainder = cap_null_cap_new(); 132 fc_ret.cleanupInfo = cap_null_cap_new(); 133 return fc_ret; 134 } 135 136 if (exposed) { 137 fail("finaliseCap: failed to finalise immediately."); 138 } 139 140 switch (cap_get_capType(cap)) { 141 case cap_cnode_cap: { 142 if (final) { 143 fc_ret.remainder = 144 Zombie_new( 145 1ul << cap_cnode_cap_get_capCNodeRadix(cap), 146 cap_cnode_cap_get_capCNodeRadix(cap), 147 cap_cnode_cap_get_capCNodePtr(cap) 148 ); 149 fc_ret.cleanupInfo = cap_null_cap_new(); 150 return fc_ret; 151 } 152 break; 153 } 154 155 case cap_thread_cap: { 156 if (final) { 157 tcb_t *tcb; 158 cte_t *cte_ptr; 159 160 tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)); 161 SMP_COND_STATEMENT(remoteTCBStall(tcb);) 162 cte_ptr = TCB_PTR_CTE_PTR(tcb, tcbCTable); 163 unbindNotification(tcb); 164 suspend(tcb); 165#ifdef CONFIG_DEBUG_BUILD 166 tcbDebugRemove(tcb); 167#endif 168 Arch_prepareThreadDelete(tcb); 169 fc_ret.remainder = 170 Zombie_new( 171 tcbArchCNodeEntries, 172 ZombieType_ZombieTCB, 173 CTE_REF(cte_ptr) 174 ); 175 fc_ret.cleanupInfo = cap_null_cap_new(); 176 return fc_ret; 177 } 178 break; 179 } 180 181 case cap_zombie_cap: 182 fc_ret.remainder = cap; 183 fc_ret.cleanupInfo = cap_null_cap_new(); 184 return fc_ret; 185 186 case cap_irq_handler_cap: 187 if (final) { 188 irq_t irq = cap_irq_handler_cap_get_capIRQ(cap); 189 190 deletingIRQHandler(irq); 191 192 fc_ret.remainder = cap_null_cap_new(); 193 fc_ret.cleanupInfo = cap; 194 return fc_ret; 195 } 196 break; 197 } 198 199 fc_ret.remainder = cap_null_cap_new(); 200 fc_ret.cleanupInfo = cap_null_cap_new(); 201 return fc_ret; 202} 203 204bool_t CONST 205hasCancelSendRights(cap_t cap) 206{ 207 switch (cap_get_capType(cap)) { 208 case cap_endpoint_cap: 209 return cap_endpoint_cap_get_capCanSend(cap) && 210 cap_endpoint_cap_get_capCanReceive(cap) && 211 cap_endpoint_cap_get_capCanGrant(cap); 212 213 default: 214 return false; 215 } 216} 217 218bool_t CONST 219sameRegionAs(cap_t cap_a, cap_t cap_b) 220{ 221 switch (cap_get_capType(cap_a)) { 222 case cap_untyped_cap: 223 if (cap_get_capIsPhysical(cap_b)) { 224 word_t aBase, bBase, aTop, bTop; 225 226 aBase = (word_t)WORD_PTR(cap_untyped_cap_get_capPtr(cap_a)); 227 bBase = (word_t)cap_get_capPtr(cap_b); 228 229 aTop = aBase + MASK(cap_untyped_cap_get_capBlockSize(cap_a)); 230 bTop = bBase + MASK(cap_get_capSizeBits(cap_b)); 231 232 return (aBase <= bBase) && (bTop <= aTop) && (bBase <= bTop); 233 } 234 break; 235 236 case cap_endpoint_cap: 237 if (cap_get_capType(cap_b) == cap_endpoint_cap) { 238 return cap_endpoint_cap_get_capEPPtr(cap_a) == 239 cap_endpoint_cap_get_capEPPtr(cap_b); 240 } 241 break; 242 243 case cap_notification_cap: 244 if (cap_get_capType(cap_b) == cap_notification_cap) { 245 return cap_notification_cap_get_capNtfnPtr(cap_a) == 246 cap_notification_cap_get_capNtfnPtr(cap_b); 247 } 248 break; 249 250 case cap_cnode_cap: 251 if (cap_get_capType(cap_b) == cap_cnode_cap) { 252 return (cap_cnode_cap_get_capCNodePtr(cap_a) == 253 cap_cnode_cap_get_capCNodePtr(cap_b)) && 254 (cap_cnode_cap_get_capCNodeRadix(cap_a) == 255 cap_cnode_cap_get_capCNodeRadix(cap_b)); 256 } 257 break; 258 259 case cap_thread_cap: 260 if (cap_get_capType(cap_b) == cap_thread_cap) { 261 return cap_thread_cap_get_capTCBPtr(cap_a) == 262 cap_thread_cap_get_capTCBPtr(cap_b); 263 } 264 break; 265 266 case cap_reply_cap: 267 if (cap_get_capType(cap_b) == cap_reply_cap) { 268 return cap_reply_cap_get_capTCBPtr(cap_a) == 269 cap_reply_cap_get_capTCBPtr(cap_b); 270 } 271 break; 272 273 case cap_domain_cap: 274 if (cap_get_capType(cap_b) == cap_domain_cap) { 275 return true; 276 } 277 break; 278 279 case cap_irq_control_cap: 280 if (cap_get_capType(cap_b) == cap_irq_control_cap || 281 cap_get_capType(cap_b) == cap_irq_handler_cap) { 282 return true; 283 } 284 break; 285 286 case cap_irq_handler_cap: 287 if (cap_get_capType(cap_b) == cap_irq_handler_cap) { 288 return (irq_t)cap_irq_handler_cap_get_capIRQ(cap_a) == 289 (irq_t)cap_irq_handler_cap_get_capIRQ(cap_b); 290 } 291 break; 292 293 default: 294 if (isArchCap(cap_a) && 295 isArchCap(cap_b)) { 296 return Arch_sameRegionAs(cap_a, cap_b); 297 } 298 break; 299 } 300 301 return false; 302} 303 304bool_t CONST 305sameObjectAs(cap_t cap_a, cap_t cap_b) 306{ 307 if (cap_get_capType(cap_a) == cap_untyped_cap) { 308 return false; 309 } 310 if (cap_get_capType(cap_a) == cap_irq_control_cap && 311 cap_get_capType(cap_b) == cap_irq_handler_cap) { 312 return false; 313 } 314 if (isArchCap(cap_a) && isArchCap(cap_b)) { 315 return Arch_sameObjectAs(cap_a, cap_b); 316 } 317 return sameRegionAs(cap_a, cap_b); 318} 319 320cap_t CONST 321updateCapData(bool_t preserve, word_t newData, cap_t cap) 322{ 323 if (isArchCap(cap)) { 324 return Arch_updateCapData(preserve, newData, cap); 325 } 326 327 switch (cap_get_capType(cap)) { 328 case cap_endpoint_cap: 329 if (!preserve && cap_endpoint_cap_get_capEPBadge(cap) == 0) { 330 return cap_endpoint_cap_set_capEPBadge(cap, newData); 331 } else { 332 return cap_null_cap_new(); 333 } 334 335 case cap_notification_cap: 336 if (!preserve && cap_notification_cap_get_capNtfnBadge(cap) == 0) { 337 return cap_notification_cap_set_capNtfnBadge(cap, newData); 338 } else { 339 return cap_null_cap_new(); 340 } 341 342 case cap_cnode_cap: { 343 word_t guard, guardSize; 344 seL4_CNode_CapData_t w = { .words = { newData } }; 345 346 guardSize = seL4_CNode_CapData_get_guardSize(w); 347 348 if (guardSize + cap_cnode_cap_get_capCNodeRadix(cap) > wordBits) { 349 return cap_null_cap_new(); 350 } else { 351 cap_t new_cap; 352 353 guard = seL4_CNode_CapData_get_guard(w) & MASK(guardSize); 354 new_cap = cap_cnode_cap_set_capCNodeGuard(cap, guard); 355 new_cap = cap_cnode_cap_set_capCNodeGuardSize(new_cap, 356 guardSize); 357 358 return new_cap; 359 } 360 } 361 362 default: 363 return cap; 364 } 365} 366 367cap_t CONST 368maskCapRights(seL4_CapRights_t cap_rights, cap_t cap) 369{ 370 if (isArchCap(cap)) { 371 return Arch_maskCapRights(cap_rights, cap); 372 } 373 374 switch (cap_get_capType(cap)) { 375 case cap_null_cap: 376 case cap_domain_cap: 377 case cap_cnode_cap: 378 case cap_untyped_cap: 379 case cap_reply_cap: 380 case cap_irq_control_cap: 381 case cap_irq_handler_cap: 382 case cap_zombie_cap: 383 case cap_thread_cap: 384 return cap; 385 386 case cap_endpoint_cap: { 387 cap_t new_cap; 388 389 new_cap = cap_endpoint_cap_set_capCanSend( 390 cap, cap_endpoint_cap_get_capCanSend(cap) & 391 seL4_CapRights_get_capAllowWrite(cap_rights)); 392 new_cap = cap_endpoint_cap_set_capCanReceive( 393 new_cap, cap_endpoint_cap_get_capCanReceive(cap) & 394 seL4_CapRights_get_capAllowRead(cap_rights)); 395 new_cap = cap_endpoint_cap_set_capCanGrant( 396 new_cap, cap_endpoint_cap_get_capCanGrant(cap) & 397 seL4_CapRights_get_capAllowGrant(cap_rights)); 398 399 return new_cap; 400 } 401 402 case cap_notification_cap: { 403 cap_t new_cap; 404 405 new_cap = cap_notification_cap_set_capNtfnCanSend( 406 cap, cap_notification_cap_get_capNtfnCanSend(cap) & 407 seL4_CapRights_get_capAllowWrite(cap_rights)); 408 new_cap = cap_notification_cap_set_capNtfnCanReceive(new_cap, 409 cap_notification_cap_get_capNtfnCanReceive(cap) & 410 seL4_CapRights_get_capAllowRead(cap_rights)); 411 412 return new_cap; 413 } 414 415 default: 416 fail("Invalid cap type"); /* Sentinel for invalid enums */ 417 } 418} 419 420cap_t 421createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory) 422{ 423 /* Handle architecture-specific objects. */ 424 if (t >= (object_t) seL4_NonArchObjectTypeCount) { 425 return Arch_createObject(t, regionBase, userSize, deviceMemory); 426 } 427 428 /* Create objects. */ 429 switch ((api_object_t)t) { 430 case seL4_TCBObject: { 431 tcb_t *tcb; 432 tcb = TCB_PTR((word_t)regionBase + TCB_OFFSET); 433 /** AUXUPD: "(True, ptr_retyps 1 434 (Ptr ((ptr_val \<acute>tcb) - ctcb_offset) :: (cte_C[5]) ptr) 435 o (ptr_retyp \<acute>tcb))" */ 436 437 /* Setup non-zero parts of the TCB. */ 438 439 Arch_initContext(&tcb->tcbArch.tcbContext); 440 tcb->tcbTimeSlice = CONFIG_TIME_SLICE; 441 tcb->tcbDomain = ksCurDomain; 442 443 /* Initialize the new TCB to the current core */ 444 SMP_COND_STATEMENT(tcb->tcbAffinity = getCurrentCPUIndex()); 445 446#ifdef CONFIG_DEBUG_BUILD 447 strlcpy(tcb->tcbName, "child of: '", TCB_NAME_LENGTH); 448 strlcat(tcb->tcbName, NODE_STATE(ksCurThread)->tcbName, TCB_NAME_LENGTH); 449 strlcat(tcb->tcbName, "'", TCB_NAME_LENGTH); 450 tcbDebugAppend(tcb); 451#endif /* CONFIG_DEBUG_BUILD */ 452 453 return cap_thread_cap_new(TCB_REF(tcb)); 454 } 455 456 case seL4_EndpointObject: 457 /** AUXUPD: "(True, ptr_retyp 458 (Ptr (ptr_val \<acute>regionBase) :: endpoint_C ptr))" */ 459 return cap_endpoint_cap_new(0, true, true, true, 460 EP_REF(regionBase)); 461 462 case seL4_NotificationObject: 463 /** AUXUPD: "(True, ptr_retyp 464 (Ptr (ptr_val \<acute>regionBase) :: notification_C ptr))" */ 465 return cap_notification_cap_new(0, true, true, 466 NTFN_REF(regionBase)); 467 468 case seL4_CapTableObject: 469 /** AUXUPD: "(True, ptr_arr_retyps (2 ^ (unat \<acute>userSize)) 470 (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */ 471 /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize) 472 (ptr_val \<acute>regionBase) 473 (4 + unat \<acute>userSize))" */ 474 return cap_cnode_cap_new(userSize, 0, 0, CTE_REF(regionBase)); 475 476 case seL4_UntypedObject: 477 /* 478 * No objects need to be created; instead, just insert caps into 479 * the destination slots. 480 */ 481 return cap_untyped_cap_new(0, !!deviceMemory, userSize, WORD_REF(regionBase)); 482 483 default: 484 fail("Invalid object type"); 485 } 486} 487 488void 489createNewObjects(object_t t, cte_t *parent, slot_range_t slots, 490 void *regionBase, word_t userSize, bool_t deviceMemory) 491{ 492 word_t objectSize; 493 void *nextFreeArea; 494 word_t i; 495 word_t totalObjectSize UNUSED; 496 497 /* ghost check that we're visiting less bytes than the max object size */ 498 objectSize = getObjectSize(t, userSize); 499 totalObjectSize = slots.length << objectSize; 500 /** GHOSTUPD: "(gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 501 \<or> \<acute>totalObjectSize <= gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state, id)" */ 502 503 /* Create the objects. */ 504 nextFreeArea = regionBase; 505 for (i = 0; i < slots.length; i++) { 506 /* Create the object. */ 507 /** AUXUPD: "(True, typ_region_bytes (ptr_val \<acute> nextFreeArea + ((\<acute> i) << unat (\<acute> objectSize))) (unat (\<acute> objectSize)))" */ 508 cap_t cap = createObject(t, (void *)((word_t)nextFreeArea + (i << objectSize)), userSize, deviceMemory); 509 510 /* Insert the cap into the user's cspace. */ 511 insertNewCap(parent, &slots.cnode[slots.offset + i], cap); 512 513 /* Move along to the next region of memory. been merged into a formula of i */ 514 } 515} 516 517exception_t 518decodeInvocation(word_t invLabel, word_t length, 519 cptr_t capIndex, cte_t *slot, cap_t cap, 520 extra_caps_t excaps, bool_t block, bool_t call, 521 word_t *buffer) 522{ 523 if (isArchCap(cap)) { 524 return Arch_decodeInvocation(invLabel, length, capIndex, 525 slot, cap, excaps, call, buffer); 526 } 527 528 switch (cap_get_capType(cap)) { 529 case cap_null_cap: 530 userError("Attempted to invoke a null cap #%lu.", capIndex); 531 current_syscall_error.type = seL4_InvalidCapability; 532 current_syscall_error.invalidCapNumber = 0; 533 return EXCEPTION_SYSCALL_ERROR; 534 535 case cap_zombie_cap: 536 userError("Attempted to invoke a zombie cap #%lu.", capIndex); 537 current_syscall_error.type = seL4_InvalidCapability; 538 current_syscall_error.invalidCapNumber = 0; 539 return EXCEPTION_SYSCALL_ERROR; 540 541 case cap_endpoint_cap: 542 if (unlikely(!cap_endpoint_cap_get_capCanSend(cap))) { 543 userError("Attempted to invoke a read-only endpoint cap #%lu.", 544 capIndex); 545 current_syscall_error.type = seL4_InvalidCapability; 546 current_syscall_error.invalidCapNumber = 0; 547 return EXCEPTION_SYSCALL_ERROR; 548 } 549 550 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 551 return performInvocation_Endpoint( 552 EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)), 553 cap_endpoint_cap_get_capEPBadge(cap), 554 cap_endpoint_cap_get_capCanGrant(cap), block, call); 555 556 case cap_notification_cap: { 557 if (unlikely(!cap_notification_cap_get_capNtfnCanSend(cap))) { 558 userError("Attempted to invoke a read-only notification cap #%lu.", 559 capIndex); 560 current_syscall_error.type = seL4_InvalidCapability; 561 current_syscall_error.invalidCapNumber = 0; 562 return EXCEPTION_SYSCALL_ERROR; 563 } 564 565 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 566 return performInvocation_Notification( 567 NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)), 568 cap_notification_cap_get_capNtfnBadge(cap)); 569 } 570 571 case cap_reply_cap: 572 if (unlikely(cap_reply_cap_get_capReplyMaster(cap))) { 573 userError("Attempted to invoke an invalid reply cap #%lu.", 574 capIndex); 575 current_syscall_error.type = seL4_InvalidCapability; 576 current_syscall_error.invalidCapNumber = 0; 577 return EXCEPTION_SYSCALL_ERROR; 578 } 579 580 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 581 return performInvocation_Reply( 582 TCB_PTR(cap_reply_cap_get_capTCBPtr(cap)), slot); 583 584 case cap_thread_cap: 585 return decodeTCBInvocation(invLabel, length, cap, 586 slot, excaps, call, buffer); 587 588 case cap_domain_cap: 589 return decodeDomainInvocation(invLabel, length, excaps, buffer); 590 591 case cap_cnode_cap: 592 return decodeCNodeInvocation(invLabel, length, cap, excaps, buffer); 593 594 case cap_untyped_cap: 595 return decodeUntypedInvocation(invLabel, length, slot, cap, excaps, 596 call, buffer); 597 598 case cap_irq_control_cap: 599 return decodeIRQControlInvocation(invLabel, length, slot, 600 excaps, buffer); 601 602 case cap_irq_handler_cap: 603 return decodeIRQHandlerInvocation(invLabel, 604 cap_irq_handler_cap_get_capIRQ(cap), excaps); 605 606 default: 607 fail("Invalid cap type"); 608 } 609} 610 611exception_t 612performInvocation_Endpoint(endpoint_t *ep, word_t badge, 613 bool_t canGrant, bool_t block, 614 bool_t call) 615{ 616 sendIPC(block, call, badge, canGrant, NODE_STATE(ksCurThread), ep); 617 618 return EXCEPTION_NONE; 619} 620 621exception_t 622performInvocation_Notification(notification_t *ntfn, word_t badge) 623{ 624 sendSignal(ntfn, badge); 625 626 return EXCEPTION_NONE; 627} 628 629exception_t 630performInvocation_Reply(tcb_t *thread, cte_t *slot) 631{ 632 doReplyTransfer(NODE_STATE(ksCurThread), thread, slot); 633 return EXCEPTION_NONE; 634} 635