L4Re - L4 Runtime Environment
__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 
40 {
55 };
56 
57 
63 {
69 };
70 
79 L4_INLINE
81 l4_vm_vmx_get_caps(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW;
82 
91 L4_INLINE
93 l4_vm_vmx_get_caps_default1(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW;
94 
95 
105 enum
106 {
129 };
130 
138 L4_INLINE
139 unsigned
140 l4_vm_vmx_field_len(unsigned field) L4_NOTHROW;
141 
149 L4_INLINE
150 unsigned
151 l4_vm_vmx_field_order(unsigned field) L4_NOTHROW;
152 
163 L4_INLINE
164 void *
165 l4_vm_vmx_field_ptr(void *vmcs, unsigned field) L4_NOTHROW;
166 
176 L4_INLINE
177 void
178 l4_vm_vmx_clear(void *vmcs, void *user_vmcs) L4_NOTHROW;
179 
189 L4_INLINE
190 void
191 l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW;
192 
193 
208 L4_INLINE
210 l4_vm_vmx_get_cr2_index(void const *vmcs) L4_NOTHROW;
211 
221 L4_INLINE
223 l4_vm_vmx_read_nat(void *vmcs, unsigned field) L4_NOTHROW;
224 
234 L4_INLINE
236 l4_vm_vmx_read_16(void *vmcs, unsigned field) L4_NOTHROW;
237 
247 L4_INLINE
249 l4_vm_vmx_read_32(void *vmcs, unsigned field) L4_NOTHROW;
250 
260 L4_INLINE
262 l4_vm_vmx_read_64(void *vmcs, unsigned field) L4_NOTHROW;
263 
273 L4_INLINE
275 l4_vm_vmx_read(void *vmcs, unsigned field) L4_NOTHROW;
276 
285 L4_INLINE
286 void
287 l4_vm_vmx_write_nat(void *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW;
288 
297 L4_INLINE
298 void
299 l4_vm_vmx_write_16(void *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW;
300 
309 L4_INLINE
310 void
311 l4_vm_vmx_write_32(void *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW;
312 
321 L4_INLINE
322 void
323 l4_vm_vmx_write_64(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW;
324 
333 L4_INLINE
334 void
335 l4_vm_vmx_write(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW;
336 
337 
338 /* Implementations */
339 
340 L4_INLINE
341 unsigned
343 {
344  switch (field >> 13)
345  {
346  case 0: return 1;
347  case 1: return 3;
348  case 2: return 2;
349  case 3: if (sizeof(l4_umword_t) == 8) return 3; else return 2;
350  default: return 0;
351  }
352 }
353 
354 
355 L4_INLINE
356 unsigned
358 {
359  return 1 << l4_vm_vmx_field_order(field);
360 }
361 
362 
363 /* Internal VCPU state layout:
364  *
365  * VCPU State:
366  * 0 - xxx: normal IA32 VCPU state (l4_vcpu_state_t)
367  * 200h: VMX capabilities (see l4_vm_vmx_get_caps)
368  * 400h: Fiasco.OC VMCS
369  *
370  * Fiasco.OC VMCS:
371  * 0h - 7h: Reserved
372  * 8h - Fh: ignored by kernel, stores current VMCS for l4_vm_vmx_clear...
373  * 10h - 13h: L4_VM_VMX_VMCS_CR2 value used by the kernel
374  * 14h - 1Fh: Reserved
375  * 20h - 3Fh: VMCS field offset table
376  * 40h - BFFh: Data (VMCS field data)
377  *
378  * VMCS field offset table:
379  * 0h - 2h: 3 offsets for 16bit fields:
380  * 0: Control fields, 1: read-only fields, 2: guest state
381  * all offsets in 64byte granules relative to the start of the VMCS
382  * 3h: Reserved
383  * 4h - 7h: Index shift values for 16bit, 64bit, 32bit, and natural width fields
384  * 8h - Ah: 3 offsets for 64bit fields
385  * Bh - Fh: Reserved
386  * 10h - 12h: 3 offsets for 32bit fields
387  * 13h - 17h: Reserved
388  * 18h - 1Ah: 3 offsets for natural width fields
389  * 1Bh: Reserved
390  * 1Ch: Offset of first VMCS field
391  * 1Dh: Full size of VMCS fields
392  * 1Eh - 1Fh: Reserved
393  *
394  */
395 
396 L4_INLINE
397 unsigned
398 l4_vm_vmx_field_offset(void const *vmcs, unsigned field) L4_NOTHROW
399 {
400  // the offset table is at 0x20 offset
401  enum { Si = 4 };
402  l4_uint8_t const *offsets = (l4_uint8_t const *)vmcs;
403  offsets += 0x20;
404  return (unsigned)offsets[field >> 10] * 64 + ((field & 0x3ff) << offsets[Si + (field >> 13)]);
405 }
406 
407 L4_INLINE
408 void *
409 l4_vm_vmx_field_ptr(void *vmcs, unsigned field) L4_NOTHROW
410 {
411  return (void *)((char *)vmcs + l4_vm_vmx_field_offset(vmcs, field));
412 }
413 
418 L4_INLINE
419 void
420 l4_vm_vmx_copy_state(void const *vmcs, void *_dst, void const *_src) L4_NOTHROW
421 {
422  l4_uint8_t const *offsets = (l4_uint8_t const *)vmcs + 0x20;
423 
424  unsigned offs = offsets[28] * 64;
425  unsigned size = offsets[29] * 64;
426  char *const dst = (char*)_dst + offs;
427  char const *const src = (char const *)_src + offs;
428  __builtin_memcpy(dst, src, size);
429 }
430 
431 L4_INLINE
432 void
433 l4_vm_vmx_clear(void *vmcs, void *user_vmcs) L4_NOTHROW
434 {
435  void **current_vmcs = (void **)((char *)vmcs + 8);
436  if (*current_vmcs != user_vmcs)
437  return;
438 
439  l4_vm_vmx_copy_state(vmcs, user_vmcs, vmcs);
440  *current_vmcs = 0;
441 }
442 
443 L4_INLINE
444 void
445 l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW
446 {
447  void **current_vmcs = (void **)((char *)vmcs + 8);
448  if (*current_vmcs == user_vmcs)
449  return;
450 
451  if (*current_vmcs && *current_vmcs != user_vmcs)
452  l4_vm_vmx_clear(vmcs, *current_vmcs);
453 
454  *current_vmcs = user_vmcs;
455  l4_vm_vmx_copy_state(vmcs, vmcs, user_vmcs);
456 }
457 
458 
459 L4_INLINE
461 l4_vm_vmx_read_nat(void *vmcs, unsigned field) L4_NOTHROW
462 { return *(l4_umword_t*)(l4_vm_vmx_field_ptr(vmcs, field)); }
463 
464 L4_INLINE
466 l4_vm_vmx_read_16(void *vmcs, unsigned field) L4_NOTHROW
467 { return *(l4_uint16_t*)(l4_vm_vmx_field_ptr(vmcs, field)); }
468 
469 L4_INLINE
471 l4_vm_vmx_read_32(void *vmcs, unsigned field) L4_NOTHROW
472 { return *(l4_uint32_t*)(l4_vm_vmx_field_ptr(vmcs, field)); }
473 
474 L4_INLINE
476 l4_vm_vmx_read_64(void *vmcs, unsigned field) L4_NOTHROW
477 { return *(l4_uint64_t*)(l4_vm_vmx_field_ptr(vmcs, field)); }
478 
479 L4_INLINE
481 l4_vm_vmx_read(void *vmcs, unsigned field) L4_NOTHROW
482 {
483  switch(field >> 13)
484  {
485  case 0: return l4_vm_vmx_read_16(vmcs, field);
486  case 1: return l4_vm_vmx_read_64(vmcs, field);
487  case 2: return l4_vm_vmx_read_32(vmcs, field);
488  case 3: return l4_vm_vmx_read_nat(vmcs, field);
489  }
490  __builtin_trap();
491 }
492 
493 L4_INLINE
494 void
495 l4_vm_vmx_write_nat(void *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW
496 { *(l4_umword_t*)(l4_vm_vmx_field_ptr(vmcs, field)) = val; }
497 
498 L4_INLINE
499 void
500 l4_vm_vmx_write_16(void *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW
501 { *(l4_uint16_t*)(l4_vm_vmx_field_ptr(vmcs, field)) = val; }
502 
503 L4_INLINE
504 void
505 l4_vm_vmx_write_32(void *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW
506 { *(l4_uint32_t*)(l4_vm_vmx_field_ptr(vmcs, field)) = val; }
507 
508 L4_INLINE
509 void
510 l4_vm_vmx_write_64(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
511 { *(l4_uint64_t*)(l4_vm_vmx_field_ptr(vmcs, field)) = val; }
512 
513 
514 L4_INLINE
515 void
516 l4_vm_vmx_write(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
517 {
518  switch(field >> 13)
519  {
520  case 0: l4_vm_vmx_write_16(vmcs, field, val); break;
521  case 1: l4_vm_vmx_write_64(vmcs, field, val); break;
522  case 2: l4_vm_vmx_write_32(vmcs, field, val); break;
523  case 3: l4_vm_vmx_write_nat(vmcs, field, val); break;
524  }
525 }
526 
527 L4_INLINE
529 l4_vm_vmx_get_caps(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
530 {
531  l4_uint64_t const *caps = (l4_uint64_t const *)((char const *)(vcpu_state) + L4_VCPU_OFFSET_EXT_INFOS);
532  return caps[cap_msr & 0xf];
533 }
534 
535 L4_INLINE
537 l4_vm_vmx_get_caps_default1(void const *vcpu_state, unsigned cap_msr) L4_NOTHROW
538 {
539  l4_uint32_t const *caps = (l4_uint32_t const *)((char const *)(vcpu_state) + L4_VCPU_OFFSET_EXT_INFOS);
540  return caps[L4_VM_VMX_NUM_CAPS_REGS * 2 + ((cap_msr & 0xf) - L4_VM_VMX_PINBASED_CTLS_DFL1_REG)];
541 }
542 
543 L4_INLINE
546 {
547  l4_uint32_t const *infos = (l4_uint32_t const *)vmcs;
548  return infos[3];
549 }
VMCS enumeration info.
Definition: __vm-vmx.h:51
Basic VMX capabilities.
Definition: __vm-vmx.h:41
void l4_vm_vmx_ptr_load(void *vmcs, void *user_vmcs) L4_NOTHROW
Loads the user_vmcs as the current VMCS.
Definition: __vm-vmx.h:445
void l4_vm_vmx_write_nat(void *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW
Write to a natural width VMCS field.
Definition: __vm-vmx.h:495
Default 1 bits in exit controls.
Definition: __vm-vmx.h:66
void l4_vm_vmx_write_32(void *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW
Write to a 32bit VMCS field.
Definition: __vm-vmx.h:505
Fixed to 0 bits of CR0.
Definition: __vm-vmx.h:47
VMCS offset of IA32e mode system call target address MSR.
Definition: __vm-vmx.h:120
VMCS offset of auxiliary TSC signature MSR.
Definition: __vm-vmx.h:124
unsigned short int l4_uint16_t
Unsigned 16bit value.
Definition: l4int.h:38
l4_uint16_t l4_vm_vmx_read_16(void *vmcs, unsigned field) L4_NOTHROW
Read a 16bit VMCS field.
Definition: __vm-vmx.h:466
Default 1 bits in processor-based controls.
Definition: __vm-vmx.h:65
Fixed to 0 bits of CR4.
Definition: __vm-vmx.h:49
L4_vm_vmx_dfl1_regs
Exported VMX capability registers (default to 1 bits).
Definition: __vm-vmx.h:62
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:342
void l4_vm_vmx_write(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
Write to an arbitrary VMCS field.
Definition: __vm-vmx.h:516
True pin-based control caps.
Definition: __vm-vmx.h:42
Offset where extended infos begin.
Definition: vcpu.h:97
Fixed to 1 bits of CR4.
Definition: __vm-vmx.h:50
unsigned l4_vm_vmx_field_len(unsigned field) L4_NOTHROW
Return length in bytes of a VMCS field.
Definition: __vm-vmx.h:357
Total number of VMX capability registers.
Definition: __vm-vmx.h:54
l4_uint32_t l4_vm_vmx_read_32(void *vmcs, unsigned field) L4_NOTHROW
Read a 32bit VMCS field.
Definition: __vm-vmx.h:471
VMCS offset of GS base address swap target MSR.
Definition: __vm-vmx.h:128
VMCS offset of IA32 mode system call target address MSR.
Definition: __vm-vmx.h:122
Default 1 bits in pin-based controls.
Definition: __vm-vmx.h:64
VMCS offset of system call flag mask MSR.
Definition: __vm-vmx.h:118
void l4_vm_vmx_write_64(void *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
Write to a 64bit VMCS field.
Definition: __vm-vmx.h:510
Misc caps.
Definition: __vm-vmx.h:46
True entry control caps.
Definition: __vm-vmx.h:45
Default 1 bits in entry controls.
Definition: __vm-vmx.h:67
VMCS offset of system call target address MSR.
Definition: __vm-vmx.h:126
unsigned long l4_umword_t
Unsigned machine word.
Definition: l4int.h:52
void l4_vm_vmx_clear(void *vmcs, void *user_vmcs) L4_NOTHROW
Saves cached state from the kernel VMCS to the user VMCS.
Definition: __vm-vmx.h:433
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:529
l4_uint64_t l4_vm_vmx_read(void *vmcs, unsigned field) L4_NOTHROW
Read any VMCS field.
Definition: __vm-vmx.h:481
l4_uint64_t l4_vm_vmx_read_64(void *vmcs, unsigned field) L4_NOTHROW
Read a 64bit VMCS field.
Definition: __vm-vmx.h:476
VMCS offset of extended control register XCR0.
Definition: __vm-vmx.h:116
unsigned char l4_uint8_t
Unsigned 8bit value.
Definition: l4int.h:36
l4_umword_t l4_vm_vmx_read_nat(void *vmcs, unsigned field) L4_NOTHROW
Read a natural width VMCS field.
Definition: __vm-vmx.h:461
True processor based control caps.
Definition: __vm-vmx.h:43
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:537
Total number of default on registers.
Definition: __vm-vmx.h:68
void l4_vm_vmx_write_16(void *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW
Write to a 16bit VMCS field.
Definition: __vm-vmx.h:500
unsigned long long l4_uint64_t
Unsigned 64bit value.
Definition: l4int.h:42
Fixed to 1 bits of CR0.
Definition: __vm-vmx.h:48
Processor based control 2 caps.
Definition: __vm-vmx.h:52
VMCS offset for CR2.
Definition: __vm-vmx.h:114
True exit control caps.
Definition: __vm-vmx.h:44
unsigned int l4_uint32_t
Unsigned 32bit value.
Definition: l4int.h:40
L4_vm_vmx_caps_regs
Exported VMX capability registers.
Definition: __vm-vmx.h:39
l4_uint32_t l4_vm_vmx_get_cr2_index(void const *vmcs) L4_NOTHROW
Get the VMCS field index of the virtual CR2 register.
Definition: __vm-vmx.h:545
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition: compiler.h:185
EPT and VPID caps.
Definition: __vm-vmx.h:53