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(*
12Accessor functions for architecture specific parts of the specification.
13*)
14
15chapter "Accessing the x64 VSpace"
16
17theory ArchVSpaceAcc_A
18imports "../KHeap_A"
19begin
20
21context Arch begin global_naming X64_A
22
23text {*
24  This part of the specification is fairly concrete as the machine architecture
25  is visible to the user in seL4 and therefore needs to be described.
26  The abstraction compared to the implementation is in the data types for
27  kernel objects. The interface which is rich in machine details remains the same.
28*}
29
30section "Encodings"
31
32text {* The high bits of a virtual ASID. *}
33definition
34  asid_high_bits_of :: "asid \<Rightarrow> asid_high_index" where
35  "asid_high_bits_of asid \<equiv> ucast (asid >> asid_low_bits)"
36
37text {* The low bits of a virtual ASID. *}
38definition
39  asid_low_bits_of :: "asid \<Rightarrow> asid_low_index" where
40  "asid_low_bits_of asid \<equiv> ucast asid"
41
42lemmas asid_bits_of_defs =
43  asid_high_bits_of_def asid_low_bits_of_def
44
45section "Kernel Heap Accessors"
46
47text {* Manipulate ASID pools, page directories and page tables in the kernel
48heap. *}
49definition
50  get_asid_pool :: "obj_ref \<Rightarrow> (asid_low_index \<rightharpoonup> obj_ref, 'z::state_ext) s_monad" where
51  "get_asid_pool ptr \<equiv> do
52     kobj \<leftarrow> get_object ptr;
53     (case kobj of ArchObj (ASIDPool pool) \<Rightarrow> return pool
54                 | _ \<Rightarrow> fail)
55   od"
56
57definition
58  set_asid_pool :: "obj_ref \<Rightarrow> (asid_low_index \<rightharpoonup> obj_ref) \<Rightarrow> (unit, 'z::state_ext) s_monad" where
59 "set_asid_pool ptr pool \<equiv> do
60    v \<leftarrow> get_object ptr;
61    assert (case v of ArchObj (arch_kernel_obj.ASIDPool p) \<Rightarrow> True | _ \<Rightarrow> False);
62    set_object ptr (ArchObj (arch_kernel_obj.ASIDPool pool))
63  od"
64
65definition
66  get_pd :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pde,'z::state_ext) s_monad" where
67  "get_pd ptr \<equiv> do
68     kobj \<leftarrow> get_object ptr;
69     (case kobj of ArchObj (PageDirectory pd) \<Rightarrow> return pd
70                 | _ \<Rightarrow> fail)
71   od"
72
73definition
74  set_pd :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pde) \<Rightarrow> (unit,'z::state_ext) s_monad" where
75  "set_pd ptr pd \<equiv> do
76     kobj \<leftarrow> get_object ptr;
77     assert (case kobj of ArchObj (PageDirectory pd) \<Rightarrow> True | _ \<Rightarrow> False);
78     set_object ptr (ArchObj (PageDirectory pd))
79   od"
80
81text {* The following function takes a pointer to a PDE in kernel memory
82  and returns the actual PDE. *}
83definition
84  get_pde :: "obj_ref \<Rightarrow> (pde,'z::state_ext) s_monad" where
85  "get_pde ptr \<equiv> do
86     base \<leftarrow> return (ptr && ~~mask pd_bits);
87     offset \<leftarrow> return ((ptr && mask pd_bits) >> word_size_bits);
88     pd \<leftarrow> get_pd base;
89     return $ pd (ucast offset)
90   od"
91
92definition
93  store_pde :: "obj_ref \<Rightarrow> pde \<Rightarrow> (unit,'z::state_ext) s_monad" where
94  "store_pde p pde \<equiv> do
95    base \<leftarrow> return (p && ~~mask pd_bits);
96    offset \<leftarrow> return ((p && mask pd_bits) >> word_size_bits);
97    pd \<leftarrow> get_pd base;
98    pd' \<leftarrow> return $ pd (ucast offset := pde);
99    set_pd base pd'
100  od"
101
102
103definition
104  get_pt :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pte,'z::state_ext) s_monad" where
105  "get_pt ptr \<equiv> do
106     kobj \<leftarrow> get_object ptr;
107     (case kobj of ArchObj (PageTable pt) \<Rightarrow> return pt
108                 | _ \<Rightarrow> fail)
109   od"
110
111definition
112  set_pt :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pte) \<Rightarrow> (unit,'z::state_ext) s_monad" where
113  "set_pt ptr pt \<equiv> do
114     kobj \<leftarrow> get_object ptr;
115     assert (case kobj of ArchObj (PageTable _) \<Rightarrow> True | _ \<Rightarrow> False);
116     set_object ptr (ArchObj (PageTable pt))
117   od"
118
119text {* The following function takes a pointer to a PTE in kernel memory
120  and returns the actual PTE. *}
121definition
122  get_pte :: "obj_ref \<Rightarrow> (pte,'z::state_ext) s_monad" where
123  "get_pte ptr \<equiv> do
124     base \<leftarrow> return (ptr && ~~mask pt_bits);
125     offset \<leftarrow> return ((ptr && mask pt_bits) >> word_size_bits);
126     pt \<leftarrow> get_pt base;
127     return $ pt (ucast offset)
128   od"
129
130definition
131  store_pte :: "obj_ref \<Rightarrow> pte \<Rightarrow> (unit,'z::state_ext) s_monad" where
132  "store_pte p pte \<equiv> do
133    base \<leftarrow> return (p && ~~mask pt_bits);
134    offset \<leftarrow> return ((p && mask pt_bits) >> word_size_bits);
135    pt \<leftarrow> get_pt base;
136    pt' \<leftarrow> return $ pt (ucast offset := pte);
137    set_pt base pt'
138  od"
139
140definition
141  get_pdpt :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pdpte,'z::state_ext) s_monad" where
142  "get_pdpt ptr \<equiv> do
143     kobj \<leftarrow> get_object ptr;
144     (case kobj of ArchObj (PDPointerTable pt) \<Rightarrow> return pt
145                 | _ \<Rightarrow> fail)
146   od"
147
148definition
149  set_pdpt :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pdpte) \<Rightarrow> (unit,'z::state_ext) s_monad" where
150  "set_pdpt ptr pt \<equiv> do
151     kobj \<leftarrow> get_object ptr;
152     assert (case kobj of ArchObj (PDPointerTable _) \<Rightarrow> True | _ \<Rightarrow> False);
153     set_object ptr (ArchObj (PDPointerTable pt))
154   od"
155
156text {* The following function takes a pointer to a PDPTE in kernel memory
157  and returns the actual PDPTE. *}
158definition
159  get_pdpte :: "obj_ref \<Rightarrow> (pdpte,'z::state_ext) s_monad" where
160  "get_pdpte ptr \<equiv> do
161     base \<leftarrow> return (ptr && ~~mask pdpt_bits);
162     offset \<leftarrow> return ((ptr && mask pdpt_bits) >> word_size_bits);
163     pt \<leftarrow> get_pdpt base;
164     return $ pt (ucast offset)
165   od"
166
167definition
168  store_pdpte :: "obj_ref \<Rightarrow> pdpte \<Rightarrow> (unit,'z::state_ext) s_monad" where
169  "store_pdpte p pte \<equiv> do
170    base \<leftarrow> return (p && ~~mask pdpt_bits);
171    offset \<leftarrow> return ((p && mask pdpt_bits) >> word_size_bits);
172    pt \<leftarrow> get_pdpt base;
173    pt' \<leftarrow> return $ pt (ucast offset := pte);
174    set_pdpt base pt'
175  od"
176
177definition
178  get_pml4 :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pml4e,'z::state_ext) s_monad" where
179  "get_pml4 ptr \<equiv> do
180     kobj \<leftarrow> get_object ptr;
181     (case kobj of ArchObj (PageMapL4 pt) \<Rightarrow> return pt
182                 | _ \<Rightarrow> fail)
183   od"
184
185definition
186  set_pml4 :: "obj_ref \<Rightarrow> (9 word \<Rightarrow> pml4e) \<Rightarrow> (unit,'z::state_ext) s_monad" where
187  "set_pml4 ptr pt \<equiv> do
188     kobj \<leftarrow> get_object ptr;
189     assert (case kobj of ArchObj (PageMapL4 _) \<Rightarrow> True | _ \<Rightarrow> False);
190     set_object ptr (ArchObj (PageMapL4 pt))
191   od"
192
193text {* The following function takes a pointer to a PML4E in kernel memory
194  and returns the actual PML4E. *}
195definition
196  get_pml4e :: "obj_ref \<Rightarrow> (pml4e,'z::state_ext) s_monad" where
197  "get_pml4e ptr \<equiv> do
198     base \<leftarrow> return (ptr && ~~mask pml4_bits);
199     offset \<leftarrow> return ((ptr && mask pml4_bits) >> word_size_bits);
200     pt \<leftarrow> get_pml4 base;
201     return $ pt (ucast offset)
202   od"
203
204definition
205  store_pml4e :: "obj_ref \<Rightarrow> pml4e \<Rightarrow> (unit,'z::state_ext) s_monad" where
206  "store_pml4e p pte \<equiv> do
207    base \<leftarrow> return (p && ~~mask pml4_bits);
208    offset \<leftarrow> return ((p && mask pml4_bits) >> word_size_bits);
209    pt \<leftarrow> get_pml4 base;
210    pt' \<leftarrow> return $ pt (ucast offset := pte);
211    set_pml4 base pt'
212  od"
213
214
215section "Basic Operations"
216
217definition
218get_pt_index :: "vspace_ref \<Rightarrow> machine_word" where
219"get_pt_index vptr \<equiv> (vptr >> pt_shift_bits) && mask ptTranslationBits"
220
221definition
222get_pd_index :: "vspace_ref \<Rightarrow> machine_word" where
223"get_pd_index vptr \<equiv> (vptr >> (pd_shift_bits)) && mask ptTranslationBits"
224
225definition
226get_pdpt_index :: "vspace_ref \<Rightarrow> machine_word" where
227"get_pdpt_index vptr \<equiv> (vptr >> (pdpt_shift_bits)) && mask ptTranslationBits"
228
229definition
230get_pml4_index :: "vspace_ref \<Rightarrow> machine_word" where
231"get_pml4_index vptr \<equiv> (vptr >> pml4_shift_bits) && mask ptTranslationBits"
232
233text {* The kernel window is mapped into every virtual address space from the
234@{term pptr_base} pointer upwards. This function copies the mappings which
235create the kernel window into a new page directory object. *}
236
237definition
238copy_global_mappings :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
239  "copy_global_mappings new_pm \<equiv> do
240    global_pm \<leftarrow> gets (x64_global_pml4 \<circ> arch_state);
241    base \<leftarrow> return $ get_pml4_index pptr_base;
242    pme_bits \<leftarrow> return word_size_bits;
243    pm_size \<leftarrow> return (1 << ptTranslationBits);
244    mapM_x (\<lambda>index. do
245        offset \<leftarrow> return (index << pme_bits);
246        pme \<leftarrow> get_pml4e (global_pm + offset);
247        store_pml4e (new_pm + offset) pme
248    od) [base  .e.  pm_size - 1]
249  od"
250
251text {* Walk the page directories and tables in software. *}
252
253definition
254lookup_pml4_slot :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> obj_ref" where
255"lookup_pml4_slot pm vptr \<equiv> let pm_index = get_pml4_index vptr
256                             in pm + (pm_index << word_size_bits)"
257
258definition
259lookup_pdpt_slot :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> (obj_ref,'z::state_ext) lf_monad" where
260"lookup_pdpt_slot pd vptr \<equiv> doE
261    pml4_slot \<leftarrow> returnOk (lookup_pml4_slot pd vptr);
262    pml4e \<leftarrow> liftE $ get_pml4e pml4_slot;
263    (case pml4e of
264          PDPointerTablePML4E tab _ _ \<Rightarrow> (doE
265            pd \<leftarrow> returnOk (ptrFromPAddr tab);
266            pd_index \<leftarrow> returnOk (get_pdpt_index vptr);
267            pd_slot \<leftarrow> returnOk (pd + (pd_index << word_size_bits));
268            returnOk pd_slot
269          odE)
270        | _ \<Rightarrow> throwError $ MissingCapability pml4_shift_bits)
271 odE"
272
273text {* A non-failing version of @{const lookup_pdpt_slot} when the pml4 is already known *}
274definition
275  lookup_pdpt_slot_no_fail :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> obj_ref"
276where
277  "lookup_pdpt_slot_no_fail pdpt vptr \<equiv>
278     pdpt + (get_pdpt_index vptr << word_size_bits)"
279
280text {* The following function takes a page-directory reference as well as
281  a virtual address and then computes a pointer to the PDE in kernel memory *}
282definition
283lookup_pd_slot :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> (obj_ref,'z::state_ext) lf_monad" where
284"lookup_pd_slot pd vptr \<equiv> doE
285    pdpt_slot \<leftarrow> lookup_pdpt_slot pd vptr;
286    pdpte \<leftarrow> liftE $ get_pdpte pdpt_slot;
287    (case pdpte of
288          PageDirectoryPDPTE tab _ _ \<Rightarrow> (doE
289            pd \<leftarrow> returnOk (ptrFromPAddr tab);
290            pd_index \<leftarrow> returnOk (get_pd_index vptr);
291            pd_slot \<leftarrow> returnOk (pd + (pd_index << word_size_bits));
292            returnOk pd_slot
293          odE)
294        | _ \<Rightarrow> throwError $ MissingCapability pdpt_shift_bits)
295 odE"
296
297text {* A non-failing version of @{const lookup_pd_slot} when the pdpt is already known *}
298definition
299  lookup_pd_slot_no_fail :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> obj_ref"
300where
301  "lookup_pd_slot_no_fail pd vptr \<equiv>
302     pd + (get_pd_index vptr << word_size_bits)"
303
304text {* The following function takes a page-directory reference as well as
305  a virtual address and then computes a pointer to the PTE in kernel memory.
306  Note that the function fails if the virtual address is mapped on a section or
307  super section. *}
308definition
309lookup_pt_slot :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> (obj_ref,'z::state_ext) lf_monad" where
310"lookup_pt_slot vspace vptr \<equiv> doE
311    pd_slot \<leftarrow> lookup_pd_slot vspace vptr;
312    pde \<leftarrow> liftE $ get_pde pd_slot;
313    (case pde of
314          PageTablePDE ptab _ _ \<Rightarrow>   (doE
315            pt \<leftarrow> returnOk (ptrFromPAddr ptab);
316            pt_index \<leftarrow> returnOk (get_pt_index vptr);
317            pt_slot \<leftarrow> returnOk (pt + (pt_index << word_size_bits));
318            returnOk pt_slot
319          odE)
320        | _ \<Rightarrow> throwError $ MissingCapability pd_shift_bits)
321   odE"
322
323text {* A non-failing version of @{const lookup_pt_slot} when the pd is already known *}
324definition
325  lookup_pt_slot_no_fail :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> obj_ref"
326where
327  "lookup_pt_slot_no_fail pt vptr \<equiv>
328     pt + (get_pt_index vptr << word_size_bits)"
329
330(* FIXME x64-vtd:
331text {* The following functions helped us locating the actual iopte *}
332definition
333  get_iopt :: "obj_ref \<Rightarrow> (16 word \<Rightarrow> iopte,'z::state_ext) s_monad" where
334  "get_iopt ptr \<equiv> do
335     kobj \<leftarrow> get_object ptr;
336     (case kobj of ArchObj (IOPageTable pt) \<Rightarrow> return pt
337                 | _ \<Rightarrow> fail)
338   od"
339
340definition
341  set_iopt :: "obj_ref \<Rightarrow> (16 word \<Rightarrow> iopte) \<Rightarrow> (unit,'z::state_ext) s_monad" where
342  "set_iopt ptr pt \<equiv> do
343     kobj \<leftarrow> get_object ptr;
344     assert (case kobj of ArchObj (PageTable _) \<Rightarrow> True | _ \<Rightarrow> False);
345     set_object ptr (ArchObj (IOPageTable pt))
346   od"
347
348definition  get_iopte :: "obj_ref \<Rightarrow> (iopte,'z::state_ext) s_monad" where
349  "get_iopte ptr \<equiv> do
350     base \<leftarrow> return (ptr && ~~mask iopt_bits);
351     offset \<leftarrow> return ((ptr && mask iopt_bits) >> 2);
352     pt \<leftarrow> get_iopt base;
353     return $ pt (ucast offset)
354   od"
355
356definition
357  store_iopte :: "obj_ref \<Rightarrow> iopte \<Rightarrow> (unit,'z::state_ext) s_monad" where
358  "store_iopte p iopte \<equiv> do
359    base \<leftarrow> return (p && ~~mask iopt_bits);
360    offset \<leftarrow> return ((p && mask iopt_bits) >> 8);
361    pt \<leftarrow> get_iopt base;
362    pt' \<leftarrow> return $ pt (ucast offset := iopte);
363    set_iopt base pt'
364  od"
365
366definition
367  get_iort :: "obj_ref \<Rightarrow> (16 word \<Rightarrow> iorte,'z::state_ext) s_monad" where
368  "get_iort ptr \<equiv> do
369     kobj \<leftarrow> get_object ptr;
370     (case kobj of ArchObj (IORootTable pt) \<Rightarrow> return pt
371                 | _ \<Rightarrow> fail)
372   od"
373
374definition
375  set_iort :: "obj_ref \<Rightarrow> (16 word \<Rightarrow> iorte) \<Rightarrow> (unit,'z::state_ext) s_monad" where
376  "set_iort ptr pt \<equiv> do
377     kobj \<leftarrow> get_object ptr;
378     assert (case kobj of ArchObj (IORootTable _) \<Rightarrow> True | _ \<Rightarrow> False);
379     set_object ptr (ArchObj (IORootTable pt))
380   od"
381
382definition  get_iorte :: "obj_ref \<Rightarrow> (iorte,'z::state_ext) s_monad" where
383  "get_iorte ptr \<equiv> do
384     base \<leftarrow> return (ptr && ~~mask iopt_bits);
385     offset \<leftarrow> return ((ptr && mask iopt_bits) >> 2);
386     pt \<leftarrow> get_iort base;
387     return $ pt (ucast offset)
388   od"
389
390definition
391  store_iorte :: "obj_ref \<Rightarrow> iorte \<Rightarrow> (unit,'z::state_ext) s_monad" where
392  "store_iorte p iorte \<equiv> do
393    base \<leftarrow> return (p && ~~mask iopt_bits);
394    offset \<leftarrow> return ((p && mask iopt_bits) >> 8);
395    rt \<leftarrow> get_iort base;
396    rt' \<leftarrow> return $ rt (ucast offset := iorte);
397    set_iort base rt'
398  od"
399
400definition
401  get_ioct :: "obj_ref \<Rightarrow> (16 word \<Rightarrow> iocte,'z::state_ext) s_monad" where
402  "get_ioct ptr \<equiv> do
403     kobj \<leftarrow> get_object ptr;
404     (case kobj of ArchObj (IOContextTable pt) \<Rightarrow> return pt
405                 | _ \<Rightarrow> fail)
406   od"
407
408definition
409  set_ioct :: "obj_ref \<Rightarrow> (16 word \<Rightarrow> iocte) \<Rightarrow> (unit,'z::state_ext) s_monad" where
410  "set_ioct ptr ct \<equiv> do
411     kobj \<leftarrow> get_object ptr;
412     assert (case kobj of ArchObj (IOContextTable _) \<Rightarrow> True | _ \<Rightarrow> False);
413     set_object ptr (ArchObj (IOContextTable ct))
414   od"
415
416definition  get_iocte :: "obj_ref \<Rightarrow> (iocte,'z::state_ext) s_monad" where
417  "get_iocte ptr \<equiv> do
418     base \<leftarrow> return (ptr && ~~mask iopt_bits);
419     offset \<leftarrow> return ((ptr && mask iopt_bits) >> 8);
420     ct \<leftarrow> get_ioct base;
421     return $ ct (ucast offset)
422   od"
423
424
425definition
426  store_iocte :: "obj_ref \<Rightarrow> iocte \<Rightarrow> (unit,'z::state_ext) s_monad" where
427  "store_iocte p iocte \<equiv> do
428    base \<leftarrow> return (p && ~~mask iopt_bits);
429    offset \<leftarrow> return ((p && mask iopt_bits) >> 8);
430    pt \<leftarrow> get_ioct base;
431    pt' \<leftarrow> return $ pt (ucast offset := iocte);
432    set_ioct base pt'
433  od"
434
435definition get_pci_fun :: "io_asid \<Rightarrow> machine_word" where
436"get_pci_fun asid \<equiv> fromIntegral asid && 0x7"
437
438definition get_pci_bus :: "io_asid \<Rightarrow> machine_word" where
439"get_pci_bus asid \<equiv> fromIntegral $ (asid >> 8) && 0xFF"
440
441definition get_pci_dev :: "io_asid \<Rightarrow> machine_word" where
442"get_pci_dev asid \<equiv> fromIntegral $ (asid >> 3) && 0x1F"
443
444definition lookup_io_context_slot :: "io_asid \<Rightarrow> (obj_ref,'z::state_ext) s_monad" where
445"lookup_io_context_slot pci_request_id \<equiv> do
446    rtptr <- gets (x64_io_root_table \<circ> arch_state);
447    root_index <- return $ get_pci_bus pci_request_id;
448    rte_ptr <- return $ rtptr + root_index;
449    rte <- get_iorte rte_ptr;
450    ct_pptr <- return $ ptrFromPAddr (context_table rte);
451    cte_ptr <- return $ ((get_pci_dev pci_request_id) << vtd_cte_size_bits)
452              || get_pci_fun pci_request_id;
453    return $ ct_pptr + ( cte_ptr << vtd_cte_size_bits)
454  od"
455
456definition get_vtd_pte_offset ::  "64 word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 64 word"
457where "get_vtd_pte_offset translation levels_to_resolve levels_remaining \<equiv>
458  let lvldiff = levels_to_resolve - levels_remaining
459  in (translation >> (vtd_pt_bits * (x64_num_io_pt_levels - 1 - lvldiff)))
460      && (mask vtd_pt_bits)"
461
462
463fun lookup_io_ptr_resolve_levels :: "obj_ref \<Rightarrow> 64 word\<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
464 ((obj_ref \<times> nat),'z::state_ext) lf_monad"
465where "lookup_io_ptr_resolve_levels iopt_ref translation levels_to_resolve
466  levels_remaining = doE
467    offset <- returnOk $ get_vtd_pte_offset translation
468      levels_to_resolve levels_remaining;
469    pte_ptr <- returnOk $ iopt_ref + offset;
470    if levels_remaining = 0
471      then returnOk $ (pte_ptr, 0)
472      else (doE
473        iopte <- liftE $ get_iopte pte_ptr;
474        slot <- returnOk $ ptrFromPAddr (frame_ptr iopte);
475        if (io_pte_rights iopte = vm_read_write)
476          then returnOk (pte_ptr, levels_remaining)
477          else lookup_io_ptr_resolve_levels slot translation levels_to_resolve
478            (levels_remaining - 1)
479      odE)
480  odE"
481
482definition lookup_io_pt_slot :: "obj_ref \<Rightarrow> 64 word \<Rightarrow>  ((obj_ref \<times> nat),'z::state_ext) lf_monad"
483where "lookup_io_pt_slot pte_ref ioaddr \<equiv> lookup_io_ptr_resolve_levels pte_ref  (ioaddr >> pageBits)
484  (x64_num_io_pt_levels - 1) (x64_num_io_pt_levels - 1)"
485
486*)
487
488
489end
490end
491