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