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