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 <types.h> 9#include <api/failures.h> 10#include <api/invocation.h> 11#include <api/syscall.h> 12#include <api/types.h> 13#include <machine/io.h> 14#include <object/structures.h> 15#include <object/objecttype.h> 16#include <object/cnode.h> 17#include <object/interrupt.h> 18#include <object/untyped.h> 19#include <kernel/cspace.h> 20#include <kernel/thread.h> 21#include <model/preemption.h> 22#include <model/statedata.h> 23#include <util.h> 24 25struct finaliseSlot_ret { 26 exception_t status; 27 bool_t success; 28 cap_t cleanupInfo; 29}; 30typedef struct finaliseSlot_ret finaliseSlot_ret_t; 31 32static finaliseSlot_ret_t finaliseSlot(cte_t *slot, bool_t exposed); 33static void emptySlot(cte_t *slot, cap_t cleanupInfo); 34static exception_t reduceZombie(cte_t *slot, bool_t exposed); 35 36#ifdef CONFIG_KERNEL_MCS 37#define CNODE_LAST_INVOCATION CNodeRotate 38#else 39#define CNODE_LAST_INVOCATION CNodeSaveCaller 40#endif 41 42exception_t decodeCNodeInvocation(word_t invLabel, word_t length, cap_t cap, 43 extra_caps_t excaps, word_t *buffer) 44{ 45 lookupSlot_ret_t lu_ret; 46 cte_t *destSlot; 47 word_t index, w_bits; 48 exception_t status; 49 50 /* Haskell error: "decodeCNodeInvocation: invalid cap" */ 51 assert(cap_get_capType(cap) == cap_cnode_cap); 52 53 if (invLabel < CNodeRevoke || invLabel > CNODE_LAST_INVOCATION) { 54 userError("CNodeCap: Illegal Operation attempted."); 55 current_syscall_error.type = seL4_IllegalOperation; 56 return EXCEPTION_SYSCALL_ERROR; 57 } 58 59 if (length < 2) { 60 userError("CNode operation: Truncated message."); 61 current_syscall_error.type = seL4_TruncatedMessage; 62 return EXCEPTION_SYSCALL_ERROR; 63 } 64 index = getSyscallArg(0, buffer); 65 w_bits = getSyscallArg(1, buffer); 66 67 lu_ret = lookupTargetSlot(cap, index, w_bits); 68 if (lu_ret.status != EXCEPTION_NONE) { 69 userError("CNode operation: Target slot invalid."); 70 return lu_ret.status; 71 } 72 destSlot = lu_ret.slot; 73 74 if (invLabel >= CNodeCopy && invLabel <= CNodeMutate) { 75 cte_t *srcSlot; 76 word_t srcIndex, srcDepth, capData; 77 bool_t isMove; 78 seL4_CapRights_t cap_rights; 79 cap_t srcRoot, newCap; 80 deriveCap_ret_t dc_ret; 81 cap_t srcCap; 82 83 if (length < 4 || excaps.excaprefs[0] == NULL) { 84 userError("CNode Copy/Mint/Move/Mutate: Truncated message."); 85 current_syscall_error.type = seL4_TruncatedMessage; 86 return EXCEPTION_SYSCALL_ERROR; 87 } 88 srcIndex = getSyscallArg(2, buffer); 89 srcDepth = getSyscallArg(3, buffer); 90 91 srcRoot = excaps.excaprefs[0]->cap; 92 93 status = ensureEmptySlot(destSlot); 94 if (status != EXCEPTION_NONE) { 95 userError("CNode Copy/Mint/Move/Mutate: Destination not empty."); 96 return status; 97 } 98 99 lu_ret = lookupSourceSlot(srcRoot, srcIndex, srcDepth); 100 if (lu_ret.status != EXCEPTION_NONE) { 101 userError("CNode Copy/Mint/Move/Mutate: Invalid source slot."); 102 return lu_ret.status; 103 } 104 srcSlot = lu_ret.slot; 105 106 if (cap_get_capType(srcSlot->cap) == cap_null_cap) { 107 userError("CNode Copy/Mint/Move/Mutate: Source slot invalid or empty."); 108 current_syscall_error.type = seL4_FailedLookup; 109 current_syscall_error.failedLookupWasSource = 1; 110 current_lookup_fault = 111 lookup_fault_missing_capability_new(srcDepth); 112 return EXCEPTION_SYSCALL_ERROR; 113 } 114 115 switch (invLabel) { 116 case CNodeCopy: 117 118 if (length < 5) { 119 userError("Truncated message for CNode Copy operation."); 120 current_syscall_error.type = seL4_TruncatedMessage; 121 return EXCEPTION_SYSCALL_ERROR; 122 } 123 124 cap_rights = rightsFromWord(getSyscallArg(4, buffer)); 125 srcCap = maskCapRights(cap_rights, srcSlot->cap); 126 dc_ret = deriveCap(srcSlot, srcCap); 127 if (dc_ret.status != EXCEPTION_NONE) { 128 userError("Error deriving cap for CNode Copy operation."); 129 return dc_ret.status; 130 } 131 newCap = dc_ret.cap; 132 isMove = false; 133 134 break; 135 136 case CNodeMint: 137 if (length < 6) { 138 userError("CNode Mint: Truncated message."); 139 current_syscall_error.type = seL4_TruncatedMessage; 140 return EXCEPTION_SYSCALL_ERROR; 141 } 142 143 cap_rights = rightsFromWord(getSyscallArg(4, buffer)); 144 capData = getSyscallArg(5, buffer); 145 srcCap = maskCapRights(cap_rights, srcSlot->cap); 146 dc_ret = deriveCap(srcSlot, 147 updateCapData(false, capData, srcCap)); 148 if (dc_ret.status != EXCEPTION_NONE) { 149 userError("Error deriving cap for CNode Mint operation."); 150 return dc_ret.status; 151 } 152 newCap = dc_ret.cap; 153 isMove = false; 154 155 break; 156 157 case CNodeMove: 158 newCap = srcSlot->cap; 159 isMove = true; 160 161 break; 162 163 case CNodeMutate: 164 if (length < 5) { 165 userError("CNode Mutate: Truncated message."); 166 current_syscall_error.type = seL4_TruncatedMessage; 167 return EXCEPTION_SYSCALL_ERROR; 168 } 169 170 capData = getSyscallArg(4, buffer); 171 newCap = updateCapData(true, capData, srcSlot->cap); 172 isMove = true; 173 174 break; 175 176 default: 177 assert(0); 178 return EXCEPTION_NONE; 179 } 180 181 if (cap_get_capType(newCap) == cap_null_cap) { 182 userError("CNode Copy/Mint/Move/Mutate: Mutated cap would be invalid."); 183 current_syscall_error.type = seL4_IllegalOperation; 184 return EXCEPTION_SYSCALL_ERROR; 185 } 186 187 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 188 if (isMove) { 189 return invokeCNodeMove(newCap, srcSlot, destSlot); 190 } else { 191 return invokeCNodeInsert(newCap, srcSlot, destSlot); 192 } 193 } 194 195 if (invLabel == CNodeRevoke) { 196 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 197 return invokeCNodeRevoke(destSlot); 198 } 199 200 if (invLabel == CNodeDelete) { 201 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 202 return invokeCNodeDelete(destSlot); 203 } 204 205#ifndef CONFIG_KERNEL_MCS 206 if (invLabel == CNodeSaveCaller) { 207 status = ensureEmptySlot(destSlot); 208 if (status != EXCEPTION_NONE) { 209 userError("CNode SaveCaller: Destination slot not empty."); 210 return status; 211 } 212 213 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 214 return invokeCNodeSaveCaller(destSlot); 215 } 216#endif 217 218 if (invLabel == CNodeCancelBadgedSends) { 219 cap_t destCap; 220 221 destCap = destSlot->cap; 222 223 if (!hasCancelSendRights(destCap)) { 224 userError("CNode CancelBadgedSends: Target cap invalid."); 225 current_syscall_error.type = seL4_IllegalOperation; 226 return EXCEPTION_SYSCALL_ERROR; 227 } 228 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 229 return invokeCNodeCancelBadgedSends(destCap); 230 } 231 232 if (invLabel == CNodeRotate) { 233 word_t pivotNewData, pivotIndex, pivotDepth; 234 word_t srcNewData, srcIndex, srcDepth; 235 cte_t *pivotSlot, *srcSlot; 236 cap_t pivotRoot, srcRoot, newSrcCap, newPivotCap; 237 238 if (length < 8 || excaps.excaprefs[0] == NULL 239 || excaps.excaprefs[1] == NULL) { 240 current_syscall_error.type = seL4_TruncatedMessage; 241 return EXCEPTION_SYSCALL_ERROR; 242 } 243 pivotNewData = getSyscallArg(2, buffer); 244 pivotIndex = getSyscallArg(3, buffer); 245 pivotDepth = getSyscallArg(4, buffer); 246 srcNewData = getSyscallArg(5, buffer); 247 srcIndex = getSyscallArg(6, buffer); 248 srcDepth = getSyscallArg(7, buffer); 249 250 pivotRoot = excaps.excaprefs[0]->cap; 251 srcRoot = excaps.excaprefs[1]->cap; 252 253 lu_ret = lookupSourceSlot(srcRoot, srcIndex, srcDepth); 254 if (lu_ret.status != EXCEPTION_NONE) { 255 return lu_ret.status; 256 } 257 srcSlot = lu_ret.slot; 258 259 lu_ret = lookupPivotSlot(pivotRoot, pivotIndex, pivotDepth); 260 if (lu_ret.status != EXCEPTION_NONE) { 261 return lu_ret.status; 262 } 263 pivotSlot = lu_ret.slot; 264 265 if (pivotSlot == srcSlot || pivotSlot == destSlot) { 266 userError("CNode Rotate: Pivot slot the same as source or dest slot."); 267 current_syscall_error.type = seL4_IllegalOperation; 268 return EXCEPTION_SYSCALL_ERROR; 269 } 270 271 if (srcSlot != destSlot) { 272 status = ensureEmptySlot(destSlot); 273 if (status != EXCEPTION_NONE) { 274 return status; 275 } 276 } 277 278 if (cap_get_capType(srcSlot->cap) == cap_null_cap) { 279 current_syscall_error.type = seL4_FailedLookup; 280 current_syscall_error.failedLookupWasSource = 1; 281 current_lookup_fault = lookup_fault_missing_capability_new(srcDepth); 282 return EXCEPTION_SYSCALL_ERROR; 283 } 284 285 if (cap_get_capType(pivotSlot->cap) == cap_null_cap) { 286 current_syscall_error.type = seL4_FailedLookup; 287 current_syscall_error.failedLookupWasSource = 0; 288 current_lookup_fault = lookup_fault_missing_capability_new(pivotDepth); 289 return EXCEPTION_SYSCALL_ERROR; 290 } 291 292 newSrcCap = updateCapData(true, srcNewData, srcSlot->cap); 293 newPivotCap = updateCapData(true, pivotNewData, pivotSlot->cap); 294 295 if (cap_get_capType(newSrcCap) == cap_null_cap) { 296 userError("CNode Rotate: Source cap invalid."); 297 current_syscall_error.type = seL4_IllegalOperation; 298 return EXCEPTION_SYSCALL_ERROR; 299 } 300 301 if (cap_get_capType(newPivotCap) == cap_null_cap) { 302 userError("CNode Rotate: Pivot cap invalid."); 303 current_syscall_error.type = seL4_IllegalOperation; 304 return EXCEPTION_SYSCALL_ERROR; 305 } 306 307 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart); 308 return invokeCNodeRotate(newSrcCap, newPivotCap, 309 srcSlot, pivotSlot, destSlot); 310 } 311 312 return EXCEPTION_NONE; 313} 314 315exception_t invokeCNodeRevoke(cte_t *destSlot) 316{ 317 return cteRevoke(destSlot); 318} 319 320exception_t invokeCNodeDelete(cte_t *destSlot) 321{ 322 return cteDelete(destSlot, true); 323} 324 325exception_t invokeCNodeCancelBadgedSends(cap_t cap) 326{ 327 word_t badge = cap_endpoint_cap_get_capEPBadge(cap); 328 if (badge) { 329 endpoint_t *ep = (endpoint_t *) 330 cap_endpoint_cap_get_capEPPtr(cap); 331 cancelBadgedSends(ep, badge); 332 } 333 return EXCEPTION_NONE; 334} 335 336exception_t invokeCNodeInsert(cap_t cap, cte_t *srcSlot, cte_t *destSlot) 337{ 338 cteInsert(cap, srcSlot, destSlot); 339 340 return EXCEPTION_NONE; 341} 342 343exception_t invokeCNodeMove(cap_t cap, cte_t *srcSlot, cte_t *destSlot) 344{ 345 cteMove(cap, srcSlot, destSlot); 346 347 return EXCEPTION_NONE; 348} 349 350exception_t invokeCNodeRotate(cap_t cap1, cap_t cap2, cte_t *slot1, 351 cte_t *slot2, cte_t *slot3) 352{ 353 if (slot1 == slot3) { 354 cteSwap(cap1, slot1, cap2, slot2); 355 } else { 356 cteMove(cap2, slot2, slot3); 357 cteMove(cap1, slot1, slot2); 358 } 359 360 return EXCEPTION_NONE; 361} 362 363#ifndef CONFIG_KERNEL_MCS 364exception_t invokeCNodeSaveCaller(cte_t *destSlot) 365{ 366 cap_t cap; 367 cte_t *srcSlot; 368 369 srcSlot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbCaller); 370 cap = srcSlot->cap; 371 372 switch (cap_get_capType(cap)) { 373 case cap_null_cap: 374 userError("CNode SaveCaller: Reply cap not present."); 375 break; 376 377 case cap_reply_cap: 378 if (!cap_reply_cap_get_capReplyMaster(cap)) { 379 cteMove(cap, srcSlot, destSlot); 380 } 381 break; 382 383 default: 384 fail("caller capability must be null or reply"); 385 break; 386 } 387 388 return EXCEPTION_NONE; 389} 390#endif 391 392/* 393 * If creating a child UntypedCap, don't allow new objects to be created in the 394 * parent. 395 */ 396static void setUntypedCapAsFull(cap_t srcCap, cap_t newCap, cte_t *srcSlot) 397{ 398 if ((cap_get_capType(srcCap) == cap_untyped_cap) 399 && (cap_get_capType(newCap) == cap_untyped_cap)) { 400 if ((cap_untyped_cap_get_capPtr(srcCap) 401 == cap_untyped_cap_get_capPtr(newCap)) 402 && (cap_untyped_cap_get_capBlockSize(newCap) 403 == cap_untyped_cap_get_capBlockSize(srcCap))) { 404 cap_untyped_cap_ptr_set_capFreeIndex(&(srcSlot->cap), 405 MAX_FREE_INDEX(cap_untyped_cap_get_capBlockSize(srcCap))); 406 } 407 } 408} 409 410void cteInsert(cap_t newCap, cte_t *srcSlot, cte_t *destSlot) 411{ 412 mdb_node_t srcMDB, newMDB; 413 cap_t srcCap; 414 bool_t newCapIsRevocable; 415 416 srcMDB = srcSlot->cteMDBNode; 417 srcCap = srcSlot->cap; 418 419 newCapIsRevocable = isCapRevocable(newCap, srcCap); 420 421 newMDB = mdb_node_set_mdbPrev(srcMDB, CTE_REF(srcSlot)); 422 newMDB = mdb_node_set_mdbRevocable(newMDB, newCapIsRevocable); 423 newMDB = mdb_node_set_mdbFirstBadged(newMDB, newCapIsRevocable); 424 425 /* Haskell error: "cteInsert to non-empty destination" */ 426 assert(cap_get_capType(destSlot->cap) == cap_null_cap); 427 /* Haskell error: "cteInsert: mdb entry must be empty" */ 428 assert((cte_t *)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && 429 (cte_t *)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL); 430 431 /* Prevent parent untyped cap from being used again if creating a child 432 * untyped from it. */ 433 setUntypedCapAsFull(srcCap, newCap, srcSlot); 434 435 destSlot->cap = newCap; 436 destSlot->cteMDBNode = newMDB; 437 mdb_node_ptr_set_mdbNext(&srcSlot->cteMDBNode, CTE_REF(destSlot)); 438 if (mdb_node_get_mdbNext(newMDB)) { 439 mdb_node_ptr_set_mdbPrev( 440 &CTE_PTR(mdb_node_get_mdbNext(newMDB))->cteMDBNode, 441 CTE_REF(destSlot)); 442 } 443} 444 445void cteMove(cap_t newCap, cte_t *srcSlot, cte_t *destSlot) 446{ 447 mdb_node_t mdb; 448 word_t prev_ptr, next_ptr; 449 450 /* Haskell error: "cteMove to non-empty destination" */ 451 assert(cap_get_capType(destSlot->cap) == cap_null_cap); 452 /* Haskell error: "cteMove: mdb entry must be empty" */ 453 assert((cte_t *)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && 454 (cte_t *)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL); 455 456 mdb = srcSlot->cteMDBNode; 457 destSlot->cap = newCap; 458 srcSlot->cap = cap_null_cap_new(); 459 destSlot->cteMDBNode = mdb; 460 srcSlot->cteMDBNode = nullMDBNode; 461 462 prev_ptr = mdb_node_get_mdbPrev(mdb); 463 if (prev_ptr) 464 mdb_node_ptr_set_mdbNext( 465 &CTE_PTR(prev_ptr)->cteMDBNode, 466 CTE_REF(destSlot)); 467 468 next_ptr = mdb_node_get_mdbNext(mdb); 469 if (next_ptr) 470 mdb_node_ptr_set_mdbPrev( 471 &CTE_PTR(next_ptr)->cteMDBNode, 472 CTE_REF(destSlot)); 473} 474 475void capSwapForDelete(cte_t *slot1, cte_t *slot2) 476{ 477 cap_t cap1, cap2; 478 479 if (slot1 == slot2) { 480 return; 481 } 482 483 cap1 = slot1->cap; 484 cap2 = slot2->cap; 485 486 cteSwap(cap1, slot1, cap2, slot2); 487} 488 489void cteSwap(cap_t cap1, cte_t *slot1, cap_t cap2, cte_t *slot2) 490{ 491 mdb_node_t mdb1, mdb2; 492 word_t next_ptr, prev_ptr; 493 494 slot1->cap = cap2; 495 slot2->cap = cap1; 496 497 mdb1 = slot1->cteMDBNode; 498 499 prev_ptr = mdb_node_get_mdbPrev(mdb1); 500 if (prev_ptr) 501 mdb_node_ptr_set_mdbNext( 502 &CTE_PTR(prev_ptr)->cteMDBNode, 503 CTE_REF(slot2)); 504 505 next_ptr = mdb_node_get_mdbNext(mdb1); 506 if (next_ptr) 507 mdb_node_ptr_set_mdbPrev( 508 &CTE_PTR(next_ptr)->cteMDBNode, 509 CTE_REF(slot2)); 510 511 mdb2 = slot2->cteMDBNode; 512 slot1->cteMDBNode = mdb2; 513 slot2->cteMDBNode = mdb1; 514 515 prev_ptr = mdb_node_get_mdbPrev(mdb2); 516 if (prev_ptr) 517 mdb_node_ptr_set_mdbNext( 518 &CTE_PTR(prev_ptr)->cteMDBNode, 519 CTE_REF(slot1)); 520 521 next_ptr = mdb_node_get_mdbNext(mdb2); 522 if (next_ptr) 523 mdb_node_ptr_set_mdbPrev( 524 &CTE_PTR(next_ptr)->cteMDBNode, 525 CTE_REF(slot1)); 526} 527 528exception_t cteRevoke(cte_t *slot) 529{ 530 cte_t *nextPtr; 531 exception_t status; 532 533 /* there is no need to check for a NullCap as NullCaps are 534 always accompanied by null mdb pointers */ 535 for (nextPtr = CTE_PTR(mdb_node_get_mdbNext(slot->cteMDBNode)); 536 nextPtr && isMDBParentOf(slot, nextPtr); 537 nextPtr = CTE_PTR(mdb_node_get_mdbNext(slot->cteMDBNode))) { 538 status = cteDelete(nextPtr, true); 539 if (status != EXCEPTION_NONE) { 540 return status; 541 } 542 543 status = preemptionPoint(); 544 if (status != EXCEPTION_NONE) { 545 return status; 546 } 547 } 548 549 return EXCEPTION_NONE; 550} 551 552exception_t cteDelete(cte_t *slot, bool_t exposed) 553{ 554 finaliseSlot_ret_t fs_ret; 555 556 fs_ret = finaliseSlot(slot, exposed); 557 if (fs_ret.status != EXCEPTION_NONE) { 558 return fs_ret.status; 559 } 560 561 if (exposed || fs_ret.success) { 562 emptySlot(slot, fs_ret.cleanupInfo); 563 } 564 return EXCEPTION_NONE; 565} 566 567static void emptySlot(cte_t *slot, cap_t cleanupInfo) 568{ 569 if (cap_get_capType(slot->cap) != cap_null_cap) { 570 mdb_node_t mdbNode; 571 cte_t *prev, *next; 572 573 mdbNode = slot->cteMDBNode; 574 prev = CTE_PTR(mdb_node_get_mdbPrev(mdbNode)); 575 next = CTE_PTR(mdb_node_get_mdbNext(mdbNode)); 576 577 if (prev) { 578 mdb_node_ptr_set_mdbNext(&prev->cteMDBNode, CTE_REF(next)); 579 } 580 if (next) { 581 mdb_node_ptr_set_mdbPrev(&next->cteMDBNode, CTE_REF(prev)); 582 } 583 if (next) 584 mdb_node_ptr_set_mdbFirstBadged(&next->cteMDBNode, 585 mdb_node_get_mdbFirstBadged(next->cteMDBNode) || 586 mdb_node_get_mdbFirstBadged(mdbNode)); 587 slot->cap = cap_null_cap_new(); 588 slot->cteMDBNode = nullMDBNode; 589 590 postCapDeletion(cleanupInfo); 591 } 592} 593 594static inline bool_t CONST capRemovable(cap_t cap, cte_t *slot) 595{ 596 switch (cap_get_capType(cap)) { 597 case cap_null_cap: 598 return true; 599 case cap_zombie_cap: { 600 word_t n = cap_zombie_cap_get_capZombieNumber(cap); 601 cte_t *z_slot = (cte_t *)cap_zombie_cap_get_capZombiePtr(cap); 602 return (n == 0 || (n == 1 && slot == z_slot)); 603 } 604 default: 605 fail("finaliseCap should only return Zombie or NullCap"); 606 } 607} 608 609static inline bool_t CONST capCyclicZombie(cap_t cap, cte_t *slot) 610{ 611 return cap_get_capType(cap) == cap_zombie_cap && 612 CTE_PTR(cap_zombie_cap_get_capZombiePtr(cap)) == slot; 613} 614 615static finaliseSlot_ret_t finaliseSlot(cte_t *slot, bool_t immediate) 616{ 617 bool_t final; 618 finaliseCap_ret_t fc_ret; 619 exception_t status; 620 finaliseSlot_ret_t ret; 621 622 while (cap_get_capType(slot->cap) != cap_null_cap) { 623 final = isFinalCapability(slot); 624 fc_ret = finaliseCap(slot->cap, final, false); 625 626 if (capRemovable(fc_ret.remainder, slot)) { 627 ret.status = EXCEPTION_NONE; 628 ret.success = true; 629 ret.cleanupInfo = fc_ret.cleanupInfo; 630 return ret; 631 } 632 633 slot->cap = fc_ret.remainder; 634 635 if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { 636 ret.status = EXCEPTION_NONE; 637 ret.success = false; 638 ret.cleanupInfo = fc_ret.cleanupInfo; 639 return ret; 640 } 641 642 status = reduceZombie(slot, immediate); 643 if (status != EXCEPTION_NONE) { 644 ret.status = status; 645 ret.success = false; 646 ret.cleanupInfo = cap_null_cap_new(); 647 return ret; 648 } 649 650 status = preemptionPoint(); 651 if (status != EXCEPTION_NONE) { 652 ret.status = status; 653 ret.success = false; 654 ret.cleanupInfo = cap_null_cap_new(); 655 return ret; 656 } 657 } 658 ret.status = EXCEPTION_NONE; 659 ret.success = true; 660 ret.cleanupInfo = cap_null_cap_new(); 661 return ret; 662} 663 664static exception_t reduceZombie(cte_t *slot, bool_t immediate) 665{ 666 cte_t *ptr; 667 word_t n, type; 668 exception_t status; 669 670 assert(cap_get_capType(slot->cap) == cap_zombie_cap); 671 ptr = (cte_t *)cap_zombie_cap_get_capZombiePtr(slot->cap); 672 n = cap_zombie_cap_get_capZombieNumber(slot->cap); 673 type = cap_zombie_cap_get_capZombieType(slot->cap); 674 675 /* Haskell error: "reduceZombie: expected unremovable zombie" */ 676 assert(n > 0); 677 678 if (immediate) { 679 cte_t *endSlot = &ptr[n - 1]; 680 681 status = cteDelete(endSlot, false); 682 if (status != EXCEPTION_NONE) { 683 return status; 684 } 685 686 switch (cap_get_capType(slot->cap)) { 687 case cap_null_cap: 688 break; 689 690 case cap_zombie_cap: { 691 cte_t *ptr2 = 692 (cte_t *)cap_zombie_cap_get_capZombiePtr(slot->cap); 693 694 if (ptr == ptr2 && 695 cap_zombie_cap_get_capZombieNumber(slot->cap) == n && 696 cap_zombie_cap_get_capZombieType(slot->cap) == type) { 697 assert(cap_get_capType(endSlot->cap) == cap_null_cap); 698 slot->cap = 699 cap_zombie_cap_set_capZombieNumber(slot->cap, n - 1); 700 } else { 701 /* Haskell error: 702 * "Expected new Zombie to be self-referential." 703 */ 704 assert(ptr2 == slot && ptr != slot); 705 } 706 break; 707 } 708 709 default: 710 fail("Expected recursion to result in Zombie."); 711 } 712 } else { 713 /* Haskell error: "Cyclic zombie passed to unexposed reduceZombie" */ 714 assert(ptr != slot); 715 716 if (cap_get_capType(ptr->cap) == cap_zombie_cap) { 717 /* Haskell error: "Moving self-referential Zombie aside." */ 718 assert(ptr != CTE_PTR(cap_zombie_cap_get_capZombiePtr(ptr->cap))); 719 } 720 721 capSwapForDelete(ptr, slot); 722 } 723 return EXCEPTION_NONE; 724} 725 726void cteDeleteOne(cte_t *slot) 727{ 728 word_t cap_type = cap_get_capType(slot->cap); 729 if (cap_type != cap_null_cap) { 730 bool_t final; 731 finaliseCap_ret_t fc_ret UNUSED; 732 733 /** GHOSTUPD: "(gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = (-1) 734 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = \<acute>cap_type, id)" */ 735 736 final = isFinalCapability(slot); 737 fc_ret = finaliseCap(slot->cap, final, true); 738 /* Haskell error: "cteDeleteOne: cap should be removable" */ 739 assert(capRemovable(fc_ret.remainder, slot) && 740 cap_get_capType(fc_ret.cleanupInfo) == cap_null_cap); 741 emptySlot(slot, cap_null_cap_new()); 742 } 743} 744 745void insertNewCap(cte_t *parent, cte_t *slot, cap_t cap) 746{ 747 cte_t *next; 748 749 next = CTE_PTR(mdb_node_get_mdbNext(parent->cteMDBNode)); 750 slot->cap = cap; 751 slot->cteMDBNode = mdb_node_new(CTE_REF(next), true, true, CTE_REF(parent)); 752 if (next) { 753 mdb_node_ptr_set_mdbPrev(&next->cteMDBNode, CTE_REF(slot)); 754 } 755 mdb_node_ptr_set_mdbNext(&parent->cteMDBNode, CTE_REF(slot)); 756} 757 758#ifndef CONFIG_KERNEL_MCS 759void setupReplyMaster(tcb_t *thread) 760{ 761 cte_t *slot; 762 763 slot = TCB_PTR_CTE_PTR(thread, tcbReply); 764 if (cap_get_capType(slot->cap) == cap_null_cap) { 765 /* Haskell asserts that no reply caps exist for this thread here. This 766 * cannot be translated. */ 767 slot->cap = cap_reply_cap_new(true, true, TCB_REF(thread)); 768 slot->cteMDBNode = nullMDBNode; 769 mdb_node_ptr_set_mdbRevocable(&slot->cteMDBNode, true); 770 mdb_node_ptr_set_mdbFirstBadged(&slot->cteMDBNode, true); 771 } 772} 773#endif 774 775bool_t PURE isMDBParentOf(cte_t *cte_a, cte_t *cte_b) 776{ 777 if (!mdb_node_get_mdbRevocable(cte_a->cteMDBNode)) { 778 return false; 779 } 780 if (!sameRegionAs(cte_a->cap, cte_b->cap)) { 781 return false; 782 } 783 switch (cap_get_capType(cte_a->cap)) { 784 case cap_endpoint_cap: { 785 word_t badge; 786 787 badge = cap_endpoint_cap_get_capEPBadge(cte_a->cap); 788 if (badge == 0) { 789 return true; 790 } 791 return (badge == cap_endpoint_cap_get_capEPBadge(cte_b->cap)) && 792 !mdb_node_get_mdbFirstBadged(cte_b->cteMDBNode); 793 break; 794 } 795 796 case cap_notification_cap: { 797 word_t badge; 798 799 badge = cap_notification_cap_get_capNtfnBadge(cte_a->cap); 800 if (badge == 0) { 801 return true; 802 } 803 return 804 (badge == cap_notification_cap_get_capNtfnBadge(cte_b->cap)) && 805 !mdb_node_get_mdbFirstBadged(cte_b->cteMDBNode); 806 break; 807 } 808 809 default: 810 return true; 811 break; 812 } 813} 814 815exception_t ensureNoChildren(cte_t *slot) 816{ 817 if (mdb_node_get_mdbNext(slot->cteMDBNode) != 0) { 818 cte_t *next; 819 820 next = CTE_PTR(mdb_node_get_mdbNext(slot->cteMDBNode)); 821 if (isMDBParentOf(slot, next)) { 822 current_syscall_error.type = seL4_RevokeFirst; 823 return EXCEPTION_SYSCALL_ERROR; 824 } 825 } 826 827 return EXCEPTION_NONE; 828} 829 830exception_t ensureEmptySlot(cte_t *slot) 831{ 832 if (cap_get_capType(slot->cap) != cap_null_cap) { 833 current_syscall_error.type = seL4_DeleteFirst; 834 return EXCEPTION_SYSCALL_ERROR; 835 } 836 837 return EXCEPTION_NONE; 838} 839 840bool_t PURE isFinalCapability(cte_t *cte) 841{ 842 mdb_node_t mdb; 843 bool_t prevIsSameObject; 844 845 mdb = cte->cteMDBNode; 846 847 if (mdb_node_get_mdbPrev(mdb) == 0) { 848 prevIsSameObject = false; 849 } else { 850 cte_t *prev; 851 852 prev = CTE_PTR(mdb_node_get_mdbPrev(mdb)); 853 prevIsSameObject = sameObjectAs(prev->cap, cte->cap); 854 } 855 856 if (prevIsSameObject) { 857 return false; 858 } else { 859 if (mdb_node_get_mdbNext(mdb) == 0) { 860 return true; 861 } else { 862 cte_t *next; 863 864 next = CTE_PTR(mdb_node_get_mdbNext(mdb)); 865 return !sameObjectAs(cte->cap, next->cap); 866 } 867 } 868} 869 870bool_t PURE slotCapLongRunningDelete(cte_t *slot) 871{ 872 if (cap_get_capType(slot->cap) == cap_null_cap) { 873 return false; 874 } else if (! isFinalCapability(slot)) { 875 return false; 876 } 877 switch (cap_get_capType(slot->cap)) { 878 case cap_thread_cap: 879 case cap_zombie_cap: 880 case cap_cnode_cap: 881 return true; 882 default: 883 return false; 884 } 885} 886 887/* This implementation is specialised to the (current) limit 888 * of one cap receive slot. */ 889cte_t *getReceiveSlots(tcb_t *thread, word_t *buffer) 890{ 891 cap_transfer_t ct; 892 cptr_t cptr; 893 lookupCap_ret_t luc_ret; 894 lookupSlot_ret_t lus_ret; 895 cte_t *slot; 896 cap_t cnode; 897 898 if (!buffer) { 899 return NULL; 900 } 901 902 ct = loadCapTransfer(buffer); 903 cptr = ct.ctReceiveRoot; 904 905 luc_ret = lookupCap(thread, cptr); 906 if (luc_ret.status != EXCEPTION_NONE) { 907 return NULL; 908 } 909 cnode = luc_ret.cap; 910 911 lus_ret = lookupTargetSlot(cnode, ct.ctReceiveIndex, ct.ctReceiveDepth); 912 if (lus_ret.status != EXCEPTION_NONE) { 913 return NULL; 914 } 915 slot = lus_ret.slot; 916 917 if (cap_get_capType(slot->cap) != cap_null_cap) { 918 return NULL; 919 } 920 921 return slot; 922} 923 924cap_transfer_t PURE loadCapTransfer(word_t *buffer) 925{ 926 const int offset = seL4_MsgMaxLength + seL4_MsgMaxExtraCaps + 2; 927 return capTransferFromWords(buffer + offset); 928} 929