1 /*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7 #include <config.h>
8 #include <api/syscall.h>
9 #include <machine/io.h>
10 #include <kernel/boot.h>
11 #include <model/statedata.h>
12 #include <arch/kernel/vspace.h>
13 #include <arch/api/invocation.h>
14 #include <arch/kernel/tlb_bitmap.h>
15 #include <mode/kernel/tlb.h>
16 #include <mode/kernel/vspace.h>
17
performPageGetAddress(void * vbase_ptr)18 static exception_t performPageGetAddress(void *vbase_ptr)
19 {
20 paddr_t capFBasePtr;
21
22 /* Get the physical address of this frame. */
23 capFBasePtr = pptr_to_paddr(vbase_ptr);
24
25 /* return it in the first message register */
26 setRegister(NODE_STATE(ksCurThread), msgRegisters[0], capFBasePtr);
27 setRegister(NODE_STATE(ksCurThread), msgInfoRegister,
28 wordFromMessageInfo(seL4_MessageInfo_new(0, 0, 0, 1)));
29
30 return EXCEPTION_NONE;
31 }
32
33
deleteASIDPool(asid_t asid_base,asid_pool_t * pool)34 void deleteASIDPool(asid_t asid_base, asid_pool_t *pool)
35 {
36 /* Haskell error: "ASID pool's base must be aligned" */
37 assert(IS_ALIGNED(asid_base, asidLowBits));
38
39 if (x86KSASIDTable[asid_base >> asidLowBits] == pool) {
40 for (unsigned int offset = 0; offset < BIT(asidLowBits); offset++) {
41 asid_map_t asid_map = pool->array[offset];
42 if (asid_map_get_type(asid_map) == asid_map_asid_map_vspace) {
43 vspace_root_t *vspace = (vspace_root_t *)asid_map_asid_map_vspace_get_vspace_root(asid_map);
44 hwASIDInvalidate(asid_base + offset, vspace);
45 }
46 }
47 x86KSASIDTable[asid_base >> asidLowBits] = NULL;
48 setVMRoot(NODE_STATE(ksCurThread));
49 }
50 }
51
performASIDControlInvocation(void * frame,cte_t * slot,cte_t * parent,asid_t asid_base)52 exception_t performASIDControlInvocation(void *frame, cte_t *slot, cte_t *parent, asid_t asid_base)
53 {
54 /** AUXUPD: "(True, typ_region_bytes (ptr_val \<acute>frame) 12)" */
55 /** GHOSTUPD: "(True, gs_clear_region (ptr_val \<acute>frame) 12)" */
56 cap_untyped_cap_ptr_set_capFreeIndex(&(parent->cap),
57 MAX_FREE_INDEX(cap_untyped_cap_get_capBlockSize(parent->cap)));
58
59 memzero(frame, BIT(pageBitsForSize(X86_SmallPage)));
60 /** AUXUPD: "(True, ptr_retyps 1 (Ptr (ptr_val \<acute>frame) :: asid_pool_C ptr))" */
61
62 cteInsert(
63 cap_asid_pool_cap_new(
64 asid_base, /* capASIDBase */
65 WORD_REF(frame) /* capASIDPool */
66 ),
67 parent,
68 slot
69 );
70 /* Haskell error: "ASID pool's base must be aligned" */
71 assert((asid_base & MASK(asidLowBits)) == 0);
72 x86KSASIDTable[asid_base >> asidLowBits] = (asid_pool_t *)frame;
73
74 return EXCEPTION_NONE;
75 }
76
deleteASID(asid_t asid,vspace_root_t * vspace)77 void deleteASID(asid_t asid, vspace_root_t *vspace)
78 {
79 asid_pool_t *poolPtr;
80
81 poolPtr = x86KSASIDTable[asid >> asidLowBits];
82 if (poolPtr != NULL) {
83 asid_map_t asid_map = poolPtr->array[asid & MASK(asidLowBits)];
84 if (asid_map_get_type(asid_map) == asid_map_asid_map_vspace &&
85 (vspace_root_t *)asid_map_asid_map_vspace_get_vspace_root(asid_map) == vspace) {
86 hwASIDInvalidate(asid, vspace);
87 poolPtr->array[asid & MASK(asidLowBits)] = asid_map_asid_map_none_new();
88 setVMRoot(NODE_STATE(ksCurThread));
89 }
90 }
91 }
92
lookupIPCBuffer(bool_t isReceiver,tcb_t * thread)93 word_t *PURE lookupIPCBuffer(bool_t isReceiver, tcb_t *thread)
94 {
95 word_t w_bufferPtr;
96 cap_t bufferCap;
97 vm_rights_t vm_rights;
98
99 w_bufferPtr = thread->tcbIPCBuffer;
100 bufferCap = TCB_PTR_CTE_PTR(thread, tcbBuffer)->cap;
101
102 if (cap_get_capType(bufferCap) != cap_frame_cap) {
103 return NULL;
104 }
105 if (unlikely(cap_frame_cap_get_capFIsDevice(bufferCap))) {
106 return NULL;
107 }
108
109 vm_rights = cap_frame_cap_get_capFVMRights(bufferCap);
110 if (vm_rights == VMReadWrite || (!isReceiver && vm_rights == VMReadOnly)) {
111 word_t basePtr, pageBits;
112
113 basePtr = cap_frame_cap_get_capFBasePtr(bufferCap);
114 pageBits = pageBitsForSize(cap_frame_cap_get_capFSize(bufferCap));
115 return (word_t *)(basePtr + (w_bufferPtr & MASK(pageBits)));
116 } else {
117 return NULL;
118 }
119 }
120
isValidVTableRoot(cap_t cap)121 bool_t CONST isValidVTableRoot(cap_t cap)
122 {
123 return isValidNativeRoot(cap);
124 }
125
126
map_kernel_window_devices(pte_t * pt,uint32_t num_ioapic,paddr_t * ioapic_paddrs,uint32_t num_drhu,paddr_t * drhu_list)127 BOOT_CODE bool_t map_kernel_window_devices(pte_t *pt, uint32_t num_ioapic, paddr_t *ioapic_paddrs, uint32_t num_drhu,
128 paddr_t *drhu_list)
129 {
130 word_t idx = (KDEV_BASE & MASK(LARGE_PAGE_BITS)) >> PAGE_BITS;
131 paddr_t phys;
132 pte_t pte;
133 unsigned int i;
134 /* map kernel devices: APIC */
135 phys = apic_get_base_paddr();
136 if (!phys) {
137 return false;
138 }
139 if (!reserve_region((p_region_t) {
140 phys, phys + 0x1000
141 })) {
142 return false;
143 }
144 pte = x86_make_device_pte(phys);
145
146 assert(idx == (PPTR_APIC & MASK(LARGE_PAGE_BITS)) >> PAGE_BITS);
147 pt[idx] = pte;
148 idx++;
149 for (i = 0; i < num_ioapic; i++) {
150 phys = ioapic_paddrs[i];
151 if (!reserve_region((p_region_t) {
152 phys, phys + 0x1000
153 })) {
154 return false;
155 }
156 pte = x86_make_device_pte(phys);
157 assert(idx == ((PPTR_IOAPIC_START + i * BIT(PAGE_BITS)) & MASK(LARGE_PAGE_BITS)) >> PAGE_BITS);
158 pt[idx] = pte;
159 idx++;
160 if (idx == BIT(PT_INDEX_BITS)) {
161 return false;
162 }
163 }
164 /* put in null mappings for any extra IOAPICs */
165 for (; i < CONFIG_MAX_NUM_IOAPIC; i++) {
166 pte = x86_make_empty_pte();
167 assert(idx == ((PPTR_IOAPIC_START + i * BIT(PAGE_BITS)) & MASK(LARGE_PAGE_BITS)) >> PAGE_BITS);
168 pt[idx] = pte;
169 idx++;
170 }
171
172 /* map kernel devices: IOMMUs */
173 for (i = 0; i < num_drhu; i++) {
174 phys = (paddr_t)drhu_list[i];
175 if (!reserve_region((p_region_t) {
176 phys, phys + 0x1000
177 })) {
178 return false;
179 }
180 pte = x86_make_device_pte(phys);
181
182 assert(idx == ((PPTR_DRHU_START + i * BIT(PAGE_BITS)) & MASK(LARGE_PAGE_BITS)) >> PAGE_BITS);
183 pt[idx] = pte;
184 idx++;
185 if (idx == BIT(PT_INDEX_BITS)) {
186 return false;
187 }
188 }
189
190 /* mark unused kernel-device pages as 'not present' */
191 while (idx < BIT(PT_INDEX_BITS)) {
192 pte = x86_make_empty_pte();
193 pt[idx] = pte;
194 idx++;
195 }
196
197 /* Check we haven't added too many kernel-device mappings.*/
198 assert(idx == BIT(PT_INDEX_BITS));
199 return true;
200 }
201
init_idt(idt_entry_t * idt)202 BOOT_CODE static void init_idt(idt_entry_t *idt)
203 {
204 init_idt_entry(idt, 0x00, int_00);
205 init_idt_entry(idt, 0x01, int_01);
206 init_idt_entry(idt, 0x02, int_02);
207 init_idt_entry(idt, 0x03, int_03);
208 init_idt_entry(idt, 0x04, int_04);
209 init_idt_entry(idt, 0x05, int_05);
210 init_idt_entry(idt, 0x06, int_06);
211 init_idt_entry(idt, 0x07, int_07);
212 init_idt_entry(idt, 0x08, int_08);
213 init_idt_entry(idt, 0x09, int_09);
214 init_idt_entry(idt, 0x0a, int_0a);
215 init_idt_entry(idt, 0x0b, int_0b);
216 init_idt_entry(idt, 0x0c, int_0c);
217 init_idt_entry(idt, 0x0d, int_0d);
218 init_idt_entry(idt, 0x0e, int_0e);
219 init_idt_entry(idt, 0x0f, int_0f);
220
221 init_idt_entry(idt, 0x10, int_10);
222 init_idt_entry(idt, 0x11, int_11);
223 init_idt_entry(idt, 0x12, int_12);
224 init_idt_entry(idt, 0x13, int_13);
225 init_idt_entry(idt, 0x14, int_14);
226 init_idt_entry(idt, 0x15, int_15);
227 init_idt_entry(idt, 0x16, int_16);
228 init_idt_entry(idt, 0x17, int_17);
229 init_idt_entry(idt, 0x18, int_18);
230 init_idt_entry(idt, 0x19, int_19);
231 init_idt_entry(idt, 0x1a, int_1a);
232 init_idt_entry(idt, 0x1b, int_1b);
233 init_idt_entry(idt, 0x1c, int_1c);
234 init_idt_entry(idt, 0x1d, int_1d);
235 init_idt_entry(idt, 0x1e, int_1e);
236 init_idt_entry(idt, 0x1f, int_1f);
237
238 init_idt_entry(idt, 0x20, int_20);
239 init_idt_entry(idt, 0x21, int_21);
240 init_idt_entry(idt, 0x22, int_22);
241 init_idt_entry(idt, 0x23, int_23);
242 init_idt_entry(idt, 0x24, int_24);
243 init_idt_entry(idt, 0x25, int_25);
244 init_idt_entry(idt, 0x26, int_26);
245 init_idt_entry(idt, 0x27, int_27);
246 init_idt_entry(idt, 0x28, int_28);
247 init_idt_entry(idt, 0x29, int_29);
248 init_idt_entry(idt, 0x2a, int_2a);
249 init_idt_entry(idt, 0x2b, int_2b);
250 init_idt_entry(idt, 0x2c, int_2c);
251 init_idt_entry(idt, 0x2d, int_2d);
252 init_idt_entry(idt, 0x2e, int_2e);
253 init_idt_entry(idt, 0x2f, int_2f);
254
255 init_idt_entry(idt, 0x30, int_30);
256 init_idt_entry(idt, 0x31, int_31);
257 init_idt_entry(idt, 0x32, int_32);
258 init_idt_entry(idt, 0x33, int_33);
259 init_idt_entry(idt, 0x34, int_34);
260 init_idt_entry(idt, 0x35, int_35);
261 init_idt_entry(idt, 0x36, int_36);
262 init_idt_entry(idt, 0x37, int_37);
263 init_idt_entry(idt, 0x38, int_38);
264 init_idt_entry(idt, 0x39, int_39);
265 init_idt_entry(idt, 0x3a, int_3a);
266 init_idt_entry(idt, 0x3b, int_3b);
267 init_idt_entry(idt, 0x3c, int_3c);
268 init_idt_entry(idt, 0x3d, int_3d);
269 init_idt_entry(idt, 0x3e, int_3e);
270 init_idt_entry(idt, 0x3f, int_3f);
271
272 init_idt_entry(idt, 0x40, int_40);
273 init_idt_entry(idt, 0x41, int_41);
274 init_idt_entry(idt, 0x42, int_42);
275 init_idt_entry(idt, 0x43, int_43);
276 init_idt_entry(idt, 0x44, int_44);
277 init_idt_entry(idt, 0x45, int_45);
278 init_idt_entry(idt, 0x46, int_46);
279 init_idt_entry(idt, 0x47, int_47);
280 init_idt_entry(idt, 0x48, int_48);
281 init_idt_entry(idt, 0x49, int_49);
282 init_idt_entry(idt, 0x4a, int_4a);
283 init_idt_entry(idt, 0x4b, int_4b);
284 init_idt_entry(idt, 0x4c, int_4c);
285 init_idt_entry(idt, 0x4d, int_4d);
286 init_idt_entry(idt, 0x4e, int_4e);
287 init_idt_entry(idt, 0x4f, int_4f);
288
289 init_idt_entry(idt, 0x50, int_50);
290 init_idt_entry(idt, 0x51, int_51);
291 init_idt_entry(idt, 0x52, int_52);
292 init_idt_entry(idt, 0x53, int_53);
293 init_idt_entry(idt, 0x54, int_54);
294 init_idt_entry(idt, 0x55, int_55);
295 init_idt_entry(idt, 0x56, int_56);
296 init_idt_entry(idt, 0x57, int_57);
297 init_idt_entry(idt, 0x58, int_58);
298 init_idt_entry(idt, 0x59, int_59);
299 init_idt_entry(idt, 0x5a, int_5a);
300 init_idt_entry(idt, 0x5b, int_5b);
301 init_idt_entry(idt, 0x5c, int_5c);
302 init_idt_entry(idt, 0x5d, int_5d);
303 init_idt_entry(idt, 0x5e, int_5e);
304 init_idt_entry(idt, 0x5f, int_5f);
305
306 init_idt_entry(idt, 0x60, int_60);
307 init_idt_entry(idt, 0x61, int_61);
308 init_idt_entry(idt, 0x62, int_62);
309 init_idt_entry(idt, 0x63, int_63);
310 init_idt_entry(idt, 0x64, int_64);
311 init_idt_entry(idt, 0x65, int_65);
312 init_idt_entry(idt, 0x66, int_66);
313 init_idt_entry(idt, 0x67, int_67);
314 init_idt_entry(idt, 0x68, int_68);
315 init_idt_entry(idt, 0x69, int_69);
316 init_idt_entry(idt, 0x6a, int_6a);
317 init_idt_entry(idt, 0x6b, int_6b);
318 init_idt_entry(idt, 0x6c, int_6c);
319 init_idt_entry(idt, 0x6d, int_6d);
320 init_idt_entry(idt, 0x6e, int_6e);
321 init_idt_entry(idt, 0x6f, int_6f);
322
323 init_idt_entry(idt, 0x70, int_70);
324 init_idt_entry(idt, 0x71, int_71);
325 init_idt_entry(idt, 0x72, int_72);
326 init_idt_entry(idt, 0x73, int_73);
327 init_idt_entry(idt, 0x74, int_74);
328 init_idt_entry(idt, 0x75, int_75);
329 init_idt_entry(idt, 0x76, int_76);
330 init_idt_entry(idt, 0x77, int_77);
331 init_idt_entry(idt, 0x78, int_78);
332 init_idt_entry(idt, 0x79, int_79);
333 init_idt_entry(idt, 0x7a, int_7a);
334 init_idt_entry(idt, 0x7b, int_7b);
335 init_idt_entry(idt, 0x7c, int_7c);
336 init_idt_entry(idt, 0x7d, int_7d);
337 init_idt_entry(idt, 0x7e, int_7e);
338 init_idt_entry(idt, 0x7f, int_7f);
339
340 init_idt_entry(idt, 0x80, int_80);
341 init_idt_entry(idt, 0x81, int_81);
342 init_idt_entry(idt, 0x82, int_82);
343 init_idt_entry(idt, 0x83, int_83);
344 init_idt_entry(idt, 0x84, int_84);
345 init_idt_entry(idt, 0x85, int_85);
346 init_idt_entry(idt, 0x86, int_86);
347 init_idt_entry(idt, 0x87, int_87);
348 init_idt_entry(idt, 0x88, int_88);
349 init_idt_entry(idt, 0x89, int_89);
350 init_idt_entry(idt, 0x8a, int_8a);
351 init_idt_entry(idt, 0x8b, int_8b);
352 init_idt_entry(idt, 0x8c, int_8c);
353 init_idt_entry(idt, 0x8d, int_8d);
354 init_idt_entry(idt, 0x8e, int_8e);
355 init_idt_entry(idt, 0x8f, int_8f);
356
357 init_idt_entry(idt, 0x90, int_90);
358 init_idt_entry(idt, 0x91, int_91);
359 init_idt_entry(idt, 0x92, int_92);
360 init_idt_entry(idt, 0x93, int_93);
361 init_idt_entry(idt, 0x94, int_94);
362 init_idt_entry(idt, 0x95, int_95);
363 init_idt_entry(idt, 0x96, int_96);
364 init_idt_entry(idt, 0x97, int_97);
365 init_idt_entry(idt, 0x98, int_98);
366 init_idt_entry(idt, 0x99, int_99);
367 init_idt_entry(idt, 0x9a, int_9a);
368 init_idt_entry(idt, 0x9b, int_9b);
369 init_idt_entry(idt, 0x9c, int_9c);
370 init_idt_entry(idt, 0x9d, int_9d);
371 init_idt_entry(idt, 0x9e, int_9e);
372 init_idt_entry(idt, 0x9f, int_9f);
373
374 init_idt_entry(idt, 0xa0, int_a0);
375 init_idt_entry(idt, 0xa1, int_a1);
376 init_idt_entry(idt, 0xa2, int_a2);
377 init_idt_entry(idt, 0xa3, int_a3);
378 init_idt_entry(idt, 0xa4, int_a4);
379 init_idt_entry(idt, 0xa5, int_a5);
380 init_idt_entry(idt, 0xa6, int_a6);
381 init_idt_entry(idt, 0xa7, int_a7);
382 init_idt_entry(idt, 0xa8, int_a8);
383 init_idt_entry(idt, 0xa9, int_a9);
384 init_idt_entry(idt, 0xaa, int_aa);
385 init_idt_entry(idt, 0xab, int_ab);
386 init_idt_entry(idt, 0xac, int_ac);
387 init_idt_entry(idt, 0xad, int_ad);
388 init_idt_entry(idt, 0xae, int_ae);
389 init_idt_entry(idt, 0xaf, int_af);
390
391 init_idt_entry(idt, 0xb0, int_b0);
392 init_idt_entry(idt, 0xb1, int_b1);
393 init_idt_entry(idt, 0xb2, int_b2);
394 init_idt_entry(idt, 0xb3, int_b3);
395 init_idt_entry(idt, 0xb4, int_b4);
396 init_idt_entry(idt, 0xb5, int_b5);
397 init_idt_entry(idt, 0xb6, int_b6);
398 init_idt_entry(idt, 0xb7, int_b7);
399 init_idt_entry(idt, 0xb8, int_b8);
400 init_idt_entry(idt, 0xb9, int_b9);
401 init_idt_entry(idt, 0xba, int_ba);
402 init_idt_entry(idt, 0xbb, int_bb);
403 init_idt_entry(idt, 0xbc, int_bc);
404 init_idt_entry(idt, 0xbd, int_bd);
405 init_idt_entry(idt, 0xbe, int_be);
406 init_idt_entry(idt, 0xbf, int_bf);
407
408 init_idt_entry(idt, 0xc0, int_c0);
409 init_idt_entry(idt, 0xc1, int_c1);
410 init_idt_entry(idt, 0xc2, int_c2);
411 init_idt_entry(idt, 0xc3, int_c3);
412 init_idt_entry(idt, 0xc4, int_c4);
413 init_idt_entry(idt, 0xc5, int_c5);
414 init_idt_entry(idt, 0xc6, int_c6);
415 init_idt_entry(idt, 0xc7, int_c7);
416 init_idt_entry(idt, 0xc8, int_c8);
417 init_idt_entry(idt, 0xc9, int_c9);
418 init_idt_entry(idt, 0xca, int_ca);
419 init_idt_entry(idt, 0xcb, int_cb);
420 init_idt_entry(idt, 0xcc, int_cc);
421 init_idt_entry(idt, 0xcd, int_cd);
422 init_idt_entry(idt, 0xce, int_ce);
423 init_idt_entry(idt, 0xcf, int_cf);
424
425 init_idt_entry(idt, 0xd0, int_d0);
426 init_idt_entry(idt, 0xd1, int_d1);
427 init_idt_entry(idt, 0xd2, int_d2);
428 init_idt_entry(idt, 0xd3, int_d3);
429 init_idt_entry(idt, 0xd4, int_d4);
430 init_idt_entry(idt, 0xd5, int_d5);
431 init_idt_entry(idt, 0xd6, int_d6);
432 init_idt_entry(idt, 0xd7, int_d7);
433 init_idt_entry(idt, 0xd8, int_d8);
434 init_idt_entry(idt, 0xd9, int_d9);
435 init_idt_entry(idt, 0xda, int_da);
436 init_idt_entry(idt, 0xdb, int_db);
437 init_idt_entry(idt, 0xdc, int_dc);
438 init_idt_entry(idt, 0xdd, int_dd);
439 init_idt_entry(idt, 0xde, int_de);
440 init_idt_entry(idt, 0xdf, int_df);
441
442 init_idt_entry(idt, 0xe0, int_e0);
443 init_idt_entry(idt, 0xe1, int_e1);
444 init_idt_entry(idt, 0xe2, int_e2);
445 init_idt_entry(idt, 0xe3, int_e3);
446 init_idt_entry(idt, 0xe4, int_e4);
447 init_idt_entry(idt, 0xe5, int_e5);
448 init_idt_entry(idt, 0xe6, int_e6);
449 init_idt_entry(idt, 0xe7, int_e7);
450 init_idt_entry(idt, 0xe8, int_e8);
451 init_idt_entry(idt, 0xe9, int_e9);
452 init_idt_entry(idt, 0xea, int_ea);
453 init_idt_entry(idt, 0xeb, int_eb);
454 init_idt_entry(idt, 0xec, int_ec);
455 init_idt_entry(idt, 0xed, int_ed);
456 init_idt_entry(idt, 0xee, int_ee);
457 init_idt_entry(idt, 0xef, int_ef);
458
459 init_idt_entry(idt, 0xf0, int_f0);
460 init_idt_entry(idt, 0xf1, int_f1);
461 init_idt_entry(idt, 0xf2, int_f2);
462 init_idt_entry(idt, 0xf3, int_f3);
463 init_idt_entry(idt, 0xf4, int_f4);
464 init_idt_entry(idt, 0xf5, int_f5);
465 init_idt_entry(idt, 0xf6, int_f6);
466 init_idt_entry(idt, 0xf7, int_f7);
467 init_idt_entry(idt, 0xf8, int_f8);
468 init_idt_entry(idt, 0xf9, int_f9);
469 init_idt_entry(idt, 0xfa, int_fa);
470 init_idt_entry(idt, 0xfb, int_fb);
471 init_idt_entry(idt, 0xfc, int_fc);
472 init_idt_entry(idt, 0xfd, int_fd);
473 init_idt_entry(idt, 0xfe, int_fe);
474 init_idt_entry(idt, 0xff, int_ff);
475 }
476
init_vm_state(void)477 BOOT_CODE bool_t init_vm_state(void)
478 {
479 word_t cacheLineSize;
480 x86KScacheLineSizeBits = getCacheLineSizeBits();
481 if (!x86KScacheLineSizeBits) {
482 return false;
483 }
484
485 cacheLineSize = BIT(x86KScacheLineSizeBits);
486 if (cacheLineSize != L1_CACHE_LINE_SIZE) {
487 printf("Configured cache line size is %d but detected size is %lu\n",
488 L1_CACHE_LINE_SIZE, cacheLineSize);
489 SMP_COND_STATEMENT(return false);
490 }
491
492 /*
493 * Work around -Waddress-of-packed-member. TSS is the first thing
494 * in the struct and so it's safe to take its address.
495 */
496 void *tss_ptr = &x86KSGlobalState[CURRENT_CPU_INDEX()].x86KStss.tss;
497 init_tss(tss_ptr);
498 init_gdt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSgdt, tss_ptr);
499 init_idt(x86KSGlobalState[CURRENT_CPU_INDEX()].x86KSidt);
500 return true;
501 }
502
init_pat_msr(void)503 BOOT_CODE bool_t init_pat_msr(void)
504 {
505 x86_pat_msr_t pat_msr;
506 /* First verify PAT is supported by the machine.
507 * See section 11.12.1 of Volume 3 of the Intel manual */
508 if ((x86_cpuid_edx(0x1, 0x0) & BIT(16)) == 0) {
509 printf("PAT support not found\n");
510 return false;
511 }
512 pat_msr.words[0] = x86_rdmsr_low(IA32_PAT_MSR);
513 pat_msr.words[1] = x86_rdmsr_high(IA32_PAT_MSR);
514 /* Set up the PAT MSR to the Intel defaults, just in case
515 * they have been changed but a bootloader somewhere along the way */
516 pat_msr = x86_pat_msr_set_pa0(pat_msr, IA32_PAT_MT_WRITE_BACK);
517 pat_msr = x86_pat_msr_set_pa1(pat_msr, IA32_PAT_MT_WRITE_THROUGH);
518 pat_msr = x86_pat_msr_set_pa2(pat_msr, IA32_PAT_MT_UNCACHED);
519 pat_msr = x86_pat_msr_set_pa3(pat_msr, IA32_PAT_MT_UNCACHEABLE);
520 /* Add the WriteCombining cache type to the PAT */
521 pat_msr = x86_pat_msr_set_pa4(pat_msr, IA32_PAT_MT_WRITE_COMBINING);
522 x86_wrmsr(IA32_PAT_MSR, ((uint64_t)pat_msr.words[1]) << 32 | pat_msr.words[0]);
523 return true;
524 }
525
write_it_asid_pool(cap_t it_ap_cap,cap_t it_vspace_cap)526 BOOT_CODE void write_it_asid_pool(cap_t it_ap_cap, cap_t it_vspace_cap)
527 {
528 asid_pool_t *ap = ASID_POOL_PTR(pptr_of_cap(it_ap_cap));
529 ap->array[IT_ASID] = asid_map_asid_map_vspace_new(pptr_of_cap(it_vspace_cap));
530 x86KSASIDTable[IT_ASID >> asidLowBits] = ap;
531 }
532
findMapForASID(asid_t asid)533 asid_map_t findMapForASID(asid_t asid)
534 {
535 asid_pool_t *poolPtr;
536
537 poolPtr = x86KSASIDTable[asid >> asidLowBits];
538 if (!poolPtr) {
539 return asid_map_asid_map_none_new();
540 }
541
542 return poolPtr->array[asid & MASK(asidLowBits)];
543 }
544
findVSpaceForASID(asid_t asid)545 findVSpaceForASID_ret_t findVSpaceForASID(asid_t asid)
546 {
547 findVSpaceForASID_ret_t ret;
548 asid_map_t asid_map;
549
550 asid_map = findMapForASID(asid);
551 if (asid_map_get_type(asid_map) != asid_map_asid_map_vspace) {
552 current_lookup_fault = lookup_fault_invalid_root_new();
553
554 ret.vspace_root = NULL;
555 ret.status = EXCEPTION_LOOKUP_FAULT;
556 return ret;
557 }
558
559 ret.vspace_root = (vspace_root_t *)asid_map_asid_map_vspace_get_vspace_root(asid_map);
560 ret.status = EXCEPTION_NONE;
561 return ret;
562 }
563
handleVMFault(tcb_t * thread,vm_fault_type_t vm_faultType)564 exception_t handleVMFault(tcb_t *thread, vm_fault_type_t vm_faultType)
565 {
566 word_t addr;
567 uint32_t fault;
568
569 addr = getFaultAddr();
570 fault = getRegister(thread, Error);
571
572 switch (vm_faultType) {
573 case X86DataFault:
574 current_fault = seL4_Fault_VMFault_new(addr, fault, false);
575 return EXCEPTION_FAULT;
576
577 case X86InstructionFault:
578 current_fault = seL4_Fault_VMFault_new(addr, fault, true);
579 return EXCEPTION_FAULT;
580
581 default:
582 fail("Invalid VM fault type");
583 }
584 }
585
WritableFromVMRights(vm_rights_t vm_rights)586 uint32_t CONST WritableFromVMRights(vm_rights_t vm_rights)
587 {
588 switch (vm_rights) {
589 case VMReadOnly:
590 return 0;
591
592 case VMKernelOnly:
593 case VMReadWrite:
594 return 1;
595
596 default:
597 fail("Invalid VM rights");
598 }
599 }
600
SuperUserFromVMRights(vm_rights_t vm_rights)601 uint32_t CONST SuperUserFromVMRights(vm_rights_t vm_rights)
602 {
603 switch (vm_rights) {
604 case VMKernelOnly:
605 return 0;
606
607 case VMReadOnly:
608 case VMReadWrite:
609 return 1;
610
611 default:
612 fail("Invalid VM rights");
613 }
614 }
615
lookupPTSlot(vspace_root_t * vspace,vptr_t vptr)616 lookupPTSlot_ret_t lookupPTSlot(vspace_root_t *vspace, vptr_t vptr)
617 {
618 lookupPTSlot_ret_t ret;
619 lookupPDSlot_ret_t pdSlot;
620
621 pdSlot = lookupPDSlot(vspace, vptr);
622 if (pdSlot.status != EXCEPTION_NONE) {
623 ret.ptSlot = NULL;
624 ret.status = pdSlot.status;
625 return ret;
626 }
627 if ((pde_ptr_get_page_size(pdSlot.pdSlot) != pde_pde_pt) ||
628 !pde_pde_pt_ptr_get_present(pdSlot.pdSlot)) {
629 current_lookup_fault = lookup_fault_missing_capability_new(PAGE_BITS + PT_INDEX_BITS);
630 ret.ptSlot = NULL;
631 ret.status = EXCEPTION_LOOKUP_FAULT;
632 return ret;
633 } else {
634 pte_t *pt;
635 pte_t *ptSlot;
636 word_t ptIndex;
637
638 pt = paddr_to_pptr(pde_pde_pt_ptr_get_pt_base_address(pdSlot.pdSlot));
639 ptIndex = (vptr >> PAGE_BITS) & MASK(PT_INDEX_BITS);
640 ptSlot = pt + ptIndex;
641
642 ret.ptSlot = ptSlot;
643 ret.status = EXCEPTION_NONE;
644 return ret;
645 }
646 }
647
checkValidIPCBuffer(vptr_t vptr,cap_t cap)648 exception_t checkValidIPCBuffer(vptr_t vptr, cap_t cap)
649 {
650 if (cap_get_capType(cap) != cap_frame_cap) {
651 userError("IPC Buffer is an invalid cap.");
652 current_syscall_error.type = seL4_IllegalOperation;
653 return EXCEPTION_SYSCALL_ERROR;
654 }
655 if (unlikely(cap_frame_cap_get_capFIsDevice(cap))) {
656 userError("Specifying a device frame as an IPC buffer is not permitted.");
657 current_syscall_error.type = seL4_IllegalOperation;
658 return EXCEPTION_SYSCALL_ERROR;
659 }
660
661 if (!IS_ALIGNED(vptr, seL4_IPCBufferSizeBits)) {
662 userError("IPC Buffer vaddr 0x%x is not aligned.", (int)vptr);
663 current_syscall_error.type = seL4_AlignmentError;
664 return EXCEPTION_SYSCALL_ERROR;
665 }
666
667 return EXCEPTION_NONE;
668 }
669
maskVMRights(vm_rights_t vm_rights,seL4_CapRights_t cap_rights_mask)670 vm_rights_t CONST maskVMRights(vm_rights_t vm_rights, seL4_CapRights_t cap_rights_mask)
671 {
672 if (vm_rights == VMReadOnly && seL4_CapRights_get_capAllowRead(cap_rights_mask)) {
673 return VMReadOnly;
674 }
675 if (vm_rights == VMReadWrite && seL4_CapRights_get_capAllowRead(cap_rights_mask)) {
676 if (!seL4_CapRights_get_capAllowWrite(cap_rights_mask)) {
677 return VMReadOnly;
678 } else {
679 return VMReadWrite;
680 }
681 }
682 return VMKernelOnly;
683 }
684
flushTable(vspace_root_t * vspace,word_t vptr,pte_t * pt,asid_t asid)685 void flushTable(vspace_root_t *vspace, word_t vptr, pte_t *pt, asid_t asid)
686 {
687 word_t i;
688 cap_t threadRoot;
689
690 assert(IS_ALIGNED(vptr, PT_INDEX_BITS + PAGE_BITS));
691
692 /* check if page table belongs to current address space */
693 threadRoot = TCB_PTR_CTE_PTR(NODE_STATE(ksCurThread), tcbVTable)->cap;
694 /* find valid mappings */
695 for (i = 0; i < BIT(PT_INDEX_BITS); i++) {
696 if (pte_get_present(pt[i])) {
697 if (config_set(CONFIG_SUPPORT_PCID) || (isValidNativeRoot(threadRoot)
698 && (vspace_root_t *)pptr_of_cap(threadRoot) == vspace)) {
699 invalidateTranslationSingleASID(vptr + (i << PAGE_BITS), asid,
700 SMP_TERNARY(tlb_bitmap_get(vspace), 0));
701 }
702 }
703 }
704 }
705
706
unmapPage(vm_page_size_t page_size,asid_t asid,vptr_t vptr,void * pptr)707 void unmapPage(vm_page_size_t page_size, asid_t asid, vptr_t vptr, void *pptr)
708 {
709 findVSpaceForASID_ret_t find_ret;
710 lookupPTSlot_ret_t lu_ret;
711 lookupPDSlot_ret_t pd_ret;
712 pde_t *pde;
713
714 find_ret = findVSpaceForASID(asid);
715 if (find_ret.status != EXCEPTION_NONE) {
716 return;
717 }
718
719 switch (page_size) {
720 case X86_SmallPage:
721 lu_ret = lookupPTSlot(find_ret.vspace_root, vptr);
722 if (lu_ret.status != EXCEPTION_NONE) {
723 return;
724 }
725 if (!(pte_ptr_get_present(lu_ret.ptSlot)
726 && (pte_ptr_get_page_base_address(lu_ret.ptSlot)
727 == pptr_to_paddr(pptr)))) {
728 return;
729 }
730 *lu_ret.ptSlot = makeUserPTEInvalid();
731 break;
732
733 case X86_LargePage:
734 pd_ret = lookupPDSlot(find_ret.vspace_root, vptr);
735 if (pd_ret.status != EXCEPTION_NONE) {
736 return;
737 }
738 pde = pd_ret.pdSlot;
739 if (!(pde_ptr_get_page_size(pde) == pde_pde_large
740 && pde_pde_large_ptr_get_present(pde)
741 && (pde_pde_large_ptr_get_page_base_address(pde)
742 == pptr_to_paddr(pptr)))) {
743 return;
744 }
745 *pde = makeUserPDEInvalid();
746 break;
747
748 default:
749 if (!modeUnmapPage(page_size, find_ret.vspace_root, vptr, pptr)) {
750 return;
751 }
752 break;
753 }
754
755 invalidateTranslationSingleASID(vptr, asid,
756 SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
757 }
758
unmapPageTable(asid_t asid,vptr_t vaddr,pte_t * pt)759 void unmapPageTable(asid_t asid, vptr_t vaddr, pte_t *pt)
760 {
761 findVSpaceForASID_ret_t find_ret;
762 lookupPDSlot_ret_t lu_ret;
763
764 find_ret = findVSpaceForASID(asid);
765 if (find_ret.status != EXCEPTION_NONE) {
766 return;
767 }
768
769 lu_ret = lookupPDSlot(find_ret.vspace_root, vaddr);
770 if (lu_ret.status != EXCEPTION_NONE) {
771 return;
772 }
773
774 /* check if the PD actually refers to the PT */
775 if (!(pde_ptr_get_page_size(lu_ret.pdSlot) == pde_pde_pt &&
776 pde_pde_pt_ptr_get_present(lu_ret.pdSlot) &&
777 (pde_pde_pt_ptr_get_pt_base_address(lu_ret.pdSlot) == pptr_to_paddr(pt)))) {
778 return;
779 }
780
781 flushTable(find_ret.vspace_root, vaddr, pt, asid);
782
783 *lu_ret.pdSlot = makeUserPDEInvalid();
784
785 invalidatePageStructureCacheASID(pptr_to_paddr(find_ret.vspace_root), asid,
786 SMP_TERNARY(tlb_bitmap_get(find_ret.vspace_root), 0));
787 }
788
performX86PageInvocationMapPTE(cap_t cap,cte_t * ctSlot,pte_t * ptSlot,pte_t pte,vspace_root_t * vspace)789 static exception_t performX86PageInvocationMapPTE(cap_t cap, cte_t *ctSlot, pte_t *ptSlot, pte_t pte,
790 vspace_root_t *vspace)
791 {
792 ctSlot->cap = cap;
793 *ptSlot = pte;
794 invalidatePageStructureCacheASID(pptr_to_paddr(vspace), cap_frame_cap_get_capFMappedASID(cap),
795 SMP_TERNARY(tlb_bitmap_get(vspace), 0));
796 return EXCEPTION_NONE;
797 }
798
performX86PageInvocationMapPDE(cap_t cap,cte_t * ctSlot,pde_t * pdSlot,pde_t pde,vspace_root_t * vspace)799 static exception_t performX86PageInvocationMapPDE(cap_t cap, cte_t *ctSlot, pde_t *pdSlot, pde_t pde,
800 vspace_root_t *vspace)
801 {
802 ctSlot->cap = cap;
803 *pdSlot = pde;
804 invalidatePageStructureCacheASID(pptr_to_paddr(vspace), cap_frame_cap_get_capFMappedASID(cap),
805 SMP_TERNARY(tlb_bitmap_get(vspace), 0));
806 return EXCEPTION_NONE;
807 }
808
809
performX86PageInvocationUnmap(cap_t cap,cte_t * ctSlot)810 static exception_t performX86PageInvocationUnmap(cap_t cap, cte_t *ctSlot)
811 {
812 assert(cap_frame_cap_get_capFMappedASID(cap));
813 assert(cap_frame_cap_get_capFMapType(cap) == X86_MappingVSpace);
814 // We have this `if` for something we just asserted to be true for simplicity of verification
815 // This has no performance implications as when this function is inlined this `if` will be
816 // inside an identical `if` and will therefore be elided
817 if (cap_frame_cap_get_capFMappedASID(cap)) {
818 unmapPage(
819 cap_frame_cap_get_capFSize(cap),
820 cap_frame_cap_get_capFMappedASID(cap),
821 cap_frame_cap_get_capFMappedAddress(cap),
822 (void *)cap_frame_cap_get_capFBasePtr(cap)
823 );
824 }
825
826 cap_frame_cap_ptr_set_capFMappedAddress(&ctSlot->cap, 0);
827 cap_frame_cap_ptr_set_capFMappedASID(&ctSlot->cap, asidInvalid);
828 cap_frame_cap_ptr_set_capFMapType(&ctSlot->cap, X86_MappingNone);
829
830 return EXCEPTION_NONE;
831 }
832
performX86FrameInvocationUnmap(cap_t cap,cte_t * cte)833 static exception_t performX86FrameInvocationUnmap(cap_t cap, cte_t *cte)
834 {
835 if (cap_frame_cap_get_capFMappedASID(cap) != asidInvalid) {
836 switch (cap_frame_cap_get_capFMapType(cap)) {
837 case X86_MappingVSpace:
838 return performX86PageInvocationUnmap(cap, cte);
839 #ifdef CONFIG_IOMMU
840 case X86_MappingIOSpace:
841 return performX86IOUnMapInvocation(cap, cte);
842 #endif
843 #ifdef CONFIG_VTX
844 case X86_MappingEPT:
845 return performX86EPTPageInvocationUnmap(cap, cte);
846 #endif
847 case X86_MappingNone:
848 fail("Mapped frame cap was not mapped");
849 break;
850 }
851 }
852
853 return EXCEPTION_NONE;
854 }
855
856 struct create_mapping_pte_return {
857 exception_t status;
858 pte_t pte;
859 pte_t *ptSlot;
860 };
861 typedef struct create_mapping_pte_return create_mapping_pte_return_t;
862
createSafeMappingEntries_PTE(paddr_t base,word_t vaddr,vm_rights_t vmRights,vm_attributes_t attr,vspace_root_t * vspace)863 static create_mapping_pte_return_t createSafeMappingEntries_PTE(paddr_t base, word_t vaddr, vm_rights_t vmRights,
864 vm_attributes_t attr,
865 vspace_root_t *vspace)
866 {
867 create_mapping_pte_return_t ret;
868 lookupPTSlot_ret_t lu_ret;
869
870 lu_ret = lookupPTSlot(vspace, vaddr);
871 if (lu_ret.status != EXCEPTION_NONE) {
872 current_syscall_error.type = seL4_FailedLookup;
873 current_syscall_error.failedLookupWasSource = false;
874 ret.status = EXCEPTION_SYSCALL_ERROR;
875 /* current_lookup_fault will have been set by lookupPTSlot */
876 return ret;
877 }
878
879 ret.pte = makeUserPTE(base, attr, vmRights);
880 ret.ptSlot = lu_ret.ptSlot;
881 ret.status = EXCEPTION_NONE;
882 return ret;
883 }
884
885 struct create_mapping_pde_return {
886 exception_t status;
887 pde_t pde;
888 pde_t *pdSlot;
889 };
890 typedef struct create_mapping_pde_return create_mapping_pde_return_t;
891
createSafeMappingEntries_PDE(paddr_t base,word_t vaddr,vm_rights_t vmRights,vm_attributes_t attr,vspace_root_t * vspace)892 static create_mapping_pde_return_t createSafeMappingEntries_PDE(paddr_t base, word_t vaddr, vm_rights_t vmRights,
893 vm_attributes_t attr,
894 vspace_root_t *vspace)
895 {
896 create_mapping_pde_return_t ret;
897 lookupPDSlot_ret_t lu_ret;
898
899 lu_ret = lookupPDSlot(vspace, vaddr);
900 if (lu_ret.status != EXCEPTION_NONE) {
901 current_syscall_error.type = seL4_FailedLookup;
902 current_syscall_error.failedLookupWasSource = false;
903 ret.status = EXCEPTION_SYSCALL_ERROR;
904 /* current_lookup_fault will have been set by lookupPDSlot */
905 return ret;
906 }
907 ret.pdSlot = lu_ret.pdSlot;
908
909 /* check for existing page table */
910 if ((pde_ptr_get_page_size(ret.pdSlot) == pde_pde_pt) &&
911 (pde_pde_pt_ptr_get_present(ret.pdSlot))) {
912 current_syscall_error.type = seL4_DeleteFirst;
913 ret.status = EXCEPTION_SYSCALL_ERROR;
914 return ret;
915 }
916
917
918 ret.pde = makeUserPDELargePage(base, attr, vmRights);
919 ret.status = EXCEPTION_NONE;
920 return ret;
921 }
922
923
decodeX86FrameInvocation(word_t invLabel,word_t length,cte_t * cte,cap_t cap,word_t * buffer)924 exception_t decodeX86FrameInvocation(
925 word_t invLabel,
926 word_t length,
927 cte_t *cte,
928 cap_t cap,
929 word_t *buffer
930 )
931 {
932 switch (invLabel) {
933 case X86PageMap: { /* Map */
934 word_t vaddr;
935 word_t vtop;
936 word_t w_rightsMask;
937 paddr_t paddr;
938 cap_t vspaceCap;
939 vspace_root_t *vspace;
940 vm_rights_t capVMRights;
941 vm_rights_t vmRights;
942 vm_attributes_t vmAttr;
943 vm_page_size_t frameSize;
944 asid_t asid;
945
946 if (length < 3 || current_extra_caps.excaprefs[0] == NULL) {
947 current_syscall_error.type = seL4_TruncatedMessage;
948
949 return EXCEPTION_SYSCALL_ERROR;
950 }
951
952 frameSize = cap_frame_cap_get_capFSize(cap);
953 vaddr = getSyscallArg(0, buffer);
954 w_rightsMask = getSyscallArg(1, buffer);
955 vmAttr = vmAttributesFromWord(getSyscallArg(2, buffer));
956 vspaceCap = current_extra_caps.excaprefs[0]->cap;
957
958 capVMRights = cap_frame_cap_get_capFVMRights(cap);
959
960 if (!isValidNativeRoot(vspaceCap)) {
961 userError("X86FrameMap: Attempting to map frame into invalid page directory cap.");
962 current_syscall_error.type = seL4_InvalidCapability;
963 current_syscall_error.invalidCapNumber = 1;
964
965 return EXCEPTION_SYSCALL_ERROR;
966 }
967 vspace = (vspace_root_t *)pptr_of_cap(vspaceCap);
968 asid = cap_get_capMappedASID(vspaceCap);
969
970 if (cap_frame_cap_get_capFMappedASID(cap) != asidInvalid) {
971 if (cap_frame_cap_get_capFMappedASID(cap) != asid) {
972 current_syscall_error.type = seL4_InvalidCapability;
973 current_syscall_error.invalidCapNumber = 1;
974
975 return EXCEPTION_SYSCALL_ERROR;
976 }
977
978 if (cap_frame_cap_get_capFMapType(cap) != X86_MappingVSpace) {
979 userError("X86Frame: Attempting to remap frame with different mapping type");
980 current_syscall_error.type = seL4_IllegalOperation;
981
982 return EXCEPTION_SYSCALL_ERROR;
983 }
984
985 if (cap_frame_cap_get_capFMappedAddress(cap) != vaddr) {
986 userError("X86Frame: Attempting to map frame into multiple addresses");
987 current_syscall_error.type = seL4_InvalidArgument;
988 current_syscall_error.invalidArgumentNumber = 0;
989
990 return EXCEPTION_SYSCALL_ERROR;
991 }
992 } else {
993 vtop = vaddr + BIT(pageBitsForSize(frameSize));
994
995 /* check vaddr and vtop against USER_TOP to catch case where vaddr + frame_size wrapped around */
996 if (vaddr > USER_TOP || vtop > USER_TOP) {
997 userError("X86Frame: Mapping address too high.");
998 current_syscall_error.type = seL4_InvalidArgument;
999 current_syscall_error.invalidArgumentNumber = 0;
1000
1001 return EXCEPTION_SYSCALL_ERROR;
1002 }
1003 }
1004
1005 {
1006 findVSpaceForASID_ret_t find_ret;
1007
1008 find_ret = findVSpaceForASID(asid);
1009 if (find_ret.status != EXCEPTION_NONE) {
1010 current_syscall_error.type = seL4_FailedLookup;
1011 current_syscall_error.failedLookupWasSource = false;
1012
1013 return EXCEPTION_SYSCALL_ERROR;
1014 }
1015
1016 if (find_ret.vspace_root != vspace) {
1017 current_syscall_error.type = seL4_InvalidCapability;
1018 current_syscall_error.invalidCapNumber = 1;
1019
1020 return EXCEPTION_SYSCALL_ERROR;
1021 }
1022 }
1023
1024 vmRights = maskVMRights(capVMRights, rightsFromWord(w_rightsMask));
1025
1026 if (!checkVPAlignment(frameSize, vaddr)) {
1027 current_syscall_error.type = seL4_AlignmentError;
1028
1029 return EXCEPTION_SYSCALL_ERROR;
1030 }
1031
1032 paddr = pptr_to_paddr((void *)cap_frame_cap_get_capFBasePtr(cap));
1033
1034 cap = cap_frame_cap_set_capFMappedASID(cap, asid);
1035 cap = cap_frame_cap_set_capFMappedAddress(cap, vaddr);
1036 cap = cap_frame_cap_set_capFMapType(cap, X86_MappingVSpace);
1037
1038 switch (frameSize) {
1039 /* PTE mappings */
1040 case X86_SmallPage: {
1041 create_mapping_pte_return_t map_ret;
1042
1043 map_ret = createSafeMappingEntries_PTE(paddr, vaddr, vmRights, vmAttr, vspace);
1044 if (map_ret.status != EXCEPTION_NONE) {
1045 return map_ret.status;
1046 }
1047
1048 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1049 return performX86PageInvocationMapPTE(cap, cte, map_ret.ptSlot, map_ret.pte, vspace);
1050 }
1051
1052 /* PDE mappings */
1053 case X86_LargePage: {
1054 create_mapping_pde_return_t map_ret;
1055
1056 map_ret = createSafeMappingEntries_PDE(paddr, vaddr, vmRights, vmAttr, vspace);
1057 if (map_ret.status != EXCEPTION_NONE) {
1058 return map_ret.status;
1059 }
1060
1061 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1062 return performX86PageInvocationMapPDE(cap, cte, map_ret.pdSlot, map_ret.pde, vspace);
1063 }
1064
1065 default: {
1066 return decodeX86ModeMapPage(invLabel, frameSize, cte, cap, vspace, vaddr, paddr, vmRights, vmAttr);
1067 }
1068 }
1069
1070 return EXCEPTION_SYSCALL_ERROR;
1071 }
1072
1073 case X86PageUnmap: { /* Unmap */
1074 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1075 return performX86FrameInvocationUnmap(cap, cte);
1076 }
1077
1078 #ifdef CONFIG_IOMMU
1079 case X86PageMapIO: { /* MapIO */
1080 return decodeX86IOMapInvocation(length, cte, cap, buffer);
1081 }
1082 #endif
1083
1084 #ifdef CONFIG_VTX
1085 case X86PageMapEPT:
1086 return decodeX86EPTPageMap(invLabel, length, cte, cap, buffer);
1087 #endif
1088
1089 case X86PageGetAddress: {
1090 /* Return it in the first message register. */
1091 assert(n_msgRegisters >= 1);
1092
1093 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1094 return performPageGetAddress((void *)cap_frame_cap_get_capFBasePtr(cap));
1095 }
1096
1097 default:
1098 current_syscall_error.type = seL4_IllegalOperation;
1099
1100 return EXCEPTION_SYSCALL_ERROR;
1101 }
1102 }
1103
performX86PageTableInvocationUnmap(cap_t cap,cte_t * ctSlot)1104 static exception_t performX86PageTableInvocationUnmap(cap_t cap, cte_t *ctSlot)
1105 {
1106
1107 if (cap_page_table_cap_get_capPTIsMapped(cap)) {
1108 pte_t *pt = PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap));
1109 unmapPageTable(
1110 cap_page_table_cap_get_capPTMappedASID(cap),
1111 cap_page_table_cap_get_capPTMappedAddress(cap),
1112 pt
1113 );
1114 clearMemory((void *)pt, cap_get_capSizeBits(cap));
1115 }
1116 cap_page_table_cap_ptr_set_capPTIsMapped(&(ctSlot->cap), 0);
1117
1118 return EXCEPTION_NONE;
1119 }
1120
performX86PageTableInvocationMap(cap_t cap,cte_t * ctSlot,pde_t pde,pde_t * pdSlot,vspace_root_t * root)1121 static exception_t performX86PageTableInvocationMap(cap_t cap, cte_t *ctSlot, pde_t pde, pde_t *pdSlot,
1122 vspace_root_t *root)
1123 {
1124 ctSlot->cap = cap;
1125 *pdSlot = pde;
1126 invalidatePageStructureCacheASID(pptr_to_paddr(root), cap_page_table_cap_get_capPTMappedASID(cap),
1127 SMP_TERNARY(tlb_bitmap_get(root), 0));
1128 return EXCEPTION_NONE;
1129 }
1130
decodeX86PageTableInvocation(word_t invLabel,word_t length,cte_t * cte,cap_t cap,word_t * buffer)1131 static exception_t decodeX86PageTableInvocation(
1132 word_t invLabel,
1133 word_t length,
1134 cte_t *cte, cap_t cap,
1135 word_t *buffer
1136 )
1137 {
1138 word_t vaddr;
1139 vm_attributes_t attr;
1140 lookupPDSlot_ret_t pdSlot;
1141 cap_t vspaceCap;
1142 vspace_root_t *vspace;
1143 pde_t pde;
1144 paddr_t paddr;
1145 asid_t asid;
1146
1147 if (invLabel == X86PageTableUnmap) {
1148 if (! isFinalCapability(cte)) {
1149 current_syscall_error.type = seL4_RevokeFirst;
1150 userError("X86PageTable: Cannot unmap if more than one cap exists.");
1151 return EXCEPTION_SYSCALL_ERROR;
1152 }
1153 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1154 return performX86PageTableInvocationUnmap(cap, cte);
1155 }
1156
1157 if (invLabel != X86PageTableMap) {
1158 userError("X86PageTable: Illegal operation.");
1159 current_syscall_error.type = seL4_IllegalOperation;
1160 return EXCEPTION_SYSCALL_ERROR;
1161 }
1162
1163 if (length < 2 || current_extra_caps.excaprefs[0] == NULL) {
1164 userError("X86PageTable: Truncated message.");
1165 current_syscall_error.type = seL4_TruncatedMessage;
1166 return EXCEPTION_SYSCALL_ERROR;
1167 }
1168
1169 if (cap_page_table_cap_get_capPTIsMapped(cap)) {
1170 userError("X86PageTable: Page table is already mapped to a page directory.");
1171 current_syscall_error.type =
1172 seL4_InvalidCapability;
1173 current_syscall_error.invalidCapNumber = 0;
1174
1175 return EXCEPTION_SYSCALL_ERROR;
1176 }
1177
1178 vaddr = getSyscallArg(0, buffer) & (~MASK(PT_INDEX_BITS + PAGE_BITS));
1179 attr = vmAttributesFromWord(getSyscallArg(1, buffer));
1180 vspaceCap = current_extra_caps.excaprefs[0]->cap;
1181
1182 if (!isValidNativeRoot(vspaceCap)) {
1183 current_syscall_error.type = seL4_InvalidCapability;
1184 current_syscall_error.invalidCapNumber = 1;
1185
1186 return EXCEPTION_SYSCALL_ERROR;
1187 }
1188
1189 vspace = (vspace_root_t *)pptr_of_cap(vspaceCap);
1190 asid = cap_get_capMappedASID(vspaceCap);
1191
1192 if (vaddr > USER_TOP) {
1193 userError("X86PageTable: Mapping address too high.");
1194 current_syscall_error.type = seL4_InvalidArgument;
1195 current_syscall_error.invalidArgumentNumber = 0;
1196
1197 return EXCEPTION_SYSCALL_ERROR;
1198 }
1199
1200 {
1201 findVSpaceForASID_ret_t find_ret;
1202
1203 find_ret = findVSpaceForASID(asid);
1204 if (find_ret.status != EXCEPTION_NONE) {
1205 current_syscall_error.type = seL4_FailedLookup;
1206 current_syscall_error.failedLookupWasSource = false;
1207
1208 return EXCEPTION_SYSCALL_ERROR;
1209 }
1210
1211 if (find_ret.vspace_root != vspace) {
1212 current_syscall_error.type = seL4_InvalidCapability;
1213 current_syscall_error.invalidCapNumber = 1;
1214
1215 return EXCEPTION_SYSCALL_ERROR;
1216 }
1217 }
1218
1219 pdSlot = lookupPDSlot(vspace, vaddr);
1220 if (pdSlot.status != EXCEPTION_NONE) {
1221 current_syscall_error.type = seL4_FailedLookup;
1222 current_syscall_error.failedLookupWasSource = false;
1223
1224 return EXCEPTION_SYSCALL_ERROR;
1225 }
1226
1227 if (((pde_ptr_get_page_size(pdSlot.pdSlot) == pde_pde_pt) && pde_pde_pt_ptr_get_present(pdSlot.pdSlot)) ||
1228 ((pde_ptr_get_page_size(pdSlot.pdSlot) == pde_pde_large) && pde_pde_large_ptr_get_present(pdSlot.pdSlot))) {
1229 current_syscall_error.type = seL4_DeleteFirst;
1230
1231 return EXCEPTION_SYSCALL_ERROR;
1232 }
1233
1234 paddr = pptr_to_paddr(PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap)));
1235 pde = makeUserPDEPageTable(paddr, attr);
1236
1237 cap = cap_page_table_cap_set_capPTIsMapped(cap, 1);
1238 cap = cap_page_table_cap_set_capPTMappedASID(cap, asid);
1239 cap = cap_page_table_cap_set_capPTMappedAddress(cap, vaddr);
1240
1241 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1242 return performX86PageTableInvocationMap(cap, cte, pde, pdSlot.pdSlot, vspace);
1243 }
1244
decodeX86MMUInvocation(word_t invLabel,word_t length,cptr_t cptr,cte_t * cte,cap_t cap,word_t * buffer)1245 exception_t decodeX86MMUInvocation(
1246 word_t invLabel,
1247 word_t length,
1248 cptr_t cptr,
1249 cte_t *cte,
1250 cap_t cap,
1251 word_t *buffer
1252 )
1253 {
1254 switch (cap_get_capType(cap)) {
1255
1256 case cap_frame_cap:
1257 return decodeX86FrameInvocation(invLabel, length, cte, cap, buffer);
1258
1259 case cap_page_table_cap:
1260 return decodeX86PageTableInvocation(invLabel, length, cte, cap, buffer);
1261
1262 case cap_asid_control_cap: {
1263 word_t i;
1264 asid_t asid_base;
1265 word_t index;
1266 word_t depth;
1267 cap_t untyped;
1268 cap_t root;
1269 cte_t *parentSlot;
1270 cte_t *destSlot;
1271 lookupSlot_ret_t lu_ret;
1272 void *frame;
1273 exception_t status;
1274
1275 if (invLabel != X86ASIDControlMakePool) {
1276 current_syscall_error.type = seL4_IllegalOperation;
1277
1278 return EXCEPTION_SYSCALL_ERROR;
1279 }
1280
1281 if (length < 2 || current_extra_caps.excaprefs[0] == NULL
1282 || current_extra_caps.excaprefs[1] == NULL) {
1283 current_syscall_error.type = seL4_TruncatedMessage;
1284 return EXCEPTION_SYSCALL_ERROR;
1285 }
1286
1287 index = getSyscallArg(0, buffer);
1288 depth = getSyscallArg(1, buffer);
1289 parentSlot = current_extra_caps.excaprefs[0];
1290 untyped = parentSlot->cap;
1291 root = current_extra_caps.excaprefs[1]->cap;
1292
1293 /* Find first free pool */
1294 for (i = 0; i < nASIDPools && x86KSASIDTable[i]; i++);
1295
1296 if (i == nASIDPools) {
1297 /* no unallocated pool is found */
1298 current_syscall_error.type = seL4_DeleteFirst;
1299
1300 return EXCEPTION_SYSCALL_ERROR;
1301 }
1302
1303 asid_base = i << asidLowBits;
1304
1305
1306 if (cap_get_capType(untyped) != cap_untyped_cap ||
1307 cap_untyped_cap_get_capBlockSize(untyped) != seL4_ASIDPoolBits ||
1308 cap_untyped_cap_get_capIsDevice(untyped)) {
1309 current_syscall_error.type = seL4_InvalidCapability;
1310 current_syscall_error.invalidCapNumber = 1;
1311
1312 return EXCEPTION_SYSCALL_ERROR;
1313 }
1314
1315 status = ensureNoChildren(parentSlot);
1316 if (status != EXCEPTION_NONE) {
1317 return status;
1318 }
1319
1320 frame = WORD_PTR(cap_untyped_cap_get_capPtr(untyped));
1321
1322 lu_ret = lookupTargetSlot(root, index, depth);
1323 if (lu_ret.status != EXCEPTION_NONE) {
1324 return lu_ret.status;
1325 }
1326 destSlot = lu_ret.slot;
1327
1328 status = ensureEmptySlot(destSlot);
1329 if (status != EXCEPTION_NONE) {
1330 return status;
1331 }
1332
1333 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1334 return performASIDControlInvocation(frame, destSlot, parentSlot, asid_base);
1335 }
1336
1337 case cap_asid_pool_cap: {
1338 cap_t vspaceCap;
1339 cte_t *vspaceCapSlot;
1340 asid_pool_t *pool;
1341 word_t i;
1342 asid_t asid;
1343
1344 if (invLabel != X86ASIDPoolAssign) {
1345 current_syscall_error.type = seL4_IllegalOperation;
1346
1347 return EXCEPTION_SYSCALL_ERROR;
1348 }
1349 if (current_extra_caps.excaprefs[0] == NULL) {
1350 current_syscall_error.type = seL4_TruncatedMessage;
1351
1352 return EXCEPTION_SYSCALL_ERROR;
1353 }
1354
1355 vspaceCapSlot = current_extra_caps.excaprefs[0];
1356 vspaceCap = vspaceCapSlot->cap;
1357
1358 if (!(isVTableRoot(vspaceCap) || VTX_TERNARY(cap_get_capType(vspaceCap) == cap_ept_pml4_cap, 0))
1359 || cap_get_capMappedASID(vspaceCap) != asidInvalid) {
1360 userError("X86ASIDPool: Invalid vspace root.");
1361 current_syscall_error.type = seL4_InvalidCapability;
1362 current_syscall_error.invalidCapNumber = 1;
1363
1364 return EXCEPTION_SYSCALL_ERROR;
1365 }
1366
1367 pool = x86KSASIDTable[cap_asid_pool_cap_get_capASIDBase(cap) >> asidLowBits];
1368 if (!pool) {
1369 current_syscall_error.type = seL4_FailedLookup;
1370 current_syscall_error.failedLookupWasSource = false;
1371 current_lookup_fault = lookup_fault_invalid_root_new();
1372 return EXCEPTION_SYSCALL_ERROR;
1373 }
1374
1375 if (pool != ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))) {
1376 current_syscall_error.type = seL4_InvalidCapability;
1377 current_syscall_error.invalidCapNumber = 0;
1378 return EXCEPTION_SYSCALL_ERROR;
1379 }
1380
1381 /* Find first free ASID */
1382 asid = cap_asid_pool_cap_get_capASIDBase(cap);
1383 for (i = 0; i < BIT(asidLowBits) && (asid + i == 0
1384 || asid_map_get_type(pool->array[i]) != asid_map_asid_map_none); i++);
1385
1386 if (i == BIT(asidLowBits)) {
1387 current_syscall_error.type = seL4_DeleteFirst;
1388
1389 return EXCEPTION_SYSCALL_ERROR;
1390 }
1391
1392 asid += i;
1393
1394 setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1395 return performASIDPoolInvocation(asid, pool, vspaceCapSlot);
1396 }
1397
1398 default:
1399 return decodeX86ModeMMUInvocation(invLabel, length, cptr, cte, cap, buffer);
1400 }
1401 }
1402