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