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