1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
4 *
5 * SPDX-License-Identifier: GPL-2.0-only
6 */
7
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
16deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap)
17{
18    deriveCap_ret_t ret;
19
20    switch (cap_get_capType(cap)) {
21
22    case cap_page_table_cap:
23        if (cap_page_table_cap_get_capPTIsMapped(cap)) {
24            ret.cap = cap;
25            ret.status = EXCEPTION_NONE;
26        } else {
27            userError("Deriving an unmapped PT cap");
28            current_syscall_error.type = seL4_IllegalOperation;
29            ret.cap = cap_null_cap_new();
30            ret.status = EXCEPTION_SYSCALL_ERROR;
31        }
32        return ret;
33
34    case cap_frame_cap:
35        cap = cap_frame_cap_set_capFMappedAddress(cap, 0);
36        ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid);
37        ret.status = EXCEPTION_NONE;
38        return ret;
39
40    case cap_asid_control_cap:
41    case cap_asid_pool_cap:
42        ret.cap = cap;
43        ret.status = EXCEPTION_NONE;
44        return ret;
45
46    default:
47        /* This assert has no equivalent in haskell,
48         * as the options are restricted by type */
49        fail("Invalid arch cap type");
50    }
51}
52
53cap_t CONST Arch_updateCapData(bool_t preserve, word_t data, cap_t cap)
54{
55    return cap;
56}
57
58cap_t CONST Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap)
59{
60    if (cap_get_capType(cap) == cap_frame_cap) {
61        vm_rights_t vm_rights;
62
63        vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap));
64        vm_rights = maskVMRights(vm_rights, cap_rights_mask);
65        return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights));
66    } else {
67        return cap;
68    }
69}
70
71finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final)
72{
73    finaliseCap_ret_t fc_ret;
74
75    switch (cap_get_capType(cap)) {
76    case cap_frame_cap:
77
78        if (cap_frame_cap_get_capFMappedASID(cap)) {
79            unmapPage(cap_frame_cap_get_capFSize(cap),
80                      cap_frame_cap_get_capFMappedASID(cap),
81                      cap_frame_cap_get_capFMappedAddress(cap),
82                      cap_frame_cap_get_capFBasePtr(cap));
83        }
84        break;
85    case cap_page_table_cap:
86        if (final && cap_page_table_cap_get_capPTIsMapped(cap)) {
87            /*
88             * This PageTable is either mapped as a vspace_root or otherwise exists
89             * as an entry in another PageTable. We check if it is a vspace_root and
90             * if it is delete the entry from the ASID pool otherwise we treat it as
91             * a mapped PageTable and unmap it from whatever page table it is mapped
92             * into.
93             */
94            asid_t asid = cap_page_table_cap_get_capPTMappedASID(cap);
95            findVSpaceForASID_ret_t find_ret = findVSpaceForASID(asid);
96            pte_t *pte = PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap));
97            if (find_ret.status == EXCEPTION_NONE && find_ret.vspace_root == pte) {
98                deleteASID(asid, pte);
99            } else {
100                unmapPageTable(asid, cap_page_table_cap_get_capPTMappedAddress(cap), pte);
101            }
102        }
103        break;
104    case cap_asid_pool_cap:
105        if (final) {
106            deleteASIDPool(
107                cap_asid_pool_cap_get_capASIDBase(cap),
108                ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))
109            );
110        }
111        break;
112    case cap_asid_control_cap:
113        break;
114    }
115    fc_ret.remainder = cap_null_cap_new();
116    fc_ret.cleanupInfo = cap_null_cap_new();
117    return fc_ret;
118}
119
120bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
121{
122    switch (cap_get_capType(cap_a)) {
123    case cap_frame_cap:
124        if (cap_get_capType(cap_b) == cap_frame_cap) {
125            word_t botA, botB, topA, topB;
126            botA = cap_frame_cap_get_capFBasePtr(cap_a);
127            botB = cap_frame_cap_get_capFBasePtr(cap_b);
128            topA = botA + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_a)));
129            topB = botB + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_b))) ;
130            return ((botA <= botB) && (topA >= topB) && (botB <= topB));
131        }
132        break;
133
134    case cap_page_table_cap:
135        if (cap_get_capType(cap_b) == cap_page_table_cap) {
136            return cap_page_table_cap_get_capPTBasePtr(cap_a) ==
137                   cap_page_table_cap_get_capPTBasePtr(cap_b);
138        }
139        break;
140    case cap_asid_control_cap:
141        if (cap_get_capType(cap_b) == cap_asid_control_cap) {
142            return true;
143        }
144        break;
145
146    case cap_asid_pool_cap:
147        if (cap_get_capType(cap_b) == cap_asid_pool_cap) {
148            return cap_asid_pool_cap_get_capASIDPool(cap_a) ==
149                   cap_asid_pool_cap_get_capASIDPool(cap_b);
150        }
151        break;
152    }
153
154    return false;
155}
156
157
158bool_t CONST Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
159{
160    if ((cap_get_capType(cap_a) == cap_frame_cap) &&
161        (cap_get_capType(cap_b) == cap_frame_cap)) {
162        return ((cap_frame_cap_get_capFBasePtr(cap_a) ==
163                 cap_frame_cap_get_capFBasePtr(cap_b)) &&
164                (cap_frame_cap_get_capFSize(cap_a) ==
165                 cap_frame_cap_get_capFSize(cap_b)) &&
166                ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) ==
167                 (cap_frame_cap_get_capFIsDevice(cap_b) == 0)));
168    }
169    return Arch_sameRegionAs(cap_a, cap_b);
170}
171
172word_t Arch_getObjectSize(word_t t)
173{
174    switch (t) {
175    case seL4_RISCV_4K_Page:
176    case seL4_RISCV_PageTableObject:
177        return seL4_PageBits;
178    case seL4_RISCV_Mega_Page:
179        return seL4_LargePageBits;
180#if CONFIG_PT_LEVELS > 2
181    case seL4_RISCV_Giga_Page:
182        return seL4_HugePageBits;
183#endif
184#if CONFIG_PT_LEVELS > 3
185    case seL4_RISCV_Tera_Page:
186        return seL4_TeraPageBits;
187#endif
188    default:
189        fail("Invalid object type");
190        return 0;
191    }
192}
193
194cap_t Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t
195                        deviceMemory)
196{
197    switch (t) {
198    case seL4_RISCV_4K_Page:
199        if (deviceMemory) {
200            /** AUXUPD: "(True, ptr_retyps 1
201                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
202            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVSmallPage
203                                                    (ptr_val \<acute>regionBase)
204                                                    (unat RISCVPageBits))" */
205        } else {
206            /** AUXUPD: "(True, ptr_retyps 1
207                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
208            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVSmallPage
209                                                    (ptr_val \<acute>regionBase)
210                                                    (unat RISCVPageBits))" */
211        }
212        return cap_frame_cap_new(
213                   asidInvalid,                    /* capFMappedASID       */
214                   (word_t) regionBase,            /* capFBasePtr          */
215                   RISCV_4K_Page,                  /* capFSize             */
216                   wordFromVMRights(VMReadWrite),  /* capFVMRights         */
217                   deviceMemory,                   /* capFIsDevice         */
218                   0                               /* capFMappedAddress    */
219               );
220
221    case seL4_RISCV_Mega_Page: {
222        if (deviceMemory) {
223            /** AUXUPD: "(True, ptr_retyps (2^9)
224                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
225            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVLargePage
226                                                    (ptr_val \<acute>regionBase)
227                                                    (unat RISCVMegaPageBits))" */
228        } else {
229            /** AUXUPD: "(True, ptr_retyps (2^9)
230                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
231            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVLargePage
232                                                    (ptr_val \<acute>regionBase)
233                                                    (unat RISCVMegaPageBits))" */
234        }
235        return cap_frame_cap_new(
236                   asidInvalid,                    /* capFMappedASID       */
237                   (word_t) regionBase,            /* capFBasePtr          */
238                   RISCV_Mega_Page,                  /* capFSize             */
239                   wordFromVMRights(VMReadWrite),  /* capFVMRights         */
240                   deviceMemory,                   /* capFIsDevice         */
241                   0                               /* capFMappedAddress    */
242               );
243    }
244
245#if CONFIG_PT_LEVELS > 2
246    case seL4_RISCV_Giga_Page: {
247        if (deviceMemory) {
248            /** AUXUPD: "(True, ptr_retyps (2^18)
249                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
250            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVHugePage
251                                                    (ptr_val \<acute>regionBase)
252                                                    (unat RISCVGigaPageBits))" */
253        } else {
254            /** AUXUPD: "(True, ptr_retyps (2^18)
255                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
256            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.RISCVHugePage
257                                                    (ptr_val \<acute>regionBase)
258                                                    (unat RISCVGigaPageBits))" */
259        }
260        return cap_frame_cap_new(
261                   asidInvalid,                    /* capFMappedASID       */
262                   (word_t) regionBase,            /* capFBasePtr          */
263                   RISCV_Giga_Page,                  /* capFSize             */
264                   wordFromVMRights(VMReadWrite),  /* capFVMRights         */
265                   deviceMemory,                   /* capFIsDevice         */
266                   0                               /* capFMappedAddress    */
267               );
268    }
269#endif
270
271    case seL4_RISCV_PageTableObject:
272        /** AUXUPD: "(True, ptr_retyps 1
273              (Ptr (ptr_val \<acute>regionBase) :: (pte_C[512]) ptr))" */
274        return cap_page_table_cap_new(
275                   asidInvalid,            /* capPTMappedASID    */
276                   (word_t)regionBase,     /* capPTBasePtr       */
277                   0,                      /* capPTIsMapped      */
278                   0                       /* capPTMappedAddress */
279               );
280
281    default:
282        /*
283         * This is a conflation of the haskell error: "Arch.createNewCaps
284         * got an API type" and the case where an invalid object type is
285         * passed (which is impossible in haskell).
286         */
287        fail("Arch_createObject got an API type or invalid object type");
288    }
289}
290
291exception_t Arch_decodeInvocation(
292    word_t label,
293    word_t length,
294    cptr_t cptr,
295    cte_t *slot,
296    cap_t cap,
297    extra_caps_t extraCaps,
298    bool_t call,
299    word_t *buffer
300)
301{
302    return decodeRISCVMMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer);
303}
304
305void Arch_prepareThreadDelete(tcb_t *thread)
306{
307#ifdef CONFIG_HAVE_FPU
308    fpuThreadDelete(thread);
309#endif
310}
311
312bool_t Arch_isFrameType(word_t type)
313{
314    switch (type) {
315#if CONFIG_PT_LEVELS == 4
316    case seL4_RISCV_Tera_Page:
317#endif
318#if CONFIG_PT_LEVELS > 2
319    case seL4_RISCV_Giga_Page:
320#endif
321    case seL4_RISCV_Mega_Page:
322    case seL4_RISCV_4K_Page:
323        return true;
324    default:
325        return false;
326    }
327}
328