1-- 2-- Copyright 2014, General Dynamics C4 Systems 3-- 4-- SPDX-License-Identifier: GPL-2.0-only 5-- 6 7#include <config.h> 8 9---- Default base size: uint32_t 10base 32 11 12-- Including the common structures_32.bf is neccessary because 13-- we need the structures to be visible here when building 14-- the capType 15#include <object/structures_32.bf> 16 17---- IA32-specific cap types 18 19block frame_cap { 20 padding 1 21 field capFSize 1 22 field capFMappedASIDLow 10 23 field_high capFMappedAddress 20 24 25 padding 1 26 field capFMapType 2 27 field capFIsDevice 1 28 field capFMappedASIDHigh 2 29 field capFVMRights 2 30 field_high capFBasePtr 20 31 field capType 4 32} 33 34-- Second-level page table 35block page_table_cap { 36 padding 8 37 field capPTIsMapped 1 38 field capPTMappedASID 12 39 field_high capPTMappedAddress 11 40 41 padding 8 42 field_high capPTBasePtr 20 43 field capType 4 44} 45 46-- First-level page table (page directory) 47block page_directory_cap { 48 padding 17 49 field capPDIsMapped 1 50 field capPDMappedASID 12 51 field_high capPDMappedAddress 2 52 53 padding 8 54 field_high capPDBasePtr 20 55 field capType 4 56} 57 58-- Cap to the table of 2^6 ASID pools 59block asid_control_cap { 60 padding 32 61 padding 28 62 field capType 4 63} 64 65-- Cap to a pool of 2^10 ASIDs 66block asid_pool_cap { 67 padding 20 68 field capASIDBase 12 69 70 padding 8 71 field_high capASIDPool 20 72 field capType 4 73} 74 75 76-- IO Port Control Cap 77block io_port_control_cap { 78 padding 32 79 80 padding 24 81 field capType 8 82} 83 84-- IO Port Cap 85block io_port_cap { 86 field capIOPortFirstPort 16 87 field capIOPortLastPort 16 88 89 padding 8 90#ifdef CONFIG_VTX 91 field capIOPortVPID 16 92#else 93 padding 16 94#endif 95 field capType 8 96} 97 98#ifdef CONFIG_IOMMU 99 100-- IO Space Cap 101block io_space_cap { 102 field capDomainID 16 103 field capPCIDevice 16 104 105 padding 28 106 field capType 4 107} 108 109block io_space_capdata { 110 field domainID 16 111 field PCIDevice 16 112} 113 114-- IO Page Table Cap 115block io_page_table_cap { 116 field capIOPTIsMapped 1 117 field capIOPTLevel 4 118 field_high capIOPTMappedAddress 11 119 field capIOPTIOASID 16 120 121 padding 4 122 field_high capIOPTBasePtr 20 123 field capType 8 124} 125 126#endif 127 128#ifdef CONFIG_VTX 129 130block vcpu_cap { 131 padding 32 132 133 field_high capVCPUPtr 24 134 field capType 8 135} 136 137-- Fourth-level EPT page table 138block ept_pt_cap { 139 field_high capPTMappedAddress 11 140 padding 4 141 field capPTIsMapped 1 142 field capPTMappedASID 16 143 144 field_high capPTBasePtr 20 145 padding 4 146 field capType 8 147} 148 149-- third-level EPT page table (page directory) 150block ept_pd_cap { 151 field_high capPDMappedAddress 3 152 padding 12 153 field capPDIsMapped 1 154 field capPDMappedASID 16 155 156 field_high capPDBasePtr 20 157 padding 4 158 field capType 8 159} 160 161-- Second-level EPT page table (page directory pointer table) 162block ept_pdpt_cap { 163 field_high capPDPTMappedAddress 1 164 padding 14 165 field capPDPTIsMapped 1 166 field capPDPTMappedASID 16 167 168 field_high capPDPTBasePtr 20 169 padding 4 170 field capType 8 171} 172 173-- First-level EPT pml4 174block ept_pml4_cap { 175 padding 15 176 field capPML4IsMapped 1 177 field capPML4MappedASID 16 178 179 field_high capPML4BasePtr 20 180 padding 4 181 field capType 8 182} 183 184#endif 185 186-- NB: odd numbers are arch caps (see isArchCap()) 187tagged_union cap capType { 188 mask 4 0xe 189 mask 8 0x0e 190 191 -- 4-bit tag caps 192 tag null_cap 0 193 tag untyped_cap 2 194 tag endpoint_cap 4 195 tag notification_cap 6 196 tag reply_cap 8 197 tag cnode_cap 10 198 tag thread_cap 12 199 -- Do not extend even 4-bit caps types beyond 12, as we use 200 -- 14 (0xe) to determine which caps are 8-bit. 201 202 -- 4-bit tag arch caps 203 tag frame_cap 1 204 tag page_table_cap 3 205 tag page_directory_cap 5 206 tag asid_control_cap 9 207 tag asid_pool_cap 11 208#ifdef CONFIG_IOMMU 209 tag io_space_cap 13 210#endif 211 -- Do not extend odd 4-bit caps types beyond 13, as we use 212 -- 15 (0xf) to determine which caps are 8-bit. 213 214 -- 8-bit tag caps 215 tag irq_control_cap 0x0e 216 tag irq_handler_cap 0x1e 217 tag zombie_cap 0x2e 218 tag domain_cap 0x3e 219#ifdef CONFIG_KERNEL_MCS 220 tag sched_context_cap 0x4e 221 tag sched_control_cap 0x5e 222#endif 223 224 -- 8-bit tag arch caps 225#ifdef CONFIG_IOMMU 226 tag io_page_table_cap 0x0f 227#endif 228 tag io_port_cap 0x1f 229#ifdef CONFIG_VTX 230 tag vcpu_cap 0x2f 231 tag ept_pt_cap 0x3f 232 tag ept_pd_cap 0x4f 233 tag ept_pdpt_cap 0x5f 234 tag ept_pml4_cap 0x6f 235#endif 236 tag io_port_control_cap 0x7f 237} 238 239---- IA32 specific fault types 240 241block VMFault { 242 field address 32 243 field FSR 5 244 padding 7 245 field instructionFault 1 246 padding 15 247 field seL4_FaultType 4 248} 249 250-- VM attributes 251 252block vm_attributes { 253 padding 29 254 field x86PATBit 1 255 field x86PCDBit 1 256 field x86PWTBit 1 257} 258 259---- IA32 specific object types 260 261-- GDT entries (Segment Desciptors) 262 263block gdt_null { 264 padding 19 265 field desc_type 3 266 padding 42 267} 268 269block gdt_code { 270 field base_high 8 271 field granularity 1 272 field operation_size 1 273 padding 1 274 field avl 1 275 field seg_limit_high 4 276 field present 1 277 field dpl 2 278 field desc_type 3 279 field readable 1 280 field accessed 1 281 field base_mid 8 282 field base_low 16 283 field seg_limit_low 16 284} 285 286block gdt_data { 287 field base_high 8 288 field granularity 1 289 field operation_size 1 290 padding 1 291 field avl 1 292 field seg_limit_high 4 293 field present 1 294 field dpl 2 295 field desc_type 3 296 field writable 1 297 field accessed 1 298 field base_mid 8 299 field base_low 16 300 field seg_limit_low 16 301} 302 303block gdt_tss { 304 field base_high 8 305 field granularity 1 306 padding 2 307 field avl 1 308 field limit_high 4 309 field present 1 310 field dpl 2 311 field desc_type 3 312 field busy 1 313 field always_1 1 314 field base_mid 8 315 field base_low 16 316 field limit_low 16 317} 318 319tagged_union gdt_entry desc_type { 320 tag gdt_null 0 321 tag gdt_tss 2 322 tag gdt_data 4 323 tag gdt_code 6 324} 325 326-- IDT entries (Gate Desciptors) 327 328block task_gate { 329 padding 16 330 field present 1 331 field dpl 2 332 padding 2 333 field type 3 334 padding 8 335 field tss_seg_selector 16 336 padding 16 337} 338 339block interrupt_gate { 340 field offset_high 16 341 field present 1 342 field dpl 2 343 padding 1 344 field gate_size 1 345 field type 3 346 padding 8 347 field seg_selector 16 348 field offset_low 16 349} 350 351block trap_gate { 352 field offset_high 16 353 field present 1 354 field dpl 2 355 padding 1 356 field gate_size 1 357 field type 3 358 padding 8 359 field seg_selector 16 360 field offset_low 16 361} 362 363tagged_union idt_entry type { 364 tag task_gate 5 365 tag interrupt_gate 6 366 tag trap_gate 7 367} 368 369-- Task State Segment (TSS) 370 371block tss { 372 field io_map_base 16 373 padding 15 374 field trap 1 375 padding 16 376 field sel_ldt 16 377 padding 16 378 field gs 16 379 padding 16 380 field fs 16 381 padding 16 382 field ds 16 383 padding 16 384 field ss 16 385 padding 16 386 field cs 16 387 padding 16 388 field es 16 389 field edi 32 390 field esi 32 391 field ebp 32 392 field esp 32 393 field ebx 32 394 field edx 32 395 field ecx 32 396 field eax 32 397 field eflags 32 398 field eip 32 399 field cr3 32 400 padding 16 401 field ss2 16 402 field esp2 32 403 padding 16 404 field ss1 16 405 field esp1 32 406 padding 16 407 field ss0 16 408 field esp0 32 409 padding 16 410 field prev_task 16 411} 412 413-- PDs and PTs 414 415block pde_pt { 416 field_high pt_base_address 20 417 field avl 3 418 padding 1 419 field page_size 1 420 padding 1 421 field accessed 1 422 field cache_disabled 1 423 field write_through 1 424 field super_user 1 425 field read_write 1 426 field present 1 427} 428 429block pde_large { 430 field_high page_base_address 11 431 padding 8 432 field pat 1 433 field avl 3 434 field global 1 435 field page_size 1 436 field dirty 1 437 field accessed 1 438 field cache_disabled 1 439 field write_through 1 440 field super_user 1 441 field read_write 1 442 field present 1 443} 444 445tagged_union pde page_size { 446 tag pde_pt 0 447 tag pde_large 1 448} 449 450block pte { 451 field_high page_base_address 20 452 field avl 3 453 field global 1 454 field pat 1 455 field dirty 1 456 field accessed 1 457 field cache_disabled 1 458 field write_through 1 459 field super_user 1 460 field read_write 1 461 field present 1 462} 463 464#ifdef CONFIG_VTX 465 466block ept_pml4e { 467 padding 32 468 field_high pdpt_base_address 20 469 padding 9 470 field execute 1 471 field write 1 472 field read 1 473} 474 475block ept_pdpte { 476 padding 32 477 field_high pd_base_address 20 478 field avl_cte_depth 3 479 padding 6 480 field execute 1 481 field write 1 482 field read 1 483} 484 485block ept_pde_2m { 486 padding 32 487 field_high page_base_address 12 488 padding 8 489 field avl_cte_depth 2 490 padding 2 491 field page_size 1 492 field ignore_pat 1 493 field type 3 494 field execute 1 495 field write 1 496 field read 1 497} 498 499block ept_pde_pt { 500 padding 32 501 field_high pt_base_address 20 502 field avl_cte_depth 3 503 padding 1 504 field page_size 1 505 padding 4 506 field execute 1 507 field write 1 508 field read 1 509} 510 511tagged_union ept_pde page_size { 512 tag ept_pde_pt 0 513 tag ept_pde_2m 1 514} 515 516block ept_pte { 517 padding 32 518 field_high page_base_address 20 519 field avl_cte_depth 2 520 padding 3 521 field ignore_pat 1 522 field type 3 523 field execute 1 524 field write 1 525 field read 1 526} 527 528block vmx_eptp { 529 field_high paddr 20 530 padding 5 531 field flags 1 532 field depth_minus_1 3 533 field memory_type 3 534} 535 536#endif 537 538block asid_map_none { 539 padding 30 540 field type 2 541} 542 543block asid_map_vspace { 544 field_high vspace_root 20 545 padding 10 546 field type 2 547} 548 549#ifdef CONFIG_VTX 550block asid_map_ept { 551 field_high ept_root 20 552 padding 10 553 field type 2 554} 555#endif 556 557tagged_union asid_map type { 558 tag asid_map_none 0 559 tag asid_map_vspace 1 560#ifdef CONFIG_VTX 561 tag asid_map_ept 2 562#endif 563} 564 565block cr3 { 566 field_high pd_base_address 20 567 padding 12 568} 569 570#include <sel4/arch/shared_types.bf> 571