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