x64: VT-x related cap and object definitions
* Adds object and cap definitions for VT-x structures (VCPU and EPT). * Extends the asid_map implementation to support ASIDs in the EPT * Adds size definitions for VCPU and EPT objects
This commit is contained in:
Adrian Danis
parent
e537ee1d67
commit
017d786317
6 changed files with 166 additions and 4 deletions
|
|
@ -151,6 +151,60 @@ block io_page_table_cap (capType, capIOPTIsMapped, capIOPTLevel, capIOPTMappedAd
|
|||
field_high capIOPTMappedAddress 48
|
||||
}
|
||||
|
||||
block vcpu_cap {
|
||||
field capVCPUPtr 64
|
||||
|
||||
field capType 5
|
||||
padding 59
|
||||
}
|
||||
|
||||
-- Fourth-level EPT page table
|
||||
block ept_pt_cap (capType, capPTMappedAddress, capPTIsMapped, capPTMappedASID, capPTBasePtr) {
|
||||
field capPTBasePtr 64
|
||||
|
||||
field capType 5
|
||||
field capPTIsMapped 1
|
||||
padding 10
|
||||
field_high capPTMappedAddress 27
|
||||
field capPTMappedASID 16
|
||||
padding 5
|
||||
}
|
||||
|
||||
-- third-level EPT page table (page directory)
|
||||
block ept_pd_cap (capType, capPDMappedAddress, capPDIsMapped, capPDMappedASID, capPDBasePtr) {
|
||||
field capPDBasePtr 64
|
||||
|
||||
field capType 5
|
||||
field capPDIsMapped 1
|
||||
padding 10
|
||||
field_high capPDMappedAddress 19
|
||||
field capPDMappedASID 16
|
||||
padding 13
|
||||
}
|
||||
|
||||
-- Second-level EPT page table (page directory pointer table)
|
||||
block ept_pdpt_cap (capType, capPDPTMappedAddress, capPDPTIsMapped, capPDPTMappedASID, capPDPTBasePtr) {
|
||||
field capPDPTBasePtr 64
|
||||
|
||||
field capType 5
|
||||
field capPDPTIsMapped 1
|
||||
padding 10
|
||||
field_high capPDPTMappedAddress 17
|
||||
field capPDPTMappedASID 16
|
||||
padding 15
|
||||
}
|
||||
|
||||
-- First-level EPT pml4
|
||||
block ept_pml4_cap (capType, capPML4IsMapped, capPML4MappedASID, capPML4BasePtr) {
|
||||
field capPML4BasePtr 64
|
||||
|
||||
field capType 5
|
||||
field capPML4IsMapped 1
|
||||
padding 42
|
||||
|
||||
field capPML4MappedASID 16
|
||||
}
|
||||
|
||||
-- NB: odd numbers are arch caps (see isArchCap())
|
||||
tagged_union cap capType {
|
||||
-- 5-bit tag caps
|
||||
|
|
@ -177,6 +231,11 @@ tagged_union cap capType {
|
|||
tag io_space_cap 15
|
||||
tag io_page_table_cap 17
|
||||
tag io_port_cap 19
|
||||
tag vcpu_cap 21
|
||||
tag ept_pt_cap 23
|
||||
tag ept_pd_cap 25
|
||||
tag ept_pdpt_cap 27
|
||||
tag ept_pml4_cap 29
|
||||
}
|
||||
|
||||
---- Arch-independent object types
|
||||
|
|
@ -364,9 +423,20 @@ block asid_map_vspace {
|
|||
field type 2
|
||||
}
|
||||
|
||||
#ifdef CONFIG_VTX
|
||||
block asid_map_ept {
|
||||
field_high ept_root 48
|
||||
padding 14
|
||||
field type 2
|
||||
}
|
||||
#endif
|
||||
|
||||
tagged_union asid_map type {
|
||||
tag asid_map_none 0
|
||||
tag asid_map_vspace 1
|
||||
#ifdef CONFIG_VTX
|
||||
tag asid_map_ept 2
|
||||
#endif
|
||||
}
|
||||
|
||||
-- PML4, PDPE, PDs and PTs, assuming 51-bit physical address
|
||||
|
|
@ -485,6 +555,77 @@ block pte {
|
|||
field present 1
|
||||
}
|
||||
|
||||
block ept_pml4e {
|
||||
padding 13
|
||||
field_high pdpt_base_address 39
|
||||
padding 9
|
||||
field execute 1
|
||||
field write 1
|
||||
field read 1
|
||||
}
|
||||
|
||||
block ept_pdpte {
|
||||
padding 13
|
||||
field_high pd_base_address 39
|
||||
field avl_cte_depth 3
|
||||
padding 6
|
||||
field execute 1
|
||||
field write 1
|
||||
field read 1
|
||||
}
|
||||
|
||||
block ept_pde_2m {
|
||||
padding 13
|
||||
field_high page_base_address 31
|
||||
padding 8
|
||||
field avl_cte_depth 2
|
||||
padding 2
|
||||
field page_size 1
|
||||
field ignore_pat 1
|
||||
field type 3
|
||||
field execute 1
|
||||
field write 1
|
||||
field read 1
|
||||
}
|
||||
|
||||
block ept_pde_4k {
|
||||
padding 13
|
||||
field_high pt_base_address 39
|
||||
field avl_cte_depth 3
|
||||
padding 1
|
||||
field page_size 1
|
||||
padding 4
|
||||
field execute 1
|
||||
field write 1
|
||||
field read 1
|
||||
}
|
||||
|
||||
tagged_union ept_pde page_size {
|
||||
tag ept_pde_4k 0
|
||||
tag ept_pde_2m 1
|
||||
}
|
||||
|
||||
block ept_pte {
|
||||
padding 13
|
||||
field_high page_base_address 39
|
||||
field avl_cte_depth 2
|
||||
padding 3
|
||||
field ignore_pat 1
|
||||
field type 3
|
||||
field execute 1
|
||||
field write 1
|
||||
field read 1
|
||||
}
|
||||
|
||||
block vmx_eptp {
|
||||
padding 13
|
||||
field_high paddr 39
|
||||
padding 5
|
||||
field flags 1
|
||||
field depth_minus_1 3
|
||||
field memory_type 3
|
||||
}
|
||||
|
||||
block cr3 {
|
||||
padding 13
|
||||
field_high pml4_base_address 39
|
||||
|
|
|
|||
|
|
@ -140,6 +140,9 @@ cap_get_capMappedASID(cap_t cap)
|
|||
case cap_page_directory_cap:
|
||||
return cap_page_directory_cap_get_capPDMappedASID(cap);
|
||||
|
||||
case cap_ept_pml4_cap:
|
||||
return cap_ept_pml4_cap_get_capPML4MappedASID(cap);
|
||||
|
||||
default:
|
||||
fail("Invalid arch cap type");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -14,6 +14,7 @@
|
|||
#define __ARCH_OBJECT_VCPU_H
|
||||
|
||||
#include <config.h>
|
||||
#include <api/failures.h>
|
||||
|
||||
#define VCPU_VMCS_SIZE 4096
|
||||
#define VCPU_IOBITMAP_SIZE 8192
|
||||
|
|
|
|||
|
|
@ -40,6 +40,12 @@
|
|||
#define seL4_HugePageBits 30
|
||||
#define seL4_ASIDPoolBits 12
|
||||
|
||||
#define seL4_X86_VCPUBits 14
|
||||
#define seL4_X86_EPTPML4Bits 12
|
||||
#define seL4_X86_EPTPDPTBits 12
|
||||
#define seL4_X86_EPTPDBits 12
|
||||
#define seL4_X86_EPTPTBits 12
|
||||
|
||||
/* Untyped size limits */
|
||||
#define seL4_MinUntypedBits 4
|
||||
#define seL4_MaxUntypedBits 47
|
||||
|
|
|
|||
|
|
@ -787,10 +787,20 @@ create_mapped_it_frame_cap(cap_t vspace_cap, pptr_t pptr, vptr_t vptr, asid_t as
|
|||
exception_t
|
||||
performASIDPoolInvocation(asid_t asid, asid_pool_t *poolPtr, cte_t *vspaceCapSlot)
|
||||
{
|
||||
cap_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid);
|
||||
cap_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1);
|
||||
poolPtr->array[asid & MASK(asidLowBits)]
|
||||
= asid_map_asid_map_vspace_new(cap_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap));
|
||||
asid_map_t asid_map;
|
||||
if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) {
|
||||
cap_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid);
|
||||
cap_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1);
|
||||
asid_map = asid_map_asid_map_vspace_new(cap_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap));
|
||||
} else {
|
||||
#ifdef CONFIG_VTX
|
||||
assert(cap_get_capType(vspaceCapSlot->cap) == cap_ept_pml4_cap);
|
||||
cap_ept_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid);
|
||||
cap_ept_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1);
|
||||
asid_map = asid_map_asid_map_ept_new(cap_ept_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap));
|
||||
#endif
|
||||
}
|
||||
poolPtr->array[asid & MASK(asidLowBits)] = asid_map;
|
||||
return EXCEPTION_NONE;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@
|
|||
#include <arch/machine/fpu.h>
|
||||
#include <arch/object/objecttype.h>
|
||||
#include <arch/object/ioport.h>
|
||||
#include <arch/kernel/ept.h>
|
||||
|
||||
#include <arch/object/iospace.h>
|
||||
#include <plat/machine/intel-vtd.h>
|
||||
|
|
|
|||
Loading…
Reference in a new issue