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
25 struct finaliseSlot_ret {
26 exception_t status;
27 bool_t success;
28 cap_t cleanupInfo;
29 };
30 typedef struct finaliseSlot_ret finaliseSlot_ret_t;
31
32 static finaliseSlot_ret_t finaliseSlot(cte_t *slot, bool_t exposed);
33 static void emptySlot(cte_t *slot, cap_t cleanupInfo);
34 static 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
decodeCNodeInvocation(word_t invLabel,word_t length,cap_t cap,word_t * buffer)42 exception_t decodeCNodeInvocation(word_t invLabel, word_t length, cap_t cap,
43 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 || current_extra_caps.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 = current_extra_caps.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 || current_extra_caps.excaprefs[0] == NULL
239 || current_extra_caps.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 = current_extra_caps.excaprefs[0]->cap;
251 srcRoot = current_extra_caps.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
invokeCNodeRevoke(cte_t * destSlot)315 exception_t invokeCNodeRevoke(cte_t *destSlot)
316 {
317 return cteRevoke(destSlot);
318 }
319
invokeCNodeDelete(cte_t * destSlot)320 exception_t invokeCNodeDelete(cte_t *destSlot)
321 {
322 return cteDelete(destSlot, true);
323 }
324
invokeCNodeCancelBadgedSends(cap_t cap)325 exception_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
invokeCNodeInsert(cap_t cap,cte_t * srcSlot,cte_t * destSlot)336 exception_t invokeCNodeInsert(cap_t cap, cte_t *srcSlot, cte_t *destSlot)
337 {
338 cteInsert(cap, srcSlot, destSlot);
339
340 return EXCEPTION_NONE;
341 }
342
invokeCNodeMove(cap_t cap,cte_t * srcSlot,cte_t * destSlot)343 exception_t invokeCNodeMove(cap_t cap, cte_t *srcSlot, cte_t *destSlot)
344 {
345 cteMove(cap, srcSlot, destSlot);
346
347 return EXCEPTION_NONE;
348 }
349
invokeCNodeRotate(cap_t cap1,cap_t cap2,cte_t * slot1,cte_t * slot2,cte_t * slot3)350 exception_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
invokeCNodeSaveCaller(cte_t * destSlot)364 exception_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 */
setUntypedCapAsFull(cap_t srcCap,cap_t newCap,cte_t * srcSlot)396 static 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
cteInsert(cap_t newCap,cte_t * srcSlot,cte_t * destSlot)410 void 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
cteMove(cap_t newCap,cte_t * srcSlot,cte_t * destSlot)445 void 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
capSwapForDelete(cte_t * slot1,cte_t * slot2)475 void 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
cteSwap(cap_t cap1,cte_t * slot1,cap_t cap2,cte_t * slot2)489 void 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
cteRevoke(cte_t * slot)528 exception_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
cteDelete(cte_t * slot,bool_t exposed)552 exception_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
emptySlot(cte_t * slot,cap_t cleanupInfo)567 static 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
capRemovable(cap_t cap,cte_t * slot)594 static 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
capCyclicZombie(cap_t cap,cte_t * slot)609 static 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
finaliseSlot(cte_t * slot,bool_t immediate)615 static 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
reduceZombie(cte_t * slot,bool_t immediate)664 static 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
cteDeleteOne(cte_t * slot)726 void 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
insertNewCap(cte_t * parent,cte_t * slot,cap_t cap)745 void 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
setupReplyMaster(tcb_t * thread)759 void 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
isMDBParentOf(cte_t * cte_a,cte_t * cte_b)775 bool_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
ensureNoChildren(cte_t * slot)815 exception_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
ensureEmptySlot(cte_t * slot)830 exception_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
isFinalCapability(cte_t * cte)840 bool_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
slotCapLongRunningDelete(cte_t * slot)870 bool_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. */
getReceiveSlots(tcb_t * thread,word_t * buffer)889 cte_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
loadCapTransfer(word_t * buffer)924 cap_transfer_t PURE loadCapTransfer(word_t *buffer)
925 {
926 const int offset = seL4_MsgMaxLength + seL4_MsgMaxExtraCaps + 2;
927 return capTransferFromWords(buffer + offset);
928 }
929