__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)
 *
 * This file is part of TUD:OS and distributed under the terms of the
 * GNU General Public License 2.
 * Please see the COPYING-GPL-2 file for details.
 *
 * As a special exception, you may use this file as part of a free software
 * library without restriction.  Specifically, if other files instantiate
 * templates or use macros or inline functions from this file, or you compile
 * this file and link it with other files to produce an executable, this
 * file does not by itself cause the resulting executable to be covered by
 * the GNU General Public License.  This exception does not however
 * invalidate any other reasons why the executable file might be covered by
 * the GNU General Public License.
 */
#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           = 0xa,  
  L4_VM_VMX_PROCBASED_CTLS2_REG     = 0xb,  
  L4_VM_VMX_EPT_VPID_CAP_REG        = 0xc,  
  L4_VM_VMX_NESTED_REVISION         = 0xd,  
  L4_VM_VMX_NUM_CAPS_REGS                   
};
 
 
enum L4_vm_vmx_dfl1_regs
{
  L4_VM_VMX_PINBASED_CTLS_DFL1_REG  = 0x1, 
  L4_VM_VMX_PROCBASED_CTLS_DFL1_REG = 0x2, 
  L4_VM_VMX_EXIT_CTLS_DFL1_REG      = 0x3, 
  L4_VM_VMX_ENTRY_CTLS_DFL1_REG     = 0x4, 
  L4_VM_VMX_NUM_DFL1_REGS                  
};
 
L4_INLINE
l4_uint64_t
l4_vm_vmx_get_caps(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW;
 
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_caps_default1(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW;
 
 
enum L4_vm_vmx_sw_fields
{
  L4_VM_VMX_VMCS_CR2                = 0x683e,
  // Custom argument passed from kernel to user space
  L4_VM_VMX_VMCS_NAT_ARG0           = 0x6840,
  // Custom argument passed from kernel to user space
  L4_VM_VMX_VMCS_NAT_ARG1           = 0x6842,
  // Custom argument passed from kernel to user space
  L4_VM_VMX_VMCS_NAT_ARG2           = 0x6844,
  // Custom argument passed from kernel to user space
  L4_VM_VMX_VMCS_NAT_ARG3           = 0x6846,
  L4_VM_VMX_VMCS_XCR0               = 0x2840,
  L4_VM_VMX_VMCS_MSR_SYSCALL_MASK   = 0x2842,
  L4_VM_VMX_VMCS_MSR_LSTAR          = 0x2844,
  L4_VM_VMX_VMCS_MSR_CSTAR          = 0x2846,
  L4_VM_VMX_VMCS_MSR_TSC_AUX        = 0x2848,
  L4_VM_VMX_VMCS_MSR_STAR           = 0x284a,
  L4_VM_VMX_VMCS_MSR_KERNEL_GS_BASE = 0x284c,
};
 
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_ext_vcpu_state_vmx_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_ext_vcpu_state_vmx_t;
 
 
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(void *vmcs, unsigned field) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_clear(void *vmcs, void *user_vmcs) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW;
 
 
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_cr2_index(void const *vmcs) L4_NOTHROW;
 
L4_INLINE
l4_umword_t
l4_vm_vmx_read_nat(void *vmcs, unsigned field) L4_NOTHROW;
 
L4_INLINE
l4_uint16_t
l4_vm_vmx_read_16(void *vmcs, unsigned field) L4_NOTHROW;
 
L4_INLINE
l4_uint32_t
l4_vm_vmx_read_32(void *vmcs, unsigned field) L4_NOTHROW;
 
L4_INLINE
l4_uint64_t
l4_vm_vmx_read_64(void *vmcs, unsigned field) L4_NOTHROW;
 
L4_INLINE
l4_uint64_t
l4_vm_vmx_read(void *vmcs, unsigned field) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_write_nat(void *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_write_16(void *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_write_32(void *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_write_64(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_write(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW;
 
L4_INLINE
void
l4_vm_vmx_set_hw_vmcs(void *vmcs, l4_cap_idx_t vmcs_cap) L4_NOTHROW;
 
L4_INLINE
l4_cap_idx_t
l4_vm_vmx_get_hw_vmcs(void *vmcs) L4_NOTHROW;
 
 
/* Implementations */
 
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_len(unsigned field) L4_NOTHROW
{
  return 1 << l4_vm_vmx_field_order(field);
}
 
L4_INLINE
unsigned
l4_vm_vmx_field_offset(void const *vmcs, unsigned field) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t const *state = (l4_ext_vcpu_state_vmx_t const *)vmcs;
 
  unsigned index = field & 0x3feU;
  unsigned size = (field >> 13) & 0x03U;
  unsigned group = (field >> 10) & 0x03U;
 
  unsigned shifted_index = index << state->offset_table.index_shifts[size];
 
  if (shifted_index >= (unsigned)state->offset_table.limits[size][group] * 64)
    return ~0U;
 
  return (unsigned)state->offset_table.offsets[size][group] * 64
         + shifted_index;
}
 
L4_INLINE
void *
l4_vm_vmx_field_ptr(void *vmcs, unsigned field) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t *state = (l4_ext_vcpu_state_vmx_t *)vmcs;
 
  unsigned offset = l4_vm_vmx_field_offset(vmcs, field);
  if (offset == ~0U)
    return 0;
 
  return (void *)(state->values + offset);
}
 
L4_INLINE
void *
l4_vm_vmx_field_ptr_offset(void *vmcs, unsigned field, unsigned *offset) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t *state = (l4_ext_vcpu_state_vmx_t *)vmcs;
 
  *offset = l4_vm_vmx_field_offset(vmcs, field);
  if (*offset == ~0U)
    return 0;
 
  return (void *)(state->values + *offset);
}
 
L4_INLINE
void
l4_vm_vmx_offset_dirty(void *vmcs, unsigned offset) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t *state = (l4_ext_vcpu_state_vmx_t *)vmcs;
 
  state->dirty_bitmap[offset / 8] |= 1U << (offset % 8);
}
 
L4_INLINE
void
l4_vm_vmx_copy_values(l4_ext_vcpu_state_vmx_t const *state, l4_uint8_t *_dst,
                      l4_uint8_t const *_src) L4_NOTHROW
{
  unsigned base_offset = state->offset_table.base_offset * 64;
  unsigned size = state->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(void *vmcs, void *user_vmcs) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t *state = (l4_ext_vcpu_state_vmx_t *)vmcs;
  l4_ext_vcpu_state_vmx_t *user_state = (l4_ext_vcpu_state_vmx_t *)user_vmcs;
 
  void **current_vmcs_ptr = (void **)&state->user_data;
  if (*current_vmcs_ptr != user_vmcs)
    return;
 
  l4_vm_vmx_set_hw_vmcs(user_state, l4_vm_vmx_get_hw_vmcs(state));
  l4_vm_vmx_copy_values(state, user_state->values, state->values);
 
  /* Due to its size, the dirty bitmap is always compied in its entirety. */
  __builtin_memcpy(user_state->dirty_bitmap, state->dirty_bitmap,
    L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP);
 
  *current_vmcs_ptr = 0;
}
 
L4_INLINE
void
l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t *state = (l4_ext_vcpu_state_vmx_t *)vmcs;
  l4_ext_vcpu_state_vmx_t *user_state = (l4_ext_vcpu_state_vmx_t *)user_vmcs;
 
  void **current_vmcs_ptr = (void **)&state->user_data;
 
  if (*current_vmcs_ptr == user_vmcs)
    return;
 
  if (*current_vmcs_ptr && *current_vmcs_ptr != user_vmcs)
    l4_vm_vmx_clear(vmcs, *current_vmcs_ptr);
 
  *current_vmcs_ptr = user_vmcs;
 
  l4_vm_vmx_set_hw_vmcs(state, l4_vm_vmx_get_hw_vmcs(user_state));
  l4_vm_vmx_copy_values(state, state->values, user_state->values);
 
  /* Due to its size, the dirty bitmap is always compied in its entirety. */
  __builtin_memcpy(state->dirty_bitmap, user_state->dirty_bitmap,
    L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP);
}
 
L4_INLINE
l4_umword_t
l4_vm_vmx_read_nat(void *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(void *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(void *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(void *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(void *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(void *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(void *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(void *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(void *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(void *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(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
{
  l4_uint64_t const *caps = (l4_uint64_t const *)((char const *)(vcpu_state) + L4_VCPU_OFFSET_EXT_INFOS);
  return caps[cap_msr & 0x0fU];
}
 
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_caps_default1(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
{
  l4_uint32_t const *caps = (l4_uint32_t const *)((char const *)(vcpu_state) + L4_VCPU_OFFSET_EXT_INFOS);
  return caps[L4_VM_VMX_NUM_CAPS_REGS * 2 + ((cap_msr & 0x0fU) - L4_VM_VMX_PINBASED_CTLS_DFL1_REG)];
}
 
L4_INLINE
l4_uint32_t
l4_vm_vmx_get_cr2_index(void const *vmcs) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t const *state = (l4_ext_vcpu_state_vmx_t const *)vmcs;
  return state->cr2_index;
}
 
L4_INLINE
void
l4_vm_vmx_set_hw_vmcs(void *vmcs, l4_cap_idx_t vmcs_cap) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t *state = (l4_ext_vcpu_state_vmx_t *)vmcs;
  state->vmcs = vmcs_cap;
}
 
L4_INLINE
l4_cap_idx_t
l4_vm_vmx_get_hw_vmcs(void *vmcs) L4_NOTHROW
{
  l4_ext_vcpu_state_vmx_t *state = (l4_ext_vcpu_state_vmx_t *)vmcs;
  return state->vmcs & L4_CAP_MASK;
}