__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_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_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,
};
enum L4_vm_vmx_sw_fields {…};
 
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;
typedef struct 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,
};
enum L4_vm_vmx_vmcs_sizes {…};
 
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_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_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;
typedef struct 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_vm_vmx_field_len(unsigned field) L4_NOTHROW {…}
 
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_vm_vmx_field_order(unsigned field) L4_NOTHROW {…}
 
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_vm_vmx_clear(l4_vm_vmx_vcpu_vmcs_t *vmcs, {…}
 
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_vm_vmx_ptr_load(l4_vm_vmx_vcpu_vmcs_t *vmcs, {…}
 
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_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_uint16_t *ptr = (l4_uint16_t *)l4_vm_vmx_field_ptr(vmcs, field);
  if (!ptr)
    return 0;
 
  return *ptr;
}
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_uint32_t *ptr = (l4_uint32_t *)l4_vm_vmx_field_ptr(vmcs, field);
  if (!ptr)
    return 0;
 
  return *ptr;
}
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_uint64_t *ptr = (l4_uint64_t *)l4_vm_vmx_field_ptr(vmcs, field);
  if (!ptr)
    return 0;
 
  return *ptr;
}
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
{
  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_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
{
  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_vm_vmx_write_nat(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, {…}
 
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_vm_vmx_write_16(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, {…}
 
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_vm_vmx_write_32(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, {…}
 
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_vm_vmx_write_64(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, {…}
 
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_vm_vmx_write(l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, {…}
 
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_vm_vmx_get_caps(l4_vm_vmx_vcpu_state_t const *vcpu_state, {…}
 
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_vm_vmx_get_caps_default1(l4_vm_vmx_vcpu_state_t const *vcpu_state, {…}
 
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_vm_vmx_get_cr2_index(l4_vm_vmx_vcpu_vmcs_t const *vmcs) 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
{
  vmcs->vmcs = vmcs_cap;
}
l4_vm_vmx_set_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs, {…}
 
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_vm_vmx_get_hw_vmcs(l4_vm_vmx_vcpu_vmcs_t *vmcs) L4_NOTHROW {…}