1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
8 * See "LICENSE_GPLv2.txt" for details.
9 *
10 * @TAG(DATA61_GPL)
11 */
12
13#include <config.h>
14#include <types.h>
15#include <api/failures.h>
16#include <kernel/vspace.h>
17#include <object/structures.h>
18#include <arch/machine.h>
19#include <arch/model/statedata.h>
20#include <arch/object/objecttype.h>
21
22bool_t
23Arch_isFrameType(word_t type)
24{
25    switch (type) {
26    case seL4_ARM_SmallPageObject:
27        return true;
28    case seL4_ARM_LargePageObject:
29        return true;
30    case seL4_ARM_HugePageObject:
31        return true;
32    default:
33        return false;
34    }
35}
36
37deriveCap_ret_t
38Arch_deriveCap(cte_t *slot, cap_t cap)
39{
40    deriveCap_ret_t ret;
41
42    switch (cap_get_capType(cap)) {
43    case cap_page_global_directory_cap:
44        if (cap_page_global_directory_cap_get_capPGDIsMapped(cap)) {
45            ret.cap = cap;
46            ret.status = EXCEPTION_NONE;
47        } else {
48            userError("Deriving a PDG cap without an assigned ASID");
49            current_syscall_error.type = seL4_IllegalOperation;
50            ret.cap = cap_null_cap_new();
51            ret.status = EXCEPTION_SYSCALL_ERROR;
52        }
53        return ret;
54
55    case cap_page_upper_directory_cap:
56        if (cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) {
57            ret.cap = cap;
58            ret.status = EXCEPTION_NONE;
59        } else {
60            userError("Deriving a PUD cap without an assigned ASID");
61            current_syscall_error.type = seL4_IllegalOperation;
62            ret.cap = cap_null_cap_new();
63            ret.status = EXCEPTION_SYSCALL_ERROR;
64        }
65        return ret;
66
67    case cap_page_directory_cap:
68        if (cap_page_directory_cap_get_capPDIsMapped(cap)) {
69            ret.cap = cap;
70            ret.status = EXCEPTION_NONE;
71        } else {
72            userError("Deriving a PD cap without an assigned ASID");
73            current_syscall_error.type = seL4_IllegalOperation;
74            ret.cap = cap_null_cap_new();
75            ret.status = EXCEPTION_SYSCALL_ERROR;
76        }
77        return ret;
78
79    case cap_page_table_cap:
80        if (cap_page_table_cap_get_capPTIsMapped(cap)) {
81            ret.cap = cap;
82            ret.status = EXCEPTION_NONE;
83        } else {
84            userError("Deriving a PT cap without an assigned ASID");
85            current_syscall_error.type = seL4_IllegalOperation;
86            ret.cap = cap_null_cap_new();
87            ret.status = EXCEPTION_SYSCALL_ERROR;
88        }
89        return ret;
90
91    case cap_frame_cap:
92        ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid);
93        ret.status = EXCEPTION_NONE;
94        return ret;
95
96    case cap_asid_control_cap:
97    case cap_asid_pool_cap:
98        ret.cap = cap;
99        ret.status = EXCEPTION_NONE;
100        return ret;
101
102#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
103    case cap_vcpu_cap:
104        ret.cap = cap;
105        ret.status = EXCEPTION_NONE;
106        return ret;
107#endif
108    default:
109        /* This assert has no equivalent in haskell,
110         * as the options are restricted by type */
111        fail("Invalid arch cap");
112    }
113}
114
115cap_t CONST
116Arch_updateCapData(bool_t preserve, word_t data, cap_t cap)
117{
118    return cap;
119}
120
121cap_t CONST
122Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap)
123{
124    if (cap_get_capType(cap) == cap_frame_cap) {
125        vm_rights_t vm_rights;
126
127        vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap));
128        vm_rights = maskVMRights(vm_rights, cap_rights_mask);
129
130        return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights));
131    } else {
132        return cap;
133    }
134}
135
136finaliseCap_ret_t
137Arch_finaliseCap(cap_t cap, bool_t final)
138{
139    finaliseCap_ret_t fc_ret;
140
141    switch (cap_get_capType(cap)) {
142    case cap_asid_pool_cap:
143        if (final) {
144            deleteASIDPool(cap_asid_pool_cap_get_capASIDBase(cap),
145                           ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap)));
146        }
147        break;
148
149    case cap_page_global_directory_cap:
150        if (final && cap_page_global_directory_cap_get_capPGDIsMapped(cap)) {
151            deleteASID(cap_page_global_directory_cap_get_capPGDMappedASID(cap),
152                       PGDE_PTR(cap_page_global_directory_cap_get_capPGDBasePtr(cap)));
153        }
154        break;
155
156    case cap_page_upper_directory_cap:
157        if (final && cap_page_upper_directory_cap_get_capPUDIsMapped(cap)) {
158            unmapPageUpperDirectory(cap_page_upper_directory_cap_get_capPUDMappedASID(cap),
159                                    cap_page_upper_directory_cap_get_capPUDMappedAddress(cap),
160                                    PUDE_PTR(cap_page_upper_directory_cap_get_capPUDBasePtr(cap)));
161        }
162        break;
163
164    case cap_page_directory_cap:
165        if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) {
166            unmapPageDirectory(cap_page_directory_cap_get_capPDMappedASID(cap),
167                               cap_page_directory_cap_get_capPDMappedAddress(cap),
168                               PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(cap)));
169        }
170        break;
171
172    case cap_page_table_cap:
173        if (final && cap_page_table_cap_get_capPTIsMapped(cap)) {
174            unmapPageTable(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_frame_cap:
181        if (cap_frame_cap_get_capFMappedASID(cap)) {
182            unmapPage(cap_frame_cap_get_capFSize(cap),
183                      cap_frame_cap_get_capFMappedASID(cap),
184                      cap_frame_cap_get_capFMappedAddress(cap),
185                      cap_frame_cap_get_capFBasePtr(cap));
186        }
187        break;
188#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
189    case cap_vcpu_cap:
190        if (final) {
191            vcpu_finalise(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap)));
192        }
193        break;
194#endif
195    }
196
197    fc_ret.remainder = cap_null_cap_new();
198    fc_ret.cleanupInfo = cap_null_cap_new();
199    return fc_ret;
200}
201
202bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
203{
204    switch (cap_get_capType(cap_a)) {
205    case cap_frame_cap:
206        if (cap_get_capType(cap_b) == cap_frame_cap) {
207
208            word_t botA, botB, topA, topB;
209            botA = cap_frame_cap_get_capFBasePtr(cap_a);
210            botB = cap_frame_cap_get_capFBasePtr(cap_b);
211            topA = botA + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_a)));
212            topB = botB + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_b))) ;
213            return ((botA <= botB) && (topA >= topB) && (botB <= topB));
214        }
215        break;
216
217    case cap_page_table_cap:
218        if (cap_get_capType(cap_b) == cap_page_table_cap) {
219            return cap_page_table_cap_get_capPTBasePtr(cap_a) ==
220                   cap_page_table_cap_get_capPTBasePtr(cap_b);
221        }
222        break;
223
224    case cap_page_directory_cap:
225        if (cap_get_capType(cap_b) == cap_page_directory_cap) {
226            return cap_page_directory_cap_get_capPDBasePtr(cap_a) ==
227                   cap_page_directory_cap_get_capPDBasePtr(cap_b);
228        }
229        break;
230
231    case cap_page_upper_directory_cap:
232        if (cap_get_capType(cap_b) == cap_page_upper_directory_cap) {
233            return cap_page_upper_directory_cap_get_capPUDBasePtr(cap_a) ==
234                   cap_page_upper_directory_cap_get_capPUDBasePtr(cap_b);
235        }
236        break;
237
238    case cap_page_global_directory_cap:
239        if (cap_get_capType(cap_b) == cap_page_global_directory_cap) {
240            return cap_page_global_directory_cap_get_capPGDBasePtr(cap_a) ==
241                   cap_page_global_directory_cap_get_capPGDBasePtr(cap_b);
242        }
243        break;
244
245    case cap_asid_control_cap:
246        if (cap_get_capType(cap_b) == cap_asid_control_cap) {
247            return true;
248        }
249        break;
250
251    case cap_asid_pool_cap:
252        if (cap_get_capType(cap_b) == cap_asid_pool_cap) {
253            return cap_asid_pool_cap_get_capASIDPool(cap_a) ==
254                   cap_asid_pool_cap_get_capASIDPool(cap_b);
255        }
256        break;
257
258#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
259    case cap_vcpu_cap:
260        if (cap_get_capType(cap_b) == cap_vcpu_cap) {
261            return cap_vcpu_cap_get_capVCPUPtr(cap_a) ==
262                   cap_vcpu_cap_get_capVCPUPtr(cap_b);
263        }
264#endif
265    }
266
267    return false;
268}
269
270bool_t CONST
271Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
272{
273    if (cap_get_capType(cap_a) == cap_frame_cap) {
274        if (cap_get_capType(cap_b) == cap_frame_cap) {
275            return ((cap_frame_cap_get_capFBasePtr(cap_a) ==
276                     cap_frame_cap_get_capFBasePtr(cap_b)) &&
277                    (cap_frame_cap_get_capFSize(cap_a) ==
278                     cap_frame_cap_get_capFSize(cap_b)) &&
279                    ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) ==
280                     (cap_frame_cap_get_capFIsDevice(cap_b) == 0)));
281        }
282    }
283    return Arch_sameRegionAs(cap_a, cap_b);
284}
285
286word_t
287Arch_getObjectSize(word_t t)
288{
289    switch (t) {
290    case seL4_ARM_SmallPageObject:
291        return ARMSmallPageBits;
292    case seL4_ARM_LargePageObject:
293        return ARMLargePageBits;
294    case seL4_ARM_HugePageObject:
295        return ARMHugePageBits;
296    case seL4_ARM_PageTableObject:
297        return seL4_PageTableBits;
298    case seL4_ARM_PageDirectoryObject:
299        return seL4_PageDirBits;
300    case seL4_ARM_PageUpperDirectoryObject:
301        return seL4_PUDBits;
302    case seL4_ARM_PageGlobalDirectoryObject:
303        return seL4_PGDBits;
304#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
305    case seL4_ARM_VCPUObject:
306        return VCPU_SIZE_BITS;
307#endif
308    default:
309        fail("Invalid object type");
310        return 0;
311    }
312}
313
314cap_t
315Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
316{
317    switch (t) {
318    case seL4_ARM_SmallPageObject:
319        return cap_frame_cap_new(
320                   asidInvalid,           /* capFMappedASID */
321                   (word_t)regionBase,    /* capFBasePtr */
322                   ARMSmallPage,          /* capFSize */
323                   0,                     /* capFMappedAddress */
324                   VMReadWrite,           /* capFVMRights */
325                   !!deviceMemory         /* capFIsDevice */
326               );
327
328    case seL4_ARM_LargePageObject:
329        return cap_frame_cap_new(
330                   asidInvalid,           /* capFMappedASID */
331                   (word_t)regionBase,    /* capFBasePtr */
332                   ARMLargePage,          /* capFSize */
333                   0,                     /* capFMappedAddress */
334                   VMReadWrite,           /* capFVMRights */
335                   !!deviceMemory         /* capFIsDevice */
336               );
337
338    case seL4_ARM_HugePageObject:
339        return cap_frame_cap_new(
340                   asidInvalid,           /* capFMappedASID */
341                   (word_t)regionBase,    /* capFBasePtr */
342                   ARMHugePage,           /* capFSize */
343                   0,                     /* capFMappedAddress */
344                   VMReadWrite,           /* capFVMRights */
345                   !!deviceMemory         /* capFIsDevice */
346               );
347
348    case seL4_ARM_PageGlobalDirectoryObject:
349        return cap_page_global_directory_cap_new(
350                   asidInvalid,           /* capPGDMappedASID   */
351                   (word_t)regionBase,    /* capPGDBasePtr      */
352                   0                      /* capPGDIsMapped     */
353               );
354
355    case seL4_ARM_PageUpperDirectoryObject:
356        return cap_page_upper_directory_cap_new(
357                   asidInvalid,           /* capPUDMappedASID    */
358                   (word_t)regionBase,    /* capPUDBasePtr       */
359                   0,                     /* capPUDIsMapped      */
360                   0                      /* capPUDMappedAddress */
361               );
362
363    case seL4_ARM_PageDirectoryObject:
364        return cap_page_directory_cap_new(
365                   asidInvalid,           /* capPDMappedASID    */
366                   (word_t)regionBase,    /* capPDBasePtr       */
367                   0,                     /* capPDIsMapped      */
368                   0                      /* capPDMappedAddress */
369               );
370
371    case seL4_ARM_PageTableObject:
372        return cap_page_table_cap_new(
373                   asidInvalid,           /* capPTMappedASID    */
374                   (word_t)regionBase,    /* capPTBasePtr       */
375                   0,                     /* capPTIsMapped      */
376                   0                      /* capPTMappedAddress */
377               );
378
379#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
380    case seL4_ARM_VCPUObject:
381        /** AUXUPD: "(True, ptr_retyp
382          (Ptr (ptr_val \<acute>regionBase) :: vcpu_C ptr))" */
383        vcpu_init(VCPU_PTR(regionBase));
384        return cap_vcpu_cap_new(VCPU_REF(regionBase));
385#endif
386
387    default:
388        fail("Arch_createObject got an API type or invalid object type");
389    }
390}
391
392exception_t
393Arch_decodeInvocation(word_t label, word_t length, cptr_t cptr,
394                      cte_t *slot, cap_t cap, extra_caps_t extraCaps,
395                      bool_t call, word_t *buffer)
396{
397
398    /* The C parser cannot handle a switch statement with only a default
399     * case. So we need to do some gymnastics to remove the switch if
400     * there are no other cases */
401#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
402    switch (cap_get_capType(cap)) {
403#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
404    case cap_vcpu_cap:
405        return decodeARMVCPUInvocation(label, length, cptr, slot, cap, extraCaps, call, buffer);
406#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */
407    default:
408#else
409{
410#endif
411    return decodeARMMMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer);
412}
413}
414
415void
416Arch_prepareThreadDelete(tcb_t * thread) {
417#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
418    if (thread->tcbArch.tcbVCPU) {
419        dissociateVCPUTCB(thread->tcbArch.tcbVCPU, thread);
420    }
421#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
422}
423