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 <config.h>
13#include <types.h>
14#include <api/failures.h>
15#include <api/syscall.h>
16#include <arch/object/objecttype.h>
17#include <machine/io.h>
18#include <object/objecttype.h>
19#include <object/structures.h>
20#include <object/notification.h>
21#include <object/endpoint.h>
22#include <object/cnode.h>
23#include <object/interrupt.h>
24#include <object/schedcontext.h>
25#include <object/schedcontrol.h>
26#include <object/tcb.h>
27#include <object/untyped.h>
28#include <model/statedata.h>
29#include <kernel/thread.h>
30#include <kernel/vspace.h>
31#include <machine.h>
32#include <util.h>
33#include <string.h>
34
35word_t getObjectSize(word_t t, word_t userObjSize)
36{
37    if (t >= seL4_NonArchObjectTypeCount) {
38        return Arch_getObjectSize(t);
39    } else {
40        switch (t) {
41        case seL4_TCBObject:
42            return seL4_TCBBits;
43        case seL4_EndpointObject:
44            return seL4_EndpointBits;
45        case seL4_NotificationObject:
46            return seL4_NotificationBits;
47        case seL4_CapTableObject:
48            return seL4_SlotBits + userObjSize;
49        case seL4_UntypedObject:
50            return userObjSize;
51        case seL4_SchedContextObject:
52            return userObjSize;
53        case seL4_ReplyObject:
54            return seL4_ReplyBits;
55        default:
56            fail("Invalid object type");
57            return 0;
58        }
59    }
60}
61
62deriveCap_ret_t
63deriveCap(cte_t *slot, cap_t cap)
64{
65    deriveCap_ret_t ret;
66
67    if (isArchCap(cap)) {
68        return Arch_deriveCap(slot, cap);
69    }
70
71    switch (cap_get_capType(cap)) {
72    case cap_zombie_cap:
73        ret.status = EXCEPTION_NONE;
74        ret.cap = cap_null_cap_new();
75        break;
76
77    case cap_irq_control_cap:
78        ret.status = EXCEPTION_NONE;
79        ret.cap = cap_null_cap_new();
80        break;
81
82    case cap_untyped_cap:
83        ret.status = ensureNoChildren(slot);
84        if (ret.status != EXCEPTION_NONE) {
85            ret.cap = cap_null_cap_new();
86        } else {
87            ret.cap = cap;
88        }
89        break;
90
91    default:
92        ret.status = EXCEPTION_NONE;
93        ret.cap = cap;
94    }
95
96    return ret;
97}
98
99finaliseCap_ret_t
100finaliseCap(cap_t cap, bool_t final, bool_t exposed)
101{
102    finaliseCap_ret_t fc_ret;
103
104    if (isArchCap(cap)) {
105        return Arch_finaliseCap(cap, final);
106    }
107
108    switch (cap_get_capType(cap)) {
109    case cap_endpoint_cap:
110        if (final) {
111            cancelAllIPC(EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)));
112        }
113
114        fc_ret.remainder = cap_null_cap_new();
115        fc_ret.cleanupInfo = cap_null_cap_new();
116        return fc_ret;
117
118    case cap_notification_cap:
119        if (final) {
120            notification_t *ntfn = NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap));
121            schedContext_unbindNtfn(SC_PTR(notification_ptr_get_ntfnSchedContext(ntfn)));
122            unbindMaybeNotification(ntfn);
123            cancelAllSignals(ntfn);
124        }
125        fc_ret.remainder = cap_null_cap_new();
126        fc_ret.cleanupInfo = cap_null_cap_new();
127        return fc_ret;
128
129    case cap_reply_cap:
130        if (final) {
131            reply_t *reply = REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap));
132            if (reply && reply->replyTCB) {
133                cancelIPC(reply->replyTCB);
134            }
135        }
136        fc_ret.remainder = cap_null_cap_new();
137        fc_ret.cleanupInfo = cap_null_cap_new();
138        return fc_ret;
139
140    case cap_null_cap:
141    case cap_domain_cap:
142        fc_ret.remainder = cap_null_cap_new();
143        fc_ret.cleanupInfo = cap_null_cap_new();
144        return fc_ret;
145    }
146
147    if (exposed) {
148        fail("finaliseCap: failed to finalise immediately.");
149    }
150
151    switch (cap_get_capType(cap)) {
152    case cap_cnode_cap: {
153        if (final) {
154            fc_ret.remainder =
155                Zombie_new(
156                    1ul << cap_cnode_cap_get_capCNodeRadix(cap),
157                    cap_cnode_cap_get_capCNodeRadix(cap),
158                    cap_cnode_cap_get_capCNodePtr(cap)
159                );
160            fc_ret.cleanupInfo = cap_null_cap_new();
161            return fc_ret;
162        }
163        break;
164    }
165
166    case cap_thread_cap: {
167        if (final) {
168            tcb_t *tcb;
169            cte_t *cte_ptr;
170
171            tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(cap));
172            SMP_COND_STATEMENT(remoteTCBStall(tcb));
173            cte_ptr = TCB_PTR_CTE_PTR(tcb, tcbCTable);
174            unbindNotification(tcb);
175            if (tcb->tcbSchedContext) {
176                schedContext_completeYieldTo(tcb->tcbSchedContext->scYieldFrom);
177                schedContext_unbindTCB(tcb->tcbSchedContext, tcb);
178            }
179            suspend(tcb);
180#ifdef CONFIG_DEBUG_BUILD
181            tcbDebugRemove(tcb);
182#endif
183            Arch_prepareThreadDelete(tcb);
184            fc_ret.remainder =
185                Zombie_new(
186                    tcbArchCNodeEntries,
187                    ZombieType_ZombieTCB,
188                    CTE_REF(cte_ptr)
189                );
190            fc_ret.cleanupInfo = cap_null_cap_new();
191            return fc_ret;
192        }
193        break;
194    }
195
196    case cap_sched_context_cap:
197        if (final) {
198            sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
199            schedContext_unbindAllTCBs(sc);
200            schedContext_unbindNtfn(sc);
201            if (sc->scReply) {
202                assert(call_stack_get_isHead(sc->scReply->replyNext));
203                sc->scReply->replyNext = call_stack_new(0, false);
204                sc->scReply = NULL;
205            }
206            if (sc->scYieldFrom) {
207                schedContext_completeYieldTo(sc->scYieldFrom);
208            }
209            fc_ret.remainder = cap_null_cap_new();
210            fc_ret.cleanupInfo = cap_null_cap_new();
211            return fc_ret;
212        }
213        break;
214
215    case cap_zombie_cap:
216        fc_ret.remainder = cap;
217        fc_ret.cleanupInfo = cap_null_cap_new();
218        return fc_ret;
219
220    case cap_irq_handler_cap:
221        if (final) {
222            irq_t irq = cap_irq_handler_cap_get_capIRQ(cap);
223
224            deletingIRQHandler(irq);
225
226            fc_ret.remainder = cap_null_cap_new();
227            fc_ret.cleanupInfo = cap;
228            return fc_ret;
229        }
230        break;
231    }
232
233    fc_ret.remainder = cap_null_cap_new();
234    fc_ret.cleanupInfo = cap_null_cap_new();
235    return fc_ret;
236}
237
238bool_t CONST
239hasCancelSendRights(cap_t cap)
240{
241    switch (cap_get_capType(cap)) {
242    case cap_endpoint_cap:
243        return cap_endpoint_cap_get_capCanSend(cap) &&
244               cap_endpoint_cap_get_capCanReceive(cap) &&
245               cap_endpoint_cap_get_capCanGrant(cap);
246
247    default:
248        return false;
249    }
250}
251
252bool_t CONST
253sameRegionAs(cap_t cap_a, cap_t cap_b)
254{
255    switch (cap_get_capType(cap_a)) {
256    case cap_untyped_cap:
257        if (cap_get_capIsPhysical(cap_b)) {
258            word_t aBase, bBase, aTop, bTop;
259
260            aBase = (word_t)WORD_PTR(cap_untyped_cap_get_capPtr(cap_a));
261            bBase = (word_t)cap_get_capPtr(cap_b);
262
263            aTop = aBase + MASK(cap_untyped_cap_get_capBlockSize(cap_a));
264            bTop = bBase + MASK(cap_get_capSizeBits(cap_b));
265
266            return (aBase <= bBase) && (bTop <= aTop) && (bBase <= bTop);
267        }
268        break;
269
270    case cap_endpoint_cap:
271        if (cap_get_capType(cap_b) == cap_endpoint_cap) {
272            return cap_endpoint_cap_get_capEPPtr(cap_a) ==
273                   cap_endpoint_cap_get_capEPPtr(cap_b);
274        }
275        break;
276
277    case cap_notification_cap:
278        if (cap_get_capType(cap_b) == cap_notification_cap) {
279            return cap_notification_cap_get_capNtfnPtr(cap_a) ==
280                   cap_notification_cap_get_capNtfnPtr(cap_b);
281        }
282        break;
283
284    case cap_cnode_cap:
285        if (cap_get_capType(cap_b) == cap_cnode_cap) {
286            return (cap_cnode_cap_get_capCNodePtr(cap_a) ==
287                    cap_cnode_cap_get_capCNodePtr(cap_b)) &&
288                   (cap_cnode_cap_get_capCNodeRadix(cap_a) ==
289                    cap_cnode_cap_get_capCNodeRadix(cap_b));
290        }
291        break;
292
293    case cap_thread_cap:
294        if (cap_get_capType(cap_b) == cap_thread_cap) {
295            return cap_thread_cap_get_capTCBPtr(cap_a) ==
296                   cap_thread_cap_get_capTCBPtr(cap_b);
297        }
298        break;
299
300    case cap_reply_cap:
301        if (cap_get_capType(cap_b) == cap_reply_cap) {
302            return cap_reply_cap_get_capReplyPtr(cap_a) ==
303                   cap_reply_cap_get_capReplyPtr(cap_b);
304        }
305        break;
306
307    case cap_domain_cap:
308        if (cap_get_capType(cap_b) == cap_domain_cap) {
309            return true;
310        }
311        break;
312
313    case cap_irq_control_cap:
314        if (cap_get_capType(cap_b) == cap_irq_control_cap ||
315                cap_get_capType(cap_b) == cap_irq_handler_cap) {
316            return true;
317        }
318        break;
319
320    case cap_irq_handler_cap:
321        if (cap_get_capType(cap_b) == cap_irq_handler_cap) {
322            return (irq_t)cap_irq_handler_cap_get_capIRQ(cap_a) ==
323                   (irq_t)cap_irq_handler_cap_get_capIRQ(cap_b);
324        }
325        break;
326
327    case cap_sched_context_cap:
328        if (cap_get_capType(cap_b) == cap_sched_context_cap) {
329            return cap_sched_context_cap_get_capSCPtr(cap_a) ==
330                   cap_sched_context_cap_get_capSCPtr(cap_b);
331        }
332        break;
333    case cap_sched_control_cap:
334        if (cap_get_capType(cap_b) == cap_sched_control_cap) {
335            return true;
336        }
337        break;
338    default:
339        if (isArchCap(cap_a) &&
340                isArchCap(cap_b)) {
341            return Arch_sameRegionAs(cap_a, cap_b);
342        }
343        break;
344    }
345
346    return false;
347}
348
349bool_t CONST
350sameObjectAs(cap_t cap_a, cap_t cap_b)
351{
352    if (cap_get_capType(cap_a) == cap_untyped_cap) {
353        return false;
354    }
355    if (cap_get_capType(cap_a) == cap_irq_control_cap &&
356            cap_get_capType(cap_b) == cap_irq_handler_cap) {
357        return false;
358    }
359    if (isArchCap(cap_a) && isArchCap(cap_b)) {
360        return Arch_sameObjectAs(cap_a, cap_b);
361    }
362    return sameRegionAs(cap_a, cap_b);
363}
364
365cap_t CONST
366updateCapData(bool_t preserve, word_t newData, cap_t cap)
367{
368    if (isArchCap(cap)) {
369        return Arch_updateCapData(preserve, newData, cap);
370    }
371
372    switch (cap_get_capType(cap)) {
373    case cap_endpoint_cap:
374        if (!preserve && cap_endpoint_cap_get_capEPBadge(cap) == 0) {
375            return cap_endpoint_cap_set_capEPBadge(cap, newData);
376        } else {
377            return cap_null_cap_new();
378        }
379
380    case cap_notification_cap:
381        if (!preserve && cap_notification_cap_get_capNtfnBadge(cap) == 0) {
382            return cap_notification_cap_set_capNtfnBadge(cap, newData);
383        } else {
384            return cap_null_cap_new();
385        }
386
387    case cap_cnode_cap: {
388        word_t guard, guardSize;
389        seL4_CNode_CapData_t w = { .words = { newData } };
390
391        guardSize = seL4_CNode_CapData_get_guardSize(w);
392
393        if (guardSize + cap_cnode_cap_get_capCNodeRadix(cap) > wordBits) {
394            return cap_null_cap_new();
395        } else {
396            cap_t new_cap;
397
398            guard = seL4_CNode_CapData_get_guard(w) & MASK(guardSize);
399            new_cap = cap_cnode_cap_set_capCNodeGuard(cap, guard);
400            new_cap = cap_cnode_cap_set_capCNodeGuardSize(new_cap,
401                                                          guardSize);
402
403            return new_cap;
404        }
405    }
406
407    default:
408        return cap;
409    }
410}
411
412cap_t CONST
413maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
414{
415    if (isArchCap(cap)) {
416        return Arch_maskCapRights(cap_rights, cap);
417    }
418
419    switch (cap_get_capType(cap)) {
420    case cap_null_cap:
421    case cap_domain_cap:
422    case cap_cnode_cap:
423    case cap_untyped_cap:
424    case cap_reply_cap:
425    case cap_irq_control_cap:
426    case cap_irq_handler_cap:
427    case cap_zombie_cap:
428    case cap_thread_cap:
429    case cap_sched_context_cap:
430    case cap_sched_control_cap:
431        return cap;
432
433    case cap_endpoint_cap: {
434        cap_t new_cap;
435
436        new_cap = cap_endpoint_cap_set_capCanSend(
437                      cap, cap_endpoint_cap_get_capCanSend(cap) &
438                      seL4_CapRights_get_capAllowWrite(cap_rights));
439        new_cap = cap_endpoint_cap_set_capCanReceive(
440                      new_cap, cap_endpoint_cap_get_capCanReceive(cap) &
441                      seL4_CapRights_get_capAllowRead(cap_rights));
442        new_cap = cap_endpoint_cap_set_capCanGrant(
443                      new_cap, cap_endpoint_cap_get_capCanGrant(cap) &
444                      seL4_CapRights_get_capAllowGrant(cap_rights));
445
446        return new_cap;
447    }
448
449    case cap_notification_cap: {
450        cap_t new_cap;
451
452        new_cap = cap_notification_cap_set_capNtfnCanSend(
453                      cap, cap_notification_cap_get_capNtfnCanSend(cap) &
454                      seL4_CapRights_get_capAllowWrite(cap_rights));
455        new_cap = cap_notification_cap_set_capNtfnCanReceive(new_cap,
456                                                             cap_notification_cap_get_capNtfnCanReceive(cap) &
457                                                             seL4_CapRights_get_capAllowRead(cap_rights));
458
459        return new_cap;
460    }
461
462    default:
463        fail("Invalid cap type"); /* Sentinel for invalid enums */
464    }
465}
466
467cap_t
468createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
469{
470    /* Handle architecture-specific objects. */
471    if (t >= (object_t) seL4_NonArchObjectTypeCount) {
472        return Arch_createObject(t, regionBase, userSize, deviceMemory);
473    }
474
475    /* Create objects. */
476    switch ((api_object_t)t) {
477    case seL4_TCBObject: {
478        tcb_t *tcb;
479        tcb = TCB_PTR((word_t)regionBase + TCB_OFFSET);
480        /** AUXUPD: "(True, ptr_retyps 1
481          (Ptr ((ptr_val \<acute>tcb) - ctcb_offset) :: (cte_C[5]) ptr)
482            o (ptr_retyp \<acute>tcb))" */
483
484        /* Setup non-zero parts of the TCB. */
485
486        Arch_initContext(&tcb->tcbArch.tcbContext);
487        tcb->tcbDomain = ksCurDomain;
488
489#ifdef CONFIG_DEBUG_BUILD
490        strlcpy(tcb->tcbName, "child of: '", TCB_NAME_LENGTH);
491        strlcat(tcb->tcbName, NODE_STATE(ksCurThread)->tcbName, TCB_NAME_LENGTH);
492        strlcat(tcb->tcbName, "'", TCB_NAME_LENGTH);
493        tcbDebugAppend(tcb);
494#endif /* CONFIG_DEBUG_BUILD */
495
496        return cap_thread_cap_new(TCB_REF(tcb));
497    }
498
499    case seL4_EndpointObject:
500        /** AUXUPD: "(True, ptr_retyp
501          (Ptr (ptr_val \<acute>regionBase) :: endpoint_C ptr))" */
502        return cap_endpoint_cap_new(0, true, true, true,
503                                    EP_REF(regionBase));
504
505    case seL4_NotificationObject:
506        /** AUXUPD: "(True, ptr_retyp
507              (Ptr (ptr_val \<acute>regionBase) :: notification_C ptr))" */
508        return cap_notification_cap_new(0, true, true,
509                                        NTFN_REF(regionBase));
510
511    case seL4_CapTableObject:
512        /** AUXUPD: "(True, ptr_arr_retyps (2 ^ (unat \<acute>userSize))
513          (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */
514        /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize)
515                                (ptr_val \<acute>regionBase)
516                                (4 + unat \<acute>userSize))" */
517        return cap_cnode_cap_new(userSize, 0, 0, CTE_REF(regionBase));
518
519    case seL4_UntypedObject:
520        /*
521         * No objects need to be created; instead, just insert caps into
522         * the destination slots.
523         */
524        return cap_untyped_cap_new(0, !!deviceMemory, userSize, WORD_REF(regionBase));
525
526    case seL4_SchedContextObject:
527        memzero(regionBase, BIT(userSize));
528        return cap_sched_context_cap_new(SC_REF(regionBase), userSize);
529
530    case seL4_ReplyObject:
531        memzero(regionBase, 1UL << seL4_ReplyBits);
532        return cap_reply_cap_new(REPLY_REF(regionBase));
533
534    default:
535        fail("Invalid object type");
536    }
537}
538
539void
540createNewObjects(object_t t, cte_t *parent, slot_range_t slots,
541                 void *regionBase, word_t userSize, bool_t deviceMemory)
542{
543    word_t objectSize;
544    void *nextFreeArea;
545    word_t i;
546    word_t totalObjectSize UNUSED;
547
548    /* ghost check that we're visiting less bytes than the max object size */
549    objectSize = getObjectSize(t, userSize);
550    totalObjectSize = slots.length << objectSize;
551    /** GHOSTUPD: "(gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0
552        \<or> \<acute>totalObjectSize <= gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state, id)" */
553
554    /* Create the objects. */
555    nextFreeArea = regionBase;
556    for (i = 0; i < slots.length; i++) {
557        /* Create the object. */
558        /** AUXUPD: "(True, typ_region_bytes (ptr_val \<acute> nextFreeArea + ((\<acute> i) << unat (\<acute> objectSize))) (unat (\<acute> objectSize)))" */
559        cap_t cap = createObject(t, (void *)((word_t)nextFreeArea + (i << objectSize)), userSize, deviceMemory);
560
561        /* Insert the cap into the user's cspace. */
562        insertNewCap(parent, &slots.cnode[slots.offset + i], cap);
563
564        /* Move along to the next region of memory. been merged into a formula of i */
565    }
566}
567
568exception_t
569decodeInvocation(word_t invLabel, word_t length,
570                 cptr_t capIndex, cte_t *slot, cap_t cap,
571                 extra_caps_t excaps, bool_t block, bool_t call,
572                 bool_t canDonate, word_t *buffer)
573{
574    if (isArchCap(cap)) {
575        return Arch_decodeInvocation(invLabel, length, capIndex,
576                                     slot, cap, excaps, call, buffer);
577    }
578
579    switch (cap_get_capType(cap)) {
580    case cap_null_cap:
581        userError("Attempted to invoke a null cap #%lu.", capIndex);
582        current_syscall_error.type = seL4_InvalidCapability;
583        current_syscall_error.invalidCapNumber = 0;
584        return EXCEPTION_SYSCALL_ERROR;
585
586    case cap_zombie_cap:
587        userError("Attempted to invoke a zombie cap #%lu.", capIndex);
588        current_syscall_error.type = seL4_InvalidCapability;
589        current_syscall_error.invalidCapNumber = 0;
590        return EXCEPTION_SYSCALL_ERROR;
591
592    case cap_endpoint_cap:
593        if (unlikely(!cap_endpoint_cap_get_capCanSend(cap))) {
594            userError("Attempted to invoke a read-only endpoint cap #%lu.",
595                      capIndex);
596            current_syscall_error.type = seL4_InvalidCapability;
597            current_syscall_error.invalidCapNumber = 0;
598            return EXCEPTION_SYSCALL_ERROR;
599        }
600
601        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
602        return performInvocation_Endpoint(
603                   EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)),
604                   cap_endpoint_cap_get_capEPBadge(cap),
605                   cap_endpoint_cap_get_capCanGrant(cap), block, call, canDonate);
606
607    case cap_notification_cap: {
608        if (unlikely(!cap_notification_cap_get_capNtfnCanSend(cap))) {
609            userError("Attempted to invoke a read-only notification cap #%lu.",
610                      capIndex);
611            current_syscall_error.type = seL4_InvalidCapability;
612            current_syscall_error.invalidCapNumber = 0;
613            return EXCEPTION_SYSCALL_ERROR;
614        }
615
616        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
617        return performInvocation_Notification(
618                   NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)),
619                   cap_notification_cap_get_capNtfnBadge(cap));
620    }
621
622    case cap_reply_cap:
623        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
624        return performInvocation_Reply(NODE_STATE(ksCurThread), REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap)));
625
626    case cap_thread_cap:
627        return decodeTCBInvocation(invLabel, length, cap,
628                                   slot, excaps, call, buffer);
629
630    case cap_domain_cap:
631        return decodeDomainInvocation(invLabel, length, excaps, buffer);
632
633    case cap_cnode_cap:
634        return decodeCNodeInvocation(invLabel, length, cap, excaps, buffer);
635
636    case cap_untyped_cap:
637        return decodeUntypedInvocation(invLabel, length, slot, cap, excaps,
638                                       call, buffer);
639
640    case cap_irq_control_cap:
641        return decodeIRQControlInvocation(invLabel, length, slot,
642                                          excaps, buffer);
643
644    case cap_irq_handler_cap:
645        return decodeIRQHandlerInvocation(invLabel,
646                                          cap_irq_handler_cap_get_capIRQ(cap), excaps);
647
648    case cap_sched_control_cap:
649        return decodeSchedControlInvocation(invLabel, cap, length, excaps, buffer);
650
651    case cap_sched_context_cap:
652        return decodeSchedContextInvocation(invLabel, cap, excaps, buffer);
653    default:
654        fail("Invalid cap type");
655    }
656}
657
658exception_t
659performInvocation_Endpoint(endpoint_t *ep, word_t badge,
660                           bool_t canGrant, bool_t block,
661                           bool_t call, bool_t canDonate)
662{
663    sendIPC(block, call, badge, canGrant, canDonate, NODE_STATE(ksCurThread), ep);
664
665    return EXCEPTION_NONE;
666}
667
668exception_t
669performInvocation_Notification(notification_t *ntfn, word_t badge)
670{
671    sendSignal(ntfn, badge);
672
673    return EXCEPTION_NONE;
674}
675
676exception_t
677performInvocation_Reply(tcb_t *sender, reply_t *reply)
678{
679    doReplyTransfer(sender, reply);
680    return EXCEPTION_NONE;
681}
682