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 11chapter "x64-Specific Data Types" 12 13theory Arch_Structs_A 14imports 15 "ExecSpec.Arch_Structs_B" 16 "../ExceptionTypes_A" 17 "../VMRights_A" 18begin 19 20context Arch begin global_naming X64_A 21 22text {* 23This theory provides architecture-specific definitions and datatypes 24including architecture-specific capabilities and objects. 25*} 26 27section {* Architecture-specific virtual memory *} 28 29type_synonym io_port = "16 word" 30type_synonym io_asid = "16 word" 31 32section {* Architecture-specific capabilities *} 33 34text {* The x64 kernel supports capabilities for ASID pools and an ASID controller capability, 35along with capabilities for IO ports and spaces, as well as virtual memory mappings. *} 36 37datatype arch_cap = 38 ASIDPoolCap (acap_asid_pool : obj_ref) (acap_asid_base : asid) 39 | ASIDControlCap 40 | IOPortCap (acap_io_port_first_port : io_port) (acap_io_port_last_port : io_port) 41 | IOPortControlCap 42(* FIXME x64-vtd: 43 | IOSpaceCap (cap_io_domain_id : "16 word") (cap_io_pci_device : "io_asid option") 44 | IOPageTableCap (cap_iopt_base_ptr : obj_ref) (cap_io_pt_level : nat) (cap_iopt_mapped_address : "(io_asid * vspace_ref) option") 45*) 46 | PageCap bool obj_ref (acap_rights : cap_rights) vmmap_type vmpage_size "(asid * vspace_ref) option" 47 | PageTableCap obj_ref "(asid * vspace_ref) option" 48 | PageDirectoryCap obj_ref "(asid * vspace_ref) option" 49 | PDPointerTableCap obj_ref "(asid * vspace_ref) option" 50 | PML4Cap obj_ref "asid option" 51 52(* cr3 Stuff *) 53datatype cr3 = cr3 obj_ref asid 54 55primrec 56 cr3_base_address :: "cr3 \<Rightarrow> obj_ref" 57where 58 "cr3_base_address (cr3 addr _) = addr" 59 60primrec 61 cr3_pcid :: "cr3 \<Rightarrow> asid" 62where 63 "cr3_pcid (cr3 _ pcid) = pcid" 64 65section {* Architecture-specific objects *} 66 67datatype table_attr = Accessed | CacheDisabled | WriteThrough | ExecuteDisable 68type_synonym table_attrs = "table_attr set" 69 70datatype frame_attr = PTAttr table_attr | Global | PAT | Dirty 71type_synonym frame_attrs = "frame_attr set" 72 73datatype pml4e 74 = InvalidPML4E 75 | PDPointerTablePML4E 76 (pml4_table : obj_ref) 77 (pml4e_attrs : table_attrs) 78 (pml4e_rights : vm_rights) 79 80datatype pdpte 81 = InvalidPDPTE 82 | PageDirectoryPDPTE 83 (pdpt_table : obj_ref) 84 (pdpt_table_attrs : table_attrs) 85 (pdpt_rights : vm_rights) 86 | HugePagePDPTE 87 (pdpt_frame : obj_ref) 88 (pdpt_frame_attrs : frame_attrs) 89 (pdpt_rights : vm_rights) 90 91datatype pde 92 = InvalidPDE 93 | PageTablePDE 94 obj_ref 95 (pt_attrs : table_attrs) 96 (pde_rights : cap_rights) 97 | LargePagePDE 98 obj_ref 99 (pde_page_attrs : frame_attrs) 100 (pde_rights: cap_rights) 101 102datatype pte 103 = InvalidPTE 104 | SmallPagePTE 105 (pte_frame: obj_ref) 106 (pte_frame_attrs : frame_attrs) 107 (pte_rights : cap_rights) 108 109 110datatype vm_page_entry = VMPTE pte | VMPDE pde | VMPDPTE pdpte 111 112datatype translation_type = NotTranslated | Translated 113 114datatype iocte = 115 InvalidIOCTE 116 | VTDCTE 117 (domain_id : word16) 118 (res_mem_reg: bool) 119 (address_width: nat) 120 (next_level_ptr: obj_ref) 121 (translation_type: translation_type) 122 (iocte_present : bool) 123 124datatype iopte = 125 InvalidIOPTE 126 | VTDPTE 127 (frame_ptr : obj_ref) 128 (io_pte_rights : vm_rights) 129 130datatype iorte = 131 InvalidIORTE 132 | VTDRTE 133 (context_table : obj_ref) 134 (iorte_present : bool) 135 136datatype arch_kernel_obj = 137 ASIDPool "9 word \<rightharpoonup> obj_ref" 138 | PageTable "9 word \<Rightarrow> pte" 139 | PageDirectory "9 word \<Rightarrow> pde" 140 | PDPointerTable "9 word \<Rightarrow> pdpte" 141 | PageMapL4 "9 word \<Rightarrow> pml4e" 142 | DataPage bool vmpage_size 143(* FIXME x64-vtd: 144 | IORootTable "16 word \<Rightarrow> iorte" 145 | IOContextTable "16 word \<Rightarrow> iocte" 146 | IOPageTable "16 word \<Rightarrow> iopte" *) 147 148definition table_size :: nat where 149 "table_size = ptTranslationBits + word_size_bits" 150 151definition iotable_size :: nat where 152 "iotable_size = ptTranslationBits + 2*word_size_bits" 153 154definition cte_level_bits :: nat where 155 "cte_level_bits \<equiv> 5" 156 157primrec 158 arch_obj_size :: "arch_cap \<Rightarrow> nat" 159where 160 "arch_obj_size (ASIDPoolCap _ _) = pageBits" 161| "arch_obj_size ASIDControlCap = 0" 162| "arch_obj_size (IOPortCap _ _) = 0" 163| "arch_obj_size IOPortControlCap = 0" 164(* FIXME x64-vtd: 165| "arch_obj_size (IOSpaceCap _ _) = 0" 166| "arch_obj_size (IOPageTableCap _ _ _) = iotable_size" *) 167| "arch_obj_size (PageCap _ _ _ _ sz _) = pageBitsForSize sz" 168| "arch_obj_size (PageTableCap _ _) = table_size" 169| "arch_obj_size (PageDirectoryCap _ _) = table_size" 170| "arch_obj_size (PDPointerTableCap _ _) = table_size" 171| "arch_obj_size (PML4Cap _ _) = table_size" 172 173primrec 174 arch_cap_is_device :: "arch_cap \<Rightarrow> bool" 175where 176 "arch_cap_is_device (ASIDPoolCap _ _) = False" 177| "arch_cap_is_device ASIDControlCap = False" 178| "arch_cap_is_device (IOPortCap _ _) = False" 179| "arch_cap_is_device IOPortControlCap = False" 180(* FIXME x64-vtd: 181| "arch_cap_is_device (IOSpaceCap _ _) = False" 182| "arch_cap_is_device (IOPageTableCap _ _ _) = False" *) 183| "arch_cap_is_device (PageCap is_dev _ _ _ _ _) = is_dev" 184| "arch_cap_is_device (PageTableCap _ _) = False" 185| "arch_cap_is_device (PageDirectoryCap _ _) = False" 186| "arch_cap_is_device (PDPointerTableCap _ _) = False" 187| "arch_cap_is_device (PML4Cap _ _) = False" 188 189definition tcb_bits :: nat where 190 "tcb_bits \<equiv> 11" 191 192definition endpoint_bits :: nat where 193 "endpoint_bits \<equiv> 4" 194 195definition ntfn_bits :: nat where 196 "ntfn_bits \<equiv> 5" 197 198definition untyped_min_bits :: nat where 199 "untyped_min_bits \<equiv> 4" 200 201definition untyped_max_bits :: nat where 202 "untyped_max_bits \<equiv> 47" 203 204primrec 205 arch_kobj_size :: "arch_kernel_obj \<Rightarrow> nat" 206where 207 "arch_kobj_size (ASIDPool _) = pageBits" 208| "arch_kobj_size (PageTable _) = table_size" 209| "arch_kobj_size (PageDirectory _) = table_size" 210| "arch_kobj_size (PDPointerTable _) = table_size" 211| "arch_kobj_size (PageMapL4 _) = table_size" 212| "arch_kobj_size (DataPage _ sz) = pageBitsForSize sz" 213 214primrec 215 aobj_ref :: "arch_cap \<rightharpoonup> obj_ref" 216where 217 "aobj_ref (ASIDPoolCap x _) = Some x" 218| "aobj_ref ASIDControlCap = None" 219| "aobj_ref (IOPortCap _ _) = None" 220| "aobj_ref IOPortControlCap = None" 221(* FIXME x64-vtd: 222| "aobj_ref (IOSpaceCap _ _) = None" 223| "aobj_ref (IOPageTableCap x _ _) = Some x" *) 224| "aobj_ref (PageCap _ x _ _ _ _) = Some x" 225| "aobj_ref (PageDirectoryCap x _) = Some x" 226| "aobj_ref (PageTableCap x _) = Some x" 227| "aobj_ref (PDPointerTableCap x _) = Some x" 228| "aobj_ref (PML4Cap x _) = Some x" 229 230 231definition 232 acap_rights_update :: "cap_rights \<Rightarrow> arch_cap \<Rightarrow> arch_cap" where 233 "acap_rights_update rs ac \<equiv> case ac of 234 PageCap dev x rs' m sz as \<Rightarrow> PageCap dev x (validate_vm_rights rs) m sz as 235 | _ \<Rightarrow> ac" 236 237section {* Architecture-specific object types and default objects *} 238 239datatype 240 aobject_type = 241 SmallPageObj 242 | LargePageObj 243 | HugePageObj 244 | PageTableObj 245 | PageDirectoryObj 246 | PDPTObj 247 | PML4Obj 248 | ASIDPoolObj 249 250datatype X64IRQState = 251 IRQFree 252 | IRQReserved 253 | IRQMSI 254 (MSIBus : machine_word) 255 (MSIDev : machine_word) 256 (MSIFunc : machine_word) 257 (MSIHandle : machine_word) 258 | IRQIOAPIC 259 (IRQioapic : machine_word) 260 (IRQPin : machine_word) 261 (IRQLevel : machine_word) 262 (IRQPolarity : machine_word) 263 (IRQMasked : bool) 264 265definition 266 arch_is_frame_type :: "aobject_type \<Rightarrow> bool" 267where 268 "arch_is_frame_type aobj \<equiv> case aobj of 269 SmallPageObj \<Rightarrow> True 270 | LargePageObj \<Rightarrow> True 271 | HugePageObj \<Rightarrow> True 272 | _ \<Rightarrow> False" 273 274definition 275 arch_default_cap :: "aobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> arch_cap" where 276 "arch_default_cap tp r n dev \<equiv> case tp of 277 SmallPageObj \<Rightarrow> PageCap dev r vm_read_write VMNoMap X64SmallPage None 278 | LargePageObj \<Rightarrow> PageCap dev r vm_read_write VMNoMap X64LargePage None 279 | HugePageObj \<Rightarrow> PageCap dev r vm_read_write VMNoMap X64HugePage None 280 | PageTableObj \<Rightarrow> PageTableCap r None 281 | PageDirectoryObj \<Rightarrow> PageDirectoryCap r None 282 | PDPTObj \<Rightarrow> PDPointerTableCap r None 283 | PML4Obj \<Rightarrow> PML4Cap r None 284 | ASIDPoolObj \<Rightarrow> ASIDPoolCap r 0" (* unused *) 285 286definition 287 default_arch_object :: "aobject_type \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> arch_kernel_obj" where 288 "default_arch_object tp dev n \<equiv> case tp of 289 SmallPageObj \<Rightarrow> DataPage dev X64SmallPage 290 | LargePageObj \<Rightarrow> DataPage dev X64LargePage 291 | HugePageObj \<Rightarrow> DataPage dev X64HugePage 292 | PageTableObj \<Rightarrow> PageTable (\<lambda>x. InvalidPTE) 293 | PageDirectoryObj \<Rightarrow> PageDirectory (\<lambda>x. InvalidPDE) 294 | PDPTObj \<Rightarrow> PDPointerTable (\<lambda>x. InvalidPDPTE) 295 | PML4Obj \<Rightarrow> PageMapL4 (\<lambda>x. InvalidPML4E) 296 | ASIDPoolObj \<Rightarrow> ASIDPool (\<lambda>_. None)" 297 298type_synonym x64_vspace_region_uses = "vspace_ref \<Rightarrow> x64vspace_region_use" 299 300end 301 302qualify X64_A (in Arch) 303 304section {* Architecture-specific state *} 305 306record arch_state = 307 x64_asid_table :: "3 word \<rightharpoonup> obj_ref" 308 x64_global_pml4 :: obj_ref 309 x64_kernel_vspace :: X64_A.x64_vspace_region_uses 310 x64_global_pts :: "obj_ref list" 311 x64_global_pdpts :: "obj_ref list" 312 x64_global_pds :: "obj_ref list" 313 x64_current_cr3 :: "X64_A.cr3" 314 x64_allocated_io_ports :: "X64_A.io_port \<Rightarrow> bool" 315 x64_num_ioapics :: "64 word" 316 x64_irq_state :: "8 word \<Rightarrow> X64_A.X64IRQState" 317 318(* FIXME x64-vtd: 319 x64_num_io_domain_bits :: "16 word" 320 x64_first_valid_io_domain :: "16 word" 321 x64_num_io_domain_id_bits :: "32 word" 322 x64_io_root_table :: obj_ref *) 323 324end_qualify 325 326context Arch begin global_naming X64_A 327 328definition 329 pd_shift_bits :: "nat" where 330 "pd_shift_bits \<equiv> pageBits + ptTranslationBits" 331 332definition 333 pt_shift_bits :: "nat" where 334 "pt_shift_bits \<equiv> pageBits" 335 336definition 337 pdpt_shift_bits :: "nat" where 338 "pdpt_shift_bits \<equiv> pageBits + ptTranslationBits + ptTranslationBits" 339 340definition 341 pml4_shift_bits :: "nat" where 342 "pml4_shift_bits \<equiv> pageBits + ptTranslationBits + ptTranslationBits + ptTranslationBits" 343 344definition 345 pt_bits :: "nat" where 346 "pt_bits \<equiv> table_size" 347 348definition 349 pd_bits :: "nat" where 350 "pd_bits \<equiv> table_size" 351 352definition 353 pdpt_bits :: "nat" where 354 "pdpt_bits \<equiv> table_size" 355 356definition 357 pml4_bits :: "nat" where 358 "pml4_bits \<equiv> table_size" 359 360definition 361 iopt_bits :: "nat" where 362 "iopt_bits \<equiv> iotable_size" 363 364definition 365 vtd_cte_size_bits :: "nat" where 366 "vtd_cte_size_bits \<equiv> 8" 367 368definition 369 vtd_pt_bits :: "nat" where 370 "vtd_pt_bits \<equiv> iotable_size" 371 372definition 373 x64_num_io_pt_levels :: "nat" where 374 "x64_num_io_pt_levels \<equiv> 4" 375 376section "Type declarations for invariant definitions" 377 378(* FIXME x64-vtd: add *) 379datatype aa_type = 380 AASIDPool 381 | APageTable 382 | APageDirectory 383 | APDPointerTable 384 | APageMapL4 385 | AUserData vmpage_size 386 | ADeviceData vmpage_size 387 388(* FIXME x64-vtd: add *) 389definition aa_type :: "arch_kernel_obj \<Rightarrow> aa_type" 390where 391 "aa_type ao \<equiv> (case ao of 392 PageTable pt \<Rightarrow> APageTable 393 | PageDirectory pd \<Rightarrow> APageDirectory 394 | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz 395 | ASIDPool f \<Rightarrow> AASIDPool 396 | PDPointerTable pdpt \<Rightarrow> APDPointerTable 397 | PageMapL4 pm \<Rightarrow> APageMapL4)" 398 399text {* For implementation reasons the badge word has differing amounts of bits *} 400definition 401 badge_bits :: nat where 402 "badge_bits \<equiv> 64" 403 404end 405 406section "Arch-specific TCB" 407 408qualify X64_A (in Arch) 409 410text \<open> Arch-specific part of a TCB: this must have at least a field for user context. \<close> 411record arch_tcb = 412 tcb_context :: user_context 413 414end_qualify 415 416context Arch begin global_naming X64_A 417 418definition 419 default_arch_tcb :: arch_tcb where 420 "default_arch_tcb \<equiv> \<lparr>tcb_context = new_context\<rparr>" 421 422text \<open> Accessors for @{text "tcb_context"} inside @{text "arch_tcb"}. 423 These are later used to implement @{text as_user}, i.e.\ need to be 424 compatible with @{text user_monad}.\<close> 425definition 426 arch_tcb_context_set :: "user_context \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb" 427where 428 "arch_tcb_context_set uc a_tcb \<equiv> a_tcb \<lparr> tcb_context := uc \<rparr>" 429 430definition 431 arch_tcb_context_get :: "arch_tcb \<Rightarrow> user_context" 432where 433 "arch_tcb_context_get a_tcb \<equiv> tcb_context a_tcb" 434 435(* FIXME: the following means that we break the set/getRegister abstraction 436 and should move some of this into the machine interface *) 437text \<open> 438 Accessors for the user register part of the @{text "arch_tcb"}. 439 (Because @{typ "register \<Rightarrow> machine_word"} may not be equal to @{typ user_context}). 440\<close> 441definition 442 arch_tcb_set_registers :: "(register \<Rightarrow> machine_word) \<Rightarrow> arch_tcb \<Rightarrow> arch_tcb" 443where 444 "arch_tcb_set_registers regs a_tcb \<equiv> 445 a_tcb \<lparr> tcb_context := UserContext (fpu_state (tcb_context a_tcb)) regs \<rparr>" 446 447definition 448 arch_tcb_get_registers :: "arch_tcb \<Rightarrow> register \<Rightarrow> machine_word" 449where 450 "arch_tcb_get_registers a_tcb \<equiv> user_regs (tcb_context a_tcb)" 451 452end 453 454end 455