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