L4Re Operating System Framework
Interface and Usage Documentation
Loading...
Searching...
No Matches
__vm-vmx.h
1
6/*
7 * (c) 2010-2013 Adam Lackorzynski <adam@os.inf.tu-dresden.de>,
8 * Alexander Warg <warg@os.inf.tu-dresden.de>
9 * economic rights: Technische Universität Dresden (Germany)
10 *
11 * This file is part of TUD:OS and distributed under the terms of the
12 * GNU General Public License 2.
13 * Please see the COPYING-GPL-2 file for details.
14 *
15 * As a special exception, you may use this file as part of a free software
16 * library without restriction. Specifically, if other files instantiate
17 * templates or use macros or inline functions from this file, or you compile
18 * this file and link it with other files to produce an executable, this
19 * file does not by itself cause the resulting executable to be covered by
20 * the GNU General Public License. This exception does not however
21 * invalidate any other reasons why the executable file might be covered by
22 * the GNU General Public License.
23 */
24#pragma once
25
26#include <l4/sys/vcpu.h>
27
57
58
71
82l4_vm_vmx_get_caps(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW;
83
94l4_vm_vmx_get_caps_default1(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW;
95
96
107{
116 // Custom argument passed from kernel to user space
117 L4_VM_VMX_VMCS_NAT_ARG0 = 0x6840,
118 // Custom argument passed from kernel to user space
119 L4_VM_VMX_VMCS_NAT_ARG1 = 0x6842,
120 // Custom argument passed from kernel to user space
121 L4_VM_VMX_VMCS_NAT_ARG2 = 0x6844,
122 // Custom argument passed from kernel to user space
123 L4_VM_VMX_VMCS_NAT_ARG3 = 0x6846,
138};
139
187{
188 l4_uint8_t offsets[4][4];
189 l4_uint8_t limits[4][4];
190 l4_uint8_t index_shifts[4];
191 l4_uint8_t base_offset;
192 l4_uint8_t size;
193
194 l4_uint8_t reserved[2];
196
197enum L4_vm_vmx_vmcs_sizes
198{
199 L4_VM_VMX_VMCS_SIZE_VALUES = 2560,
200 L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP = 320,
201};
202
232{
233 l4_uint64_t reserved0;
234
235 l4_uint64_t user_data;
236 l4_uint32_t cr2_index;
237 l4_uint8_t reserved1[4];
238
239 l4_cap_idx_t vmcs;
240
241 /*
242 * Since the capability type size depends on the platform, we add a 32-bit
243 * padding if necessary.
244 */
245
246#if L4_MWORD_BITS == 32
247 l4_uint32_t padding0;
248#elif L4_MWORD_BITS == 64
249 /* No padding needed. */
250#else
251 #error Unsupported machine word size.
252#endif
253
254 l4_vmx_offset_table_t offset_table;
255 l4_uint8_t reserved2[120];
256
257 l4_uint8_t values[L4_VM_VMX_VMCS_SIZE_VALUES];
258 l4_uint8_t dirty_bitmap[L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP];
260
261
270unsigned
271l4_vm_vmx_field_len(unsigned field) L4_NOTHROW;
272
281unsigned
282l4_vm_vmx_field_order(unsigned field) L4_NOTHROW;
283
299void *
300l4_vm_vmx_field_ptr(void *vmcs, unsigned field) L4_NOTHROW;
301
312void
313l4_vm_vmx_clear(void *vmcs, void *user_vmcs) L4_NOTHROW;
314
325void
326l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW;
327
328
345l4_vm_vmx_get_cr2_index(void const *vmcs) L4_NOTHROW;
346
358l4_vm_vmx_read_nat(void *vmcs, unsigned field) L4_NOTHROW;
359
371l4_vm_vmx_read_16(void *vmcs, unsigned field) L4_NOTHROW;
372
384l4_vm_vmx_read_32(void *vmcs, unsigned field) L4_NOTHROW;
385
397l4_vm_vmx_read_64(void *vmcs, unsigned field) L4_NOTHROW;
398
410l4_vm_vmx_read(void *vmcs, unsigned field) L4_NOTHROW;
411
421void
422l4_vm_vmx_write_nat(void *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW;
423
433void
434l4_vm_vmx_write_16(void *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW;
435
445void
446l4_vm_vmx_write_32(void *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW;
447
457void
458l4_vm_vmx_write_64(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW;
459
469void
470l4_vm_vmx_write(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW;
471
498void
499l4_vm_vmx_set_hw_vmcs(void *vmcs, l4_cap_idx_t vmcs_cap) L4_NOTHROW;
500
512
513
514/* Implementations */
515
517unsigned
519{
520 unsigned size = (field >> 13) & 0x03U;
521
522 switch (size)
523 {
524 case 0: return 1; /* 16 bits */
525 case 1: return 3; /* 64 bits */
526 case 2: return 2; /* 32 bits */
527 case 3: return (sizeof(l4_umword_t) == 8) ? 3 : 2; /* Natural width */
528 }
529
530 __builtin_trap();
531}
532
534unsigned
536{
537 return 1 << l4_vm_vmx_field_order(field);
538}
539
541unsigned
542l4_vm_vmx_field_offset(void const *vmcs, unsigned field) L4_NOTHROW
543{
544 l4_ext_vcpu_state_vmx_t const *state = (l4_ext_vcpu_state_vmx_t const *)vmcs;
545
546 unsigned index = field & 0x3feU;
547 unsigned size = (field >> 13) & 0x03U;
548 unsigned group = (field >> 10) & 0x03U;
549
550 unsigned shifted_index = index << state->offset_table.index_shifts[size];
551
552 if (shifted_index >= (unsigned)state->offset_table.limits[size][group] * 64)
553 return ~0U;
554
555 return (unsigned)state->offset_table.offsets[size][group] * 64
556 + shifted_index;
557}
558
560void *
561l4_vm_vmx_field_ptr(void *vmcs, unsigned field) L4_NOTHROW
562{
564
565 unsigned offset = l4_vm_vmx_field_offset(vmcs, field);
566 if (offset == ~0U)
567 return 0;
568
569 return (void *)(state->values + offset);
570}
571
578void *
579l4_vm_vmx_field_ptr_offset(void *vmcs, unsigned field, unsigned *offset) L4_NOTHROW
580{
582
583 *offset = l4_vm_vmx_field_offset(vmcs, field);
584 if (*offset == ~0U)
585 return 0;
586
587 return (void *)(state->values + *offset);
588}
589
596void
597l4_vm_vmx_offset_dirty(void *vmcs, unsigned offset) L4_NOTHROW
598{
600
601 state->dirty_bitmap[offset / 8] |= 1U << (offset % 8);
602}
603
609void
610l4_vm_vmx_copy_values(l4_ext_vcpu_state_vmx_t const *state, l4_uint8_t *_dst,
611 l4_uint8_t const *_src) L4_NOTHROW
612{
613 unsigned base_offset = state->offset_table.base_offset * 64;
614 unsigned size = state->offset_table.size * 64;
615
616 void *dst = _dst + base_offset;
617 void const *src = _src + base_offset;
618 __builtin_memcpy(dst, src, size);
619}
620
622void
623l4_vm_vmx_clear(void *vmcs, void *user_vmcs) L4_NOTHROW
624{
626 l4_ext_vcpu_state_vmx_t *user_state = (l4_ext_vcpu_state_vmx_t *)user_vmcs;
627
628 void **current_vmcs_ptr = (void **)&state->user_data;
629 if (*current_vmcs_ptr != user_vmcs)
630 return;
631
633 l4_vm_vmx_copy_values(state, user_state->values, state->values);
634
635 /* Due to its size, the dirty bitmap is always compied in its entirety. */
636 __builtin_memcpy(user_state->dirty_bitmap, state->dirty_bitmap,
637 L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP);
638
639 *current_vmcs_ptr = 0;
640}
641
643void
644l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW
645{
647 l4_ext_vcpu_state_vmx_t *user_state = (l4_ext_vcpu_state_vmx_t *)user_vmcs;
648
649 void **current_vmcs_ptr = (void **)&state->user_data;
650
651 if (*current_vmcs_ptr == user_vmcs)
652 return;
653
654 if (*current_vmcs_ptr && *current_vmcs_ptr != user_vmcs)
655 l4_vm_vmx_clear(vmcs, *current_vmcs_ptr);
656
657 *current_vmcs_ptr = user_vmcs;
658
660 l4_vm_vmx_copy_values(state, state->values, user_state->values);
661
662 /* Due to its size, the dirty bitmap is always compied in its entirety. */
663 __builtin_memcpy(state->dirty_bitmap, user_state->dirty_bitmap,
664 L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP);
665}
666
669l4_vm_vmx_read_nat(void *vmcs, unsigned field) L4_NOTHROW
670{
671 l4_umword_t *ptr = (l4_umword_t *)l4_vm_vmx_field_ptr(vmcs, field);
672 if (!ptr)
673 return 0;
674
675 return *ptr;
676}
677
680l4_vm_vmx_read_16(void *vmcs, unsigned field) L4_NOTHROW
681{
682 l4_uint16_t *ptr = (l4_uint16_t *)l4_vm_vmx_field_ptr(vmcs, field);
683 if (!ptr)
684 return 0;
685
686 return *ptr;
687}
688
691l4_vm_vmx_read_32(void *vmcs, unsigned field) L4_NOTHROW
692{
693 l4_uint32_t *ptr = (l4_uint32_t *)l4_vm_vmx_field_ptr(vmcs, field);
694 if (!ptr)
695 return 0;
696
697 return *ptr;
698}
699
702l4_vm_vmx_read_64(void *vmcs, unsigned field) L4_NOTHROW
703{
704 l4_uint64_t *ptr = (l4_uint64_t *)l4_vm_vmx_field_ptr(vmcs, field);
705 if (!ptr)
706 return 0;
707
708 return *ptr;
709}
710
713l4_vm_vmx_read(void *vmcs, unsigned field) L4_NOTHROW
714{
715 unsigned size = (field >> 13) & 0x03U;
716
717 switch (size)
718 {
719 case 0: return l4_vm_vmx_read_16(vmcs, field);
720 case 1: return l4_vm_vmx_read_64(vmcs, field);
721 case 2: return l4_vm_vmx_read_32(vmcs, field);
722 case 3: return l4_vm_vmx_read_nat(vmcs, field);
723 }
724
725 __builtin_trap();
726}
727
729void
730l4_vm_vmx_write_nat(void *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW
731{
732 unsigned offset;
733 l4_umword_t *ptr = (l4_umword_t *)l4_vm_vmx_field_ptr_offset(vmcs, field,
734 &offset);
735
736 if ((ptr) && (*ptr != val))
737 {
738 *ptr = val;
739 l4_vm_vmx_offset_dirty(vmcs, offset);
740 }
741}
742
744void
745l4_vm_vmx_write_16(void *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW
746{
747 unsigned offset;
748 l4_uint16_t *ptr = (l4_uint16_t *)l4_vm_vmx_field_ptr_offset(vmcs, field,
749 &offset);
750
751 if ((ptr) && (*ptr != val))
752 {
753 *ptr = val;
754 l4_vm_vmx_offset_dirty(vmcs, offset);
755 }
756}
757
759void
760l4_vm_vmx_write_32(void *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW
761{
762 unsigned offset;
763 l4_uint32_t *ptr = (l4_uint32_t *)l4_vm_vmx_field_ptr_offset(vmcs, field,
764 &offset);
765
766 if ((ptr) && (*ptr != val))
767 {
768 *ptr = val;
769 l4_vm_vmx_offset_dirty(vmcs, offset);
770 }
771}
772
774void
775l4_vm_vmx_write_64(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
776{
777 unsigned offset;
778 l4_uint64_t *ptr = (l4_uint64_t *)l4_vm_vmx_field_ptr_offset(vmcs, field,
779 &offset);
780
781 if ((ptr) && (*ptr != val))
782 {
783 *ptr = val;
784 l4_vm_vmx_offset_dirty(vmcs, offset);
785 }
786}
787
789void
790l4_vm_vmx_write(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
791{
792 unsigned size = (field >> 13) & 0x03U;
793
794 switch (size)
795 {
796 case 0: l4_vm_vmx_write_16(vmcs, field, val); break;
797 case 1: l4_vm_vmx_write_64(vmcs, field, val); break;
798 case 2: l4_vm_vmx_write_32(vmcs, field, val); break;
799 case 3: l4_vm_vmx_write_nat(vmcs, field, val); break;
800 }
801}
802
805l4_vm_vmx_get_caps(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
806{
807 l4_uint64_t const *caps = (l4_uint64_t const *)((char const *)(vcpu_state) + L4_VCPU_OFFSET_EXT_INFOS);
808 return caps[cap_msr & 0x0fU];
809}
810
813l4_vm_vmx_get_caps_default1(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
814{
815 l4_uint32_t const *caps = (l4_uint32_t const *)((char const *)(vcpu_state) + L4_VCPU_OFFSET_EXT_INFOS);
816 return caps[L4_VM_VMX_NUM_CAPS_REGS * 2 + ((cap_msr & 0x0fU) - L4_VM_VMX_PINBASED_CTLS_DFL1_REG)];
817}
818
822{
823 l4_ext_vcpu_state_vmx_t const *state = (l4_ext_vcpu_state_vmx_t const *)vmcs;
824 return state->cr2_index;
825}
826
828void
830{
832 state->vmcs = vmcs_cap;
833}
834
838{
840 return state->vmcs & L4_CAP_MASK;
841}
unsigned long l4_umword_t
Unsigned machine word.
Definition l4int.h:51
unsigned char l4_uint8_t
Unsigned 8bit value.
Definition l4int.h:36
unsigned int l4_uint32_t
Unsigned 32bit value.
Definition l4int.h:40
unsigned short int l4_uint16_t
Unsigned 16bit value.
Definition l4int.h:38
unsigned long long l4_uint64_t
Unsigned 64bit value.
Definition l4int.h:42
unsigned long l4_cap_idx_t
Capability selector type.
Definition types.h:359
@ L4_CAP_MASK
Mask to get only the relevant bits of an l4_cap_idx_t.
Definition consts.h:166
@ L4_VCPU_OFFSET_EXT_INFOS
Offset where extended infos begin.
Definition __vcpu-arch.h:49
void l4_vm_vmx_write_nat(void *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW
Write to a natural-width software VMCS field.
Definition __vm-vmx.h:730
void l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW
Loads the user_vmcs as the current software VMCS.
Definition __vm-vmx.h:644
l4_uint16_t l4_vm_vmx_read_16(void *vmcs, unsigned field) L4_NOTHROW
Read a 16-bit software VMCS field.
Definition __vm-vmx.h:680
L4_vm_vmx_sw_fields
Additional (virtual) VMCS fields.
Definition __vm-vmx.h:107
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:518
void l4_vm_vmx_write_32(void *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW
Write to a 32-bit software VMCS field.
Definition __vm-vmx.h:760
l4_uint32_t l4_vm_vmx_get_cr2_index(void const *vmcs) L4_NOTHROW
Get the software VMCS field index of the virtual CR2 register.
Definition __vm-vmx.h:821
void l4_vm_vmx_clear(void *vmcs, void *user_vmcs) L4_NOTHROW
Saves cached state from the kernel software VMCS to the user software VMCS.
Definition __vm-vmx.h:623
l4_uint64_t l4_vm_vmx_read(void *vmcs, unsigned field) L4_NOTHROW
Read any software VMCS field.
Definition __vm-vmx.h:713
l4_uint32_t l4_vm_vmx_read_32(void *vmcs, unsigned field) L4_NOTHROW
Read a 32-bit software VMCS field.
Definition __vm-vmx.h:691
l4_cap_idx_t l4_vm_vmx_get_hw_vmcs(void *vmcs) L4_NOTHROW
Get the hardware VMCS object capability associated with the software VMCS.
Definition __vm-vmx.h:837
unsigned l4_vm_vmx_field_len(unsigned field) L4_NOTHROW
Return length in bytes of a VMCS field.
Definition __vm-vmx.h:535
L4_vm_vmx_caps_regs
Exported VMX capability registers.
Definition __vm-vmx.h:40
l4_uint32_t l4_vm_vmx_get_caps_default1(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
Get a default to one capability register for VMX.
Definition __vm-vmx.h:813
void l4_vm_vmx_write(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
Write to an arbitrary software VMCS field.
Definition __vm-vmx.h:790
void l4_vm_vmx_write_64(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
Write to a 64-bit software VMCS field.
Definition __vm-vmx.h:775
l4_umword_t l4_vm_vmx_read_nat(void *vmcs, unsigned field) L4_NOTHROW
Read a natural-width software VMCS field.
Definition __vm-vmx.h:669
l4_uint64_t l4_vm_vmx_read_64(void *vmcs, unsigned field) L4_NOTHROW
Read a 64-bit software VMCS field.
Definition __vm-vmx.h:702
L4_vm_vmx_dfl1_regs
Exported VMX capability registers (default to 1 bits).
Definition __vm-vmx.h:64
l4_uint64_t l4_vm_vmx_get_caps(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
Get a capability register for VMX.
Definition __vm-vmx.h:805
void l4_vm_vmx_write_16(void *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW
Write to a 16-bit software VMCS field.
Definition __vm-vmx.h:745
void l4_vm_vmx_set_hw_vmcs(void *vmcs, l4_cap_idx_t vmcs_cap) L4_NOTHROW
Associate the software VMCS with a hardware VMCS object capability.
Definition __vm-vmx.h:829
@ L4_VM_VMX_VMCS_MSR_LSTAR
VMCS offset of IA32e mode system call target address MSR.
Definition __vm-vmx.h:129
@ L4_VM_VMX_VMCS_MSR_STAR
VMCS offset of system call target address MSR.
Definition __vm-vmx.h:135
@ L4_VM_VMX_VMCS_CR2
VMCS offset for CR2.
Definition __vm-vmx.h:115
@ L4_VM_VMX_VMCS_XCR0
VMCS offset of extended control register XCR0.
Definition __vm-vmx.h:125
@ L4_VM_VMX_VMCS_MSR_TSC_AUX
VMCS offset of auxiliary TSC signature MSR.
Definition __vm-vmx.h:133
@ L4_VM_VMX_VMCS_MSR_KERNEL_GS_BASE
VMCS offset of GS base address swap target MSR.
Definition __vm-vmx.h:137
@ L4_VM_VMX_VMCS_MSR_SYSCALL_MASK
VMCS offset of system call flag mask MSR.
Definition __vm-vmx.h:127
@ L4_VM_VMX_VMCS_MSR_CSTAR
VMCS offset of IA32 mode system call target address MSR.
Definition __vm-vmx.h:131
@ L4_VM_VMX_TRUE_PROCBASED_CTLS_REG
True processor based control caps.
Definition __vm-vmx.h:43
@ L4_VM_VMX_MISC_REG
Misc caps.
Definition __vm-vmx.h:46
@ L4_VM_VMX_PROCBASED_CTLS2_REG
Processor based control 2 caps.
Definition __vm-vmx.h:52
@ L4_VM_VMX_EPT_VPID_CAP_REG
EPT and VPID caps.
Definition __vm-vmx.h:53
@ L4_VM_VMX_CR4_FIXED1_REG
Fixed to 1 bits of CR4.
Definition __vm-vmx.h:50
@ L4_VM_VMX_NUM_CAPS_REGS
Total number of VMX capability registers.
Definition __vm-vmx.h:55
@ L4_VM_VMX_CR4_FIXED0_REG
Fixed to 0 bits of CR4.
Definition __vm-vmx.h:49
@ L4_VM_VMX_TRUE_ENTRY_CTLS_REG
True entry control caps.
Definition __vm-vmx.h:45
@ L4_VM_VMX_NESTED_REVISION
Nested VMCS revision.
Definition __vm-vmx.h:54
@ L4_VM_VMX_CR0_FIXED1_REG
Fixed to 1 bits of CR0.
Definition __vm-vmx.h:48
@ L4_VM_VMX_CR0_FIXED0_REG
Fixed to 0 bits of CR0.
Definition __vm-vmx.h:47
@ L4_VM_VMX_VMCS_ENUM_REG
VMCS enumeration info.
Definition __vm-vmx.h:51
@ L4_VM_VMX_TRUE_EXIT_CTLS_REG
True exit control caps.
Definition __vm-vmx.h:44
@ L4_VM_VMX_TRUE_PINBASED_CTLS_REG
True pin-based control caps.
Definition __vm-vmx.h:42
@ L4_VM_VMX_BASIC_REG
Basic VMX capabilities.
Definition __vm-vmx.h:41
@ L4_VM_VMX_ENTRY_CTLS_DFL1_REG
Default 1 bits in entry controls.
Definition __vm-vmx.h:68
@ L4_VM_VMX_EXIT_CTLS_DFL1_REG
Default 1 bits in exit controls.
Definition __vm-vmx.h:67
@ L4_VM_VMX_PINBASED_CTLS_DFL1_REG
Default 1 bits in pin-based controls.
Definition __vm-vmx.h:65
@ L4_VM_VMX_NUM_DFL1_REGS
Total number of default on registers.
Definition __vm-vmx.h:69
@ L4_VM_VMX_PROCBASED_CTLS_DFL1_REG
Default 1 bits in processor-based controls.
Definition __vm-vmx.h:66
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition compiler.h:188
#define L4_INLINE
L4 Inline function attribute.
Definition compiler.h:62
VMX extended vCPU state.
Definition __vm-vmx.h:232
Software VMCS field offset table.
Definition __vm-vmx.h:187
vCPU API