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
18static 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
34void 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
52exception_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
77void 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
93word_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
121bool_t CONST isValidVTableRoot(cap_t cap)
122{
123    return isValidNativeRoot(cap);
124}
125
126
127BOOT_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
202BOOT_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
477BOOT_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
503BOOT_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
526BOOT_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
533asid_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
545findVSpaceForASID_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
564exception_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
586uint32_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
601uint32_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
616lookupPTSlot_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
648exception_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
670vm_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
685void 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
707void 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
759void 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
789static 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
799static 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
810static 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
833static 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
856struct create_mapping_pte_return {
857    exception_t status;
858    pte_t pte;
859    pte_t *ptSlot;
860};
861typedef struct create_mapping_pte_return create_mapping_pte_return_t;
862
863static 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
885struct create_mapping_pde_return {
886    exception_t status;
887    pde_t pde;
888    pde_t *pdSlot;
889};
890typedef struct create_mapping_pde_return create_mapping_pde_return_t;
891
892static 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
924exception_t decodeX86FrameInvocation(
925    word_t invLabel,
926    word_t length,
927    cte_t *cte,
928    cap_t cap,
929    extra_caps_t excaps,
930    word_t *buffer
931)
932{
933    switch (invLabel) {
934    case X86PageMap: { /* Map */
935        word_t          vaddr;
936        word_t          vtop;
937        word_t          w_rightsMask;
938        paddr_t         paddr;
939        cap_t           vspaceCap;
940        vspace_root_t  *vspace;
941        vm_rights_t     capVMRights;
942        vm_rights_t     vmRights;
943        vm_attributes_t vmAttr;
944        vm_page_size_t  frameSize;
945        asid_t          asid;
946
947        if (length < 3 || excaps.excaprefs[0] == NULL) {
948            current_syscall_error.type = seL4_TruncatedMessage;
949
950            return EXCEPTION_SYSCALL_ERROR;
951        }
952
953        frameSize = cap_frame_cap_get_capFSize(cap);
954        vaddr = getSyscallArg(0, buffer);
955        w_rightsMask = getSyscallArg(1, buffer);
956        vmAttr = vmAttributesFromWord(getSyscallArg(2, buffer));
957        vspaceCap = excaps.excaprefs[0]->cap;
958
959        capVMRights = cap_frame_cap_get_capFVMRights(cap);
960
961        if (!isValidNativeRoot(vspaceCap)) {
962            userError("X86FrameMap: Attempting to map frame into invalid page directory cap.");
963            current_syscall_error.type = seL4_InvalidCapability;
964            current_syscall_error.invalidCapNumber = 1;
965
966            return EXCEPTION_SYSCALL_ERROR;
967        }
968        vspace = (vspace_root_t *)pptr_of_cap(vspaceCap);
969        asid = cap_get_capMappedASID(vspaceCap);
970
971        if (cap_frame_cap_get_capFMappedASID(cap) != asidInvalid) {
972            if (cap_frame_cap_get_capFMappedASID(cap) != asid) {
973                current_syscall_error.type = seL4_InvalidCapability;
974                current_syscall_error.invalidCapNumber = 1;
975
976                return EXCEPTION_SYSCALL_ERROR;
977            }
978
979            if (cap_frame_cap_get_capFMapType(cap) != X86_MappingVSpace) {
980                userError("X86Frame: Attempting to remap frame with different mapping type");
981                current_syscall_error.type = seL4_IllegalOperation;
982
983                return EXCEPTION_SYSCALL_ERROR;
984            }
985
986            if (cap_frame_cap_get_capFMappedAddress(cap) != vaddr) {
987                userError("X86Frame: Attempting to map frame into multiple addresses");
988                current_syscall_error.type = seL4_InvalidArgument;
989                current_syscall_error.invalidArgumentNumber = 0;
990
991                return EXCEPTION_SYSCALL_ERROR;
992            }
993        } else {
994            vtop = vaddr + BIT(pageBitsForSize(frameSize));
995
996            /* check vaddr and vtop against USER_TOP to catch case where vaddr + frame_size wrapped around */
997            if (vaddr > USER_TOP || vtop > USER_TOP) {
998                userError("X86Frame: Mapping address too high.");
999                current_syscall_error.type = seL4_InvalidArgument;
1000                current_syscall_error.invalidArgumentNumber = 0;
1001
1002                return EXCEPTION_SYSCALL_ERROR;
1003            }
1004        }
1005
1006        {
1007            findVSpaceForASID_ret_t find_ret;
1008
1009            find_ret = findVSpaceForASID(asid);
1010            if (find_ret.status != EXCEPTION_NONE) {
1011                current_syscall_error.type = seL4_FailedLookup;
1012                current_syscall_error.failedLookupWasSource = false;
1013
1014                return EXCEPTION_SYSCALL_ERROR;
1015            }
1016
1017            if (find_ret.vspace_root != vspace) {
1018                current_syscall_error.type = seL4_InvalidCapability;
1019                current_syscall_error.invalidCapNumber = 1;
1020
1021                return EXCEPTION_SYSCALL_ERROR;
1022            }
1023        }
1024
1025        vmRights = maskVMRights(capVMRights, rightsFromWord(w_rightsMask));
1026
1027        if (!checkVPAlignment(frameSize, vaddr)) {
1028            current_syscall_error.type = seL4_AlignmentError;
1029
1030            return EXCEPTION_SYSCALL_ERROR;
1031        }
1032
1033        paddr = pptr_to_paddr((void *)cap_frame_cap_get_capFBasePtr(cap));
1034
1035        cap = cap_frame_cap_set_capFMappedASID(cap, asid);
1036        cap = cap_frame_cap_set_capFMappedAddress(cap, vaddr);
1037        cap = cap_frame_cap_set_capFMapType(cap, X86_MappingVSpace);
1038
1039        switch (frameSize) {
1040        /* PTE mappings */
1041        case X86_SmallPage: {
1042            create_mapping_pte_return_t map_ret;
1043
1044            map_ret = createSafeMappingEntries_PTE(paddr, vaddr, vmRights, vmAttr, vspace);
1045            if (map_ret.status != EXCEPTION_NONE) {
1046                return map_ret.status;
1047            }
1048
1049            setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1050            return performX86PageInvocationMapPTE(cap, cte, map_ret.ptSlot, map_ret.pte, vspace);
1051        }
1052
1053        /* PDE mappings */
1054        case X86_LargePage: {
1055            create_mapping_pde_return_t map_ret;
1056
1057            map_ret = createSafeMappingEntries_PDE(paddr, vaddr, vmRights, vmAttr, vspace);
1058            if (map_ret.status != EXCEPTION_NONE) {
1059                return map_ret.status;
1060            }
1061
1062            setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1063            return performX86PageInvocationMapPDE(cap, cte, map_ret.pdSlot, map_ret.pde, vspace);
1064        }
1065
1066        default: {
1067            return decodeX86ModeMapPage(invLabel, frameSize, cte, cap, vspace, vaddr, paddr, vmRights, vmAttr);
1068        }
1069        }
1070
1071        return EXCEPTION_SYSCALL_ERROR;
1072    }
1073
1074    case X86PageUnmap: { /* Unmap */
1075        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1076        return performX86FrameInvocationUnmap(cap, cte);
1077    }
1078
1079#ifdef CONFIG_IOMMU
1080    case X86PageMapIO: { /* MapIO */
1081        return decodeX86IOMapInvocation(length, cte, cap, excaps, buffer);
1082    }
1083#endif
1084
1085#ifdef CONFIG_VTX
1086    case X86PageMapEPT:
1087        return decodeX86EPTPageMap(invLabel, length, cte, cap, excaps, buffer);
1088#endif
1089
1090    case X86PageGetAddress: {
1091        /* Return it in the first message register. */
1092        assert(n_msgRegisters >= 1);
1093
1094        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1095        return performPageGetAddress((void *)cap_frame_cap_get_capFBasePtr(cap));
1096    }
1097
1098    default:
1099        current_syscall_error.type = seL4_IllegalOperation;
1100
1101        return EXCEPTION_SYSCALL_ERROR;
1102    }
1103}
1104
1105static exception_t performX86PageTableInvocationUnmap(cap_t cap, cte_t *ctSlot)
1106{
1107
1108    if (cap_page_table_cap_get_capPTIsMapped(cap)) {
1109        pte_t *pt = PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap));
1110        unmapPageTable(
1111            cap_page_table_cap_get_capPTMappedASID(cap),
1112            cap_page_table_cap_get_capPTMappedAddress(cap),
1113            pt
1114        );
1115        clearMemory((void *)pt, cap_get_capSizeBits(cap));
1116    }
1117    cap_page_table_cap_ptr_set_capPTIsMapped(&(ctSlot->cap), 0);
1118
1119    return EXCEPTION_NONE;
1120}
1121
1122static exception_t performX86PageTableInvocationMap(cap_t cap, cte_t *ctSlot, pde_t pde, pde_t *pdSlot,
1123                                                    vspace_root_t *root)
1124{
1125    ctSlot->cap = cap;
1126    *pdSlot = pde;
1127    invalidatePageStructureCacheASID(pptr_to_paddr(root), cap_page_table_cap_get_capPTMappedASID(cap),
1128                                     SMP_TERNARY(tlb_bitmap_get(root), 0));
1129    return EXCEPTION_NONE;
1130}
1131
1132static exception_t decodeX86PageTableInvocation(
1133    word_t invLabel,
1134    word_t length,
1135    cte_t *cte, cap_t cap,
1136    extra_caps_t excaps,
1137    word_t *buffer
1138)
1139{
1140    word_t          vaddr;
1141    vm_attributes_t attr;
1142    lookupPDSlot_ret_t pdSlot;
1143    cap_t           vspaceCap;
1144    vspace_root_t  *vspace;
1145    pde_t           pde;
1146    paddr_t         paddr;
1147    asid_t          asid;
1148
1149    if (invLabel == X86PageTableUnmap) {
1150        if (! isFinalCapability(cte)) {
1151            current_syscall_error.type = seL4_RevokeFirst;
1152            userError("X86PageTable: Cannot unmap if more than one cap exists.");
1153            return EXCEPTION_SYSCALL_ERROR;
1154        }
1155        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1156        return performX86PageTableInvocationUnmap(cap, cte);
1157    }
1158
1159    if (invLabel != X86PageTableMap) {
1160        userError("X86PageTable: Illegal operation.");
1161        current_syscall_error.type = seL4_IllegalOperation;
1162        return EXCEPTION_SYSCALL_ERROR;
1163    }
1164
1165    if (length < 2 || excaps.excaprefs[0] == NULL) {
1166        userError("X86PageTable: Truncated message.");
1167        current_syscall_error.type = seL4_TruncatedMessage;
1168        return EXCEPTION_SYSCALL_ERROR;
1169    }
1170
1171    if (cap_page_table_cap_get_capPTIsMapped(cap)) {
1172        userError("X86PageTable: Page table is already mapped to a page directory.");
1173        current_syscall_error.type =
1174            seL4_InvalidCapability;
1175        current_syscall_error.invalidCapNumber = 0;
1176
1177        return EXCEPTION_SYSCALL_ERROR;
1178    }
1179
1180    vaddr = getSyscallArg(0, buffer) & (~MASK(PT_INDEX_BITS + PAGE_BITS));
1181    attr = vmAttributesFromWord(getSyscallArg(1, buffer));
1182    vspaceCap = excaps.excaprefs[0]->cap;
1183
1184    if (!isValidNativeRoot(vspaceCap)) {
1185        current_syscall_error.type = seL4_InvalidCapability;
1186        current_syscall_error.invalidCapNumber = 1;
1187
1188        return EXCEPTION_SYSCALL_ERROR;
1189    }
1190
1191    vspace = (vspace_root_t *)pptr_of_cap(vspaceCap);
1192    asid = cap_get_capMappedASID(vspaceCap);
1193
1194    if (vaddr > USER_TOP) {
1195        userError("X86PageTable: Mapping address too high.");
1196        current_syscall_error.type = seL4_InvalidArgument;
1197        current_syscall_error.invalidArgumentNumber = 0;
1198
1199        return EXCEPTION_SYSCALL_ERROR;
1200    }
1201
1202    {
1203        findVSpaceForASID_ret_t find_ret;
1204
1205        find_ret = findVSpaceForASID(asid);
1206        if (find_ret.status != EXCEPTION_NONE) {
1207            current_syscall_error.type = seL4_FailedLookup;
1208            current_syscall_error.failedLookupWasSource = false;
1209
1210            return EXCEPTION_SYSCALL_ERROR;
1211        }
1212
1213        if (find_ret.vspace_root != vspace) {
1214            current_syscall_error.type = seL4_InvalidCapability;
1215            current_syscall_error.invalidCapNumber = 1;
1216
1217            return EXCEPTION_SYSCALL_ERROR;
1218        }
1219    }
1220
1221    pdSlot = lookupPDSlot(vspace, vaddr);
1222    if (pdSlot.status != EXCEPTION_NONE) {
1223        current_syscall_error.type = seL4_FailedLookup;
1224        current_syscall_error.failedLookupWasSource = false;
1225
1226        return EXCEPTION_SYSCALL_ERROR;
1227    }
1228
1229    if (((pde_ptr_get_page_size(pdSlot.pdSlot) == pde_pde_pt) && pde_pde_pt_ptr_get_present(pdSlot.pdSlot)) ||
1230        ((pde_ptr_get_page_size(pdSlot.pdSlot) == pde_pde_large) && pde_pde_large_ptr_get_present(pdSlot.pdSlot))) {
1231        current_syscall_error.type = seL4_DeleteFirst;
1232
1233        return EXCEPTION_SYSCALL_ERROR;
1234    }
1235
1236    paddr = pptr_to_paddr(PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap)));
1237    pde = makeUserPDEPageTable(paddr, attr);
1238
1239    cap = cap_page_table_cap_set_capPTIsMapped(cap, 1);
1240    cap = cap_page_table_cap_set_capPTMappedASID(cap, asid);
1241    cap = cap_page_table_cap_set_capPTMappedAddress(cap, vaddr);
1242
1243    setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1244    return performX86PageTableInvocationMap(cap, cte, pde, pdSlot.pdSlot, vspace);
1245}
1246
1247exception_t decodeX86MMUInvocation(
1248    word_t invLabel,
1249    word_t length,
1250    cptr_t cptr,
1251    cte_t *cte,
1252    cap_t cap,
1253    extra_caps_t excaps,
1254    word_t *buffer
1255)
1256{
1257    switch (cap_get_capType(cap)) {
1258
1259    case cap_frame_cap:
1260        return decodeX86FrameInvocation(invLabel, length, cte, cap, excaps, buffer);
1261
1262    case cap_page_table_cap:
1263        return decodeX86PageTableInvocation(invLabel, length, cte, cap, excaps, buffer);
1264
1265    case cap_asid_control_cap: {
1266        word_t     i;
1267        asid_t           asid_base;
1268        word_t           index;
1269        word_t           depth;
1270        cap_t            untyped;
1271        cap_t            root;
1272        cte_t           *parentSlot;
1273        cte_t           *destSlot;
1274        lookupSlot_ret_t lu_ret;
1275        void            *frame;
1276        exception_t      status;
1277
1278        if (invLabel != X86ASIDControlMakePool) {
1279            current_syscall_error.type = seL4_IllegalOperation;
1280
1281            return EXCEPTION_SYSCALL_ERROR;
1282        }
1283
1284        if (length < 2 || excaps.excaprefs[0] == NULL
1285            || excaps.excaprefs[1] == NULL) {
1286            current_syscall_error.type = seL4_TruncatedMessage;
1287            return EXCEPTION_SYSCALL_ERROR;
1288        }
1289
1290        index = getSyscallArg(0, buffer);
1291        depth = getSyscallArg(1, buffer);
1292        parentSlot = excaps.excaprefs[0];
1293        untyped = parentSlot->cap;
1294        root = excaps.excaprefs[1]->cap;
1295
1296        /* Find first free pool */
1297        for (i = 0; i < nASIDPools && x86KSASIDTable[i]; i++);
1298
1299        if (i == nASIDPools) {
1300            /* no unallocated pool is found */
1301            current_syscall_error.type = seL4_DeleteFirst;
1302
1303            return EXCEPTION_SYSCALL_ERROR;
1304        }
1305
1306        asid_base = i << asidLowBits;
1307
1308
1309        if (cap_get_capType(untyped) != cap_untyped_cap ||
1310            cap_untyped_cap_get_capBlockSize(untyped) != seL4_ASIDPoolBits ||
1311            cap_untyped_cap_get_capIsDevice(untyped)) {
1312            current_syscall_error.type = seL4_InvalidCapability;
1313            current_syscall_error.invalidCapNumber = 1;
1314
1315            return EXCEPTION_SYSCALL_ERROR;
1316        }
1317
1318        status = ensureNoChildren(parentSlot);
1319        if (status != EXCEPTION_NONE) {
1320            return status;
1321        }
1322
1323        frame = WORD_PTR(cap_untyped_cap_get_capPtr(untyped));
1324
1325        lu_ret = lookupTargetSlot(root, index, depth);
1326        if (lu_ret.status != EXCEPTION_NONE) {
1327            return lu_ret.status;
1328        }
1329        destSlot = lu_ret.slot;
1330
1331        status = ensureEmptySlot(destSlot);
1332        if (status != EXCEPTION_NONE) {
1333            return status;
1334        }
1335
1336        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1337        return performASIDControlInvocation(frame, destSlot, parentSlot, asid_base);
1338    }
1339
1340    case cap_asid_pool_cap: {
1341        cap_t        vspaceCap;
1342        cte_t       *vspaceCapSlot;
1343        asid_pool_t *pool;
1344        word_t i;
1345        asid_t       asid;
1346
1347        if (invLabel != X86ASIDPoolAssign) {
1348            current_syscall_error.type = seL4_IllegalOperation;
1349
1350            return EXCEPTION_SYSCALL_ERROR;
1351        }
1352        if (excaps.excaprefs[0] == NULL) {
1353            current_syscall_error.type = seL4_TruncatedMessage;
1354
1355            return EXCEPTION_SYSCALL_ERROR;
1356        }
1357
1358        vspaceCapSlot = excaps.excaprefs[0];
1359        vspaceCap = vspaceCapSlot->cap;
1360
1361        if (!(isVTableRoot(vspaceCap) || VTX_TERNARY(cap_get_capType(vspaceCap) == cap_ept_pml4_cap, 0))
1362            || cap_get_capMappedASID(vspaceCap) != asidInvalid) {
1363            userError("X86ASIDPool: Invalid vspace root.");
1364            current_syscall_error.type = seL4_InvalidCapability;
1365            current_syscall_error.invalidCapNumber = 1;
1366
1367            return EXCEPTION_SYSCALL_ERROR;
1368        }
1369
1370        pool = x86KSASIDTable[cap_asid_pool_cap_get_capASIDBase(cap) >> asidLowBits];
1371        if (!pool) {
1372            current_syscall_error.type = seL4_FailedLookup;
1373            current_syscall_error.failedLookupWasSource = false;
1374            current_lookup_fault = lookup_fault_invalid_root_new();
1375            return EXCEPTION_SYSCALL_ERROR;
1376        }
1377
1378        if (pool != ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))) {
1379            current_syscall_error.type = seL4_InvalidCapability;
1380            current_syscall_error.invalidCapNumber = 0;
1381            return EXCEPTION_SYSCALL_ERROR;
1382        }
1383
1384        /* Find first free ASID */
1385        asid = cap_asid_pool_cap_get_capASIDBase(cap);
1386        for (i = 0; i < BIT(asidLowBits) && (asid + i == 0
1387                                             || asid_map_get_type(pool->array[i]) != asid_map_asid_map_none); i++);
1388
1389        if (i == BIT(asidLowBits)) {
1390            current_syscall_error.type = seL4_DeleteFirst;
1391
1392            return EXCEPTION_SYSCALL_ERROR;
1393        }
1394
1395        asid += i;
1396
1397        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
1398        return performASIDPoolInvocation(asid, pool, vspaceCapSlot);
1399    }
1400
1401    default:
1402        return decodeX86ModeMMUInvocation(invLabel, length, cptr, cte, cap, excaps, buffer);
1403    }
1404}
1405