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 <machine/fpu.h>
15#include <arch/object/objecttype.h>
16#include <arch/object/ioport.h>
17#include <arch/kernel/ept.h>
18
19#include <arch/object/iospace.h>
20#include <plat/machine/intel-vtd.h>
21
22
23bool_t Arch_isFrameType(word_t type)
24{
25    switch (type) {
26    case seL4_X86_4K:
27        return true;
28    case seL4_X86_LargePageObject:
29        return true;
30    case seL4_X64_HugePageObject:
31        return true;
32    default:
33        return false;
34    }
35}
36
37deriveCap_ret_t Mode_deriveCap(cte_t *slot, cap_t cap)
38{
39    deriveCap_ret_t ret;
40
41    switch (cap_get_capType(cap)) {
42    case cap_pml4_cap:
43        if (cap_pml4_cap_get_capPML4IsMapped(cap)) {
44            ret.cap = cap;
45            ret.status = EXCEPTION_NONE;
46        } else {
47            userError("Deriving a PML4 cap without an assigned ASID");
48            current_syscall_error.type = seL4_IllegalOperation;
49            ret.cap = cap_null_cap_new();
50            ret.status = EXCEPTION_SYSCALL_ERROR;
51        }
52        return ret;
53
54    case cap_pdpt_cap:
55        if (cap_pdpt_cap_get_capPDPTIsMapped(cap)) {
56            ret.cap = cap;
57            ret.status = EXCEPTION_NONE;
58        } else {
59            userError("Deriving an unmapped PTPD cap");
60            current_syscall_error.type = seL4_IllegalOperation;
61            ret.cap = cap_null_cap_new();
62            ret.status = EXCEPTION_SYSCALL_ERROR;
63        }
64        return ret;
65
66    case cap_frame_cap:
67        cap = cap_frame_cap_set_capFMapType(cap, X86_MappingNone);
68        ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid);
69        ret.status = EXCEPTION_NONE;
70        return ret;
71
72    default:
73        fail("Invalid arch cap type");
74    }
75}
76
77finaliseCap_ret_t Mode_finaliseCap(cap_t cap, bool_t final)
78{
79    finaliseCap_ret_t fc_ret;
80
81    switch (cap_get_capType(cap)) {
82
83    case cap_pml4_cap:
84        if (final && cap_pml4_cap_get_capPML4IsMapped(cap)) {
85            deleteASID(
86                cap_pml4_cap_get_capPML4MappedASID(cap),
87                PML4E_PTR(cap_pml4_cap_get_capPML4BasePtr(cap))
88            );
89        }
90        break;
91
92    case cap_pdpt_cap:
93        if (final && cap_pdpt_cap_get_capPDPTIsMapped(cap)) {
94            unmapPDPT(
95                cap_pdpt_cap_get_capPDPTMappedASID(cap),
96                cap_pdpt_cap_get_capPDPTMappedAddress(cap),
97                PDPTE_PTR(cap_pdpt_cap_get_capPDPTBasePtr(cap))
98            );
99        }
100        break;
101
102    case cap_frame_cap:
103        if (cap_frame_cap_get_capFMappedASID(cap)) {
104            switch (cap_frame_cap_get_capFMapType(cap)) {
105#ifdef CONFIG_VTX
106            case X86_MappingEPT:
107                unmapEPTPage(
108                    cap_frame_cap_get_capFSize(cap),
109                    cap_frame_cap_get_capFMappedASID(cap),
110                    cap_frame_cap_get_capFMappedAddress(cap),
111                    (void *)cap_frame_cap_get_capFBasePtr(cap)
112                );
113                break;
114#endif
115#ifdef CONFIG_IOMMU
116            case X86_MappingIOSpace:
117                unmapIOPage(cap);
118                break;
119#endif
120            case X86_MappingVSpace:
121                unmapPage(
122                    cap_frame_cap_get_capFSize(cap),
123                    cap_frame_cap_get_capFMappedASID(cap),
124                    cap_frame_cap_get_capFMappedAddress(cap),
125                    (void *)cap_frame_cap_get_capFBasePtr(cap)
126                );
127                break;
128            default:
129                fail("Invalid map type");
130            }
131        }
132        break;
133
134    default:
135        fail("Invalid arch cap type");
136    }
137
138    fc_ret.remainder = cap_null_cap_new();
139    fc_ret.cleanupInfo = cap_null_cap_new();
140    return fc_ret;
141}
142
143bool_t CONST Mode_sameRegionAs(cap_t cap_a, cap_t cap_b)
144{
145    switch (cap_get_capType(cap_a)) {
146
147    case cap_pdpt_cap:
148        if (cap_get_capType(cap_b) == cap_pdpt_cap) {
149            return cap_pdpt_cap_get_capPDPTBasePtr(cap_a) ==
150                   cap_pdpt_cap_get_capPDPTBasePtr(cap_b);
151        }
152        return false;
153
154    case cap_pml4_cap:
155        if (cap_get_capType(cap_b) == cap_pml4_cap) {
156            return cap_pml4_cap_get_capPML4BasePtr(cap_a) ==
157                   cap_pml4_cap_get_capPML4BasePtr(cap_b);
158        }
159        return false;
160    default:
161        return false;
162    }
163}
164
165word_t Mode_getObjectSize(word_t t)
166{
167    switch (t) {
168    case seL4_X64_PML4Object:
169        return seL4_PML4Bits;
170
171    case seL4_X64_HugePageObject:
172        return pageBitsForSize(X64_HugePage);
173
174    default:
175        fail("Invalid object type");
176        return 0;
177    }
178}
179
180cap_t Mode_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
181{
182    switch (t) {
183
184    case seL4_X86_4K:
185        if (deviceMemory) {
186            /** AUXUPD: "(True, ptr_retyps 1
187                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
188            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64SmallPage
189                                                    (ptr_val \<acute>regionBase)
190                                                    (unat X64SmallPageBits))" */
191        } else {
192            /** AUXUPD: "(True, ptr_retyps 1
193                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
194            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64SmallPage
195                                                    (ptr_val \<acute>regionBase)
196                                                    (unat X64SmallPageBits))" */
197        }
198        return cap_frame_cap_new(
199                   asidInvalid,        /* capFMappedASID           */
200                   (word_t)regionBase, /* capFBasePtr              */
201                   X86_SmallPage,      /* capFSize                 */
202                   X86_MappingNone,    /* capFMapType              */
203                   0,                  /* capFMappedAddress        */
204                   VMReadWrite,        /* capFVMRights             */
205                   deviceMemory        /* capFIsDevice             */
206               );
207
208    case seL4_X86_LargePageObject:
209        if (deviceMemory) {
210            /** AUXUPD: "(True, ptr_retyps 512
211                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
212            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64LargePage
213                                                    (ptr_val \<acute>regionBase)
214                                                    (unat X64LargePageBits))" */
215        } else {
216            /** AUXUPD: "(True, ptr_retyps 512
217                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
218            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64LargePage
219                                                    (ptr_val \<acute>regionBase)
220                                                    (unat X64LargePageBits))" */
221        }
222        return cap_frame_cap_new(
223                   asidInvalid,        /* capFMappedASID           */
224                   (word_t)regionBase, /* capFBasePtr              */
225                   X86_LargePage,      /* capFSize                 */
226                   X86_MappingNone,    /* capFMapType              */
227                   0,                  /* capFMappedAddress        */
228                   VMReadWrite,        /* capFVMRights             */
229                   deviceMemory        /* capFIsDevice             */
230               );
231
232    case seL4_X64_HugePageObject:
233        if (deviceMemory) {
234            /** AUXUPD: "(True, ptr_retyps 262144
235                     (Ptr (ptr_val \<acute>regionBase) :: user_data_device_C ptr))" */
236            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64HugePage
237                                                    (ptr_val \<acute>regionBase)
238                                                    (unat X64HugePageBits))" */
239        } else {
240            /** AUXUPD: "(True, ptr_retyps 262144
241                     (Ptr (ptr_val \<acute>regionBase) :: user_data_C ptr))" */
242            /** GHOSTUPD: "(True, gs_new_frames vmpage_size.X64HugePage
243                                                    (ptr_val \<acute>regionBase)
244                                                    (unat X64HugePageBits))" */
245        }
246        return cap_frame_cap_new(
247                   asidInvalid,        /* capFMappedASID           */
248                   (word_t)regionBase, /* capFBasePtr              */
249                   X64_HugePage,       /* capFSize                 */
250                   X86_MappingNone,    /* capFMapType              */
251                   0,                  /* capFMappedAddress        */
252                   VMReadWrite,        /* capFVMRights             */
253                   deviceMemory        /* capFIsDevice             */
254               );
255
256    case seL4_X86_PageTableObject:
257        /** AUXUPD: "(True, ptr_retyps 1
258              (Ptr (ptr_val \<acute>regionBase) :: (pte_C[512]) ptr))" */
259        return cap_page_table_cap_new(
260                   asidInvalid,            /* capPTMappedASID    */
261                   (word_t)regionBase,     /* capPTBasePtr       */
262                   0,                      /* capPTIsMapped      */
263                   0                       /* capPTMappedAddress */
264               );
265
266    case seL4_X86_PageDirectoryObject:
267        /** AUXUPD: "(True, ptr_retyps 1
268              (Ptr (ptr_val \<acute>regionBase) :: (pde_C[512]) ptr))" */
269        return cap_page_directory_cap_new(
270                   asidInvalid,                /* capPDMappedASID      */
271                   (word_t)regionBase,         /* capPDBasePtr         */
272                   0,                          /* capPDIsMapped        */
273                   0                           /* capPDMappedAddress   */
274               );
275
276    case seL4_X86_PDPTObject:
277        /** AUXUPD: "(True, ptr_retyps 1
278              (Ptr (ptr_val \<acute>regionBase) :: (pdpte_C[512]) ptr))" */
279        return cap_pdpt_cap_new(
280                   asidInvalid,                /* capPDPTMappedASID    */
281                   (word_t)regionBase,         /* capPDPTBasePtr       */
282                   0,                          /* capPDPTIsMapped      */
283                   0                           /* capPDPTMappedAddress */
284               );
285
286    case seL4_X64_PML4Object:
287        /** AUXUPD: "(True, ptr_retyps 1
288              (Ptr (ptr_val \<acute>regionBase) :: (pml4e_C[512]) ptr))" */
289        copyGlobalMappings(PML4_PTR(regionBase));
290        return cap_pml4_cap_new(
291                   asidInvalid,                /* capPML4MappedASID   */
292                   (word_t)regionBase,         /* capPML4BasePtr      */
293                   0                           /* capPML4IsMapped     */
294               );
295
296#ifdef CONFIG_IOMMU
297    case seL4_X86_IOPageTableObject:
298        return cap_io_page_table_cap_new(
299                   0,
300                   0,
301                   0,
302                   asidInvalid,
303                   (word_t)regionBase
304               );
305#endif
306
307    default:
308        /*
309         * This is a conflation of the haskell error: "Arch.createNewCaps
310         * got an API type" and the case where an invalid object type is
311         * passed (which is impossible in haskell).
312         */
313        fail("Arch_createObject got an API type or invalid object type");
314    }
315}
316
317exception_t Mode_decodeInvocation(
318    word_t label,
319    word_t length,
320    cptr_t cptr,
321    cte_t *slot,
322    cap_t cap,
323    extra_caps_t extraCaps,
324    word_t *buffer
325)
326{
327    switch (cap_get_capType(cap)) {
328    case cap_pml4_cap:
329    case cap_pdpt_cap:
330    case cap_page_directory_cap:
331    case cap_page_table_cap:
332    case cap_frame_cap:
333        return decodeX86MMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer);
334
335    default:
336        current_syscall_error.type = seL4_InvalidCapability;
337        current_syscall_error.invalidCapNumber = 0;
338        return EXCEPTION_SYSCALL_ERROR;
339    }
340}
341