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
Arch_deriveCap(cte_t * slot,cap_t cap)16 deriveCap_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
Arch_updateCapData(bool_t preserve,word_t data,cap_t cap)53 cap_t CONST Arch_updateCapData(bool_t preserve, word_t data, cap_t cap)
54 {
55 return cap;
56 }
57
Arch_maskCapRights(seL4_CapRights_t cap_rights_mask,cap_t cap)58 cap_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
Arch_finaliseCap(cap_t cap,bool_t final)71 finaliseCap_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
Arch_sameRegionAs(cap_t cap_a,cap_t cap_b)120 bool_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
Arch_sameObjectAs(cap_t cap_a,cap_t cap_b)158 bool_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
Arch_getObjectSize(word_t t)172 word_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
Arch_createObject(object_t t,void * regionBase,word_t userSize,bool_t deviceMemory)194 cap_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
Arch_decodeInvocation(word_t label,word_t length,cptr_t cptr,cte_t * slot,cap_t cap,bool_t call,word_t * buffer)291 exception_t Arch_decodeInvocation(
292 word_t label,
293 word_t length,
294 cptr_t cptr,
295 cte_t *slot,
296 cap_t cap,
297 bool_t call,
298 word_t *buffer
299 )
300 {
301 return decodeRISCVMMUInvocation(label, length, cptr, slot, cap, buffer);
302 }
303
Arch_prepareThreadDelete(tcb_t * thread)304 void Arch_prepareThreadDelete(tcb_t *thread)
305 {
306 #ifdef CONFIG_HAVE_FPU
307 fpuThreadDelete(thread);
308 #endif
309 }
310
Arch_isFrameType(word_t type)311 bool_t Arch_isFrameType(word_t type)
312 {
313 switch (type) {
314 #if CONFIG_PT_LEVELS == 4
315 case seL4_RISCV_Tera_Page:
316 #endif
317 #if CONFIG_PT_LEVELS > 2
318 case seL4_RISCV_Giga_Page:
319 #endif
320 case seL4_RISCV_Mega_Page:
321 case seL4_RISCV_4K_Page:
322 return true;
323 default:
324 return false;
325 }
326 }
327