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 <config.h>
12#include <types.h>
13#include <api/failures.h>
14#include <kernel/vspace.h>
15#include <object/structures.h>
16#include <arch/machine.h>
17#include <arch/model/statedata.h>
18#include <arch/object/objecttype.h>
19#include <arch/machine/tlb.h>
20#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
21#include <arch/object/vcpu.h>
22#endif
23
24bool_t
25Arch_isFrameType(word_t type)
26{
27    switch (type) {
28    case seL4_ARM_SmallPageObject:
29        return true;
30    case seL4_ARM_LargePageObject:
31        return true;
32    case seL4_ARM_SectionObject:
33        return true;
34    case seL4_ARM_SuperSectionObject:
35        return true;
36    default:
37        return false;
38    }
39}
40
41deriveCap_ret_t
42Arch_deriveCap(cte_t *slot, cap_t cap)
43{
44    deriveCap_ret_t ret;
45
46    switch (cap_get_capType(cap)) {
47    case cap_page_table_cap:
48        if (cap_page_table_cap_get_capPTIsMapped(cap)) {
49            ret.cap = cap;
50            ret.status = EXCEPTION_NONE;
51        } else {
52            userError("Deriving an unmapped PT cap");
53            current_syscall_error.type = seL4_IllegalOperation;
54            ret.cap = cap_null_cap_new();
55            ret.status = EXCEPTION_SYSCALL_ERROR;
56        }
57        return ret;
58
59    case cap_page_directory_cap:
60        if (cap_page_directory_cap_get_capPDIsMapped(cap)) {
61            ret.cap = cap;
62            ret.status = EXCEPTION_NONE;
63        } else {
64            userError("Deriving a PD cap without an assigned ASID");
65            current_syscall_error.type = seL4_IllegalOperation;
66            ret.cap = cap_null_cap_new();
67            ret.status = EXCEPTION_SYSCALL_ERROR;
68        }
69        return ret;
70
71    /* This is a deviation from haskell, which has only
72     * one frame cap type on ARM */
73    case cap_small_frame_cap:
74        ret.cap = cap_small_frame_cap_set_capFMappedASID(cap, asidInvalid);
75        ret.status = EXCEPTION_NONE;
76        return ret;
77
78    case cap_frame_cap:
79        ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid);
80        ret.status = EXCEPTION_NONE;
81        return ret;
82
83    case cap_asid_control_cap:
84    case cap_asid_pool_cap:
85        ret.cap = cap;
86        ret.status = EXCEPTION_NONE;
87        return ret;
88
89#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
90    case cap_vcpu_cap:
91        ret.cap = cap;
92        ret.status = EXCEPTION_NONE;
93        return ret;
94#endif
95
96#ifdef CONFIG_ARM_SMMU
97    case cap_io_space_cap:
98        ret.cap = cap;
99        ret.status = EXCEPTION_NONE;
100        return ret;
101
102    case cap_io_page_table_cap:
103        if (cap_io_page_table_cap_get_capIOPTIsMapped(cap)) {
104            ret.cap = cap;
105            ret.status = EXCEPTION_NONE;
106        } else {
107            userError("Deriving a IOPT cap without an assigned IOASID");
108            current_syscall_error.type = seL4_IllegalOperation;
109            ret.cap = cap_null_cap_new();
110            ret.status = EXCEPTION_SYSCALL_ERROR;
111        }
112        return ret;
113#endif
114    default:
115        /* This assert has no equivalent in haskell,
116         * as the options are restricted by type */
117        fail("Invalid arch cap");
118    }
119}
120
121cap_t CONST
122Arch_updateCapData(bool_t preserve, word_t data, cap_t cap)
123{
124    return cap;
125}
126
127cap_t CONST
128Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap)
129{
130    if (cap_get_capType(cap) == cap_small_frame_cap) {
131        vm_rights_t vm_rights;
132
133        vm_rights = vmRightsFromWord(
134                        cap_small_frame_cap_get_capFVMRights(cap));
135        vm_rights = maskVMRights(vm_rights, cap_rights_mask);
136        return cap_small_frame_cap_set_capFVMRights(cap,
137                                                    wordFromVMRights(vm_rights));
138    } else if (cap_get_capType(cap) == cap_frame_cap) {
139        vm_rights_t vm_rights;
140
141        vm_rights = vmRightsFromWord(
142                        cap_frame_cap_get_capFVMRights(cap));
143        vm_rights = maskVMRights(vm_rights, cap_rights_mask);
144        return cap_frame_cap_set_capFVMRights(cap,
145                                              wordFromVMRights(vm_rights));
146    } else {
147        return cap;
148    }
149}
150
151finaliseCap_ret_t
152Arch_finaliseCap(cap_t cap, bool_t final)
153{
154    finaliseCap_ret_t fc_ret;
155
156    switch (cap_get_capType(cap)) {
157    case cap_asid_pool_cap:
158        if (final) {
159            deleteASIDPool(cap_asid_pool_cap_get_capASIDBase(cap),
160                           ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap)));
161        }
162        break;
163
164    case cap_page_directory_cap:
165        if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) {
166            deleteASID(cap_page_directory_cap_get_capPDMappedASID(cap),
167                       PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(cap)));
168        }
169        break;
170
171    case cap_page_table_cap:
172        if (final && cap_page_table_cap_get_capPTIsMapped(cap)) {
173            unmapPageTable(
174                cap_page_table_cap_get_capPTMappedASID(cap),
175                cap_page_table_cap_get_capPTMappedAddress(cap),
176                PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap)));
177        }
178        break;
179
180    case cap_small_frame_cap:
181        if (cap_small_frame_cap_get_capFMappedASID(cap)) {
182#ifdef CONFIG_ARM_SMMU
183            if (isIOSpaceFrameCap(cap)) {
184                unmapIOPage(cap);
185                break;
186            }
187#endif
188
189            unmapPage(ARMSmallPage,
190                      cap_small_frame_cap_get_capFMappedASID(cap),
191                      cap_small_frame_cap_get_capFMappedAddress(cap),
192                      (void *)cap_small_frame_cap_get_capFBasePtr(cap));
193        }
194        break;
195
196    case cap_frame_cap:
197        if (cap_frame_cap_get_capFMappedASID(cap)) {
198#ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER
199            /* If the last cap to the user-level log buffer frame is being revoked,
200             * reset the ksLog so that the kernel doesn't log anymore
201             */
202            if (unlikely(cap_frame_cap_get_capFSize(cap) == ARMSection)) {
203                if (pptr_to_paddr((void *)cap_frame_cap_get_capFBasePtr(cap)) == ksUserLogBuffer) {
204                    ksUserLogBuffer = 0;
205
206                    /* Invalidate log page table entries */
207                    clearMemory((void *) armKSGlobalLogPT, BIT(seL4_PageTableBits));
208
209                    cleanCacheRange_PoU((pptr_t) &armKSGlobalLogPT[0],
210                                        (pptr_t) &armKSGlobalLogPT[0] + BIT(seL4_PageTableBits),
211                                        addrFromPPtr((void *)&armKSGlobalLogPT[0]));
212
213                    for (int idx = 0; idx < BIT(PT_INDEX_BITS); idx++) {
214                        invalidateTranslationSingle(KS_LOG_PPTR + (idx << seL4_PageBits));
215                    }
216
217                    userError("Log buffer frame is invalidated, kernel can't benchmark anymore");
218                }
219            }
220#endif /* CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER */
221
222            unmapPage(cap_frame_cap_get_capFSize(cap),
223                      cap_frame_cap_get_capFMappedASID(cap),
224                      cap_frame_cap_get_capFMappedAddress(cap),
225                      (void *)cap_frame_cap_get_capFBasePtr(cap));
226        }
227        break;
228
229#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
230    case cap_vcpu_cap:
231        if (final) {
232            vcpu_finalise(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap)));
233        }
234        break;
235#endif
236
237#ifdef CONFIG_ARM_SMMU
238    case cap_io_space_cap:
239        if (final) {
240            clearIOPageDirectory(cap);
241        }
242        break;
243
244    case cap_io_page_table_cap:
245        if (final && cap_io_page_table_cap_get_capIOPTIsMapped(cap)) {
246            deleteIOPageTable(cap);
247        }
248        break;
249#endif
250
251    default:
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
261Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
262{
263    switch (cap_get_capType(cap_a)) {
264    case cap_small_frame_cap:
265    case cap_frame_cap:
266        if (cap_get_capType(cap_b) == cap_small_frame_cap ||
267                cap_get_capType(cap_b) == cap_frame_cap) {
268            word_t botA, botB, topA, topB;
269            botA = generic_frame_cap_get_capFBasePtr(cap_a);
270            botB = generic_frame_cap_get_capFBasePtr(cap_b);
271            topA = botA + MASK (pageBitsForSize(generic_frame_cap_get_capFSize(cap_a)));
272            topB = botB + MASK (pageBitsForSize(generic_frame_cap_get_capFSize(cap_b))) ;
273            return ((botA <= botB) && (topA >= topB) && (botB <= topB));
274        }
275        break;
276
277    case cap_page_table_cap:
278        if (cap_get_capType(cap_b) == cap_page_table_cap) {
279            return cap_page_table_cap_get_capPTBasePtr(cap_a) ==
280                   cap_page_table_cap_get_capPTBasePtr(cap_b);
281        }
282        break;
283
284    case cap_page_directory_cap:
285        if (cap_get_capType(cap_b) == cap_page_directory_cap) {
286            return cap_page_directory_cap_get_capPDBasePtr(cap_a) ==
287                   cap_page_directory_cap_get_capPDBasePtr(cap_b);
288        }
289        break;
290
291    case cap_asid_control_cap:
292        if (cap_get_capType(cap_b) == cap_asid_control_cap) {
293            return true;
294        }
295        break;
296
297    case cap_asid_pool_cap:
298        if (cap_get_capType(cap_b) == cap_asid_pool_cap) {
299            return cap_asid_pool_cap_get_capASIDPool(cap_a) ==
300                   cap_asid_pool_cap_get_capASIDPool(cap_b);
301        }
302        break;
303
304#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
305    case cap_vcpu_cap:
306        if (cap_get_capType(cap_b) == cap_vcpu_cap) {
307            return cap_vcpu_cap_get_capVCPUPtr(cap_a) ==
308                   cap_vcpu_cap_get_capVCPUPtr(cap_b);
309        }
310        break;
311#endif
312
313#ifdef CONFIG_ARM_SMMU
314    case cap_io_space_cap:
315        if (cap_get_capType(cap_b) == cap_io_space_cap) {
316            return cap_io_space_cap_get_capModuleID(cap_a) ==
317                   cap_io_space_cap_get_capModuleID(cap_b);
318        }
319        break;
320
321    case cap_io_page_table_cap:
322        if (cap_get_capType(cap_b) == cap_io_page_table_cap) {
323            return cap_io_page_table_cap_get_capIOPTBasePtr(cap_a) ==
324                   cap_io_page_table_cap_get_capIOPTBasePtr(cap_b);
325        }
326        break;
327#endif
328    }
329
330    return false;
331}
332
333bool_t CONST
334Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
335{
336    if (cap_get_capType(cap_a) == cap_small_frame_cap) {
337        if (cap_get_capType(cap_b) == cap_small_frame_cap) {
338            return ((cap_small_frame_cap_get_capFBasePtr(cap_a) ==
339                     cap_small_frame_cap_get_capFBasePtr(cap_b)) &&
340                    ((cap_small_frame_cap_get_capFIsDevice(cap_a) == 0) ==
341                     (cap_small_frame_cap_get_capFIsDevice(cap_b) == 0)));
342        } else if (cap_get_capType(cap_b) == cap_frame_cap) {
343            return false;
344        }
345    }
346    if (cap_get_capType(cap_a) == cap_frame_cap) {
347        if (cap_get_capType(cap_b) == cap_frame_cap) {
348            return ((cap_frame_cap_get_capFBasePtr(cap_a) ==
349                     cap_frame_cap_get_capFBasePtr(cap_b)) &&
350                    (cap_frame_cap_get_capFSize(cap_a) ==
351                     cap_frame_cap_get_capFSize(cap_b)) &&
352                    ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) ==
353                     (cap_frame_cap_get_capFIsDevice(cap_b) == 0)));
354        } else if (cap_get_capType(cap_b) == cap_small_frame_cap) {
355            return false;
356        }
357    }
358    return Arch_sameRegionAs(cap_a, cap_b);
359}
360
361word_t
362Arch_getObjectSize(word_t t)
363{
364    switch (t) {
365    case seL4_ARM_SmallPageObject:
366        return ARMSmallPageBits;
367    case seL4_ARM_LargePageObject:
368        return ARMLargePageBits;
369    case seL4_ARM_SectionObject:
370        return ARMSectionBits;
371    case seL4_ARM_SuperSectionObject:
372        return ARMSuperSectionBits;
373    case seL4_ARM_PageTableObject:
374        return PTE_SIZE_BITS + PT_INDEX_BITS;
375    case seL4_ARM_PageDirectoryObject:
376        return PDE_SIZE_BITS + PD_INDEX_BITS;
377#ifdef CONFIG_ARM_SMMU
378    case seL4_ARM_IOPageTableObject:
379        return seL4_IOPageTableBits;
380#endif
381#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
382    case seL4_ARM_VCPUObject:
383        return VCPU_SIZE_BITS;
384#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
385    default:
386        fail("Invalid object type");
387        return 0;
388    }
389}
390
391cap_t
392Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
393{
394    switch (t) {
395    case seL4_ARM_SmallPageObject:
396        if (deviceMemory) {
397            /** AUXUPD: "(True, ptr_retyps 1
398                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
399            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSmallPage
400                                                    (ptr_val \<acute>regionBase)
401                                                    (unat ARMSmallPageBits))" */
402        } else {
403            /** AUXUPD: "(True, ptr_retyps 1
404                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
405            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSmallPage
406                                                    (ptr_val \<acute>regionBase)
407                                                    (unat ARMSmallPageBits))" */
408        }
409        return cap_small_frame_cap_new(
410                   ASID_LOW(asidInvalid), VMReadWrite,
411                   0, !!deviceMemory,
412#ifdef CONFIG_ARM_SMMU
413                   0,
414#endif
415                   ASID_HIGH(asidInvalid),
416                   (word_t)regionBase);
417
418    case seL4_ARM_LargePageObject:
419        if (deviceMemory) {
420            /** AUXUPD: "(True, ptr_retyps 16
421                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
422            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMLargePage
423                                                    (ptr_val \<acute>regionBase)
424                                                    (unat ARMLargePageBits))" */
425        } else {
426            /** AUXUPD: "(True, ptr_retyps 16
427                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
428            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMLargePage
429                                                    (ptr_val \<acute>regionBase)
430                                                    (unat ARMLargePageBits))" */
431        }
432        return cap_frame_cap_new(
433                   ARMLargePage, ASID_LOW(asidInvalid), VMReadWrite,
434                   0, !!deviceMemory, ASID_HIGH(asidInvalid),
435                   (word_t)regionBase);
436
437    case seL4_ARM_SectionObject:
438        if (deviceMemory) {
439#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
440            /** AUXUPD: "(True, ptr_retyps 512
441                 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
442#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
443            /** AUXUPD: "(True, ptr_retyps 256
444                 (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
445#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
446            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSection
447                                            (ptr_val \<acute>regionBase)
448                                            (unat ARMSectionBits))" */
449        } else {
450#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
451            /** AUXUPD: "(True, ptr_retyps 512
452                 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
453#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
454            /** AUXUPD: "(True, ptr_retyps 256
455                 (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
456#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
457            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSection
458                                            (ptr_val \<acute>regionBase)
459                                            (unat ARMSectionBits))" */
460        }
461        return cap_frame_cap_new(
462                   ARMSection, ASID_LOW(asidInvalid), VMReadWrite,
463                   0, !!deviceMemory, ASID_HIGH(asidInvalid),
464                   (word_t)regionBase);
465
466    case seL4_ARM_SuperSectionObject:
467        if (deviceMemory) {
468#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
469            /** AUXUPD: "(True, ptr_retyps 8192
470                    (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
471#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
472            /** AUXUPD: "(True, ptr_retyps 4096
473                    (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
474#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
475            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSuperSection
476                                                (ptr_val \<acute>regionBase)
477                                                (unat ARMSuperSectionBits))" */
478        } else {
479#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
480            /** AUXUPD: "(True, ptr_retyps 8192
481                    (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
482#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
483            /** AUXUPD: "(True, ptr_retyps 4096
484                    (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
485#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
486            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.ARMSuperSection
487                                                (ptr_val \<acute>regionBase)
488                                                (unat ARMSuperSectionBits))" */
489        }
490        return cap_frame_cap_new(
491                   ARMSuperSection, ASID_LOW(asidInvalid), VMReadWrite,
492                   0, !!deviceMemory, ASID_HIGH(asidInvalid),
493                   (word_t)regionBase);
494
495    case seL4_ARM_PageTableObject:
496#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
497        /** AUXUPD: "(True, ptr_retyps 1
498              (Ptr (ptr_val \<acute>regionBase) :: (pte_C[512]) ptr))" */
499#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
500        /** AUXUPD: "(True, ptr_retyps 1
501              (Ptr (ptr_val \<acute>regionBase) :: (pte_C[256]) ptr))" */
502#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
503
504        return cap_page_table_cap_new(false, asidInvalid, 0,
505                                      (word_t)regionBase);
506
507    case seL4_ARM_PageDirectoryObject:
508#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
509        /** AUXUPD: "(True, ptr_retyps 1
510              (Ptr (ptr_val \<acute>regionBase) :: (pde_C[2048]) ptr))" */
511#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
512        /** AUXUPD: "(True, ptr_retyps 1
513              (Ptr (ptr_val \<acute>regionBase) :: (pde_C[4096]) ptr))" */
514#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
515        copyGlobalMappings((pde_t *)regionBase);
516        cleanCacheRange_PoU((word_t)regionBase,
517                            (word_t)regionBase + (1 << (PD_INDEX_BITS + PDE_SIZE_BITS)) - 1,
518                            addrFromPPtr(regionBase));
519
520        return cap_page_directory_cap_new(false, asidInvalid,
521                                          (word_t)regionBase);
522#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
523    case seL4_ARM_VCPUObject:
524        /** AUXUPD: "(True, ptr_retyp
525          (Ptr (ptr_val \<acute>regionBase) :: vcpu_C ptr))" */
526        vcpu_init(VCPU_PTR(regionBase));
527        return cap_vcpu_cap_new(VCPU_REF(regionBase));
528#endif
529
530#ifdef CONFIG_ARM_SMMU
531    case seL4_ARM_IOPageTableObject:
532        /* When the untyped was zeroed it was cleaned to the PoU, but the SMMUs
533         * typically pull directly from RAM, so we do a futher clean to RAM here */
534        cleanCacheRange_RAM((word_t)regionBase,
535                            (word_t)regionBase + (1 << seL4_IOPageTableBits) - 1,
536                            addrFromPPtr(regionBase));
537        return cap_io_page_table_cap_new(0, asidInvalid, (word_t)regionBase, 0);
538#endif
539    default:
540        /*
541         * This is a conflation of the haskell error: "Arch.createNewCaps
542         * got an API type" and the case where an invalid object type is
543         * passed (which is impossible in haskell).
544         */
545        fail("Arch_createObject got an API type or invalid object type");
546    }
547}
548
549exception_t
550Arch_decodeInvocation(word_t invLabel, word_t length, cptr_t cptr,
551                      cte_t *slot, cap_t cap, extra_caps_t excaps,
552                      bool_t call, word_t *buffer)
553{
554    /* The C parser cannot handle a switch statement with only a default
555     * case. So we need to do some gymnastics to remove the switch if
556     * there are no other cases */
557#if defined(CONFIG_ARM_SMMU) || defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
558    switch (cap_get_capType(cap)) {
559#ifdef CONFIG_ARM_SMMU
560    case cap_io_space_cap:
561        return decodeARMIOSpaceInvocation(invLabel, cap);
562    case cap_io_page_table_cap:
563        return decodeARMIOPTInvocation(invLabel, length, slot, cap, excaps, buffer);
564#endif
565#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
566    case cap_vcpu_cap:
567        return decodeARMVCPUInvocation(invLabel, length, cptr, slot, cap, excaps, call, buffer);
568#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */
569    default:
570#else
571{
572#endif
573    return decodeARMMMUInvocation(invLabel, length, cptr, slot, cap, excaps, buffer);
574}
575}
576
577void
578Arch_prepareThreadDelete(tcb_t * thread) {
579#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
580    if (thread->tcbArch.tcbVCPU) {
581        dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread);
582    }
583#else  /* CONFIG_ARM_HYPERVISOR_SUPPORT */
584    /* No action required on ARM. */
585#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
586}
587
588