1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <config.h>
8#include <types.h>
9#include <api/failures.h>
10#include <kernel/vspace.h>
11#include <object/structures.h>
12#include <arch/machine.h>
13#include <arch/model/statedata.h>
14#include <arch/object/objecttype.h>
15
16bool_t Arch_isFrameType(word_t type)
17{
18    switch (type) {
19    case seL4_ARM_SmallPageObject:
20        return true;
21    case seL4_ARM_LargePageObject:
22        return true;
23    case seL4_ARM_HugePageObject:
24        return true;
25    default:
26        return false;
27    }
28}
29
30deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap)
31{
32    deriveCap_ret_t ret;
33
34    switch (cap_get_capType(cap)) {
35    case cap_page_global_directory_cap:
36        if (cap_page_global_directory_cap_get_capPGDIsMapped(cap)) {
37            ret.cap = cap;
38            ret.status = EXCEPTION_NONE;
39        } else {
40            userError("Deriving a PDG cap without an assigned ASID");
41            current_syscall_error.type = seL4_IllegalOperation;
42            ret.cap = cap_null_cap_new();
43            ret.status = EXCEPTION_SYSCALL_ERROR;
44        }
45        return ret;
46
47    case cap_page_upper_directory_cap:
48        if (cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) {
49            ret.cap = cap;
50            ret.status = EXCEPTION_NONE;
51        } else {
52            userError("Deriving a PUD cap without an assigned ASID");
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    case cap_page_table_cap:
72        if (cap_page_table_cap_get_capPTIsMapped(cap)) {
73            ret.cap = cap;
74            ret.status = EXCEPTION_NONE;
75        } else {
76            userError("Deriving a PT cap without an assigned ASID");
77            current_syscall_error.type = seL4_IllegalOperation;
78            ret.cap = cap_null_cap_new();
79            ret.status = EXCEPTION_SYSCALL_ERROR;
80        }
81        return ret;
82
83    case cap_frame_cap:
84        ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid);
85        ret.status = EXCEPTION_NONE;
86        return ret;
87
88    case cap_asid_control_cap:
89    case cap_asid_pool_cap:
90        ret.cap = cap;
91        ret.status = EXCEPTION_NONE;
92        return ret;
93
94#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
95    case cap_vcpu_cap:
96        ret.cap = cap;
97        ret.status = EXCEPTION_NONE;
98        return ret;
99#endif
100#ifdef CONFIG_ARM_SMMU
101    case cap_sid_control_cap:
102    case cap_cb_control_cap:
103        ret.cap = cap_null_cap_new();
104        ret.status = EXCEPTION_NONE;
105        return ret;
106    case cap_sid_cap:
107    case cap_cb_cap:
108        ret.cap = cap;
109        ret.status = EXCEPTION_NONE;
110        return ret;
111#endif
112    default:
113        /* This assert has no equivalent in haskell,
114         * as the options are restricted by type */
115        fail("Invalid arch cap");
116    }
117}
118
119cap_t CONST Arch_updateCapData(bool_t preserve, word_t data, cap_t cap)
120{
121    return cap;
122}
123
124cap_t CONST Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap)
125{
126    if (cap_get_capType(cap) == cap_frame_cap) {
127        vm_rights_t vm_rights;
128
129        vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap));
130        vm_rights = maskVMRights(vm_rights, cap_rights_mask);
131
132        return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights));
133    } else {
134        return cap;
135    }
136}
137
138finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final)
139{
140    finaliseCap_ret_t fc_ret;
141
142    switch (cap_get_capType(cap)) {
143    case cap_asid_pool_cap:
144        if (final) {
145            deleteASIDPool(cap_asid_pool_cap_get_capASIDBase(cap),
146                           ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap)));
147        }
148        break;
149
150    case cap_page_global_directory_cap:
151#ifdef CONFIG_ARM_SMMU
152        if (cap_page_global_directory_cap_get_capPGDMappedCB(cap) != CB_INVALID) {
153            smmu_cb_delete_vspace(cap_page_global_directory_cap_get_capPGDMappedCB(cap),
154                                  cap_page_global_directory_cap_get_capPGDMappedASID(cap));
155        }
156#endif
157        if (final && cap_page_global_directory_cap_get_capPGDIsMapped(cap)) {
158            deleteASID(cap_page_global_directory_cap_get_capPGDMappedASID(cap),
159                       VSPACE_PTR(cap_page_global_directory_cap_get_capPGDBasePtr(cap)));
160        }
161        break;
162
163    case cap_page_upper_directory_cap:
164#ifdef AARCH64_VSPACE_S2_START_L1
165#ifdef CONFIG_ARM_SMMU
166        if (cap_page_upper_directory_cap_get_capPGDMappedCB(cap) != CB_INVALID) {
167            smmu_cb_delete_vspace(cap_page_upper_directory_cap_get_capPUDMappedCB(cap),
168                                  cap_page_upper_directory_cap_get_capPUDMappedASID(cap));
169        }
170#endif
171        if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) {
172            deleteASID(cap_page_upper_directory_cap_get_capPUDMappedASID(cap),
173                       PUDE_PTR(cap_page_upper_directory_cap_get_capPUDBasePtr(cap)));
174        }
175#else
176        if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) {
177            unmapPageUpperDirectory(cap_page_upper_directory_cap_get_capPUDMappedASID(cap),
178                                    cap_page_upper_directory_cap_get_capPUDMappedAddress(cap),
179                                    PUDE_PTR(cap_page_upper_directory_cap_get_capPUDBasePtr(cap)));
180        }
181
182#endif
183        break;
184
185    case cap_page_directory_cap:
186        if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) {
187            unmapPageDirectory(cap_page_directory_cap_get_capPDMappedASID(cap),
188                               cap_page_directory_cap_get_capPDMappedAddress(cap),
189                               PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(cap)));
190        }
191        break;
192
193    case cap_page_table_cap:
194        if (final && cap_page_table_cap_get_capPTIsMapped(cap)) {
195            unmapPageTable(cap_page_table_cap_get_capPTMappedASID(cap),
196                           cap_page_table_cap_get_capPTMappedAddress(cap),
197                           PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap)));
198        }
199        break;
200
201    case cap_frame_cap:
202        if (cap_frame_cap_get_capFMappedASID(cap)) {
203            unmapPage(cap_frame_cap_get_capFSize(cap),
204                      cap_frame_cap_get_capFMappedASID(cap),
205                      cap_frame_cap_get_capFMappedAddress(cap),
206                      cap_frame_cap_get_capFBasePtr(cap));
207        }
208        break;
209#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
210    case cap_vcpu_cap:
211        if (final) {
212            vcpu_finalise(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap)));
213        }
214        break;
215#endif
216#ifdef CONFIG_ARM_SMMU
217    case cap_cb_cap:
218        if (cap_cb_cap_get_capBindSID(cap) != SID_INVALID) {
219            smmu_sid_unbind(cap_cb_cap_get_capBindSID(cap));
220        }
221        if (final) {
222            smmu_delete_cb(cap);
223        }
224        break;
225    case cap_sid_cap:
226        if (final) {
227            smmu_delete_sid(cap);
228        }
229        break;
230#endif
231    }
232
233    fc_ret.remainder = cap_null_cap_new();
234    fc_ret.cleanupInfo = cap_null_cap_new();
235    return fc_ret;
236}
237
238bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
239{
240    switch (cap_get_capType(cap_a)) {
241    case cap_frame_cap:
242        if (cap_get_capType(cap_b) == cap_frame_cap) {
243
244            word_t botA, botB, topA, topB;
245            botA = cap_frame_cap_get_capFBasePtr(cap_a);
246            botB = cap_frame_cap_get_capFBasePtr(cap_b);
247            topA = botA + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_a)));
248            topB = botB + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_b))) ;
249            return ((botA <= botB) && (topA >= topB) && (botB <= topB));
250        }
251        break;
252
253    case cap_page_table_cap:
254        if (cap_get_capType(cap_b) == cap_page_table_cap) {
255            return cap_page_table_cap_get_capPTBasePtr(cap_a) ==
256                   cap_page_table_cap_get_capPTBasePtr(cap_b);
257        }
258        break;
259
260    case cap_page_directory_cap:
261        if (cap_get_capType(cap_b) == cap_page_directory_cap) {
262            return cap_page_directory_cap_get_capPDBasePtr(cap_a) ==
263                   cap_page_directory_cap_get_capPDBasePtr(cap_b);
264        }
265        break;
266
267    case cap_page_upper_directory_cap:
268        if (cap_get_capType(cap_b) == cap_page_upper_directory_cap) {
269            return cap_page_upper_directory_cap_get_capPUDBasePtr(cap_a) ==
270                   cap_page_upper_directory_cap_get_capPUDBasePtr(cap_b);
271        }
272        break;
273
274    case cap_page_global_directory_cap:
275        if (cap_get_capType(cap_b) == cap_page_global_directory_cap) {
276            return cap_page_global_directory_cap_get_capPGDBasePtr(cap_a) ==
277                   cap_page_global_directory_cap_get_capPGDBasePtr(cap_b);
278        }
279        break;
280
281    case cap_asid_control_cap:
282        if (cap_get_capType(cap_b) == cap_asid_control_cap) {
283            return true;
284        }
285        break;
286
287    case cap_asid_pool_cap:
288        if (cap_get_capType(cap_b) == cap_asid_pool_cap) {
289            return cap_asid_pool_cap_get_capASIDPool(cap_a) ==
290                   cap_asid_pool_cap_get_capASIDPool(cap_b);
291        }
292        break;
293
294#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
295    case cap_vcpu_cap:
296        if (cap_get_capType(cap_b) == cap_vcpu_cap) {
297            return cap_vcpu_cap_get_capVCPUPtr(cap_a) ==
298                   cap_vcpu_cap_get_capVCPUPtr(cap_b);
299        }
300        break;
301#endif
302#ifdef CONFIG_ARM_SMMU
303    case cap_sid_control_cap:
304        if (cap_get_capType(cap_b) == cap_sid_control_cap ||
305            cap_get_capType(cap_b) == cap_sid_cap) {
306            return true;
307        }
308        break;
309    case cap_cb_control_cap:
310        if (cap_get_capType(cap_b) == cap_cb_control_cap ||
311            cap_get_capType(cap_b) == cap_cb_cap) {
312            return true;
313        }
314        break;
315    case cap_sid_cap:
316        if (cap_get_capType(cap_b) == cap_sid_cap) {
317            return cap_sid_cap_get_capSID(cap_a) ==
318                   cap_sid_cap_get_capSID(cap_b);
319        }
320        break;
321    case cap_cb_cap:
322        if (cap_get_capType(cap_b) == cap_cb_cap) {
323            return cap_cb_cap_get_capCB(cap_a) ==
324                   cap_cb_cap_get_capCB(cap_b);
325        }
326        break;
327#endif
328    }
329    return false;
330}
331
332bool_t CONST Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
333{
334    if (cap_get_capType(cap_a) == cap_frame_cap) {
335        if (cap_get_capType(cap_b) == cap_frame_cap) {
336            return ((cap_frame_cap_get_capFBasePtr(cap_a) ==
337                     cap_frame_cap_get_capFBasePtr(cap_b)) &&
338                    (cap_frame_cap_get_capFSize(cap_a) ==
339                     cap_frame_cap_get_capFSize(cap_b)) &&
340                    ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) ==
341                     (cap_frame_cap_get_capFIsDevice(cap_b) == 0)));
342        }
343    }
344#ifdef CONFIG_ARM_SMMU
345    if (cap_get_capType(cap_a) == cap_sid_control_cap &&
346        cap_get_capType(cap_b) == cap_sid_cap) {
347        return false;
348    }
349    if (cap_get_capType(cap_a) == cap_cb_control_cap &&
350        cap_get_capType(cap_b) == cap_cb_cap) {
351        return false;
352    }
353#endif
354    return Arch_sameRegionAs(cap_a, cap_b);
355}
356
357word_t Arch_getObjectSize(word_t t)
358{
359    switch (t) {
360    case seL4_ARM_SmallPageObject:
361        return ARMSmallPageBits;
362    case seL4_ARM_LargePageObject:
363        return ARMLargePageBits;
364    case seL4_ARM_HugePageObject:
365        return ARMHugePageBits;
366    case seL4_ARM_PageTableObject:
367        return seL4_PageTableBits;
368    case seL4_ARM_PageDirectoryObject:
369        return seL4_PageDirBits;
370    case seL4_ARM_PageUpperDirectoryObject:
371        return seL4_PUDBits;
372#ifndef AARCH64_VSPACE_S2_START_L1
373    case seL4_ARM_PageGlobalDirectoryObject:
374        return seL4_PGDBits;
375#endif
376#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
377    case seL4_ARM_VCPUObject:
378        return VCPU_SIZE_BITS;
379#endif
380    default:
381        fail("Invalid object type");
382        return 0;
383    }
384}
385
386cap_t Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
387{
388    switch (t) {
389    case seL4_ARM_SmallPageObject:
390        return cap_frame_cap_new(
391                   asidInvalid,           /* capFMappedASID */
392                   (word_t)regionBase,    /* capFBasePtr */
393                   ARMSmallPage,          /* capFSize */
394                   0,                     /* capFMappedAddress */
395                   VMReadWrite,           /* capFVMRights */
396                   !!deviceMemory         /* capFIsDevice */
397               );
398
399    case seL4_ARM_LargePageObject:
400        return cap_frame_cap_new(
401                   asidInvalid,           /* capFMappedASID */
402                   (word_t)regionBase,    /* capFBasePtr */
403                   ARMLargePage,          /* capFSize */
404                   0,                     /* capFMappedAddress */
405                   VMReadWrite,           /* capFVMRights */
406                   !!deviceMemory         /* capFIsDevice */
407               );
408
409    case seL4_ARM_HugePageObject:
410        return cap_frame_cap_new(
411                   asidInvalid,           /* capFMappedASID */
412                   (word_t)regionBase,    /* capFBasePtr */
413                   ARMHugePage,           /* capFSize */
414                   0,                     /* capFMappedAddress */
415                   VMReadWrite,           /* capFVMRights */
416                   !!deviceMemory         /* capFIsDevice */
417               );
418#ifndef AARCH64_VSPACE_S2_START_L1
419    case seL4_ARM_PageGlobalDirectoryObject:
420#ifdef CONFIG_ARM_SMMU
421
422        return cap_page_global_directory_cap_new(
423                   asidInvalid,           /* capPGDMappedASID   */
424                   (word_t)regionBase,    /* capPGDBasePtr      */
425                   0,                     /* capPGDIsMapped     */
426                   CB_INVALID             /* capPGDMappedCB     */
427               );
428#else
429
430        return cap_page_global_directory_cap_new(
431                   asidInvalid,           /* capPGDMappedASID   */
432                   (word_t)regionBase,    /* capPGDBasePtr      */
433                   0                      /* capPGDIsMapped     */
434               );
435#endif /*!CONFIG_ARM_SMMU*/
436#endif /*!AARCH64_VSPACE_S2_START_L1*/
437    case seL4_ARM_PageUpperDirectoryObject:
438        return cap_page_upper_directory_cap_new(
439                   asidInvalid,           /* capPUDMappedASID    */
440                   (word_t)regionBase,    /* capPUDBasePtr       */
441                   0,                     /* capPUDIsMapped      */
442                   0                      /* capPUDMappedAddress */
443               );
444
445    case seL4_ARM_PageDirectoryObject:
446        return cap_page_directory_cap_new(
447                   asidInvalid,           /* capPDMappedASID    */
448                   (word_t)regionBase,    /* capPDBasePtr       */
449                   0,                     /* capPDIsMapped      */
450                   0                      /* capPDMappedAddress */
451               );
452
453    case seL4_ARM_PageTableObject:
454        return cap_page_table_cap_new(
455                   asidInvalid,           /* capPTMappedASID    */
456                   (word_t)regionBase,    /* capPTBasePtr       */
457                   0,                     /* capPTIsMapped      */
458                   0                      /* capPTMappedAddress */
459               );
460
461#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
462    case seL4_ARM_VCPUObject:
463        /** AUXUPD: "(True, ptr_retyp
464          (Ptr (ptr_val \<acute>regionBase) :: vcpu_C ptr))" */
465        vcpu_init(VCPU_PTR(regionBase));
466        return cap_vcpu_cap_new(VCPU_REF(regionBase));
467#endif
468
469    default:
470        fail("Arch_createObject got an API type or invalid object type");
471    }
472}
473
474exception_t Arch_decodeInvocation(word_t label, word_t length, cptr_t cptr,
475                                  cte_t *slot, cap_t cap, extra_caps_t extraCaps,
476                                  bool_t call, word_t *buffer)
477{
478
479    /* The C parser cannot handle a switch statement with only a default
480     * case. So we need to do some gymnastics to remove the switch if
481     * there are no other cases */
482#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_ARM_SMMU)
483    switch (cap_get_capType(cap)) {
484#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
485    case cap_vcpu_cap:
486        return decodeARMVCPUInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer);
487#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */
488#ifdef CONFIG_ARM_SMMU
489    case cap_sid_control_cap:
490        return decodeARMSIDControlInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer);
491    case cap_sid_cap:
492        return decodeARMSIDInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer);
493    case cap_cb_control_cap:
494        return decodeARMCBControlInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer);
495    case cap_cb_cap:
496        return decodeARMCBInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer);
497#endif /*CONFIG_ARM_SMMU*/
498    default:
499#else
500{
501#endif
502    return decodeARMMMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer);
503}
504}
505
506void
507Arch_prepareThreadDelete(tcb_t * thread) {
508#ifdef CONFIG_HAVE_FPU
509    fpuThreadDelete(thread);
510#endif
511
512#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
513    if (thread->tcbArch.tcbVCPU) {
514        dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread);
515    }
516#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
517}
518