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