Loading...
Searching...
No Matches
__vm-vmx.h
/*
* (c) 2010-2013 Adam Lackorzynski <adam@os.inf.tu-dresden.de>,
* Alexander Warg <warg@os.inf.tu-dresden.de>
* economic rights: Technische Universität Dresden (Germany)
*
* License: see LICENSE.spdx (in this directory or the directories above)
*/
#pragma once
#include <l4/sys/vcpu.h>
enum L4_vm_vmx_caps_regs
{
L4_VM_VMX_BASIC_REG = 0,
L4_VM_VMX_TRUE_PINBASED_CTLS_REG = 1,
L4_VM_VMX_TRUE_PROCBASED_CTLS_REG = 2,
L4_VM_VMX_TRUE_EXIT_CTLS_REG = 3,
L4_VM_VMX_TRUE_ENTRY_CTLS_REG = 4,
L4_VM_VMX_MISC_REG = 5,
L4_VM_VMX_CR0_FIXED0_REG = 6,
L4_VM_VMX_CR0_FIXED1_REG = 7,
L4_VM_VMX_CR4_FIXED0_REG = 8,
L4_VM_VMX_CR4_FIXED1_REG = 9,
L4_VM_VMX_VMCS_ENUM_REG = 10,
L4_VM_VMX_PROCBASED_CTLS2_REG = 11,
L4_VM_VMX_EPT_VPID_CAP_REG = 12,
L4_VM_VMX_NESTED_REVISION = 13,
L4_VM_VMX_NUM_CAPS_REGS
};
enum L4_vm_vmx_dfl1_regs
{
L4_VM_VMX_PINBASED_CTLS_DFL1_REG = 0,
L4_VM_VMX_PROCBASED_CTLS_DFL1_REG = 1,
L4_VM_VMX_EXIT_CTLS_DFL1_REG = 2,
L4_VM_VMX_ENTRY_CTLS_DFL1_REG = 3,
L4_VM_VMX_NUM_DFL1_REGS
};
enum L4_vm_vmx_sw_fields
{
L4_VM_VMX_VMCS_CR2 = 0x6880,
L4_VM_VMX_VMCS_NAT_ARG0 = 0x6882,
L4_VM_VMX_VMCS_NAT_ARG1 = 0x6884,
L4_VM_VMX_VMCS_NAT_ARG2 = 0x6886,
L4_VM_VMX_VMCS_NAT_ARG3 = 0x6888,
L4_VM_VMX_VMCS_XCR0 = 0x2880,
L4_VM_VMX_VMCS_MSR_SYSCALL_MASK = 0x2882,
L4_VM_VMX_VMCS_MSR_LSTAR = 0x2884,
L4_VM_VMX_VMCS_MSR_CSTAR = 0x2886,
L4_VM_VMX_VMCS_MSR_TSC_AUX = 0x2888,
L4_VM_VMX_VMCS_MSR_STAR = 0x288a,
L4_VM_VMX_VMCS_MSR_KERNEL_GS_BASE = 0x288c,
};
typedef struct l4_vmx_offset_table_t
{
l4_uint8_t offsets[4][4];
l4_uint8_t limits[4][4];
l4_uint8_t index_shifts[4];
l4_uint8_t base_offset;
l4_uint8_t size;
l4_uint8_t reserved[2];
} l4_vmx_offset_table_t;
enum L4_vm_vmx_vmcs_sizes
{
L4_VM_VMX_VMCS_SIZE_VALUES = 2560,
L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP = 320,
};
typedef struct l4_vm_vmx_vcpu_vmcs_t
{
l4_uint64_t reserved0;
l4_uint64_t user_data;
l4_uint32_t cr2_index;
l4_uint8_t reserved1[4];
l4_cap_idx_t vmcs;
/*
* Since the capability type size depends on the platform, we add a 32-bit
* padding if necessary.
*/
#if L4_MWORD_BITS == 32
l4_uint32_t padding0;
#elif L4_MWORD_BITS == 64
/* No padding needed. */
#else
#error Unsupported machine word size.
#endif
l4_vmx_offset_table_t offset_table;
l4_uint8_t reserved2[120];
l4_uint8_t values[L4_VM_VMX_VMCS_SIZE_VALUES];
l4_uint8_t dirty_bitmap[L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP];
} l4_vm_vmx_vcpu_vmcs_t;
typedef struct l4_vm_vmx_vcpu_infos_t
{
l4_uint64_t caps[L4_VM_VMX_NUM_CAPS_REGS];
l4_uint32_t dfl1[L4_VM_VMX_NUM_DFL1_REGS];
} l4_vm_vmx_vcpu_infos_t;
typedef struct l4_vm_vmx_vcpu_state_t
{
l4_vcpu_state_t vcpu_state;
l4_uint8_t padding0[L4_VCPU_OFFSET_EXT_INFOS - sizeof(l4_vcpu_state_t)];
l4_vm_vmx_vcpu_infos_t infos;
l4_uint8_t padding1[L4_VCPU_OFFSET_EXT_STATE - L4_VCPU_OFFSET_EXT_INFOS
- sizeof(l4_vm_vmx_vcpu_infos_t)];
l4_vm_vmx_vcpu_vmcs_t vmcs;
} l4_vm_vmx_vcpu_state_t;
L4_INLINE
l4_uint64_t
l4_vm_vmx_get_caps(l4_vm_vmx_vcpu_state_t const *vcpu_state,
enum L4_vm_vmx_caps_regs caps_reg) L4_NOTHROW;
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_caps_default1(l4_vm_vmx_vcpu_state_t const *vcpu_state,
enum L4_vm_vmx_dfl1_regs dfl1_reg) L4_NOTHROW;
L4_INLINE
unsigned
l4_vm_vmx_field_len(unsigned field) L4_NOTHROW;
L4_INLINE
unsigned
l4_vm_vmx_field_order(unsigned field) L4_NOTHROW;
L4_INLINE
void *
l4_vm_vmx_field_ptr(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_clear(l4_vm_vmx_vcpu_vmcs_t *vmcs,
l4_vm_vmx_vcpu_vmcs_t *dest_vmcs) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_ptr_load(l4_vm_vmx_vcpu_vmcs_t *vmcs,
l4_vm_vmx_vcpu_vmcs_t *src_vmcs) L4_NOTHROW;
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_cr2_index(l4_vm_vmx_vcpu_vmcs_t const *vmcs) L4_NOTHROW;
L4_INLINE
l4_umword_t
l4_vm_vmx_read_nat(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW;
L4_INLINE
l4_uint16_t
l4_vm_vmx_read_16(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW;
L4_INLINE
l4_uint32_t
l4_vm_vmx_read_32(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW;
L4_INLINE
l4_uint64_t
l4_vm_vmx_read_64(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW;
L4_INLINE
l4_uint64_t
l4_vm_vmx_read(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_write_nat(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_umword_t val) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_write_16(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint16_t val) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_write_32(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint32_t val) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_write_64(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint64_t val) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_write(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint64_t val) L4_NOTHROW;
L4_INLINE
void
l4_vm_vmx_set_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs,
l4_cap_idx_t vmcs_cap) L4_NOTHROW;
L4_INLINE
l4_cap_idx_t
l4_vm_vmx_get_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs) L4_NOTHROW;
/* Implementations */
L4_INLINE
unsigned
l4_vm_vmx_field_len(unsigned field) L4_NOTHROW
{
return 1 << l4_vm_vmx_field_order(field);
}
L4_INLINE
unsigned
l4_vm_vmx_field_order(unsigned field) L4_NOTHROW
{
unsigned size = (field >> 13) & 0x03U;
switch (size)
{
case 0: return 1; /* 16 bits */
case 1: return 3; /* 64 bits */
case 2: return 2; /* 32 bits */
case 3: return (sizeof(l4_umword_t) == 8) ? 3 : 2; /* Natural width */
}
__builtin_trap();
}
L4_INLINE
unsigned
l4_vm_vmx_field_offset(l4_vm_vmx_vcpu_vmcs_t const *vmcs,
unsigned field) L4_NOTHROW
{
unsigned index = field & 0x3feU;
unsigned size = (field >> 13) & 0x03U;
unsigned group = (field >> 10) & 0x03U;
unsigned shifted_index = index << vmcs->offset_table.index_shifts[size];
if (shifted_index >= (unsigned)vmcs->offset_table.limits[size][group] * 64)
return ~0U;
return (unsigned)vmcs->offset_table.offsets[size][group] * 64
+ shifted_index;
}
L4_INLINE
void *
l4_vm_vmx_field_ptr(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
{
unsigned offset = l4_vm_vmx_field_offset(vmcs, field);
if (offset == ~0U)
return 0;
return (void *)(vmcs->values + offset);
}
L4_INLINE
void *
l4_vm_vmx_field_ptr_offset(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
unsigned *offset) L4_NOTHROW
{
*offset = l4_vm_vmx_field_offset(vmcs, field);
if (*offset == ~0U)
return 0;
return (void *)(vmcs->values + *offset);
}
L4_INLINE
void
l4_vm_vmx_offset_dirty(l4_vm_vmx_vcpu_vmcs_t *vmcs,
unsigned offset) L4_NOTHROW
{
vmcs->dirty_bitmap[offset / 8] |= 1U << (offset % 8);
}
L4_INLINE
void
l4_vm_vmx_copy_values(l4_vm_vmx_vcpu_vmcs_t const *vmcs, l4_uint8_t *_dst,
l4_uint8_t const *_src) L4_NOTHROW
{
unsigned base_offset = vmcs->offset_table.base_offset * 64;
unsigned size = vmcs->offset_table.size * 64;
void *dst = _dst + base_offset;
void const *src = _src + base_offset;
__builtin_memcpy(dst, src, size);
}
L4_INLINE
void
l4_vm_vmx_clear(l4_vm_vmx_vcpu_vmcs_t *vmcs,
l4_vm_vmx_vcpu_vmcs_t *dest_vmcs) L4_NOTHROW
{
l4_vm_vmx_vcpu_vmcs_t **current_vmcs_ptr
= (l4_vm_vmx_vcpu_vmcs_t **)&vmcs->user_data;
if (*current_vmcs_ptr != dest_vmcs)
return;
l4_vm_vmx_set_hw_vmcs(dest_vmcs, l4_vm_vmx_get_hw_vmcs(vmcs));
l4_vm_vmx_copy_values(vmcs, dest_vmcs->values, vmcs->values);
/* Due to its size, the dirty bitmap is always compied in its entirety. */
__builtin_memcpy(dest_vmcs->dirty_bitmap, vmcs->dirty_bitmap,
L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP);
*current_vmcs_ptr = 0;
}
L4_INLINE
void
l4_vm_vmx_ptr_load(l4_vm_vmx_vcpu_vmcs_t *vmcs,
l4_vm_vmx_vcpu_vmcs_t *src_vmcs) L4_NOTHROW
{
l4_vm_vmx_vcpu_vmcs_t **current_vmcs_ptr
= (l4_vm_vmx_vcpu_vmcs_t **)&vmcs->user_data;
if (*current_vmcs_ptr == src_vmcs)
return;
if (*current_vmcs_ptr && *current_vmcs_ptr != src_vmcs)
l4_vm_vmx_clear(vmcs, *current_vmcs_ptr);
*current_vmcs_ptr = src_vmcs;
l4_vm_vmx_set_hw_vmcs(vmcs, l4_vm_vmx_get_hw_vmcs(src_vmcs));
l4_vm_vmx_copy_values(vmcs, vmcs->values, src_vmcs->values);
/* Due to its size, the dirty bitmap is always compied in its entirety. */
__builtin_memcpy(vmcs->dirty_bitmap, src_vmcs->dirty_bitmap,
L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP);
}
L4_INLINE
l4_umword_t
l4_vm_vmx_read_nat(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
{
l4_umword_t *ptr = (l4_umword_t *)l4_vm_vmx_field_ptr(vmcs, field);
if (!ptr)
return 0;
return *ptr;
}
L4_INLINE
l4_uint16_t
l4_vm_vmx_read_16(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
{
l4_uint16_t *ptr = (l4_uint16_t *)l4_vm_vmx_field_ptr(vmcs, field);
if (!ptr)
return 0;
return *ptr;
}
L4_INLINE
l4_uint32_t
l4_vm_vmx_read_32(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
{
l4_uint32_t *ptr = (l4_uint32_t *)l4_vm_vmx_field_ptr(vmcs, field);
if (!ptr)
return 0;
return *ptr;
}
L4_INLINE
l4_uint64_t
l4_vm_vmx_read_64(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
{
l4_uint64_t *ptr = (l4_uint64_t *)l4_vm_vmx_field_ptr(vmcs, field);
if (!ptr)
return 0;
return *ptr;
}
L4_INLINE
l4_uint64_t
l4_vm_vmx_read(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
{
unsigned size = (field >> 13) & 0x03U;
switch (size)
{
case 0: return l4_vm_vmx_read_16(vmcs, field);
case 1: return l4_vm_vmx_read_64(vmcs, field);
case 2: return l4_vm_vmx_read_32(vmcs, field);
case 3: return l4_vm_vmx_read_nat(vmcs, field);
}
__builtin_trap();
}
L4_INLINE
void
l4_vm_vmx_write_nat(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_umword_t val) L4_NOTHROW
{
unsigned offset;
l4_umword_t *ptr
= (l4_umword_t *)l4_vm_vmx_field_ptr_offset(vmcs, field, &offset);
if ((ptr) && (*ptr != val))
{
*ptr = val;
l4_vm_vmx_offset_dirty(vmcs, offset);
}
}
L4_INLINE
void
l4_vm_vmx_write_16(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint16_t val) L4_NOTHROW
{
unsigned offset;
l4_uint16_t *ptr
= (l4_uint16_t *)l4_vm_vmx_field_ptr_offset(vmcs, field, &offset);
if ((ptr) && (*ptr != val))
{
*ptr = val;
l4_vm_vmx_offset_dirty(vmcs, offset);
}
}
L4_INLINE
void
l4_vm_vmx_write_32(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint32_t val) L4_NOTHROW
{
unsigned offset;
l4_uint32_t *ptr
= (l4_uint32_t *)l4_vm_vmx_field_ptr_offset(vmcs, field, &offset);
if ((ptr) && (*ptr != val))
{
*ptr = val;
l4_vm_vmx_offset_dirty(vmcs, offset);
}
}
L4_INLINE
void
l4_vm_vmx_write_64(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint64_t val) L4_NOTHROW
{
unsigned offset;
l4_uint64_t *ptr
= (l4_uint64_t *)l4_vm_vmx_field_ptr_offset(vmcs, field, &offset);
if ((ptr) && (*ptr != val))
{
*ptr = val;
l4_vm_vmx_offset_dirty(vmcs, offset);
}
}
L4_INLINE
void
l4_vm_vmx_write(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field,
l4_uint64_t val) L4_NOTHROW
{
unsigned size = (field >> 13) & 0x03U;
switch (size)
{
case 0: l4_vm_vmx_write_16(vmcs, field, val); break;
case 1: l4_vm_vmx_write_64(vmcs, field, val); break;
case 2: l4_vm_vmx_write_32(vmcs, field, val); break;
case 3: l4_vm_vmx_write_nat(vmcs, field, val); break;
}
}
L4_INLINE
l4_uint64_t
l4_vm_vmx_get_caps(l4_vm_vmx_vcpu_state_t const *vcpu_state,
enum L4_vm_vmx_caps_regs caps_reg) L4_NOTHROW
{
return vcpu_state->infos.caps[caps_reg];
}
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_caps_default1(l4_vm_vmx_vcpu_state_t const *vcpu_state,
enum L4_vm_vmx_dfl1_regs dfl1_reg) L4_NOTHROW
{
return vcpu_state->infos.dfl1[dfl1_reg];
}
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_cr2_index(l4_vm_vmx_vcpu_vmcs_t const *vmcs) L4_NOTHROW
{
return vmcs->cr2_index;
}
L4_INLINE
void
l4_vm_vmx_set_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs,
l4_cap_idx_t vmcs_cap) L4_NOTHROW
{
vmcs->vmcs = vmcs_cap;
}
L4_INLINE
l4_cap_idx_t
l4_vm_vmx_get_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs) L4_NOTHROW
{
return vmcs->vmcs & L4_CAP_MASK;
}
l4_umword_t
unsigned long l4_umword_t
Unsigned machine word.
Definition l4int.h:40
l4_uint8_t
unsigned char l4_uint8_t
Unsigned 8bit value.
Definition l4int.h:25
l4_uint32_t
unsigned int l4_uint32_t
Unsigned 32bit value.
Definition l4int.h:29
l4_uint16_t
unsigned short int l4_uint16_t
Unsigned 16bit value.
Definition l4int.h:27
l4_uint64_t
unsigned long long l4_uint64_t
Unsigned 64bit value.
Definition l4int.h:31
l4_cap_idx_t
unsigned long l4_cap_idx_t
Capability selector type.
Definition types.h:336
L4_CAP_MASK
@ L4_CAP_MASK
Mask to get only the relevant bits of an l4_cap_idx_t.
Definition consts.h:151
L4_VCPU_OFFSET_EXT_INFOS
@ L4_VCPU_OFFSET_EXT_INFOS
Offset where extended infos begin.
Definition __vcpu-arch.h:38
L4_VCPU_OFFSET_EXT_STATE
@ L4_VCPU_OFFSET_EXT_STATE
Offset where extended state begins.
Definition __vcpu-arch.h:37
l4_vm_vmx_write_nat
void l4_vm_vmx_write_nat(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW
Write to a natural-width software VMCS field.
Definition __vm-vmx.h:804
l4_vm_vmx_write
void l4_vm_vmx_write(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
Write to an arbitrary software VMCS field.
Definition __vm-vmx.h:868
l4_vm_vmx_read_nat
l4_umword_t l4_vm_vmx_read_nat(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
Read a natural-width software VMCS field.
Definition __vm-vmx.h:743
L4_vm_vmx_sw_fields
L4_vm_vmx_sw_fields
Additional (software-defined) VMCS fields.
Definition __vm-vmx.h:70
l4_vm_vmx_read_64
l4_uint64_t l4_vm_vmx_read_64(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
Read a 64-bit software VMCS field.
Definition __vm-vmx.h:776
l4_vm_vmx_field_order
unsigned l4_vm_vmx_field_order(unsigned field) L4_NOTHROW
Return length in power of two (bytes) of a VMCS field.
Definition __vm-vmx.h:600
l4_vm_vmx_ptr_load
void l4_vm_vmx_ptr_load(l4_vm_vmx_vcpu_vmcs_t *vmcs, l4_vm_vmx_vcpu_vmcs_t *src_vmcs) L4_NOTHROW
Load the content from a different software VMCS to the software VMCS.
Definition __vm-vmx.h:719
l4_vm_vmx_get_hw_vmcs
l4_cap_idx_t l4_vm_vmx_get_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs) L4_NOTHROW
Get the vCPU context (i.e.
Definition __vm-vmx.h:915
l4_vm_vmx_get_cr2_index
l4_uint32_t l4_vm_vmx_get_cr2_index(l4_vm_vmx_vcpu_vmcs_t const *vmcs) L4_NOTHROW
Get the software VMCS field index of the virtual CR2 register.
Definition __vm-vmx.h:900
l4_vm_vmx_read_16
l4_uint16_t l4_vm_vmx_read_16(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
Read a 16-bit software VMCS field.
Definition __vm-vmx.h:754
l4_vm_vmx_write_64
void l4_vm_vmx_write_64(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
Write to a 64-bit software VMCS field.
Definition __vm-vmx.h:852
l4_vm_vmx_write_16
void l4_vm_vmx_write_16(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW
Write to a 16-bit software VMCS field.
Definition __vm-vmx.h:820
l4_vm_vmx_read
l4_uint64_t l4_vm_vmx_read(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
Read any software VMCS field.
Definition __vm-vmx.h:787
l4_vm_vmx_set_hw_vmcs
void l4_vm_vmx_set_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs, l4_cap_idx_t vmcs_cap) L4_NOTHROW
Associate the software VMCS with a vCPU context, i.e.
Definition __vm-vmx.h:907
l4_vm_vmx_get_caps_default1
l4_uint32_t l4_vm_vmx_get_caps_default1(l4_vm_vmx_vcpu_state_t const *vcpu_state, enum L4_vm_vmx_dfl1_regs dfl1_reg) L4_NOTHROW
Get a default to one capability register for VMX.
Definition __vm-vmx.h:892
l4_vm_vmx_field_len
unsigned l4_vm_vmx_field_len(unsigned field) L4_NOTHROW
Return length in bytes of a VMCS field.
Definition __vm-vmx.h:593
L4_vm_vmx_caps_regs
L4_vm_vmx_caps_regs
Exported VMX capability registers.
Definition __vm-vmx.h:29
L4_vm_vmx_vmcs_sizes
L4_vm_vmx_vmcs_sizes
Sizes of software VMCS members.
Definition __vm-vmx.h:171
l4_vm_vmx_get_caps
l4_uint64_t l4_vm_vmx_get_caps(l4_vm_vmx_vcpu_state_t const *vcpu_state, enum L4_vm_vmx_caps_regs caps_reg) L4_NOTHROW
Get a capability register for VMX.
Definition __vm-vmx.h:884
l4_vm_vmx_read_32
l4_uint32_t l4_vm_vmx_read_32(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
Read a 32-bit software VMCS field.
Definition __vm-vmx.h:765
l4_vm_vmx_write_32
void l4_vm_vmx_write_32(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW
Write to a 32-bit software VMCS field.
Definition __vm-vmx.h:836
L4_vm_vmx_dfl1_regs
L4_vm_vmx_dfl1_regs
Exported VMX capability registers (default to 1 bits).
Definition __vm-vmx.h:52
l4_vm_vmx_clear
void l4_vm_vmx_clear(l4_vm_vmx_vcpu_vmcs_t *vmcs, l4_vm_vmx_vcpu_vmcs_t *dest_vmcs) L4_NOTHROW
Save the content from the software VMCS to a different software VMCS.
Definition __vm-vmx.h:698
L4_VM_VMX_VMCS_MSR_LSTAR
@ L4_VM_VMX_VMCS_MSR_LSTAR
VMCS offset of IA32e mode system call target address MSR.
Definition __vm-vmx.h:92
L4_VM_VMX_VMCS_NAT_ARG3
@ L4_VM_VMX_VMCS_NAT_ARG3
Custom argument passed from kernel to user space.
Definition __vm-vmx.h:86
L4_VM_VMX_VMCS_MSR_STAR
@ L4_VM_VMX_VMCS_MSR_STAR
VMCS offset of system call target address MSR.
Definition __vm-vmx.h:98
L4_VM_VMX_VMCS_CR2
@ L4_VM_VMX_VMCS_CR2
Software VMCS offset for CR2.
Definition __vm-vmx.h:78
L4_VM_VMX_VMCS_XCR0
@ L4_VM_VMX_VMCS_XCR0
VMCS offset of extended control register XCR0.
Definition __vm-vmx.h:88
L4_VM_VMX_VMCS_MSR_TSC_AUX
@ L4_VM_VMX_VMCS_MSR_TSC_AUX
VMCS offset of auxiliary TSC signature MSR.
Definition __vm-vmx.h:96
L4_VM_VMX_VMCS_NAT_ARG1
@ L4_VM_VMX_VMCS_NAT_ARG1
Custom argument passed from kernel to user space.
Definition __vm-vmx.h:82
L4_VM_VMX_VMCS_MSR_KERNEL_GS_BASE
@ L4_VM_VMX_VMCS_MSR_KERNEL_GS_BASE
VMCS offset of GS base address swap target MSR.
Definition __vm-vmx.h:100
L4_VM_VMX_VMCS_NAT_ARG0
@ L4_VM_VMX_VMCS_NAT_ARG0
Custom argument passed from kernel to user space.
Definition __vm-vmx.h:80
L4_VM_VMX_VMCS_NAT_ARG2
@ L4_VM_VMX_VMCS_NAT_ARG2
Custom argument passed from kernel to user space.
Definition __vm-vmx.h:84
L4_VM_VMX_VMCS_MSR_SYSCALL_MASK
@ L4_VM_VMX_VMCS_MSR_SYSCALL_MASK
VMCS offset of system call flag mask MSR.
Definition __vm-vmx.h:90
L4_VM_VMX_VMCS_MSR_CSTAR
@ L4_VM_VMX_VMCS_MSR_CSTAR
VMCS offset of IA32 mode system call target address MSR.
Definition __vm-vmx.h:94
L4_VM_VMX_TRUE_PROCBASED_CTLS_REG
@ L4_VM_VMX_TRUE_PROCBASED_CTLS_REG
True processor based control caps.
Definition __vm-vmx.h:32
L4_VM_VMX_MISC_REG
@ L4_VM_VMX_MISC_REG
Misc caps.
Definition __vm-vmx.h:35
L4_VM_VMX_PROCBASED_CTLS2_REG
@ L4_VM_VMX_PROCBASED_CTLS2_REG
Processor based control 2 caps.
Definition __vm-vmx.h:41
L4_VM_VMX_EPT_VPID_CAP_REG
@ L4_VM_VMX_EPT_VPID_CAP_REG
EPT and VPID caps.
Definition __vm-vmx.h:42
L4_VM_VMX_CR4_FIXED1_REG
@ L4_VM_VMX_CR4_FIXED1_REG
Fixed to 1 bits of CR4.
Definition __vm-vmx.h:39
L4_VM_VMX_NUM_CAPS_REGS
@ L4_VM_VMX_NUM_CAPS_REGS
Total number of VMX capability registers.
Definition __vm-vmx.h:44
L4_VM_VMX_CR4_FIXED0_REG
@ L4_VM_VMX_CR4_FIXED0_REG
Fixed to 0 bits of CR4.
Definition __vm-vmx.h:38
L4_VM_VMX_TRUE_ENTRY_CTLS_REG
@ L4_VM_VMX_TRUE_ENTRY_CTLS_REG
True entry control caps.
Definition __vm-vmx.h:34
L4_VM_VMX_NESTED_REVISION
@ L4_VM_VMX_NESTED_REVISION
Nested VMCS revision.
Definition __vm-vmx.h:43
L4_VM_VMX_CR0_FIXED1_REG
@ L4_VM_VMX_CR0_FIXED1_REG
Fixed to 1 bits of CR0.
Definition __vm-vmx.h:37
L4_VM_VMX_CR0_FIXED0_REG
@ L4_VM_VMX_CR0_FIXED0_REG
Fixed to 0 bits of CR0.
Definition __vm-vmx.h:36
L4_VM_VMX_VMCS_ENUM_REG
@ L4_VM_VMX_VMCS_ENUM_REG
VMCS enumeration info.
Definition __vm-vmx.h:40
L4_VM_VMX_TRUE_EXIT_CTLS_REG
@ L4_VM_VMX_TRUE_EXIT_CTLS_REG
True exit control caps.
Definition __vm-vmx.h:33
L4_VM_VMX_TRUE_PINBASED_CTLS_REG
@ L4_VM_VMX_TRUE_PINBASED_CTLS_REG
True pin-based control caps.
Definition __vm-vmx.h:31
L4_VM_VMX_BASIC_REG
@ L4_VM_VMX_BASIC_REG
Basic VMX capabilities.
Definition __vm-vmx.h:30
L4_VM_VMX_VMCS_SIZE_VALUES
@ L4_VM_VMX_VMCS_SIZE_VALUES
Size of the software VMCS values member.
Definition __vm-vmx.h:173
L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP
@ L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP
Size of the software VMCS dirty bitmap member.
Definition __vm-vmx.h:175
L4_VM_VMX_ENTRY_CTLS_DFL1_REG
@ L4_VM_VMX_ENTRY_CTLS_DFL1_REG
Default 1 bits in entry controls.
Definition __vm-vmx.h:56
L4_VM_VMX_EXIT_CTLS_DFL1_REG
@ L4_VM_VMX_EXIT_CTLS_DFL1_REG
Default 1 bits in exit controls.
Definition __vm-vmx.h:55
L4_VM_VMX_PINBASED_CTLS_DFL1_REG
@ L4_VM_VMX_PINBASED_CTLS_DFL1_REG
Default 1 bits in pin-based controls.
Definition __vm-vmx.h:53
L4_VM_VMX_NUM_DFL1_REGS
@ L4_VM_VMX_NUM_DFL1_REGS
Total number of default on registers.
Definition __vm-vmx.h:57
L4_VM_VMX_PROCBASED_CTLS_DFL1_REG
@ L4_VM_VMX_PROCBASED_CTLS_DFL1_REG
Default 1 bits in processor-based controls.
Definition __vm-vmx.h:54
L4_NOTHROW
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition compiler.h:161
L4_INLINE
#define L4_INLINE
L4 Inline function attribute.
Definition compiler.h:51
l4_vcpu_state_t
State of a vCPU.
Definition vcpu.h:76
l4_vm_vmx_vcpu_infos_t
VMX information members.
Definition __vm-vmx.h:240
l4_vm_vmx_vcpu_infos_t::caps
l4_uint64_t caps[L4_VM_VMX_NUM_CAPS_REGS]
Exported VMX capability registers. See L4_vm_vmx_caps_regs.
Definition __vm-vmx.h:242
l4_vm_vmx_vcpu_infos_t::dfl1
l4_uint32_t dfl1[L4_VM_VMX_NUM_DFL1_REGS]
Exported VMX capability registers (default to 1 bits).
Definition __vm-vmx.h:246
l4_vm_vmx_vcpu_state_t
VMX vCPU state.
Definition __vm-vmx.h:268
l4_vm_vmx_vcpu_vmcs_t
VMX software VMCS.
Definition __vm-vmx.h:206
l4_vmx_offset_table_t
Software VMCS field offset table.
Definition __vm-vmx.h:156
vcpu.h
vCPU API