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 
getObjectSize(word_t t,word_t userObjSize)33 word_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 
deriveCap(cte_t * slot,cap_t cap)62 deriveCap_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 
finaliseCap(cap_t cap,bool_t final,bool_t exposed)104 finaliseCap_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                     cancelIPC(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             sched_context_t *sc = SC_PTR(tcb->tcbSchedContext);
193             if (sc) {
194                 schedContext_unbindTCB(sc, tcb);
195                 if (sc->scYieldFrom) {
196                     schedContext_completeYieldTo(sc->scYieldFrom);
197                 }
198             }
199 #endif
200             suspend(tcb);
201 #ifdef CONFIG_DEBUG_BUILD
202             tcbDebugRemove(tcb);
203 #endif
204             Arch_prepareThreadDelete(tcb);
205             fc_ret.remainder =
206                 Zombie_new(
207                     tcbArchCNodeEntries,
208                     ZombieType_ZombieTCB,
209                     CTE_REF(cte_ptr)
210                 );
211             fc_ret.cleanupInfo = cap_null_cap_new();
212             return fc_ret;
213         }
214         break;
215     }
216 
217 #ifdef CONFIG_KERNEL_MCS
218     case cap_sched_context_cap:
219         if (final) {
220             sched_context_t *sc = SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
221             schedContext_unbindAllTCBs(sc);
222             schedContext_unbindNtfn(sc);
223             if (sc->scReply) {
224                 assert(call_stack_get_isHead(sc->scReply->replyNext));
225                 sc->scReply->replyNext = call_stack_new(0, false);
226                 sc->scReply = NULL;
227             }
228             if (sc->scYieldFrom) {
229                 schedContext_completeYieldTo(sc->scYieldFrom);
230             }
231             /* mark the sc as no longer valid */
232             sc->scRefillMax = 0;
233             fc_ret.remainder = cap_null_cap_new();
234             fc_ret.cleanupInfo = cap_null_cap_new();
235             return fc_ret;
236         }
237         break;
238 #endif
239 
240     case cap_zombie_cap:
241         fc_ret.remainder = cap;
242         fc_ret.cleanupInfo = cap_null_cap_new();
243         return fc_ret;
244 
245     case cap_irq_handler_cap:
246         if (final) {
247             irq_t irq = IDX_TO_IRQT(cap_irq_handler_cap_get_capIRQ(cap));
248 
249             deletingIRQHandler(irq);
250 
251             fc_ret.remainder = cap_null_cap_new();
252             fc_ret.cleanupInfo = cap;
253             return fc_ret;
254         }
255         break;
256     }
257 
258     fc_ret.remainder = cap_null_cap_new();
259     fc_ret.cleanupInfo = cap_null_cap_new();
260     return fc_ret;
261 }
262 
hasCancelSendRights(cap_t cap)263 bool_t CONST hasCancelSendRights(cap_t cap)
264 {
265     switch (cap_get_capType(cap)) {
266     case cap_endpoint_cap:
267         return cap_endpoint_cap_get_capCanSend(cap) &&
268                cap_endpoint_cap_get_capCanReceive(cap) &&
269                cap_endpoint_cap_get_capCanGrantReply(cap) &&
270                cap_endpoint_cap_get_capCanGrant(cap);
271 
272     default:
273         return false;
274     }
275 }
276 
sameRegionAs(cap_t cap_a,cap_t cap_b)277 bool_t CONST sameRegionAs(cap_t cap_a, cap_t cap_b)
278 {
279     switch (cap_get_capType(cap_a)) {
280     case cap_untyped_cap:
281         if (cap_get_capIsPhysical(cap_b)) {
282             word_t aBase, bBase, aTop, bTop;
283 
284             aBase = (word_t)WORD_PTR(cap_untyped_cap_get_capPtr(cap_a));
285             bBase = (word_t)cap_get_capPtr(cap_b);
286 
287             aTop = aBase + MASK(cap_untyped_cap_get_capBlockSize(cap_a));
288             bTop = bBase + MASK(cap_get_capSizeBits(cap_b));
289 
290             return (aBase <= bBase) && (bTop <= aTop) && (bBase <= bTop);
291         }
292         break;
293 
294     case cap_endpoint_cap:
295         if (cap_get_capType(cap_b) == cap_endpoint_cap) {
296             return cap_endpoint_cap_get_capEPPtr(cap_a) ==
297                    cap_endpoint_cap_get_capEPPtr(cap_b);
298         }
299         break;
300 
301     case cap_notification_cap:
302         if (cap_get_capType(cap_b) == cap_notification_cap) {
303             return cap_notification_cap_get_capNtfnPtr(cap_a) ==
304                    cap_notification_cap_get_capNtfnPtr(cap_b);
305         }
306         break;
307 
308     case cap_cnode_cap:
309         if (cap_get_capType(cap_b) == cap_cnode_cap) {
310             return (cap_cnode_cap_get_capCNodePtr(cap_a) ==
311                     cap_cnode_cap_get_capCNodePtr(cap_b)) &&
312                    (cap_cnode_cap_get_capCNodeRadix(cap_a) ==
313                     cap_cnode_cap_get_capCNodeRadix(cap_b));
314         }
315         break;
316 
317     case cap_thread_cap:
318         if (cap_get_capType(cap_b) == cap_thread_cap) {
319             return cap_thread_cap_get_capTCBPtr(cap_a) ==
320                    cap_thread_cap_get_capTCBPtr(cap_b);
321         }
322         break;
323 
324     case cap_reply_cap:
325         if (cap_get_capType(cap_b) == cap_reply_cap) {
326 #ifdef CONFIG_KERNEL_MCS
327             return cap_reply_cap_get_capReplyPtr(cap_a) ==
328                    cap_reply_cap_get_capReplyPtr(cap_b);
329 #else
330             return cap_reply_cap_get_capTCBPtr(cap_a) ==
331                    cap_reply_cap_get_capTCBPtr(cap_b);
332 #endif
333         }
334         break;
335 
336     case cap_domain_cap:
337         if (cap_get_capType(cap_b) == cap_domain_cap) {
338             return true;
339         }
340         break;
341 
342     case cap_irq_control_cap:
343         if (cap_get_capType(cap_b) == cap_irq_control_cap ||
344             cap_get_capType(cap_b) == cap_irq_handler_cap) {
345             return true;
346         }
347         break;
348 
349     case cap_irq_handler_cap:
350         if (cap_get_capType(cap_b) == cap_irq_handler_cap) {
351             return (word_t)cap_irq_handler_cap_get_capIRQ(cap_a) ==
352                    (word_t)cap_irq_handler_cap_get_capIRQ(cap_b);
353         }
354         break;
355 
356 #ifdef CONFIG_KERNEL_MCS
357     case cap_sched_context_cap:
358         if (cap_get_capType(cap_b) == cap_sched_context_cap) {
359             return (cap_sched_context_cap_get_capSCPtr(cap_a) ==
360                     cap_sched_context_cap_get_capSCPtr(cap_b)) &&
361                    (cap_sched_context_cap_get_capSCSizeBits(cap_a) ==
362                     cap_sched_context_cap_get_capSCSizeBits(cap_b));
363         }
364         break;
365     case cap_sched_control_cap:
366         if (cap_get_capType(cap_b) == cap_sched_control_cap) {
367             return true;
368         }
369         break;
370 #endif
371     default:
372         if (isArchCap(cap_a) &&
373             isArchCap(cap_b)) {
374             return Arch_sameRegionAs(cap_a, cap_b);
375         }
376         break;
377     }
378 
379     return false;
380 }
381 
sameObjectAs(cap_t cap_a,cap_t cap_b)382 bool_t CONST sameObjectAs(cap_t cap_a, cap_t cap_b)
383 {
384     if (cap_get_capType(cap_a) == cap_untyped_cap) {
385         return false;
386     }
387     if (cap_get_capType(cap_a) == cap_irq_control_cap &&
388         cap_get_capType(cap_b) == cap_irq_handler_cap) {
389         return false;
390     }
391     if (isArchCap(cap_a) && isArchCap(cap_b)) {
392         return Arch_sameObjectAs(cap_a, cap_b);
393     }
394     return sameRegionAs(cap_a, cap_b);
395 }
396 
updateCapData(bool_t preserve,word_t newData,cap_t cap)397 cap_t CONST updateCapData(bool_t preserve, word_t newData, cap_t cap)
398 {
399     if (isArchCap(cap)) {
400         return Arch_updateCapData(preserve, newData, cap);
401     }
402 
403     switch (cap_get_capType(cap)) {
404     case cap_endpoint_cap:
405         if (!preserve && cap_endpoint_cap_get_capEPBadge(cap) == 0) {
406             return cap_endpoint_cap_set_capEPBadge(cap, newData);
407         } else {
408             return cap_null_cap_new();
409         }
410 
411     case cap_notification_cap:
412         if (!preserve && cap_notification_cap_get_capNtfnBadge(cap) == 0) {
413             return cap_notification_cap_set_capNtfnBadge(cap, newData);
414         } else {
415             return cap_null_cap_new();
416         }
417 
418     case cap_cnode_cap: {
419         word_t guard, guardSize;
420         seL4_CNode_CapData_t w = { .words = { newData } };
421 
422         guardSize = seL4_CNode_CapData_get_guardSize(w);
423 
424         if (guardSize + cap_cnode_cap_get_capCNodeRadix(cap) > wordBits) {
425             return cap_null_cap_new();
426         } else {
427             cap_t new_cap;
428 
429             guard = seL4_CNode_CapData_get_guard(w) & MASK(guardSize);
430             new_cap = cap_cnode_cap_set_capCNodeGuard(cap, guard);
431             new_cap = cap_cnode_cap_set_capCNodeGuardSize(new_cap,
432                                                           guardSize);
433 
434             return new_cap;
435         }
436     }
437 
438     default:
439         return cap;
440     }
441 }
442 
maskCapRights(seL4_CapRights_t cap_rights,cap_t cap)443 cap_t CONST maskCapRights(seL4_CapRights_t cap_rights, cap_t cap)
444 {
445     if (isArchCap(cap)) {
446         return Arch_maskCapRights(cap_rights, cap);
447     }
448 
449     switch (cap_get_capType(cap)) {
450     case cap_null_cap:
451     case cap_domain_cap:
452     case cap_cnode_cap:
453     case cap_untyped_cap:
454     case cap_irq_control_cap:
455     case cap_irq_handler_cap:
456     case cap_zombie_cap:
457     case cap_thread_cap:
458 #ifdef CONFIG_KERNEL_MCS
459     case cap_sched_context_cap:
460     case cap_sched_control_cap:
461 #endif
462         return cap;
463 
464     case cap_endpoint_cap: {
465         cap_t new_cap;
466 
467         new_cap = cap_endpoint_cap_set_capCanSend(
468                       cap, cap_endpoint_cap_get_capCanSend(cap) &
469                       seL4_CapRights_get_capAllowWrite(cap_rights));
470         new_cap = cap_endpoint_cap_set_capCanReceive(
471                       new_cap, cap_endpoint_cap_get_capCanReceive(cap) &
472                       seL4_CapRights_get_capAllowRead(cap_rights));
473         new_cap = cap_endpoint_cap_set_capCanGrant(
474                       new_cap, cap_endpoint_cap_get_capCanGrant(cap) &
475                       seL4_CapRights_get_capAllowGrant(cap_rights));
476         new_cap = cap_endpoint_cap_set_capCanGrantReply(
477                       new_cap, cap_endpoint_cap_get_capCanGrantReply(cap) &
478                       seL4_CapRights_get_capAllowGrantReply(cap_rights));
479 
480         return new_cap;
481     }
482 
483     case cap_notification_cap: {
484         cap_t new_cap;
485 
486         new_cap = cap_notification_cap_set_capNtfnCanSend(
487                       cap, cap_notification_cap_get_capNtfnCanSend(cap) &
488                       seL4_CapRights_get_capAllowWrite(cap_rights));
489         new_cap = cap_notification_cap_set_capNtfnCanReceive(new_cap,
490                                                              cap_notification_cap_get_capNtfnCanReceive(cap) &
491                                                              seL4_CapRights_get_capAllowRead(cap_rights));
492 
493         return new_cap;
494     }
495     case cap_reply_cap: {
496         cap_t new_cap;
497 
498         new_cap = cap_reply_cap_set_capReplyCanGrant(
499                       cap, cap_reply_cap_get_capReplyCanGrant(cap) &
500                       seL4_CapRights_get_capAllowGrant(cap_rights));
501         return new_cap;
502     }
503 
504 
505     default:
506         fail("Invalid cap type"); /* Sentinel for invalid enums */
507     }
508 }
509 
createObject(object_t t,void * regionBase,word_t userSize,bool_t deviceMemory)510 cap_t createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
511 {
512     /* Handle architecture-specific objects. */
513     if (t >= (object_t) seL4_NonArchObjectTypeCount) {
514         return Arch_createObject(t, regionBase, userSize, deviceMemory);
515     }
516 
517     /* Create objects. */
518     switch ((api_object_t)t) {
519     case seL4_TCBObject: {
520         tcb_t *tcb;
521         tcb = TCB_PTR((word_t)regionBase + TCB_OFFSET);
522         /** AUXUPD: "(True, ptr_retyps 1
523           (Ptr ((ptr_val \<acute>tcb) - ctcb_offset) :: (cte_C[5]) ptr)
524             o (ptr_retyp \<acute>tcb))" */
525 
526         /* Setup non-zero parts of the TCB. */
527 
528         Arch_initContext(&tcb->tcbArch.tcbContext);
529 #ifndef CONFIG_KERNEL_MCS
530         tcb->tcbTimeSlice = CONFIG_TIME_SLICE;
531 #endif
532         tcb->tcbDomain = ksCurDomain;
533 #ifndef CONFIG_KERNEL_MCS
534         /* Initialize the new TCB to the current core */
535         SMP_COND_STATEMENT(tcb->tcbAffinity = getCurrentCPUIndex());
536 #endif
537 #ifdef CONFIG_DEBUG_BUILD
538         strlcpy(TCB_PTR_DEBUG_PTR(tcb)->tcbName, "child of: '", TCB_NAME_LENGTH);
539         strlcat(TCB_PTR_DEBUG_PTR(tcb)->tcbName, TCB_PTR_DEBUG_PTR(NODE_STATE(ksCurThread))->tcbName, TCB_NAME_LENGTH);
540         strlcat(TCB_PTR_DEBUG_PTR(tcb)->tcbName, "'", TCB_NAME_LENGTH);
541         tcbDebugAppend(tcb);
542 #endif /* CONFIG_DEBUG_BUILD */
543 
544         return cap_thread_cap_new(TCB_REF(tcb));
545     }
546 
547     case seL4_EndpointObject:
548         /** AUXUPD: "(True, ptr_retyp
549           (Ptr (ptr_val \<acute>regionBase) :: endpoint_C ptr))" */
550         return cap_endpoint_cap_new(0, true, true, true, true,
551                                     EP_REF(regionBase));
552 
553     case seL4_NotificationObject:
554         /** AUXUPD: "(True, ptr_retyp
555               (Ptr (ptr_val \<acute>regionBase) :: notification_C ptr))" */
556         return cap_notification_cap_new(0, true, true,
557                                         NTFN_REF(regionBase));
558 
559     case seL4_CapTableObject:
560         /** AUXUPD: "(True, ptr_arr_retyps (2 ^ (unat \<acute>userSize))
561           (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */
562         /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize)
563                                 (ptr_val \<acute>regionBase)
564                                 (4 + unat \<acute>userSize))" */
565         return cap_cnode_cap_new(userSize, 0, 0, CTE_REF(regionBase));
566 
567     case seL4_UntypedObject:
568         /*
569          * No objects need to be created; instead, just insert caps into
570          * the destination slots.
571          */
572         return cap_untyped_cap_new(0, !!deviceMemory, userSize, WORD_REF(regionBase));
573 
574 #ifdef CONFIG_KERNEL_MCS
575     case seL4_SchedContextObject:
576         memzero(regionBase, BIT(userSize));
577         return cap_sched_context_cap_new(SC_REF(regionBase), userSize);
578 
579     case seL4_ReplyObject:
580         memzero(regionBase, 1UL << seL4_ReplyBits);
581         return cap_reply_cap_new(REPLY_REF(regionBase), true);
582 #endif
583 
584     default:
585         fail("Invalid object type");
586     }
587 }
588 
createNewObjects(object_t t,cte_t * parent,cte_t * destCNode,word_t destOffset,word_t destLength,void * regionBase,word_t userSize,bool_t deviceMemory)589 void createNewObjects(object_t t, cte_t *parent,
590                       cte_t *destCNode, word_t destOffset, word_t destLength,
591                       void *regionBase, word_t userSize, bool_t deviceMemory)
592 {
593     word_t objectSize;
594     void *nextFreeArea;
595     word_t i;
596     word_t totalObjectSize UNUSED;
597 
598     /* ghost check that we're visiting less bytes than the max object size */
599     objectSize = getObjectSize(t, userSize);
600     totalObjectSize = destLength << objectSize;
601     /** GHOSTUPD: "(gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0
602         \<or> \<acute>totalObjectSize <= gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state, id)" */
603 
604     /* Create the objects. */
605     nextFreeArea = regionBase;
606     for (i = 0; i < destLength; i++) {
607         /* Create the object. */
608         /** AUXUPD: "(True, typ_region_bytes (ptr_val \<acute> nextFreeArea + ((\<acute> i) << unat (\<acute> objectSize))) (unat (\<acute> objectSize)))" */
609         cap_t cap = createObject(t, (void *)((word_t)nextFreeArea + (i << objectSize)), userSize, deviceMemory);
610 
611         /* Insert the cap into the user's cspace. */
612         insertNewCap(parent, &destCNode[destOffset + i], cap);
613 
614         /* Move along to the next region of memory. been merged into a formula of i */
615     }
616 }
617 
618 #ifdef CONFIG_KERNEL_MCS
decodeInvocation(word_t invLabel,word_t length,cptr_t capIndex,cte_t * slot,cap_t cap,bool_t block,bool_t call,bool_t canDonate,bool_t firstPhase,word_t * buffer)619 exception_t decodeInvocation(word_t invLabel, word_t length,
620                              cptr_t capIndex, cte_t *slot, cap_t cap,
621                              bool_t block, bool_t call,
622                              bool_t canDonate, bool_t firstPhase, word_t *buffer)
623 #else
624 exception_t decodeInvocation(word_t invLabel, word_t length,
625                              cptr_t capIndex, cte_t *slot, cap_t cap,
626                              bool_t block, bool_t call,
627                              word_t *buffer)
628 #endif
629 {
630     if (isArchCap(cap)) {
631         return Arch_decodeInvocation(invLabel, length, capIndex,
632                                      slot, cap, call, buffer);
633     }
634 
635     switch (cap_get_capType(cap)) {
636     case cap_null_cap:
637         userError("Attempted to invoke a null cap #%lu.", capIndex);
638         current_syscall_error.type = seL4_InvalidCapability;
639         current_syscall_error.invalidCapNumber = 0;
640         return EXCEPTION_SYSCALL_ERROR;
641 
642     case cap_zombie_cap:
643         userError("Attempted to invoke a zombie cap #%lu.", capIndex);
644         current_syscall_error.type = seL4_InvalidCapability;
645         current_syscall_error.invalidCapNumber = 0;
646         return EXCEPTION_SYSCALL_ERROR;
647 
648     case cap_endpoint_cap:
649         if (unlikely(!cap_endpoint_cap_get_capCanSend(cap))) {
650             userError("Attempted to invoke a read-only endpoint cap #%lu.",
651                       capIndex);
652             current_syscall_error.type = seL4_InvalidCapability;
653             current_syscall_error.invalidCapNumber = 0;
654             return EXCEPTION_SYSCALL_ERROR;
655         }
656 
657         setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
658 #ifdef CONFIG_KERNEL_MCS
659         return performInvocation_Endpoint(
660                    EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)),
661                    cap_endpoint_cap_get_capEPBadge(cap),
662                    cap_endpoint_cap_get_capCanGrant(cap),
663                    cap_endpoint_cap_get_capCanGrantReply(cap), block, call, canDonate);
664 #else
665         return performInvocation_Endpoint(
666                    EP_PTR(cap_endpoint_cap_get_capEPPtr(cap)),
667                    cap_endpoint_cap_get_capEPBadge(cap),
668                    cap_endpoint_cap_get_capCanGrant(cap),
669                    cap_endpoint_cap_get_capCanGrantReply(cap), block, call);
670 #endif
671 
672     case cap_notification_cap: {
673         if (unlikely(!cap_notification_cap_get_capNtfnCanSend(cap))) {
674             userError("Attempted to invoke a read-only notification cap #%lu.",
675                       capIndex);
676             current_syscall_error.type = seL4_InvalidCapability;
677             current_syscall_error.invalidCapNumber = 0;
678             return EXCEPTION_SYSCALL_ERROR;
679         }
680 
681         setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
682         return performInvocation_Notification(
683                    NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)),
684                    cap_notification_cap_get_capNtfnBadge(cap));
685     }
686 
687 #ifdef CONFIG_KERNEL_MCS
688     case cap_reply_cap:
689         setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
690         return performInvocation_Reply(
691                    NODE_STATE(ksCurThread),
692                    REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap)),
693                    cap_reply_cap_get_capReplyCanGrant(cap));
694 #else
695     case cap_reply_cap:
696         if (unlikely(cap_reply_cap_get_capReplyMaster(cap))) {
697             userError("Attempted to invoke an invalid reply cap #%lu.",
698                       capIndex);
699             current_syscall_error.type = seL4_InvalidCapability;
700             current_syscall_error.invalidCapNumber = 0;
701             return EXCEPTION_SYSCALL_ERROR;
702         }
703 
704         setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
705         return performInvocation_Reply(
706                    TCB_PTR(cap_reply_cap_get_capTCBPtr(cap)), slot,
707                    cap_reply_cap_get_capReplyCanGrant(cap));
708 
709 #endif
710 
711     case cap_thread_cap:
712 #ifdef CONFIG_KERNEL_MCS
713         if (unlikely(firstPhase)) {
714             userError("Cannot invoke thread capabilities in the first phase of an invocation");
715             current_syscall_error.type = seL4_InvalidCapability;
716             current_syscall_error.invalidCapNumber = 0;
717             return EXCEPTION_SYSCALL_ERROR;
718         }
719 #endif
720         return decodeTCBInvocation(invLabel, length, cap, slot, call, buffer);
721 
722     case cap_domain_cap:
723 #ifdef CONFIG_KERNEL_MCS
724         if (unlikely(firstPhase)) {
725             userError("Cannot invoke domain capabilities in the first phase of an invocation");
726             current_syscall_error.type = seL4_InvalidCapability;
727             current_syscall_error.invalidCapNumber = 0;
728             return EXCEPTION_SYSCALL_ERROR;
729         }
730 #endif
731         return decodeDomainInvocation(invLabel, length, buffer);
732 
733     case cap_cnode_cap:
734 #ifdef CONFIG_KERNEL_MCS
735         if (unlikely(firstPhase)) {
736             userError("Cannot invoke cnode capabilities in the first phase of an invocation");
737             current_syscall_error.type = seL4_InvalidCapability;
738             current_syscall_error.invalidCapNumber = 0;
739             return EXCEPTION_SYSCALL_ERROR;
740         }
741 #endif
742         return decodeCNodeInvocation(invLabel, length, cap, buffer);
743 
744     case cap_untyped_cap:
745         return decodeUntypedInvocation(invLabel, length, slot, cap, call, buffer);
746 
747     case cap_irq_control_cap:
748         return decodeIRQControlInvocation(invLabel, length, slot, buffer);
749 
750     case cap_irq_handler_cap:
751         return decodeIRQHandlerInvocation(invLabel,
752                                           IDX_TO_IRQT(cap_irq_handler_cap_get_capIRQ(cap)));
753 
754 #ifdef CONFIG_KERNEL_MCS
755     case cap_sched_control_cap:
756         if (unlikely(firstPhase)) {
757             userError("Cannot invoke sched control capabilities in the first phase of an invocation");
758             current_syscall_error.type = seL4_InvalidCapability;
759             current_syscall_error.invalidCapNumber = 0;
760             return EXCEPTION_SYSCALL_ERROR;
761         }
762         return decodeSchedControlInvocation(invLabel, cap, length, buffer);
763 
764     case cap_sched_context_cap:
765         if (unlikely(firstPhase)) {
766             userError("Cannot invoke sched context capabilities in the first phase of an invocation");
767             current_syscall_error.type = seL4_InvalidCapability;
768             current_syscall_error.invalidCapNumber = 0;
769             return EXCEPTION_SYSCALL_ERROR;
770         }
771         return decodeSchedContextInvocation(invLabel, cap, buffer);
772 #endif
773     default:
774         fail("Invalid cap type");
775     }
776 }
777 
778 #ifdef CONFIG_KERNEL_MCS
performInvocation_Endpoint(endpoint_t * ep,word_t badge,bool_t canGrant,bool_t canGrantReply,bool_t block,bool_t call,bool_t canDonate)779 exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
780                                        bool_t canGrant, bool_t canGrantReply,
781                                        bool_t block, bool_t call, bool_t canDonate)
782 {
783     sendIPC(block, call, badge, canGrant, canGrantReply, canDonate, NODE_STATE(ksCurThread), ep);
784 
785     return EXCEPTION_NONE;
786 }
787 #else
performInvocation_Endpoint(endpoint_t * ep,word_t badge,bool_t canGrant,bool_t canGrantReply,bool_t block,bool_t call)788 exception_t performInvocation_Endpoint(endpoint_t *ep, word_t badge,
789                                        bool_t canGrant, bool_t canGrantReply,
790                                        bool_t block, bool_t call)
791 {
792     sendIPC(block, call, badge, canGrant, canGrantReply, NODE_STATE(ksCurThread), ep);
793 
794     return EXCEPTION_NONE;
795 }
796 #endif
797 
performInvocation_Notification(notification_t * ntfn,word_t badge)798 exception_t performInvocation_Notification(notification_t *ntfn, word_t badge)
799 {
800     sendSignal(ntfn, badge);
801 
802     return EXCEPTION_NONE;
803 }
804 
805 #ifdef CONFIG_KERNEL_MCS
performInvocation_Reply(tcb_t * thread,reply_t * reply,bool_t canGrant)806 exception_t performInvocation_Reply(tcb_t *thread, reply_t *reply, bool_t canGrant)
807 {
808     doReplyTransfer(thread, reply, canGrant);
809     return EXCEPTION_NONE;
810 }
811 #else
performInvocation_Reply(tcb_t * thread,cte_t * slot,bool_t canGrant)812 exception_t performInvocation_Reply(tcb_t *thread, cte_t *slot, bool_t canGrant)
813 {
814     doReplyTransfer(NODE_STATE(ksCurThread), thread, slot, canGrant);
815     return EXCEPTION_NONE;
816 }
817 #endif
818 
cap_get_capSizeBits(cap_t cap)819 word_t CONST cap_get_capSizeBits(cap_t cap)
820 {
821 
822     cap_tag_t ctag;
823 
824     ctag = cap_get_capType(cap);
825 
826     switch (ctag) {
827     case cap_untyped_cap:
828         return cap_untyped_cap_get_capBlockSize(cap);
829 
830     case cap_endpoint_cap:
831         return seL4_EndpointBits;
832 
833     case cap_notification_cap:
834         return seL4_NotificationBits;
835 
836     case cap_cnode_cap:
837         return cap_cnode_cap_get_capCNodeRadix(cap) + seL4_SlotBits;
838 
839     case cap_thread_cap:
840         return seL4_TCBBits;
841 
842     case cap_zombie_cap: {
843         word_t type = cap_zombie_cap_get_capZombieType(cap);
844         if (type == ZombieType_ZombieTCB) {
845             return seL4_TCBBits;
846         }
847         return ZombieType_ZombieCNode(type) + seL4_SlotBits;
848     }
849 
850     case cap_null_cap:
851         return 0;
852 
853     case cap_domain_cap:
854         return 0;
855 
856     case cap_reply_cap:
857 #ifdef CONFIG_KERNEL_MCS
858         return seL4_ReplyBits;
859 #else
860         return 0;
861 #endif
862 
863     case cap_irq_control_cap:
864 #ifdef CONFIG_KERNEL_MCS
865     case cap_sched_control_cap:
866 #endif
867         return 0;
868 
869     case cap_irq_handler_cap:
870         return 0;
871 
872 #ifdef CONFIG_KERNEL_MCS
873     case cap_sched_context_cap:
874         return cap_sched_context_cap_get_capSCSizeBits(cap);
875 #endif
876 
877     default:
878         return cap_get_archCapSizeBits(cap);
879     }
880 
881 }
882 
883 /* Returns whether or not this capability has memory associated
884  * with it or not. Referring to this as 'being physical' is to
885  * match up with the Haskell and abstract specifications */
cap_get_capIsPhysical(cap_t cap)886 bool_t CONST cap_get_capIsPhysical(cap_t cap)
887 {
888     cap_tag_t ctag;
889 
890     ctag = cap_get_capType(cap);
891 
892     switch (ctag) {
893     case cap_untyped_cap:
894         return true;
895 
896     case cap_endpoint_cap:
897         return true;
898 
899     case cap_notification_cap:
900         return true;
901 
902     case cap_cnode_cap:
903         return true;
904 
905     case cap_thread_cap:
906 #ifdef CONFIG_KERNEL_MCS
907     case cap_sched_context_cap:
908 #endif
909         return true;
910 
911     case cap_zombie_cap:
912         return true;
913 
914     case cap_domain_cap:
915         return false;
916 
917     case cap_reply_cap:
918 #ifdef CONFIG_KERNEL_MCS
919         return true;
920 #else
921         return false;
922 #endif
923 
924     case cap_irq_control_cap:
925 #ifdef CONFIG_KERNEL_MCS
926     case cap_sched_control_cap:
927 #endif
928         return false;
929 
930     case cap_irq_handler_cap:
931         return false;
932 
933     default:
934         return cap_get_archCapIsPhysical(cap);
935     }
936 }
937 
cap_get_capPtr(cap_t cap)938 void *CONST cap_get_capPtr(cap_t cap)
939 {
940     cap_tag_t ctag;
941 
942     ctag = cap_get_capType(cap);
943 
944     switch (ctag) {
945     case cap_untyped_cap:
946         return WORD_PTR(cap_untyped_cap_get_capPtr(cap));
947 
948     case cap_endpoint_cap:
949         return EP_PTR(cap_endpoint_cap_get_capEPPtr(cap));
950 
951     case cap_notification_cap:
952         return NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap));
953 
954     case cap_cnode_cap:
955         return CTE_PTR(cap_cnode_cap_get_capCNodePtr(cap));
956 
957     case cap_thread_cap:
958         return TCB_PTR_CTE_PTR(cap_thread_cap_get_capTCBPtr(cap), 0);
959 
960     case cap_zombie_cap:
961         return CTE_PTR(cap_zombie_cap_get_capZombiePtr(cap));
962 
963     case cap_domain_cap:
964         return NULL;
965 
966     case cap_reply_cap:
967 #ifdef CONFIG_KERNEL_MCS
968         return REPLY_PTR(cap_reply_cap_get_capReplyPtr(cap));
969 #else
970         return NULL;
971 #endif
972 
973     case cap_irq_control_cap:
974 #ifdef CONFIG_KERNEL_MCS
975     case cap_sched_control_cap:
976 #endif
977         return NULL;
978 
979     case cap_irq_handler_cap:
980         return NULL;
981 
982 #ifdef CONFIG_KERNEL_MCS
983     case cap_sched_context_cap:
984         return SC_PTR(cap_sched_context_cap_get_capSCPtr(cap));
985 #endif
986 
987     default:
988         return cap_get_archCapPtr(cap);
989 
990     }
991 }
992 
isCapRevocable(cap_t derivedCap,cap_t srcCap)993 bool_t CONST isCapRevocable(cap_t derivedCap, cap_t srcCap)
994 {
995     if (isArchCap(derivedCap)) {
996         return Arch_isCapRevocable(derivedCap, srcCap);
997     }
998     switch (cap_get_capType(derivedCap)) {
999     case cap_endpoint_cap:
1000         return (cap_endpoint_cap_get_capEPBadge(derivedCap) !=
1001                 cap_endpoint_cap_get_capEPBadge(srcCap));
1002 
1003     case cap_notification_cap:
1004         return (cap_notification_cap_get_capNtfnBadge(derivedCap) !=
1005                 cap_notification_cap_get_capNtfnBadge(srcCap));
1006 
1007     case cap_irq_handler_cap:
1008         return (cap_get_capType(srcCap) ==
1009                 cap_irq_control_cap);
1010 
1011     case cap_untyped_cap:
1012         return true;
1013 
1014     default:
1015         return false;
1016     }
1017 }
1018