1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#include <assert.h> 8#include <config.h> 9#include <types.h> 10#include <api/failures.h> 11#include <api/syscall.h> 12#include <arch/object/objecttype.h> 13#include <machine/io.h> 14#include <object/objecttype.h> 15#include <object/structures.h> 16#include <object/notification.h> 17#include <object/endpoint.h> 18#include <object/cnode.h> 19#include <object/interrupt.h> 20#ifdef CONFIG_KERNEL_MCS 21#include <object/schedcontext.h> 22#include <object/schedcontrol.h> 23#endif 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#ifdef CONFIG_KERNEL_MCS 50 case seL4_SchedContextObject: 51 return userObjSize; 52 case seL4_ReplyObject: 53 return seL4_ReplyBits; 54#endif 55 default: 56 fail("Invalid object type"); 57 return 0; 58 } 59 } 60} 61 62deriveCap_ret_t deriveCap(cte_t *slot, cap_t cap) 63{ 64 deriveCap_ret_t ret; 65 66 if (isArchCap(cap)) { 67 return Arch_deriveCap(slot, cap); 68 } 69 70 switch (cap_get_capType(cap)) { 71 case cap_zombie_cap: 72 ret.status = EXCEPTION_NONE; 73 ret.cap = cap_null_cap_new(); 74 break; 75 76 case cap_irq_control_cap: 77 ret.status = EXCEPTION_NONE; 78 ret.cap = cap_null_cap_new(); 79 break; 80 81 case cap_untyped_cap: 82 ret.status = ensureNoChildren(slot); 83 if (ret.status != EXCEPTION_NONE) { 84 ret.cap = cap_null_cap_new(); 85 } else { 86 ret.cap = cap; 87 } 88 break; 89 90#ifndef CONFIG_KERNEL_MCS 91 case cap_reply_cap: 92 ret.status = EXCEPTION_NONE; 93 ret.cap = cap_null_cap_new(); 94 break; 95#endif 96 default: 97 ret.status = EXCEPTION_NONE; 98 ret.cap = cap; 99 } 100 101 return ret; 102} 103 104finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed) 105{ 106 finaliseCap_ret_t fc_ret; 107 108 if (isArchCap(cap)) { 109 return Arch_finaliseCap(cap, final); 110 } 111 112 switch (cap_get_capType(cap)) { 113 case cap_endpoint_cap: 114 if (final) { 115 cancelAllIPC(EP_PTR(cap_endpoint_cap_get_capEPPtr(cap))); 116 } 117 118 fc_ret.remainder = cap_null_cap_new(); 119 fc_ret.cleanupInfo = cap_null_cap_new(); 120 return fc_ret; 121 122 case cap_notification_cap: 123 if (final) { 124 notification_t *ntfn = NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)); 125#ifdef CONFIG_KERNEL_MCS 126 schedContext_unbindNtfn(SC_PTR(notification_ptr_get_ntfnSchedContext(ntfn))); 127#endif 128 unbindMaybeNotification(ntfn); 129 cancelAllSignals(ntfn); 130 } 131 fc_ret.remainder = cap_null_cap_new(); 132 fc_ret.cleanupInfo = cap_null_cap_new(); 133 return fc_ret; 134 135 case cap_reply_cap: 136#ifdef CONFIG_KERNEL_MCS 137 if (final) { 138 reply_t *reply = REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap)); 139 if (reply && reply->replyTCB) { 140 switch (thread_state_get_tsType(reply->replyTCB->tcbState)) { 141 case ThreadState_BlockedOnReply: 142 reply_remove(reply, reply->replyTCB); 143 break; 144 case ThreadState_BlockedOnReceive: 145 reply_unlink(reply, reply->replyTCB); 146 break; 147 default: 148 fail("Invalid tcb state"); 149 } 150 } 151 } 152 fc_ret.remainder = cap_null_cap_new(); 153 fc_ret.cleanupInfo = cap_null_cap_new(); 154 return fc_ret; 155#endif 156 case cap_null_cap: 157 case cap_domain_cap: 158 fc_ret.remainder = cap_null_cap_new(); 159 fc_ret.cleanupInfo = cap_null_cap_new(); 160 return fc_ret; 161 } 162 163 if (exposed) { 164 fail("finaliseCap: failed to finalise immediately."); 165 } 166 167 switch (cap_get_capType(cap)) { 168 case cap_cnode_cap: { 169 if (final) { 170 fc_ret.remainder = 171 Zombie_new( 172 1ul << cap_cnode_cap_get_capCNodeRadix(cap), 173 cap_cnode_cap_get_capCNodeRadix(cap), 174 cap_cnode_cap_get_capCNodePtr(cap) 175 ); 176 fc_ret.cleanupInfo = cap_null_cap_new(); 177 return fc_ret; 178 } 179 break; 180 } 181 182 case cap_thread_cap: { 183 if (final) { 184 tcb_t *tcb; 185 cte_t *cte_ptr; 186 187 tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap)); 188 SMP_COND_STATEMENT(remoteTCBStall(tcb);) 189 cte_ptr = TCB_PTR_CTE_PTR(tcb, tcbCTable); 190 unbindNotification(tcb); 191#ifdef CONFIG_KERNEL_MCS 192 if (tcb->tcbSchedContext) { 193 schedContext_completeYieldTo(tcb->tcbSchedContext->scYieldFrom); 194 schedContext_unbindTCB(tcb->tcbSchedContext, tcb); 195 } 196#endif 197 suspend(tcb); 198#ifdef CONFIG_DEBUG_BUILD 199 tcbDebugRemove(tcb); 200#endif 201 Arch_prepareThreadDelete(tcb); 202 fc_ret.remainder = 203 Zombie_new( 204 tcbArchCNodeEntries, 205 ZombieType_ZombieTCB, 206 CTE_REF(cte_ptr) 207 ); 208 fc_ret.cleanupInfo = cap_null_cap_new(); 209 return fc_ret; 210 } 211 break; 212 } 213 214#ifdef CONFIG_KERNEL_MCS 215 case cap_sched_context_cap: 216 if (final) { 217 sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap)); 218 schedContext_unbindAllTCBs(sc); 219 schedContext_unbindNtfn(sc); 220 if (sc->scReply) { 221 assert(call_stack_get_isHead(sc->scReply->replyNext)); 222 sc->scReply->replyNext = call_stack_new(0, false); 223 sc->scReply = NULL; 224 } 225 if (sc->scYieldFrom) { 226 schedContext_completeYieldTo(sc->scYieldFrom); 227 } 228 /* mark the sc as no longer valid */ 229 sc->scRefillMax = 0; 230 fc_ret.remainder = cap_null_cap_new(); 231 fc_ret.cleanupInfo = cap_null_cap_new(); 232 return fc_ret; 233 } 234 break; 235#endif 236 237 case cap_zombie_cap: 238 fc_ret.remainder = cap; 239 fc_ret.cleanupInfo = cap_null_cap_new(); 240 return fc_ret; 241 242 case cap_irq_handler_cap: 243 if (final) { 244 irq_t irq = IDX_TO_IRQT(cap_irq_handler_cap_get_capIRQ(cap)); 245 246 deletingIRQHandler(irq); 247 248 fc_ret.remainder = cap_null_cap_new(); 249 fc_ret.cleanupInfo = cap; 250 return fc_ret; 251 } 252 break; 253 } 254 255 fc_ret.remainder = cap_null_cap_new(); 256 fc_ret.cleanupInfo = cap_null_cap_new(); 257 return fc_ret; 258} 259 260bool_t CONST hasCancelSendRights(cap_t cap) 261{ 262 switch (cap_get_capType(cap)) { 263 case cap_endpoint_cap: 264 return cap_endpoint_cap_get_capCanSend(cap) && 265 cap_endpoint_cap_get_capCanReceive(cap) && 266 cap_endpoint_cap_get_capCanGrantReply(cap) && 267 cap_endpoint_cap_get_capCanGrant(cap); 268 269 default: 270 return false; 271 } 272} 273 274bool_t CONST sameRegionAs(cap_t cap_a, cap_t cap_b) 275{ 276 switch (cap_get_capType(cap_a)) { 277 case cap_untyped_cap: 278 if (cap_get_capIsPhysical(cap_b)) { 279 word_t aBase, bBase, aTop, bTop; 280 281 aBase = (word_t)WORD_PTR(cap_untyped_cap_get_capPtr(cap_a)); 282 bBase = (word_t)cap_get_capPtr(cap_b); 283 284 aTop = aBase + MASK(cap_untyped_cap_get_capBlockSize(cap_a)); 285 bTop = bBase + MASK(cap_get_capSizeBits(cap_b)); 286 287 return (aBase <= bBase) && (bTop <= aTop) && (bBase <= bTop); 288 } 289 break; 290 291 case cap_endpoint_cap: 292 if (cap_get_capType(cap_b) == cap_endpoint_cap) { 293 return cap_endpoint_cap_get_capEPPtr(cap_a) == 294 cap_endpoint_cap_get_capEPPtr(cap_b); 295 } 296 break; 297 298 case cap_notification_cap: 299 if (cap_get_capType(cap_b) == cap_notification_cap) { 300 return cap_notification_cap_get_capNtfnPtr(cap_a) == 301 cap_notification_cap_get_capNtfnPtr(cap_b); 302 } 303 break; 304 305 case cap_cnode_cap: 306 if (cap_get_capType(cap_b) == cap_cnode_cap) { 307 return (cap_cnode_cap_get_capCNodePtr(cap_a) == 308 cap_cnode_cap_get_capCNodePtr(cap_b)) && 309 (cap_cnode_cap_get_capCNodeRadix(cap_a) == 310 cap_cnode_cap_get_capCNodeRadix(cap_b)); 311 } 312 break; 313 314 case cap_thread_cap: 315 if (cap_get_capType(cap_b) == cap_thread_cap) { 316 return cap_thread_cap_get_capTCBPtr(cap_a) == 317 cap_thread_cap_get_capTCBPtr(cap_b); 318 } 319 break; 320 321 case cap_reply_cap: 322 if (cap_get_capType(cap_b) == cap_reply_cap) { 323#ifdef CONFIG_KERNEL_MCS 324 return cap_reply_cap_get_capReplyPtr(cap_a) == 325 cap_reply_cap_get_capReplyPtr(cap_b); 326#else 327 return cap_reply_cap_get_capTCBPtr(cap_a) == 328 cap_reply_cap_get_capTCBPtr(cap_b); 329#endif 330 } 331 break; 332 333 case cap_domain_cap: 334 if (cap_get_capType(cap_b) == cap_domain_cap) { 335 return true; 336 } 337 break; 338 339 case cap_irq_control_cap: 340 if (cap_get_capType(cap_b) == cap_irq_control_cap || 341 cap_get_capType(cap_b) == cap_irq_handler_cap) { 342 return true; 343 } 344 break; 345 346 case cap_irq_handler_cap: 347 if (cap_get_capType(cap_b) == cap_irq_handler_cap) { 348 return (word_t)cap_irq_handler_cap_get_capIRQ(cap_a) == 349 (word_t)cap_irq_handler_cap_get_capIRQ(cap_b); 350 } 351 break; 352 353#ifdef CONFIG_KERNEL_MCS 354 case cap_sched_context_cap: 355 if (cap_get_capType(cap_b) == cap_sched_context_cap) { 356 return (cap_sched_context_cap_get_capSCPtr(cap_a) == 357 cap_sched_context_cap_get_capSCPtr(cap_b)) && 358 (cap_sched_context_cap_get_capSCSizeBits(cap_a) == 359 cap_sched_context_cap_get_capSCSizeBits(cap_b)); 360 } 361 break; 362 case cap_sched_control_cap: 363 if (cap_get_capType(cap_b) == cap_sched_control_cap) { 364 return true; 365 } 366 break; 367#endif 368 default: 369 if (isArchCap(cap_a) && 370 isArchCap(cap_b)) { 371 return Arch_sameRegionAs(cap_a, cap_b); 372 } 373 break; 374 } 375 376 return false; 377} 378 379bool_t CONST sameObjectAs(cap_t cap_a, cap_t cap_b) 380{ 381 if (cap_get_capType(cap_a) == cap_untyped_cap) { 382 return false; 383 } 384 if (cap_get_capType(cap_a) == cap_irq_control_cap && 385 cap_get_capType(cap_b) == cap_irq_handler_cap) { 386 return false; 387 } 388 if (isArchCap(cap_a) && isArchCap(cap_b)) { 389 return Arch_sameObjectAs(cap_a, cap_b); 390 } 391 return sameRegionAs(cap_a, cap_b); 392} 393 394cap_t CONST updateCapData(bool_t preserve, word_t newData, cap_t cap) 395{ 396 if (isArchCap(cap)) { 397 return Arch_updateCapData(preserve, newData, cap); 398 } 399 400 switch (cap_get_capType(cap)) { 401 case cap_endpoint_cap: 402 if (!preserve && cap_endpoint_cap_get_capEPBadge(cap) == 0) { 403 return cap_endpoint_cap_set_capEPBadge(cap, newData); 404 } else { 405 return cap_null_cap_new(); 406 } 407 408 case cap_notification_cap: 409 if (!preserve && cap_notification_cap_get_capNtfnBadge(cap) == 0) { 410 return cap_notification_cap_set_capNtfnBadge(cap, newData); 411 } else { 412 return cap_null_cap_new(); 413 } 414 415 case cap_cnode_cap: { 416 word_t guard, guardSize; 417 seL4_CNode_CapData_t w = { .words = { newData } }; 418 419 guardSize = seL4_CNode_CapData_get_guardSize(w); 420 421 if (guardSize + cap_cnode_cap_get_capCNodeRadix(cap) > wordBits) { 422 return cap_null_cap_new(); 423 } else { 424 cap_t new_cap; 425 426 guard = seL4_CNode_CapData_get_guard(w) & MASK(guardSize); 427 new_cap = cap_cnode_cap_set_capCNodeGuard(cap, guard); 428 new_cap = cap_cnode_cap_set_capCNodeGuardSize(new_cap, 429 guardSize); 430 431 return new_cap; 432 } 433 } 434 435 default: 436 return cap; 437 } 438} 439 440cap_t CONST maskCapRights(seL4_CapRights_t cap_rights, cap_t cap) 441{ 442 if (isArchCap(cap)) { 443 return Arch_maskCapRights(cap_rights, cap); 444 } 445 446 switch (cap_get_capType(cap)) { 447 case cap_null_cap: 448 case cap_domain_cap: 449 case cap_cnode_cap: 450 case cap_untyped_cap: 451 case cap_irq_control_cap: 452 case cap_irq_handler_cap: 453 case cap_zombie_cap: 454 case cap_thread_cap: 455#ifdef CONFIG_KERNEL_MCS 456 case cap_sched_context_cap: 457 case cap_sched_control_cap: 458#endif 459 return cap; 460 461 case cap_endpoint_cap: { 462 cap_t new_cap; 463 464 new_cap = cap_endpoint_cap_set_capCanSend( 465 cap, cap_endpoint_cap_get_capCanSend(cap) & 466 seL4_CapRights_get_capAllowWrite(cap_rights)); 467 new_cap = cap_endpoint_cap_set_capCanReceive( 468 new_cap, cap_endpoint_cap_get_capCanReceive(cap) & 469 seL4_CapRights_get_capAllowRead(cap_rights)); 470 new_cap = cap_endpoint_cap_set_capCanGrant( 471 new_cap, cap_endpoint_cap_get_capCanGrant(cap) & 472 seL4_CapRights_get_capAllowGrant(cap_rights)); 473 new_cap = cap_endpoint_cap_set_capCanGrantReply( 474 new_cap, cap_endpoint_cap_get_capCanGrantReply(cap) & 475 seL4_CapRights_get_capAllowGrantReply(cap_rights)); 476 477 return new_cap; 478 } 479 480 case cap_notification_cap: { 481 cap_t new_cap; 482 483 new_cap = cap_notification_cap_set_capNtfnCanSend( 484 cap, cap_notification_cap_get_capNtfnCanSend(cap) & 485 seL4_CapRights_get_capAllowWrite(cap_rights)); 486 new_cap = cap_notification_cap_set_capNtfnCanReceive(new_cap, 487 cap_notification_cap_get_capNtfnCanReceive(cap) & 488 seL4_CapRights_get_capAllowRead(cap_rights)); 489 490 return new_cap; 491 } 492 case cap_reply_cap: { 493 cap_t new_cap; 494 495 new_cap = cap_reply_cap_set_capReplyCanGrant( 496 cap, cap_reply_cap_get_capReplyCanGrant(cap) & 497 seL4_CapRights_get_capAllowGrant(cap_rights)); 498 return new_cap; 499 } 500 501 502 default: 503 fail("Invalid cap type"); /* Sentinel for invalid enums */ 504 } 505} 506 507cap_t createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory) 508{ 509 /* Handle architecture-specific objects. */ 510 if (t >= (object_t) seL4_NonArchObjectTypeCount) { 511 return Arch_createObject(t, regionBase, userSize, deviceMemory); 512 } 513 514 /* Create objects. */ 515 switch ((api_object_t)t) { 516 case seL4_TCBObject: { 517 tcb_t *tcb; 518 tcb = TCB_PTR((word_t)regionBase + TCB_OFFSET); 519 /** AUXUPD: "(True, ptr_retyps 1 520 (Ptr ((ptr_val \<acute>tcb) - ctcb_offset) :: (cte_C[5]) ptr) 521 o (ptr_retyp \<acute>tcb))" */ 522 523 /* Setup non-zero parts of the TCB. */ 524 525 Arch_initContext(&tcb->tcbArch.tcbContext); 526#ifndef CONFIG_KERNEL_MCS 527 tcb->tcbTimeSlice = CONFIG_TIME_SLICE; 528#endif 529 tcb->tcbDomain = ksCurDomain; 530#ifndef CONFIG_KERNEL_MCS 531 /* Initialize the new TCB to the current core */ 532 SMP_COND_STATEMENT(tcb->tcbAffinity = getCurrentCPUIndex()); 533#endif 534#ifdef CONFIG_DEBUG_BUILD 535 strlcpy(TCB_PTR_DEBUG_PTR(tcb)->tcbName, "child of: '", TCB_NAME_LENGTH); 536 strlcat(TCB_PTR_DEBUG_PTR(tcb)->tcbName, TCB_PTR_DEBUG_PTR(NODE_STATE(ksCurThread))->tcbName, TCB_NAME_LENGTH); 537 strlcat(TCB_PTR_DEBUG_PTR(tcb)->tcbName, "'", TCB_NAME_LENGTH); 538 tcbDebugAppend(tcb); 539#endif /* CONFIG_DEBUG_BUILD */ 540 541 return cap_thread_cap_new(TCB_REF(tcb)); 542 } 543 544 case seL4_EndpointObject: 545 /** AUXUPD: "(True, ptr_retyp 546 (Ptr (ptr_val \<acute>regionBase) :: endpoint_C ptr))" */ 547 return cap_endpoint_cap_new(0, true, true, true, true, 548 EP_REF(regionBase)); 549 550 case seL4_NotificationObject: 551 /** AUXUPD: "(True, ptr_retyp 552 (Ptr (ptr_val \<acute>regionBase) :: notification_C ptr))" */ 553 return cap_notification_cap_new(0, true, true, 554 NTFN_REF(regionBase)); 555 556 case seL4_CapTableObject: 557 /** AUXUPD: "(True, ptr_arr_retyps (2 ^ (unat \<acute>userSize)) 558 (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */ 559 /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize) 560 (ptr_val \<acute>regionBase) 561 (4 + unat \<acute>userSize))" */ 562 return cap_cnode_cap_new(userSize, 0, 0, CTE_REF(regionBase)); 563 564 case seL4_UntypedObject: 565 /* 566 * No objects need to be created; instead, just insert caps into 567 * the destination slots. 568 */ 569 return cap_untyped_cap_new(0, !!deviceMemory, userSize, WORD_REF(regionBase)); 570 571#ifdef CONFIG_KERNEL_MCS 572 case seL4_SchedContextObject: 573 memzero(regionBase, BIT(userSize)); 574 return cap_sched_context_cap_new(SC_REF(regionBase), userSize); 575 576 case seL4_ReplyObject: 577 memzero(regionBase, 1UL << seL4_ReplyBits); 578 return cap_reply_cap_new(REPLY_REF(regionBase), true); 579#endif 580 581 default: 582 fail("Invalid object type"); 583 } 584} 585 586void createNewObjects(object_t t, cte_t *parent, slot_range_t slots, 587 void *regionBase, word_t userSize, bool_t deviceMemory) 588{ 589 word_t objectSize; 590 void *nextFreeArea; 591 word_t i; 592 word_t totalObjectSize UNUSED; 593 594 /* ghost check that we're visiting less bytes than the max object size */ 595 objectSize = getObjectSize(t, userSize); 596 totalObjectSize = slots.length << objectSize; 597 /** GHOSTUPD: "(gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 598 \<or> \<acute>totalObjectSize <= gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state, id)" */ 599 600 /* Create the objects. */ 601 nextFreeArea = regionBase; 602 for (i = 0; i < slots.length; i++) { 603 /* Create the object. */ 604 /** AUXUPD: "(True, typ_region_bytes (ptr_val \<acute> nextFreeArea + ((\<acute> i) << unat (\<acute> objectSize))) (unat (\<acute> objectSize)))" */ 605 cap_t cap = createObject(t, (void *)((word_t)nextFreeArea + (i << objectSize)), userSize, deviceMemory); 606 607 /* Insert the cap into the user's cspace. */ 608 insertNewCap(parent, &slots.cnode[slots.offset + i], cap); 609 610 /* Move along to the next region of memory. been merged into a formula of i */ 611 } 612} 613 614#ifdef CONFIG_KERNEL_MCS 615exception_t decodeInvocation(word_t invLabel, word_t length, 616 cptr_t capIndex, cte_t *slot, cap_t cap, 617 extra_caps_t excaps, bool_t block, bool_t call, 618 bool_t canDonate, bool_t firstPhase, word_t *buffer) 619#else 620exception_t decodeInvocation(word_t invLabel, word_t length, 621 cptr_t capIndex, cte_t *slot, cap_t cap, 622 extra_caps_t excaps, bool_t block, bool_t call, 623 word_t *buffer) 624#endif 625{ 626 if (isArchCap(cap)) { 627 return Arch_decodeInvocation(invLabel, length, capIndex, 628 slot, cap, excaps, call, buffer); 629 } 630 631 switch (cap_get_capType(cap)) { 632 case cap_null_cap: 633 userError("Attempted to invoke a null cap #%lu.", capIndex); 634 current_syscall_error.type = seL4_InvalidCapability; 635 current_syscall_error.invalidCapNumber = 0; 636 return EXCEPTION_SYSCALL_ERROR; 637 638 case cap_zombie_cap: 639 userError("Attempted to invoke a zombie cap #%lu.", capIndex); 640 current_syscall_error.type = seL4_InvalidCapability; 641 current_syscall_error.invalidCapNumber = 0; 642 return EXCEPTION_SYSCALL_ERROR; 643 644 case cap_endpoint_cap: 645 if (unlikely(!cap_endpoint_cap_get_capCanSend(cap))) { 646 userError("Attempted to invoke a read-only endpoint cap #%lu.", 647 capIndex); 648 current_syscall_error.type = seL4_InvalidCapability; 649 current_syscall_error.invalidCapNumber = 0; 650 return EXCEPTION_SYSCALL_ERROR; 651 } 652 653 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 654#ifdef CONFIG_KERNEL_MCS 655 return performInvocation_Endpoint( 656 EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)), 657 cap_endpoint_cap_get_capEPBadge(cap), 658 cap_endpoint_cap_get_capCanGrant(cap), 659 cap_endpoint_cap_get_capCanGrantReply(cap), block, call, canDonate); 660#else 661 return performInvocation_Endpoint( 662 EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)), 663 cap_endpoint_cap_get_capEPBadge(cap), 664 cap_endpoint_cap_get_capCanGrant(cap), 665 cap_endpoint_cap_get_capCanGrantReply(cap), block, call); 666#endif 667 668 case cap_notification_cap: { 669 if (unlikely(!cap_notification_cap_get_capNtfnCanSend(cap))) { 670 userError("Attempted to invoke a read-only notification cap #%lu.", 671 capIndex); 672 current_syscall_error.type = seL4_InvalidCapability; 673 current_syscall_error.invalidCapNumber = 0; 674 return EXCEPTION_SYSCALL_ERROR; 675 } 676 677 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 678 return performInvocation_Notification( 679 NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)), 680 cap_notification_cap_get_capNtfnBadge(cap)); 681 } 682 683#ifdef CONFIG_KERNEL_MCS 684 case cap_reply_cap: 685 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 686 return performInvocation_Reply( 687 NODE_STATE(ksCurThread), 688 REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap)), 689 cap_reply_cap_get_capReplyCanGrant(cap)); 690#else 691 case cap_reply_cap: 692 if (unlikely(cap_reply_cap_get_capReplyMaster(cap))) { 693 userError("Attempted to invoke an invalid reply cap #%lu.", 694 capIndex); 695 current_syscall_error.type = seL4_InvalidCapability; 696 current_syscall_error.invalidCapNumber = 0; 697 return EXCEPTION_SYSCALL_ERROR; 698 } 699 700 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 701 return performInvocation_Reply( 702 TCB_PTR(cap_reply_cap_get_capTCBPtr(cap)), slot, 703 cap_reply_cap_get_capReplyCanGrant(cap)); 704 705#endif 706 707 case cap_thread_cap: 708#ifdef CONFIG_KERNEL_MCS 709 if (unlikely(firstPhase)) { 710 userError("Cannot invoke thread capabilities in the first phase of an invocation"); 711 current_syscall_error.type = seL4_InvalidCapability; 712 current_syscall_error.invalidCapNumber = 0; 713 return EXCEPTION_SYSCALL_ERROR; 714 } 715#endif 716 return decodeTCBInvocation(invLabel, length, cap, 717 slot, excaps, call, buffer); 718 719 case cap_domain_cap: 720#ifdef CONFIG_KERNEL_MCS 721 if (unlikely(firstPhase)) { 722 userError("Cannot invoke domain capabilities in the first phase of an invocation"); 723 current_syscall_error.type = seL4_InvalidCapability; 724 current_syscall_error.invalidCapNumber = 0; 725 return EXCEPTION_SYSCALL_ERROR; 726 } 727#endif 728 return decodeDomainInvocation(invLabel, length, excaps, buffer); 729 730 case cap_cnode_cap: 731#ifdef CONFIG_KERNEL_MCS 732 if (unlikely(firstPhase)) { 733 userError("Cannot invoke cnode capabilities in the first phase of an invocation"); 734 current_syscall_error.type = seL4_InvalidCapability; 735 current_syscall_error.invalidCapNumber = 0; 736 return EXCEPTION_SYSCALL_ERROR; 737 } 738#endif 739 return decodeCNodeInvocation(invLabel, length, cap, excaps, buffer); 740 741 case cap_untyped_cap: 742 return decodeUntypedInvocation(invLabel, length, slot, cap, excaps, 743 call, buffer); 744 745 case cap_irq_control_cap: 746 return decodeIRQControlInvocation(invLabel, length, slot, 747 excaps, buffer); 748 749 case cap_irq_handler_cap: 750 return decodeIRQHandlerInvocation(invLabel, 751 IDX_TO_IRQT(cap_irq_handler_cap_get_capIRQ(cap)), excaps); 752 753#ifdef CONFIG_KERNEL_MCS 754 case cap_sched_control_cap: 755 if (unlikely(firstPhase)) { 756 userError("Cannot invoke sched control capabilities in the first phase of an invocation"); 757 current_syscall_error.type = seL4_InvalidCapability; 758 current_syscall_error.invalidCapNumber = 0; 759 return EXCEPTION_SYSCALL_ERROR; 760 } 761 return decodeSchedControlInvocation(invLabel, cap, length, excaps, buffer); 762 763 case cap_sched_context_cap: 764 if (unlikely(firstPhase)) { 765 userError("Cannot invoke sched context capabilities in the first phase of an invocation"); 766 current_syscall_error.type = seL4_InvalidCapability; 767 current_syscall_error.invalidCapNumber = 0; 768 return EXCEPTION_SYSCALL_ERROR; 769 } 770 return decodeSchedContextInvocation(invLabel, cap, excaps, buffer); 771#endif 772 default: 773 fail("Invalid cap type"); 774 } 775} 776 777#ifdef CONFIG_KERNEL_MCS 778exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge, 779 bool_t canGrant, bool_t canGrantReply, 780 bool_t block, bool_t call, bool_t canDonate) 781{ 782 sendIPC(block, call, badge, canGrant, canGrantReply, canDonate, NODE_STATE(ksCurThread), ep); 783 784 return EXCEPTION_NONE; 785} 786#else 787exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge, 788 bool_t canGrant, bool_t canGrantReply, 789 bool_t block, bool_t call) 790{ 791 sendIPC(block, call, badge, canGrant, canGrantReply, NODE_STATE(ksCurThread), ep); 792 793 return EXCEPTION_NONE; 794} 795#endif 796 797exception_t performInvocation_Notification(notification_t *ntfn, word_t badge) 798{ 799 sendSignal(ntfn, badge); 800 801 return EXCEPTION_NONE; 802} 803 804#ifdef CONFIG_KERNEL_MCS 805exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply, bool_t canGrant) 806{ 807 doReplyTransfer(thread, reply, canGrant); 808 return EXCEPTION_NONE; 809} 810#else 811exception_t performInvocation_Reply(tcb_t *thread, cte_t *slot, bool_t canGrant) 812{ 813 doReplyTransfer(NODE_STATE(ksCurThread), thread, slot, canGrant); 814 return EXCEPTION_NONE; 815} 816#endif 817