Palacios Public Git Repository

To checkout Palacios execute

  git clone http://v3vee.org/palacios/palacios.web/palacios.git
This will give you the master branch. You probably want the devel branch or one of the release branches. To switch to the devel branch, simply execute
  cd palacios
  git checkout --track -b devel origin/devel
The other branches are similar.


Cleaned up configuration of time management; most advanced time features are
[palacios.git] / palacios / src / palacios / vmx.c
index 6c2939d..ca875bb 100644 (file)
@@ -7,13 +7,11 @@
  * and the University of New Mexico.  You can find out more at 
  * http://www.v3vee.org
  *
- * Copyright (c) 2008, Peter Dinda <pdinda@northwestern.edu> 
- * Copyright (c) 2008, Jack Lange <jarusl@cs.northwestern.edu>
- * Copyright (c) 2008, The V3VEE Project <http://www.v3vee.org> 
+ * Copyright (c) 2011, Jack Lange <jarusl@cs.northwestern.edu>
+ * Copyright (c) 2011, The V3VEE Project <http://www.v3vee.org> 
  * All rights reserved.
  *
- * Author: Peter Dinda <pdinda@northwestern.edu>
- *         Jack Lange <jarusl@cs.northwestern.edu>
+ * Author: Jack Lange <jarusl@cs.northwestern.edu>
  *
  * This is free software.  You are permitted to use,
  * redistribute, and modify it as specified in the file "V3VEE_LICENSE".
 
 
 #include <palacios/vmx.h>
-#include <palacios/vmcs.h>
 #include <palacios/vmm.h>
+#include <palacios/vmx_handler.h>
+#include <palacios/vmcs.h>
 #include <palacios/vmx_lowlevel.h>
 #include <palacios/vmm_lowlevel.h>
-#include <palacios/vmm_config.h>
 #include <palacios/vmm_ctrl_regs.h>
+#include <palacios/vmm_config.h>
+#include <palacios/vmm_time.h>
+#include <palacios/vm_guest_mem.h>
+#include <palacios/vmm_direct_paging.h>
+#include <palacios/vmx_io.h>
+#include <palacios/vmx_msr.h>
+#include <palacios/vmm_decoder.h>
+#include <palacios/vmm_barrier.h>
+
+#ifdef V3_CONFIG_CHECKPOINT
+#include <palacios/vmm_checkpoint.h>
+#endif
 
+#include <palacios/vmx_ept.h>
+#include <palacios/vmx_assist.h>
+#include <palacios/vmx_hw_info.h>
 
-// 
-// 
-// CRUFT
-//
-//
+#ifndef V3_CONFIG_DEBUG_VMX
+#undef PrintDebug
+#define PrintDebug(fmt, args...)
+#endif
 
-#if 0
 
-#include <palacios/vmm_util.h>
-#include <palacios/vmm_string.h>
-#include <palacios/vmm_ctrl_regs.h>
+/* These fields contain the hardware feature sets supported by the local CPU */
+static struct vmx_hw_info hw_info;
 
+extern v3_cpu_arch_t v3_cpu_types[];
 
+static addr_t host_vmcs_ptrs[V3_CONFIG_MAX_CPUS] = { [0 ... V3_CONFIG_MAX_CPUS - 1] = 0};
 
-extern int Launch_VM(ullong_t vmcsPtr, uint_t eip);
+extern int v3_vmx_launch(struct v3_gprs * vm_regs, struct guest_info * info, struct v3_ctrl_regs * ctrl_regs);
+extern int v3_vmx_resume(struct v3_gprs * vm_regs, struct guest_info * info, struct v3_ctrl_regs * ctrl_regs);
 
-#define NUMPORTS 65536
+static int inline check_vmcs_write(vmcs_field_t field, addr_t val) {
+    int ret = 0;
 
+    ret = vmcs_write(field, val);
+
+    if (ret != VMX_SUCCESS) {
+        PrintError("VMWRITE error on %s!: %d\n", v3_vmcs_field_to_str(field), ret);
+        return 1;
+    }
+
+    return 0;
+}
 
-#define VMXASSIST_INFO_PORT   0x0e9
-#define ROMBIOS_PANIC_PORT    0x400
-#define ROMBIOS_PANIC_PORT2   0x401
-#define ROMBIOS_INFO_PORT     0x402
-#define ROMBIOS_DEBUG_PORT    0x403
+static int inline check_vmcs_read(vmcs_field_t field, void * val) {
+    int ret = 0;
 
+    ret = vmcs_read(field, val);
 
+    if (ret != VMX_SUCCESS) {
+        PrintError("VMREAD error on %s!: %d\n", v3_vmcs_field_to_str(field), ret);
+    }
 
-static uint_t GetLinearIP(struct VM * vm) {
-  if (vm->state == VM_VMXASSIST_V8086_BIOS || vm->state == VM_VMXASSIST_V8086) { 
-    return vm->vmcs.guestStateArea.cs.baseAddr + vm->vmcs.guestStateArea.rip;
-  } else {
-    return vm->vmcs.guestStateArea.rip;
-  }
+    return ret;
 }
 
 
 
 
-#define MAX_CODE 512
-#define INSTR_OFFSET_START 17
-#define NOP_SEQ_LEN        10
-#define INSTR_OFFSET_END   (INSTR_OFFSET_START + NOP_SEQ_LEN - 1)
-#define TEMPLATE_CODE_LEN  35
+static addr_t allocate_vmcs() {
+    struct vmcs_data * vmcs_page = NULL;
 
-uint_t oldesp = 0;
-uint_t myregs = 0;
+    PrintDebug("Allocating page\n");
 
+    vmcs_page = (struct vmcs_data *)V3_VAddr(V3_AllocPages(1));
+    memset(vmcs_page, 0, 4096);
 
+    vmcs_page->revision = hw_info.basic_info.revision;
+    PrintDebug("VMX Revision: 0x%x\n", vmcs_page->revision);
 
+    return (addr_t)V3_PAddr((void *)vmcs_page);
+}
 
 
-extern uint_t VMCS_LAUNCH();
-extern uint_t Init_VMCS_HostState();
-extern uint_t Init_VMCS_GuestState();
 
 
+static int init_vmcs_bios(struct guest_info * core, struct vmx_data * vmx_state) {
+    int vmx_ret = 0;
 
+    // disable global interrupts for vm state initialization
+    v3_disable_ints();
 
-extern int Get_CR2();
-extern int vmRunning;
+    PrintDebug("Loading VMCS\n");
+    vmx_ret = vmcs_load(vmx_state->vmcs_ptr_phys);
+    vmx_state->state = VMX_UNLAUNCHED;
 
+    if (vmx_ret != VMX_SUCCESS) {
+        PrintError("VMPTRLD failed\n");
+        return -1;
+    }
 
 
+    /*** Setup default state from HW ***/
 
+    vmx_state->pin_ctrls.value = hw_info.pin_ctrls.def_val;
+    vmx_state->pri_proc_ctrls.value = hw_info.proc_ctrls.def_val;
+    vmx_state->exit_ctrls.value = hw_info.exit_ctrls.def_val;
+    vmx_state->entry_ctrls.value = hw_info.entry_ctrls.def_val;
+    vmx_state->sec_proc_ctrls.value = hw_info.sec_proc_ctrls.def_val;
 
-void DecodeCurrentInstruction(struct VM *vm, struct Instruction *inst)
-{
-  // this is a gruesome hack
-  uint_t address = GetLinearIP(vm);
-  uint_t length = vm->vmcs.exitInfoFields.instrLength;
-  unsigned char *t = (unsigned char *) address;
+    /* Print Control MSRs */
+    PrintDebug("CR0 MSR: %p\n", (void *)(addr_t)hw_info.cr0.value);
+    PrintDebug("CR4 MSR: %p\n", (void *)(addr_t)hw_info.cr4.value);
 
 
-  
-  PrintTrace("DecodeCurrentInstruction: instruction is\n");
-  PrintTraceMemDump(t,length);
-  
-  if (length==3 && t[0]==0x0f && t[1]==0x22 && t[2]==0xc0) { 
-    // mov from eax to cr0
-    // usually used to signal
-    inst->type=VM_MOV_TO_CR0;
-    inst->address=address;
-    inst->size=length;
-    inst->input1=vm->registers.eax;
-    inst->input2=vm->vmcs.guestStateArea.cr0;
-    inst->output=vm->registers.eax;
-    PrintTrace("MOV FROM EAX TO CR0\n");
-  } else {
-    inst->type=VM_UNKNOWN_INST;
-  }
-}
 
+    /******* Setup Host State **********/
 
+    /* Cache GDTR, IDTR, and TR in host struct */
 
-static void ConfigureExits(struct VM *vm)
-{
-  CopyOutVMCSExecCtrlFields(&(vm->vmcs.execCtrlFields));
-
-  vm->vmcs.execCtrlFields.pinCtrls |= 0 
-    // EXTERNAL_INTERRUPT_EXITING 
-    | NMI_EXITING;
-  vm->vmcs.execCtrlFields.procCtrls |= 0
-      // INTERRUPT_WINDOWS_EXIT 
-      | USE_TSC_OFFSETTING
-      | HLT_EXITING  
-      | INVLPG_EXITING           
-      | MWAIT_EXITING            
-      | RDPMC_EXITING           
-      | RDTSC_EXITING         
-      | MOVDR_EXITING         
-      | UNCONDITION_IO_EXITING
-      | MONITOR_EXITING       
-      | PAUSE_EXITING         ;
-
-  CopyInVMCSExecCtrlFields(&(vm->vmcs.execCtrlFields));
-  
-  CopyOutVMCSExitCtrlFields(&(vm->vmcs.exitCtrlFields));
 
-  vm->vmcs.exitCtrlFields.exitCtrls |= ACK_IRQ_ON_EXIT;
-  
-  CopyInVMCSExitCtrlFields(&(vm->vmcs.exitCtrlFields));
+    /********** Setup VMX Control Fields ***********/
 
+    /* Add external interrupts, NMI exiting, and virtual NMI */
+    vmx_state->pin_ctrls.nmi_exit = 1;
+    vmx_state->pin_ctrls.ext_int_exit = 1;
 
-/*   VMCS_READ(VM_EXIT_CTRLS, &flags); */
-/*   flags |= ACK_IRQ_ON_EXIT; */
-/*   VMCS_WRITE(VM_EXIT_CTRLS, &flags); */
-}
 
+    vmx_state->pri_proc_ctrls.hlt_exit = 1;
 
-extern int RunVMM();
-extern int SAFE_VM_LAUNCH();
 
-int MyLaunch(struct VM *vm)
-{
-  ullong_t vmcs = (ullong_t)((uint_t) (vm->vmcsregion));
-  uint_t entry_eip = vm->descriptor.entry_ip;
-  uint_t exit_eip = vm->descriptor.exit_eip;
-  uint_t guest_esp = vm->descriptor.guest_esp;
-  uint_t f = 0xffffffff;
-  uint_t tmpReg = 0;
-  int ret;
-  int vmm_ret = 0;
+    vmx_state->pri_proc_ctrls.pause_exit = 0;
+    vmx_state->pri_proc_ctrls.tsc_offset = 1;
+#ifdef V3_CONFIG_TIME_VIRTUALIZE_TSC
+    vmx_state->pri_proc_ctrls.rdtsc_exit = 1;
+#endif
 
-  PrintTrace("Guest ESP: 0x%x (%u)\n", guest_esp, guest_esp);
+    /* Setup IO map */
+    vmx_state->pri_proc_ctrls.use_io_bitmap = 1;
+    vmx_ret |= check_vmcs_write(VMCS_IO_BITMAP_A_ADDR, (addr_t)V3_PAddr(core->vm_info->io_map.arch_data));
+    vmx_ret |= check_vmcs_write(VMCS_IO_BITMAP_B_ADDR, 
+            (addr_t)V3_PAddr(core->vm_info->io_map.arch_data) + PAGE_SIZE_4KB);
 
-  exit_eip = (uint_t)RunVMM;
 
-  PrintTrace("Clear\n");
-  VMCS_CLEAR(vmcs);
-  PrintTrace("Load\n");
-  VMCS_LOAD(vmcs);
+    vmx_state->pri_proc_ctrls.use_msr_bitmap = 1;
+    vmx_ret |= check_vmcs_write(VMCS_MSR_BITMAP, (addr_t)V3_PAddr(core->vm_info->msr_map.arch_data));
 
 
-  PrintTrace("VMCS_LINK_PTR\n");
-  VMCS_WRITE(VMCS_LINK_PTR, &f);
-  PrintTrace("VMCS_LINK_PTR_HIGH\n");
-  VMCS_WRITE(VMCS_LINK_PTR_HIGH, &f);
 
-  SetCtrlBitsCorrectly(IA32_VMX_PINBASED_CTLS_MSR, PIN_VM_EXEC_CTRLS);
-  SetCtrlBitsCorrectly(IA32_VMX_PROCBASED_CTLS_MSR, PROC_VM_EXEC_CTRLS);
-  SetCtrlBitsCorrectly(IA32_VMX_EXIT_CTLS_MSR, VM_EXIT_CTRLS);
-  SetCtrlBitsCorrectly(IA32_VMX_ENTRY_CTLS_MSR, VM_ENTRY_CTRLS);
-
-  //
-  //
-  //SetCtrlBitsCorrectly(IA32_something,GUEST_IA32_DEBUGCTL);
-  //SetCtrlBitsCorrectly(IA32_something,GUEST_IA32_DEBUGCTL_HIGH);
-
-
-  /* Host state */
-  PrintTrace("Setting up host state\n");
-  SetCRBitsCorrectly(IA32_VMX_CR0_FIXED0_MSR, IA32_VMX_CR0_FIXED1_MSR, HOST_CR0);
-  SetCRBitsCorrectly(IA32_VMX_CR4_FIXED0_MSR, IA32_VMX_CR4_FIXED1_MSR, HOST_CR4);
-  ret = Init_VMCS_HostState();
-
-  if (ret != VMX_SUCCESS) {
-    if (ret == VMX_FAIL_VALID) {
-      PrintTrace("Init Host state: VMCS FAILED WITH ERROR\n");
-    } else {
-      PrintTrace("Init Host state: Invalid VMCS\n");
-    }
-    return ret;
-  }
+#ifdef __V3_64BIT__
+    // Ensure host runs in 64-bit mode at each VM EXIT
+    vmx_state->exit_ctrls.host_64_on = 1;
+#endif
 
-  //  PrintTrace("HOST_RIP: %x (%u)\n", exit_eip, exit_eip);
-  VMCS_WRITE(HOST_RIP, &exit_eip);
+    // Hook all accesses to EFER register
+    v3_hook_msr(core->vm_info, EFER_MSR, 
+               &v3_handle_efer_read,
+               &v3_handle_efer_write, 
+               core);
 
-  /* Guest state */
-  PrintTrace("Setting up guest state\n");
-  PrintTrace("GUEST_RIP: %x (%u)\n", entry_eip, entry_eip);
-  VMCS_WRITE(GUEST_RIP, &entry_eip);
+    // Restore host's EFER register on each VM EXIT
+    vmx_state->exit_ctrls.ld_efer = 1;
 
-  SetCRBitsCorrectly(IA32_VMX_CR0_FIXED0_MSR, IA32_VMX_CR0_FIXED1_MSR, GUEST_CR0);
-  SetCRBitsCorrectly(IA32_VMX_CR4_FIXED0_MSR, IA32_VMX_CR4_FIXED1_MSR, GUEST_CR4);
-  ret = Init_VMCS_GuestState();
+    // Save/restore guest's EFER register to/from VMCS on VM EXIT/ENTRY
+    vmx_state->exit_ctrls.save_efer = 1;
+    vmx_state->entry_ctrls.ld_efer  = 1;
 
-  PrintTrace("InitGuestState returned\n");
+    // Cause VM_EXIT whenever CR4.VMXE or CR4.PAE bits are written
+    vmx_ret |= check_vmcs_write(VMCS_CR4_MASK, CR4_VMXE | CR4_PAE);
 
-  if (ret != VMX_SUCCESS) {
-    if (ret == VMX_FAIL_VALID) {
-      PrintTrace("Init Guest state: VMCS FAILED WITH ERROR\n");
-    } else {
-      PrintTrace("Init Guest state: Invalid VMCS\n");
-    }
-    return ret;
-  }
-  PrintTrace("GUEST_RSP: %x (%u)\n", guest_esp, (uint_t)guest_esp);
-  VMCS_WRITE(GUEST_RSP, &guest_esp);
 
-  //  tmpReg = 0x4100;
-  tmpReg = 0xffffffff;
-  if (VMCS_WRITE(EXCEPTION_BITMAP, &tmpReg) != VMX_SUCCESS) {
-    PrintInfo("Bitmap error\n");
-  }
+    /* Setup paging */
+    if (core->shdw_pg_mode == SHADOW_PAGING) {
+        PrintDebug("Creating initial shadow page table\n");
 
-  ConfigureExits(vm);
+        if (v3_init_passthrough_pts(core) == -1) {
+            PrintError("Could not initialize passthrough page tables\n");
+            return -1;
+        }
+        
+#define CR0_PE 0x00000001
+#define CR0_PG 0x80000000
+#define CR0_WP 0x00010000 // To ensure mem hooks work
+        vmx_ret |= check_vmcs_write(VMCS_CR0_MASK, (CR0_PE | CR0_PG | CR0_WP));
 
-  PrintTrace("VMCS_LAUNCH\n");
+        core->ctrl_regs.cr3 = core->direct_map_pt;
 
-  vm->state=VM_VMXASSIST_STARTUP;
+        // vmx_state->pinbased_ctrls |= NMI_EXIT;
 
-  vmm_ret = SAFE_VM_LAUNCH();
+        /* Add CR exits */
+        vmx_state->pri_proc_ctrls.cr3_ld_exit = 1;
+        vmx_state->pri_proc_ctrls.cr3_str_exit = 1;
+       
+       vmx_state->pri_proc_ctrls.invlpg_exit = 1;
+       
+       /* Add page fault exits */
+       vmx_state->excp_bmap.pf = 1;
 
-  PrintTrace("VMM error %d\n", vmm_ret);
+       // Setup VMX Assist
+       v3_vmxassist_init(core, vmx_state);
 
-  return vmm_ret;
-}
+    } else if ((core->shdw_pg_mode == NESTED_PAGING) && 
+              (v3_cpu_types[core->pcpu_id] == V3_VMX_EPT_CPU)) {
 
+#define CR0_PE 0x00000001
+#define CR0_PG 0x80000000
+#define CR0_WP 0x00010000 // To ensure mem hooks work
+        vmx_ret |= check_vmcs_write(VMCS_CR0_MASK, (CR0_PE | CR0_PG | CR0_WP));
 
+        // vmx_state->pinbased_ctrls |= NMI_EXIT;
 
-  
-int VMLaunch(struct VMDescriptor *vm) 
-{
-  VMCS * vmcs = CreateVMCS();
-  int rc;
-
-  ullong_t vmcs_ptr = (ullong_t)((uint_t)vmcs);
-  uint_t top = (vmcs_ptr >> 32) & 0xffffffff;
-  uint_t bottom = (vmcs_ptr) & 0xffffffff;
-
-  theVM.vmcsregion = vmcs;
-  theVM.descriptor = *vm;
-
-  PrintTrace("vmcs_ptr_top=%x vmcs_ptr_bottom=%x, eip=%x\n", top, bottom, vm->entry_ip);
-  rc = MyLaunch(&theVM); // vmcs_ptr, vm->entry_ip, vm->exit_eip, vm->guest_esp);
-  PrintTrace("Returned from MyLaunch();\n");
-  return rc;
-}
+        /* Disable CR exits */
+       vmx_state->pri_proc_ctrls.cr3_ld_exit = 0;
+       vmx_state->pri_proc_ctrls.cr3_str_exit = 0;
 
+       vmx_state->pri_proc_ctrls.invlpg_exit = 0;
 
+       /* Add page fault exits */
+       //      vmx_state->excp_bmap.pf = 1; // This should never happen..., enabled to catch bugs
+       
+       // Setup VMX Assist
+       v3_vmxassist_init(core, vmx_state);
 
+       /* Enable EPT */
+       vmx_state->pri_proc_ctrls.sec_ctrls = 1; // Enable secondary proc controls
+       vmx_state->sec_proc_ctrls.enable_ept = 1; // enable EPT paging
 
-//
-//
-//  END CRUFT
-//
-//
 
-#endif
 
-static int update_vmcs_host_state(struct guest_info * info) {
-    addr_t tmp;
-    struct vmx_data * arch_data = (struct vmx_data *)(info->vmm_data);
-    struct v3_msr tmp_msr;
+       if (v3_init_ept(core, &hw_info) == -1) {
+           PrintError("Error initializing EPT\n");
+           return -1;
+       }
 
-    __asm__ __volatile__ ( "movq    %%cr0, %0; "               
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_CR0, tmp);
+    } else if ((core->shdw_pg_mode == NESTED_PAGING) && 
+              (v3_cpu_types[core->pcpu_id] == V3_VMX_EPT_UG_CPU)) {
+       int i = 0;
+       // For now we will assume that unrestricted guest mode is assured w/ EPT
 
 
-    __asm__ __volatile__ ( "movq %%cr3, %0; "          
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_CR3, tmp);
+       core->vm_regs.rsp = 0x00;
+       core->rip = 0xfff0;
+       core->vm_regs.rdx = 0x00000f00;
+       core->ctrl_regs.rflags = 0x00000002; // The reserved bit is always 1
+       core->ctrl_regs.cr0 = 0x60010010; // Set the WP flag so the memory hooks work in real-mode
 
 
-    __asm__ __volatile__ ( "movq %%cr4, %0; "          
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_CR4, tmp);
+       core->segments.cs.selector = 0xf000;
+       core->segments.cs.limit = 0xffff;
+       core->segments.cs.base = 0x0000000f0000LL;
 
+       // (raw attributes = 0xf3)
+       core->segments.cs.type = 0xb;
+       core->segments.cs.system = 0x1;
+       core->segments.cs.dpl = 0x0;
+       core->segments.cs.present = 1;
 
 
-    vmcs_write(VMCS_HOST_GDTR_BASE, arch_data->host_state.gdtr.base);
-    vmcs_write(VMCS_HOST_IDTR_BASE, arch_data->host_state.idtr.base);
-    vmcs_write(VMCS_HOST_TR_BASE, arch_data->host_state.tr.base);
 
-#define FS_BASE_MSR 0xc0000100
-#define GS_BASE_MSR 0xc0000101
+       struct v3_segment * segregs [] = {&(core->segments.ss), &(core->segments.ds), 
+                                         &(core->segments.es), &(core->segments.fs), 
+                                         &(core->segments.gs), NULL};
 
-    // FS.BASE MSR
-    v3_get_msr(FS_BASE_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_HOST_FS_BASE, tmp_msr.value);    
+       for ( i = 0; segregs[i] != NULL; i++) {
+           struct v3_segment * seg = segregs[i];
+       
+           seg->selector = 0x0000;
+           //    seg->base = seg->selector << 4;
+           seg->base = 0x00000000;
+           seg->limit = 0xffff;
 
-    // GS.BASE MSR
-    v3_get_msr(GS_BASE_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_HOST_GS_BASE, tmp_msr.value);    
 
+           seg->type = 0x3;
+           seg->system = 0x1;
+           seg->dpl = 0x0;
+           seg->present = 1;
+           //    seg->granularity = 1;
 
+       }
 
-    __asm__ __volatile__ ( "movq %%cs, %0; "           
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_CS_SELECTOR, tmp);
 
-    __asm__ __volatile__ ( "movq %%ss, %0; "           
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_SS_SELECTOR, tmp);
+       core->segments.gdtr.limit = 0x0000ffff;
+       core->segments.gdtr.base = 0x0000000000000000LL;
 
-    __asm__ __volatile__ ( "movq %%ds, %0; "           
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_DS_SELECTOR, tmp);
+       core->segments.idtr.limit = 0x0000ffff;
+       core->segments.idtr.base = 0x0000000000000000LL;
 
-    __asm__ __volatile__ ( "movq %%es, %0; "           
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_ES_SELECTOR, tmp);
+       core->segments.ldtr.selector = 0x0000;
+       core->segments.ldtr.limit = 0x0000ffff;
+       core->segments.ldtr.base = 0x0000000000000000LL;
+       core->segments.ldtr.type = 2;
+       core->segments.ldtr.present = 1;
 
-    __asm__ __volatile__ ( "movq %%fs, %0; "           
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_FS_SELECTOR, tmp);
+       core->segments.tr.selector = 0x0000;
+       core->segments.tr.limit = 0x0000ffff;
+       core->segments.tr.base = 0x0000000000000000LL;
+       core->segments.tr.type = 0xb;
+       core->segments.tr.present = 1;
 
-    __asm__ __volatile__ ( "movq %%gs, %0; "           
-                          : "=q"(tmp)
-                          :
-    );
-    vmcs_write(VMCS_HOST_GS_SELECTOR, tmp);
+       //      core->dbg_regs.dr6 = 0x00000000ffff0ff0LL;
+       core->dbg_regs.dr7 = 0x0000000000000400LL;
 
-    vmcs_write(VMCS_HOST_TR_SELECTOR, arch_data->host_state.tr.selector);
+       /* Enable EPT */
+       vmx_state->pri_proc_ctrls.sec_ctrls = 1; // Enable secondary proc controls
+       vmx_state->sec_proc_ctrls.enable_ept = 1; // enable EPT paging
+       vmx_state->sec_proc_ctrls.unrstrct_guest = 1; // enable unrestricted guest operation
 
 
-#define SYSENTER_CS_MSR 0x00000174
-#define SYSENTER_ESP_MSR 0x00000175
-#define SYSENTER_EIP_MSR 0x00000176
+       /* Disable shadow paging stuff */
+       vmx_state->pri_proc_ctrls.cr3_ld_exit = 0;
+       vmx_state->pri_proc_ctrls.cr3_str_exit = 0;
 
-   // SYSENTER CS MSR
-    v3_get_msr(SYSENTER_CS_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_HOST_SYSENTER_CS, tmp_msr.value);
+       vmx_state->pri_proc_ctrls.invlpg_exit = 0;
 
-    // SYSENTER_ESP MSR
-    v3_get_msr(SYSENTER_ESP_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_HOST_SYSENTER_ESP, tmp_msr.value);
 
-    // SYSENTER_EIP MSR
-    v3_get_msr(SYSENTER_EIP_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_HOST_SYSENTER_EIP, tmp_msr.value);
+       if (v3_init_ept(core, &hw_info) == -1) {
+           PrintError("Error initializing EPT\n");
+           return -1;
+       }
 
+    } else {
+       PrintError("Invalid Virtual paging mode\n");
+       return -1;
+    }
 
 
-    return 0;
-}
+    // hook vmx msrs
 
+    // Setup SYSCALL/SYSENTER MSRs in load/store area
+    
+    // save STAR, LSTAR, FMASK, KERNEL_GS_BASE MSRs in MSR load/store area
+    {
+#define IA32_STAR 0xc0000081
+#define IA32_LSTAR 0xc0000082
+#define IA32_FMASK 0xc0000084
+#define IA32_KERN_GS_BASE 0xc0000102
 
+#define IA32_CSTAR 0xc0000083 // Compatibility mode STAR (ignored for now... hopefully its not that important...)
 
+       int msr_ret = 0;
 
-static addr_t vmxon_ptr_phys;
-extern int v3_vmx_exit_handler();
-extern int v3_vmx_vmlaunch();
+       struct vmcs_msr_entry * exit_store_msrs = NULL;
+       struct vmcs_msr_entry * exit_load_msrs = NULL;
+       struct vmcs_msr_entry * entry_load_msrs = NULL;;
+       int max_msrs = (hw_info.misc_info.max_msr_cache_size + 1) * 4;
 
+       V3_Print("Setting up MSR load/store areas (max_msr_count=%d)\n", max_msrs);
 
-#if 0
-// For the 32 bit reserved bit fields 
-// MB1s are in the low 32 bits, MBZs are in the high 32 bits of the MSR
-static uint32_t sanitize_bits1(uint32_t msr_num, uint32_t val) {
-    v3_msr_t mask_msr;
+       if (max_msrs < 4) {
+           PrintError("Max MSR cache size is too small (%d)\n", max_msrs);
+           return -1;
+       }
 
-    PrintDebug("sanitize_bits1 (MSR:%x)\n", msr_num);
+       vmx_state->msr_area = V3_VAddr(V3_AllocPages(1));
 
-    v3_get_msr(msr_num, &mask_msr.hi, &mask_msr.lo);
+       if (vmx_state->msr_area == NULL) {
+           PrintError("could not allocate msr load/store area\n");
+           return -1;
+       }
 
-    PrintDebug("MSR %x = %x : %x \n", msr_num, mask_msr.hi, mask_msr.lo);
+       msr_ret |= check_vmcs_write(VMCS_EXIT_MSR_STORE_CNT, 4);
+       msr_ret |= check_vmcs_write(VMCS_EXIT_MSR_LOAD_CNT, 4);
+       msr_ret |= check_vmcs_write(VMCS_ENTRY_MSR_LOAD_CNT, 4);
+       
+       
+       exit_store_msrs = (struct vmcs_msr_entry *)(vmx_state->msr_area);
+       exit_load_msrs = (struct vmcs_msr_entry *)(vmx_state->msr_area + (sizeof(struct vmcs_msr_entry) * 4));
+       entry_load_msrs = (struct vmcs_msr_entry *)(vmx_state->msr_area + (sizeof(struct vmcs_msr_entry) * 8));
 
-    val &= mask_msr.lo;
-    val &= mask_msr.hi;
-  
-    return val;
-}
 
+       exit_store_msrs[0].index = IA32_STAR;
+       exit_store_msrs[1].index = IA32_LSTAR;
+       exit_store_msrs[2].index = IA32_FMASK;
+       exit_store_msrs[3].index = IA32_KERN_GS_BASE;
+       
+       memcpy(exit_store_msrs, exit_load_msrs, sizeof(struct vmcs_msr_entry) * 4);
+       memcpy(exit_store_msrs, entry_load_msrs, sizeof(struct vmcs_msr_entry) * 4);
+
+       
+       v3_get_msr(IA32_STAR, &(exit_load_msrs[0].hi), &(exit_load_msrs[0].lo));
+       v3_get_msr(IA32_LSTAR, &(exit_load_msrs[1].hi), &(exit_load_msrs[1].lo));
+       v3_get_msr(IA32_FMASK, &(exit_load_msrs[2].hi), &(exit_load_msrs[2].lo));
+       v3_get_msr(IA32_KERN_GS_BASE, &(exit_load_msrs[3].hi), &(exit_load_msrs[3].lo));
 
+       msr_ret |= check_vmcs_write(VMCS_EXIT_MSR_STORE_ADDR, (addr_t)V3_PAddr(exit_store_msrs));
+       msr_ret |= check_vmcs_write(VMCS_EXIT_MSR_LOAD_ADDR, (addr_t)V3_PAddr(exit_load_msrs));
+       msr_ret |= check_vmcs_write(VMCS_ENTRY_MSR_LOAD_ADDR, (addr_t)V3_PAddr(entry_load_msrs));
 
-static addr_t sanitize_bits2(uint32_t msr_num0, uint32_t msr_num1, addr_t val) {
-    v3_msr_t msr0, msr1;
-    addr_t msr0_val, msr1_val;
+    }    
 
-    PrintDebug("sanitize_bits2 (MSR0=%x, MSR1=%x)\n", msr_num0, msr_num1);
+    /* Sanity check ctrl/reg fields against hw_defaults */
 
-    v3_get_msr(msr_num0, &msr0.hi, &msr0.lo);
-    v3_get_msr(msr_num1, &msr1.hi, &msr1.lo);
+
+
+
+    /*** Write all the info to the VMCS ***/
   
-    // This generates a mask that is the natural bit width of the CPU
-    msr0_val = msr0.value;
-    msr1_val = msr1.value;
+    /*
+    {
+       // IS THIS NECESSARY???
+#define DEBUGCTL_MSR 0x1d9
+       struct v3_msr tmp_msr;
+       v3_get_msr(DEBUGCTL_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
+       vmx_ret |= check_vmcs_write(VMCS_GUEST_DBG_CTL, tmp_msr.value);
+       core->dbg_regs.dr7 = 0x400;
+    }
+    */
+
+#ifdef __V3_64BIT__
+    vmx_ret |= check_vmcs_write(VMCS_LINK_PTR, (addr_t)0xffffffffffffffffULL);
+#else
+    vmx_ret |= check_vmcs_write(VMCS_LINK_PTR, (addr_t)0xffffffffUL);
+    vmx_ret |= check_vmcs_write(VMCS_LINK_PTR_HIGH, (addr_t)0xffffffffUL);
+#endif
 
-    PrintDebug("MSR %x = %p, %x = %p \n", msr_num0, (void*)msr0_val, msr_num1, (void*)msr1_val);
 
-    val &= msr0_val;
-    val &= msr1_val;
+
+    if (v3_update_vmcs_ctrl_fields(core)) {
+        PrintError("Could not write control fields!\n");
+        return -1;
+    }
+    
+    if (v3_update_vmcs_host_state(core)) {
+        PrintError("Could not write host state\n");
+        return -1;
+    }
+
+    // reenable global interrupts for vm state initialization now
+    // that the vm state is initialized. If another VM kicks us off, 
+    // it'll update our vmx state so that we know to reload ourself
+    v3_enable_ints();
 
-    return val;
+    return 0;
 }
 
-static int setup_base_host_state() {
+int v3_init_vmx_vmcs(struct guest_info * core, v3_vm_class_t vm_class) {
+    struct vmx_data * vmx_state = NULL;
+    int vmx_ret = 0;
     
+    vmx_state = (struct vmx_data *)V3_Malloc(sizeof(struct vmx_data));
+    memset(vmx_state, 0, sizeof(struct vmx_data));
+
+    PrintDebug("vmx_data pointer: %p\n", (void *)vmx_state);
+
+    PrintDebug("Allocating VMCS\n");
+    vmx_state->vmcs_ptr_phys = allocate_vmcs();
 
+    PrintDebug("VMCS pointer: %p\n", (void *)(vmx_state->vmcs_ptr_phys));
 
-    //   vmwrite(HOST_IDTR_BASE, 
+    core->vmm_data = vmx_state;
+    vmx_state->state = VMX_UNLAUNCHED;
+
+    PrintDebug("Initializing VMCS (addr=%p)\n", core->vmm_data);
+    
+    // TODO: Fix vmcs fields so they're 32-bit
 
+    PrintDebug("Clearing VMCS: %p\n", (void *)vmx_state->vmcs_ptr_phys);
+    vmx_ret = vmcs_clear(vmx_state->vmcs_ptr_phys);
 
+    if (vmx_ret != VMX_SUCCESS) {
+        PrintError("VMCLEAR failed\n");
+        return -1; 
+    }
+
+    if (vm_class == V3_PC_VM) {
+       PrintDebug("Initializing VMCS\n");
+       if (init_vmcs_bios(core, vmx_state) == -1) {
+           PrintError("Error initializing VMCS to BIOS state\n");
+           return -1;
+       }
+    } else {
+       PrintError("Invalid VM Class\n");
+       return -1;
+    }
+
+    PrintDebug("Serializing VMCS: %p\n", (void *)vmx_state->vmcs_ptr_phys);
+    vmx_ret = vmcs_clear(vmx_state->vmcs_ptr_phys);
+
+    return 0;
 }
 
 
-#endif
+int v3_deinit_vmx_vmcs(struct guest_info * core) {
+    struct vmx_data * vmx_state = core->vmm_data;
 
-static int inline check_vmcs_write(vmcs_field_t field, addr_t val)
-{
-    int ret = 0;
-    ret = vmcs_write(field,val);
+    V3_FreePages((void *)(vmx_state->vmcs_ptr_phys), 1);
+    V3_FreePages(V3_PAddr(vmx_state->msr_area), 1);
 
-    if (ret != VMX_SUCCESS) {
-        PrintError("VMWRITE error on %s!: %d\n", v3_vmcs_field_to_str(field), ret);
-        return 1;
+    V3_Free(vmx_state);
+
+    return 0;
+}
+
+
+
+#ifdef V3_CONFIG_CHECKPOINT
+/* 
+ * JRL: This is broken
+ */
+int v3_vmx_save_core(struct guest_info * core, void * ctx){
+    uint64_t vmcs_ptr = vmcs_store();
+
+    v3_chkpt_save(ctx, "vmcs_data", PAGE_SIZE, (void *)vmcs_ptr);
+
+    return 0;
+}
+
+int v3_vmx_load_core(struct guest_info * core, void * ctx){
+    struct vmx_data * vmx_info = (struct vmx_data *)(core->vmm_data);
+    struct cr0_32 * shadow_cr0;
+    char vmcs[PAGE_SIZE_4KB];
+
+    v3_chkpt_load(ctx, "vmcs_data", PAGE_SIZE_4KB, vmcs);
+
+    vmcs_clear(vmx_info->vmcs_ptr_phys);
+    vmcs_load((addr_t)vmcs);
+
+    v3_vmx_save_vmcs(core);
+
+    shadow_cr0 = (struct cr0_32 *)&(core->ctrl_regs.cr0);
+
+
+    /* Get the CPU mode to set the guest_ia32e entry ctrl */
+
+    if (core->shdw_pg_mode == SHADOW_PAGING) {
+       if (v3_get_vm_mem_mode(core) == VIRTUAL_MEM) {
+           if (v3_activate_shadow_pt(core) == -1) {
+               PrintError("Failed to activate shadow page tables\n");
+               return -1;
+           }
+       } else {
+           if (v3_activate_passthrough_pt(core) == -1) {
+               PrintError("Failed to activate passthrough page tables\n");
+               return -1;
+           }
+       }
     }
 
     return 0;
 }
+#endif
 
 
-static void inline translate_segment_access(struct v3_segment * v3_seg,  
-                                           struct vmcs_segment_access * access)
-{
-    access->type = v3_seg->type;
-    access->desc_type = v3_seg->system;
-    access->dpl = v3_seg->dpl;
-    access->present = v3_seg->present;
-    access->avail = v3_seg->avail;
-    access->long_mode = v3_seg->long_mode;
-    access->db = v3_seg->db;
-    access->granularity = v3_seg->granularity;
+void v3_flush_vmx_vm_core(struct guest_info * core) {
+    struct vmx_data * vmx_info = (struct vmx_data *)(core->vmm_data);
+    vmcs_clear(vmx_info->vmcs_ptr_phys);
+    vmx_info->state = VMX_UNLAUNCHED;
 }
 
-static int inline vmcs_write_guest_segments(struct guest_info* info)
-{
-    int ret = 0;
-    struct vmcs_segment_access access;
 
-    memset(&access, 0, sizeof(access));
 
-    /* CS Segment */
-    translate_segment_access(&(info->segments.cs), &access);
+static int update_irq_exit_state(struct guest_info * info) {
+    struct vmx_exit_idt_vec_info idt_vec_info;
 
-    ret &= check_vmcs_write(VMCS_GUEST_CS_BASE, info->segments.cs.base);
-    ret &= check_vmcs_write(VMCS_GUEST_CS_SELECTOR, info->segments.cs.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_CS_LIMIT, info->segments.cs.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_CS_ACCESS, access.value);
+    check_vmcs_read(VMCS_IDT_VECTOR_INFO, &(idt_vec_info.value));
 
-    /* SS Segment */
-    translate_segment_access(&(info->segments.ss), &access);
+    if ((info->intr_core_state.irq_started == 1) && (idt_vec_info.valid == 0)) {
+#ifdef V3_CONFIG_DEBUG_INTERRUPTS
+        V3_Print("Calling v3_injecting_intr\n");
+#endif
+        info->intr_core_state.irq_started = 0;
+        v3_injecting_intr(info, info->intr_core_state.irq_vector, V3_EXTERNAL_IRQ);
+    }
 
-    ret &= check_vmcs_write(VMCS_GUEST_SS_BASE, info->segments.ss.base);
-    ret &= check_vmcs_write(VMCS_GUEST_SS_SELECTOR, info->segments.ss.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_SS_LIMIT, info->segments.ss.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_SS_ACCESS, access.value);
+    return 0;
+}
 
-    /* DS Segment */
-    translate_segment_access(&(info->segments.ds), &access);
+static int update_irq_entry_state(struct guest_info * info) {
+    struct vmx_exit_idt_vec_info idt_vec_info;
+    struct vmcs_interrupt_state intr_core_state;
+    struct vmx_data * vmx_info = (struct vmx_data *)(info->vmm_data);
 
-    ret &= check_vmcs_write(VMCS_GUEST_DS_BASE, info->segments.ds.base);
-    ret &= check_vmcs_write(VMCS_GUEST_DS_SELECTOR, info->segments.ds.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_DS_LIMIT, info->segments.ds.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_DS_ACCESS, access.value);
+    check_vmcs_read(VMCS_IDT_VECTOR_INFO, &(idt_vec_info.value));
+    check_vmcs_read(VMCS_GUEST_INT_STATE, &(intr_core_state));
 
+    /* Check for pending exceptions to inject */
+    if (v3_excp_pending(info)) {
+        struct vmx_entry_int_info int_info;
+        int_info.value = 0;
 
-    /* ES Segment */
-    translate_segment_access(&(info->segments.es), &access);
+        // In VMX, almost every exception is hardware
+        // Software exceptions are pretty much only for breakpoint or overflow
+        int_info.type = 3;
+        int_info.vector = v3_get_excp_number(info);
 
-    ret &= check_vmcs_write(VMCS_GUEST_ES_BASE, info->segments.es.base);
-    ret &= check_vmcs_write(VMCS_GUEST_ES_SELECTOR, info->segments.es.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_ES_LIMIT, info->segments.es.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_ES_ACCESS, access.value);
+        if (info->excp_state.excp_error_code_valid) {
+            check_vmcs_write(VMCS_ENTRY_EXCP_ERR, info->excp_state.excp_error_code);
+            int_info.error_code = 1;
 
-    /* FS Segment */
-    translate_segment_access(&(info->segments.fs), &access);
+#ifdef V3_CONFIG_DEBUG_INTERRUPTS
+            V3_Print("Injecting exception %d with error code %x\n", 
+                    int_info.vector, info->excp_state.excp_error_code);
+#endif
+        }
 
-    ret &= check_vmcs_write(VMCS_GUEST_FS_BASE, info->segments.fs.base);
-    ret &= check_vmcs_write(VMCS_GUEST_FS_SELECTOR, info->segments.fs.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_FS_LIMIT, info->segments.fs.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_FS_ACCESS, access.value);
+        int_info.valid = 1;
+#ifdef V3_CONFIG_DEBUG_INTERRUPTS
+        V3_Print("Injecting exception %d (EIP=%p)\n", int_info.vector, (void *)(addr_t)info->rip);
+#endif
+        check_vmcs_write(VMCS_ENTRY_INT_INFO, int_info.value);
 
-    /* GS Segment */
-    translate_segment_access(&(info->segments.gs), &access);
+        v3_injecting_excp(info, int_info.vector);
 
-    ret &= check_vmcs_write(VMCS_GUEST_GS_BASE, info->segments.gs.base);
-    ret &= check_vmcs_write(VMCS_GUEST_GS_SELECTOR, info->segments.gs.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_GS_LIMIT, info->segments.gs.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_GS_ACCESS, access.value);
+    } else if ((((struct rflags *)&(info->ctrl_regs.rflags))->intr == 1) && 
+              (intr_core_state.val == 0)) {
+       
+        if ((info->intr_core_state.irq_started == 1) && (idt_vec_info.valid == 1)) {
 
-    /* LDTR segment */
-    translate_segment_access(&(info->segments.ldtr), &access);
+#ifdef V3_CONFIG_DEBUG_INTERRUPTS
+            V3_Print("IRQ pending from previous injection\n");
+#endif
 
-    ret &= check_vmcs_write(VMCS_GUEST_LDTR_BASE, info->segments.ldtr.base);
-    ret &= check_vmcs_write(VMCS_GUEST_LDTR_SELECTOR, info->segments.ldtr.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_LDTR_LIMIT, info->segments.ldtr.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_LDTR_ACCESS, access.value);
+            // Copy the IDT vectoring info over to reinject the old interrupt
+            if (idt_vec_info.error_code == 1) {
+                uint32_t err_code = 0;
+
+                check_vmcs_read(VMCS_IDT_VECTOR_ERR, &err_code);
+                check_vmcs_write(VMCS_ENTRY_EXCP_ERR, err_code);
+            }
+
+            idt_vec_info.undef = 0;
+            check_vmcs_write(VMCS_ENTRY_INT_INFO, idt_vec_info.value);
+
+        } else {
+            struct vmx_entry_int_info ent_int;
+            ent_int.value = 0;
+
+            switch (v3_intr_pending(info)) {
+                case V3_EXTERNAL_IRQ: {
+                    info->intr_core_state.irq_vector = v3_get_intr(info); 
+                    ent_int.vector = info->intr_core_state.irq_vector;
+                    ent_int.type = 0;
+                    ent_int.error_code = 0;
+                    ent_int.valid = 1;
+
+#ifdef V3_CONFIG_DEBUG_INTERRUPTS
+                    V3_Print("Injecting Interrupt %d at exit %u(EIP=%p)\n", 
+                              info->intr_core_state.irq_vector, 
+                              (uint32_t)info->num_exits, 
+                              (void *)(addr_t)info->rip);
+#endif
 
-    /* TR Segment */
-    translate_segment_access(&(info->segments.tr), &access);
+                    check_vmcs_write(VMCS_ENTRY_INT_INFO, ent_int.value);
+                    info->intr_core_state.irq_started = 1;
+
+                    break;
+                }
+                case V3_NMI:
+                    PrintDebug("Injecting NMI\n");
+
+                    ent_int.type = 2;
+                    ent_int.vector = 2;
+                    ent_int.valid = 1;
+                    check_vmcs_write(VMCS_ENTRY_INT_INFO, ent_int.value);
+
+                    break;
+                case V3_SOFTWARE_INTR:
+                    PrintDebug("Injecting software interrupt\n");
+                    ent_int.type = 4;
+
+                    ent_int.valid = 1;
+                    check_vmcs_write(VMCS_ENTRY_INT_INFO, ent_int.value);
+
+                   break;
+                case V3_VIRTUAL_IRQ:
+                    // Not sure what to do here, Intel doesn't have virtual IRQs
+                    // May be the same as external interrupts/IRQs
+
+                   break;
+                case V3_INVALID_INTR:
+                default:
+                    break;
+            }
+        }
+    } else if ((v3_intr_pending(info)) && (vmx_info->pri_proc_ctrls.int_wndw_exit == 0)) {
+        // Enable INTR window exiting so we know when IF=1
+        uint32_t instr_len;
 
-    ret &= check_vmcs_write(VMCS_GUEST_TR_BASE, info->segments.tr.base);
-    ret &= check_vmcs_write(VMCS_GUEST_TR_SELECTOR, info->segments.ldtr.selector);
-    ret &= check_vmcs_write(VMCS_GUEST_TR_LIMIT, info->segments.tr.limit);
-    ret &= check_vmcs_write(VMCS_GUEST_TR_ACCESS, access.value);
+        check_vmcs_read(VMCS_EXIT_INSTR_LEN, &instr_len);
 
-    /* GDTR Segment */
+#ifdef V3_CONFIG_DEBUG_INTERRUPTS
+        V3_Print("Enabling Interrupt-Window exiting: %d\n", instr_len);
+#endif
 
-    ret &= check_vmcs_write(VMCS_GUEST_GDTR_BASE, info->segments.gdtr.base);
-    ret &= check_vmcs_write(VMCS_GUEST_GDTR_LIMIT, info->segments.gdtr.limit);
+        vmx_info->pri_proc_ctrls.int_wndw_exit = 1;
+        check_vmcs_write(VMCS_PROC_CTRLS, vmx_info->pri_proc_ctrls.value);
+    }
 
-    /* IDTR Segment*/
-    ret &= check_vmcs_write(VMCS_GUEST_IDTR_BASE, info->segments.idtr.base);
-    ret &= check_vmcs_write(VMCS_GUEST_IDTR_LIMIT, info->segments.idtr.limit);
 
-    return ret;
+    return 0;
 }
 
-static void setup_v8086_mode_for_boot(struct guest_info * vm_info)
-{
 
-    ((struct vmx_data *)vm_info->vmm_data)->state = VMXASSIST_V8086_BIOS;
-    ((struct rflags *)&(vm_info->ctrl_regs.rflags))->vm = 1;
-    ((struct rflags *)&(vm_info->ctrl_regs.rflags))->iopl = 3;
 
-   
-    vm_info->rip = 0xfff0;
-
-    vm_info->segments.cs.selector = 0xf000;
-    vm_info->segments.cs.base = 0xf000 << 4;
-    vm_info->segments.cs.limit = 0xffff;
-    vm_info->segments.cs.type = 3;
-    vm_info->segments.cs.system = 1;
-    vm_info->segments.cs.dpl = 3;
-    vm_info->segments.cs.present = 1;
-    vm_info->segments.cs.granularity = 0;
+static struct vmx_exit_info exit_log[10];
 
+static void print_exit_log(struct guest_info * info) {
+    int cnt = info->num_exits % 10;
     int i = 0;
-    struct v3_segment * seg_ptr = (struct v3_segment *)&(vm_info->segments);
-
-    /* Set values for selectors ds through ss */
-    for(i = 1; i < 6 ; i++) {
-        seg_ptr[i].selector = 0x0000;
-        seg_ptr[i].base = 0x00000;
-        seg_ptr[i].type = 3;
-        seg_ptr[i].system = 1;
-        seg_ptr[i].dpl = 3;
-        seg_ptr[i].present = 1;
-        seg_ptr[i].granularity = 0;
-    }
+    
+
+    V3_Print("\nExit Log (%d total exits):\n", (uint32_t)info->num_exits);
+
+    for (i = 0; i < 10; i++) {
+       struct vmx_exit_info * tmp = &exit_log[cnt];
+
+       V3_Print("%d:\texit_reason = %p\n", i, (void *)(addr_t)tmp->exit_reason);
+       V3_Print("\texit_qual = %p\n", (void *)tmp->exit_qual);
+       V3_Print("\tint_info = %p\n", (void *)(addr_t)tmp->int_info);
+       V3_Print("\tint_err = %p\n", (void *)(addr_t)tmp->int_err);
+       V3_Print("\tinstr_info = %p\n", (void *)(addr_t)tmp->instr_info);
+
+       cnt--;
+
+       if (cnt == -1) {
+           cnt = 9;
+       }
 
-    for(i = 6; i < 10; i++) {
-        seg_ptr[i].base = 0x0;
-        seg_ptr[i].limit = 0xffff;
     }
 
-    vm_info->segments.ldtr.selector = 0x0;
-    vm_info->segments.ldtr.type = 2;
-    vm_info->segments.ldtr.system = 0;
-    vm_info->segments.ldtr.present = 1;
-    vm_info->segments.ldtr.granularity = 0;
-
-    vm_info->segments.tr.selector = 0x0;
-    vm_info->segments.tr.type = 3;
-    vm_info->segments.tr.system = 0;
-    vm_info->segments.tr.present = 1;
-    vm_info->segments.tr.granularity = 0;
 }
 
+/* 
+ * CAUTION and DANGER!!! 
+ * 
+ * The VMCS CANNOT(!!) be accessed outside of the cli/sti calls inside this function
+ * When exectuing a symbiotic call, the VMCS WILL be overwritten, so any dependencies 
+ * on its contents will cause things to break. The contents at the time of the exit WILL 
+ * change before the exit handler is executed.
+ */
+int v3_vmx_enter(struct guest_info * info) {
+    int ret = 0;
+    uint32_t tsc_offset_low, tsc_offset_high;
+    struct vmx_exit_info exit_info;
+    struct vmx_data * vmx_info = (struct vmx_data *)(info->vmm_data);
 
-static addr_t allocate_vmcs() 
-{
-    reg_ex_t msr;
-    PrintDebug("Allocating page\n");
-    struct vmcs_data * vmcs_page = (struct vmcs_data *)V3_VAddr(V3_AllocPages(1));
+    // Conditionally yield the CPU if the timeslice has expired
+    v3_yield_cond(info);
 
+    // Perform any additional yielding needed for time adjustment
+    v3_adjust_time(info);
 
-    memset(vmcs_page, 0, 4096);
+    // disable global interrupts for vm state transition
+    v3_disable_ints();
 
-    v3_get_msr(VMX_BASIC_MSR, &(msr.e_reg.high), &(msr.e_reg.low));
-    
-    vmcs_page->revision = ((struct vmx_basic_msr*)&msr)->revision;
-    PrintDebug("VMX Revision: 0x%x\n",vmcs_page->revision);
+    // Update timer devices late after being in the VM so that as much 
+    // of hte time in the VM is accounted for as possible. Also do it before
+    // updating IRQ entry state so that any interrupts the timers raise get 
+    // handled on the next VM entry. Must be done with interrupts disabled.
+    v3_update_timers(info);
 
-    return (addr_t)V3_PAddr((void *)vmcs_page);
-}
+    if (vmcs_store() != vmx_info->vmcs_ptr_phys) {
+       vmcs_clear(vmx_info->vmcs_ptr_phys);
+       vmcs_load(vmx_info->vmcs_ptr_phys);
+       vmx_info->state = VMX_UNLAUNCHED;
+    }
 
+    v3_vmx_restore_vmcs(info);
 
 
-static int init_vmcs_bios(struct guest_info * vm_info) 
-{
+#ifdef V3_CONFIG_SYMCALL
+    if (info->sym_core_state.symcall_state.sym_call_active == 0) {
+       update_irq_entry_state(info);
+    }
+#else 
+    update_irq_entry_state(info);
+#endif
 
-    setup_v8086_mode_for_boot(vm_info);
+    {
+       addr_t guest_cr3;
+       vmcs_read(VMCS_GUEST_CR3, &guest_cr3);
+       vmcs_write(VMCS_GUEST_CR3, guest_cr3);
+    }
 
-    // TODO: Fix vmcs fields so they're 32-bit
-    struct vmx_data * vmx_data = (struct vmx_data *)vm_info->vmm_data;
-    int vmx_ret;
+    // Perform last-minute time bookkeeping prior to entering the VM
+    v3_time_enter_vm(info);
 
-    // Have to do a whole lot of flag setting here
-    PrintDebug("Clearing VMCS\n");
-    vmx_ret = vmcs_clear(vmx_data->vmcs_ptr_phys);
+    tsc_offset_high = (uint32_t)((v3_tsc_host_offset(&info->time_state) >> 32) & 0xffffffff);
+    tsc_offset_low = (uint32_t)(v3_tsc_host_offset(&info->time_state) & 0xffffffff);
+    check_vmcs_write(VMCS_TSC_OFFSET_HIGH, tsc_offset_high);
+    check_vmcs_write(VMCS_TSC_OFFSET, tsc_offset_low);
 
-    if (vmx_ret != VMX_SUCCESS) {
-        PrintError("VMCLEAR failed\n");
+    if (v3_update_vmcs_host_state(info)) {
+       v3_enable_ints();
+        PrintError("Could not write host state\n");
         return -1;
     }
 
-    PrintDebug("Loading VMCS\n");
-    vmx_ret = vmcs_load(vmx_data->vmcs_ptr_phys);
 
-    if (vmx_ret != VMX_SUCCESS) {
-        PrintError("VMPTRLD failed\n");
-        return -1;
+    if (vmx_info->state == VMX_UNLAUNCHED) {
+       vmx_info->state = VMX_LAUNCHED;
+
+       info->vm_info->run_state = VM_RUNNING;
+       ret = v3_vmx_launch(&(info->vm_regs), info, &(info->ctrl_regs));
+    } else {
+       V3_ASSERT(vmx_info->state != VMX_UNLAUNCHED);
+       ret = v3_vmx_resume(&(info->vm_regs), info, &(info->ctrl_regs));
     }
+    
 
-    struct v3_msr tmp_msr;
 
-    /* Write VMX Control Fields */
-    v3_get_msr(VMX_PINBASED_CTLS_MSR,&(tmp_msr.hi),&(tmp_msr.lo));
-    vmcs_write(VMCS_PIN_CTRLS, tmp_msr.lo);
+    //  PrintDebug("VMX Exit: ret=%d\n", ret);
 
-    v3_get_msr(VMX_PROCBASED_CTLS_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_PROC_CTRLS, tmp_msr.lo);
+    if (ret != VMX_SUCCESS) {
+       uint32_t error = 0;
+        vmcs_read(VMCS_INSTR_ERR, &error);
 
-    v3_get_msr(VMX_EXIT_CTLS_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_EXIT_CTRLS, tmp_msr.lo);
+       v3_enable_ints();
 
-    v3_get_msr(VMX_ENTRY_CTLS_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
-    vmcs_write(VMCS_ENTRY_CTRLS, tmp_msr.lo);
+       PrintError("VMENTRY Error: %d (launch_ret = %d)\n", error, ret);
+       return -1;
+    }
 
-    /* Cache GDTR, IDTR, and TR in host struct */
-    struct {
-        uint16_t selector;
-        addr_t   base;
-    } __attribute__((packed)) tmp_seg;
-    
-    addr_t gdtr_base;
-
-    __asm__ __volatile__(
-                        "sgdt (%0);"
-                        :
-                        : "q"(&tmp_seg)
-                        : "memory"
-                        );
-    vmx_data->host_state.gdtr.base = gdtr_base = tmp_seg.base;
-
-    __asm__ __volatile__(
-                        "sidt (%0);"
-                        :
-                        : "q"(&tmp_seg)
-                        : "memory"
-                        );
-    vmx_data->host_state.idtr.base = tmp_seg.base;
-
-    __asm__ __volatile__(
-                        "str (%0);"
-                        :
-                        : "q"(&tmp_seg)
-                        : "memory"
-                        );
-    vmx_data->host_state.tr.selector = tmp_seg.selector;
-
-    struct tss_descriptor desc = ((struct tss_descriptor *)gdtr_base)[tmp_seg.selector];
-    
-    tmp_seg.base = (
-                   (desc.base1) |
-                   (desc.base2 << 16) |
-                   (desc.base3 << 24) |
-#ifdef __V3_64BIT__
-                   ((uint64_t)desc.base4 << 32)
-#else 
-                   (0)
-#endif
-                );
 
-    vmx_data->host_state.tr.base = tmp_seg.base;
 
-    update_vmcs_host_state(vm_info);
-    vmcs_write(VMCS_HOST_RIP, (addr_t)&v3_vmx_exit_handler);
+    // Immediate exit from VM time bookkeeping
+    v3_time_exit_vm(info);
 
-    // Setup guest state 
-    // TODO: This is not 32-bit safe!
-    vmx_ret &= check_vmcs_write(VMCS_GUEST_RIP, vm_info->rip);
-    vmx_ret &= check_vmcs_write(VMCS_GUEST_CR0, 0x60000010);
+    info->num_exits++;
 
-    vmx_ret &= vmcs_write_guest_segments(vm_info);
+    /* Update guest state */
+    v3_vmx_save_vmcs(info);
 
-    vmx_ret &= check_vmcs_write(VMCS_GUEST_RFLAGS, vm_info->ctrl_regs.rflags);
-    vmx_ret &= check_vmcs_write(VMCS_LINK_PTR, 0xffffffffffffffff);
+    // info->cpl = info->segments.cs.selector & 0x3;
 
-    if (vmx_ret != 0) {
-       PrintError("Could not initialize VMCS segments\n");
-        return -1;
+    info->mem_mode = v3_get_vm_mem_mode(info);
+    info->cpu_mode = v3_get_vm_cpu_mode(info);
+
+
+    check_vmcs_read(VMCS_EXIT_INSTR_LEN, &(exit_info.instr_len));
+    check_vmcs_read(VMCS_EXIT_INSTR_INFO, &(exit_info.instr_info));
+    check_vmcs_read(VMCS_EXIT_REASON, &(exit_info.exit_reason));
+    check_vmcs_read(VMCS_EXIT_QUAL, &(exit_info.exit_qual));
+    check_vmcs_read(VMCS_EXIT_INT_INFO, &(exit_info.int_info));
+    check_vmcs_read(VMCS_EXIT_INT_ERR, &(exit_info.int_err));
+    check_vmcs_read(VMCS_GUEST_LINEAR_ADDR, &(exit_info.guest_linear_addr));
+
+    if (info->shdw_pg_mode == NESTED_PAGING) {
+       check_vmcs_read(VMCS_GUEST_PHYS_ADDR, &(exit_info.ept_fault_addr));
     }
 
-    v3_print_vmcs_guest_state();
-    return 0;
-}
+    //PrintDebug("VMX Exit taken, id-qual: %u-%lu\n", exit_info.exit_reason, exit_info.exit_qual);
+
+    exit_log[info->num_exits % 10] = exit_info;
+
+#ifdef V3_CONFIG_SYMCALL
+    if (info->sym_core_state.symcall_state.sym_call_active == 0) {
+       update_irq_exit_state(info);
+    }
+#else
+    update_irq_exit_state(info);
+#endif
+
+    if (exit_info.exit_reason == VMEXIT_INTR_WINDOW) {
+       // This is a special case whose only job is to inject an interrupt
+       vmcs_read(VMCS_PROC_CTRLS, &(vmx_info->pri_proc_ctrls.value));
+        vmx_info->pri_proc_ctrls.int_wndw_exit = 0;
+        vmcs_write(VMCS_PROC_CTRLS, vmx_info->pri_proc_ctrls.value);
+
+#ifdef V3_CONFIG_DEBUG_INTERRUPTS
+       V3_Print("Interrupts available again! (RIP=%llx)\n", info->rip);
+#endif
+    }
+
+    // reenable global interrupts after vm exit
+    v3_enable_ints();
+
+    // Conditionally yield the CPU if the timeslice has expired
+    v3_yield_cond(info);
+
+    if (v3_handle_vmx_exit(info, &exit_info) == -1) {
+       PrintError("Error in VMX exit handler (Exit reason=%x)\n", exit_info.exit_reason);
+       return -1;
+    }
 
-int v3_vmx_handle_exit()
-{
-    PrintDebug("Exit taken!\n");
     return 0;
 }
 
-static int init_vmx_guest(struct guest_info * info, struct v3_vm_config * config_ptr) {
-    PrintDebug("Entering init_vmx_guest\n");
-    v3_pre_config_guest(info, config_ptr);
 
-    struct vmx_data * data = NULL;
+int v3_start_vmx_guest(struct guest_info * info) {
 
-    data = (struct vmx_data *)V3_Malloc(sizeof(struct vmx_data));
+    PrintDebug("Starting VMX core %u\n", info->vcpu_id);
 
-    PrintDebug("vmx_data pointer: %p\n", (void *)data);
+    if (info->vcpu_id == 0) {
+       info->core_run_state = CORE_RUNNING;
+       info->vm_info->run_state = VM_RUNNING;
+    } else {
 
-    PrintDebug("Allocating VMCS\n");
-    data->vmcs_ptr_phys = allocate_vmcs();
+        PrintDebug("VMX core %u: Waiting for core initialization\n", info->vcpu_id);
 
-    PrintDebug("VMCS pointer: %p\n", (void *)(data->vmcs_ptr_phys));
+        while (info->core_run_state == CORE_STOPPED) {
+            v3_yield(info);
+            //PrintDebug("VMX core %u: still waiting for INIT\n",info->vcpu_id);
+        }
+       
+       PrintDebug("VMX core %u initialized\n", info->vcpu_id);
 
-    info->vmm_data = data;
+       // We'll be paranoid about race conditions here
+       v3_wait_at_barrier(info);
+    }
 
-    PrintDebug("Initializing VMCS (addr=%p)\n", info->vmm_data);
 
-    if (init_vmcs_bios(info) != 0) {
-       PrintError("Could not initialize VMCS BIOS\n");
-        return -1;
-    }
+    PrintDebug("VMX core %u: I am starting at CS=0x%x (base=0x%p, limit=0x%x),  RIP=0x%p\n",
+               info->vcpu_id, info->segments.cs.selector, (void *)(info->segments.cs.base),
+               info->segments.cs.limit, (void *)(info->rip));
 
-    //v3_post_config_guest(info, config_ptr);
 
-    return 0;
-}
+    PrintDebug("VMX core %u: Launching VMX VM on logical core %u\n", info->vcpu_id, info->pcpu_id);
 
+    v3_start_time(info);
 
-static int start_vmx_guest(struct guest_info* info) {
-    uint32_t error = 0;
-    int ret = 0;
+    while (1) {
 
-    PrintDebug("Attempting VMLAUNCH\n");
+       if (info->vm_info->run_state == VM_STOPPED) {
+           info->core_run_state = CORE_STOPPED;
+           break;
+       }
 
-    ret = v3_vmx_vmlaunch();
+       if (v3_vmx_enter(info) == -1) {
 
-    PrintDebug("Returned from VMLAUNCH\n");
+           addr_t host_addr;
+            addr_t linear_addr = 0;
+            
+            info->vm_info->run_state = VM_ERROR;
+            
+            V3_Print("VMX core %u: VMX ERROR!!\n", info->vcpu_id); 
+            
+            v3_print_guest_state(info);
+            
+            V3_Print("VMX core %u\n", info->vcpu_id); 
 
-    vmcs_read(VMCS_INSTR_ERR, &error, 4);
+            linear_addr = get_addr_linear(info, info->rip, &(info->segments.cs));
+            
+            if (info->mem_mode == PHYSICAL_MEM) {
+                v3_gpa_to_hva(info, linear_addr, &host_addr);
+            } else if (info->mem_mode == VIRTUAL_MEM) {
+                v3_gva_to_hva(info, linear_addr, &host_addr);
+            }
+            
+            V3_Print("VMX core %u: Host Address of rip = 0x%p\n", info->vcpu_id, (void *)host_addr);
+            
+            V3_Print("VMX core %u: Instr (15 bytes) at %p:\n", info->vcpu_id, (void *)host_addr);
+            v3_dump_mem((uint8_t *)host_addr, 15);
+            
+            v3_print_stack(info);
+
+
+           v3_print_vmcs();
+           print_exit_log(info);
+           return -1;
+       }
+
+       v3_wait_at_barrier(info);
+
+
+       if (info->vm_info->run_state == VM_STOPPED) {
+           info->core_run_state = CORE_STOPPED;
+           break;
+       }
+/*
+       if ((info->num_exits % 5000) == 0) {
+           V3_Print("VMX Exit number %d\n", (uint32_t)info->num_exits);
+       }
+*/
 
-    if (ret != VMX_SUCCESS) {
-        PrintError("VMLAUNCH failed: %d\n", error);
     }
 
-    return -1;
+    return 0;
 }
 
 
 
 
-
+#define VMX_FEATURE_CONTROL_MSR     0x0000003a
+#define CPUID_VMX_FEATURES 0x00000005  /* LOCK and VMXON */
+#define CPUID_1_ECX_VTXFLAG 0x00000020
 
 int v3_is_vmx_capable() {
     v3_msr_t feature_msr;
-    addr_t eax = 0, ebx = 0, ecx = 0, edx = 0;
+    uint32_t eax = 0, ebx = 0, ecx = 0, edx = 0;
 
     v3_cpuid(0x1, &eax, &ebx, &ecx, &edx);
 
-    PrintDebug("ECX: %p\n", (void*)ecx);
+    PrintDebug("ECX: 0x%x\n", ecx);
 
     if (ecx & CPUID_1_ECX_VTXFLAG) {
         v3_get_msr(VMX_FEATURE_CONTROL_MSR, &(feature_msr.hi), &(feature_msr.lo));
        
-        PrintTrace("MSRREGlow: 0x%.8x\n", feature_msr.lo);
+        PrintDebug("MSRREGlow: 0x%.8x\n", feature_msr.lo);
 
-        if ((feature_msr.lo & FEATURE_CONTROL_VALID) != FEATURE_CONTROL_VALID) {
+        if ((feature_msr.lo & CPUID_VMX_FEATURES) != CPUID_VMX_FEATURES) {
             PrintDebug("VMX is locked -- enable in the BIOS\n");
             return 0;
         }
@@ -833,71 +1021,85 @@ int v3_is_vmx_capable() {
     return 1;
 }
 
-static int has_vmx_nested_paging() {
+
+int v3_reset_vmx_vm_core(struct guest_info * core, addr_t rip) {
+    // init vmcs bios
+    
+    if ((core->shdw_pg_mode == NESTED_PAGING) && 
+       (v3_cpu_types[core->pcpu_id] == V3_VMX_EPT_UG_CPU)) {
+       // easy 
+        core->rip = 0;
+       core->segments.cs.selector = rip << 8;
+       core->segments.cs.limit = 0xffff;
+       core->segments.cs.base = rip << 12;
+    } else {
+       core->vm_regs.rdx = core->vcpu_id;
+       core->vm_regs.rbx = rip;
+    }
+
     return 0;
 }
 
 
 
-void v3_init_vmx(struct v3_ctrl_ops * vm_ops) {
-    extern v3_cpu_arch_t v3_cpu_type;
-
-    struct v3_msr tmp_msr;
-    uint64_t ret=0;
+void v3_init_vmx_cpu(int cpu_id) {
+    addr_t vmx_on_region = 0;
 
-    v3_get_msr(VMX_CR4_FIXED0_MSR,&(tmp_msr.hi),&(tmp_msr.lo));
-    
-    __asm__ __volatile__ (
-                         "movq %%cr4, %%rbx;"
-                         "orq  $0x00002000, %%rbx;"
-                         "movq %%rbx, %0;"
-                         : "=m"(ret) 
-                         :
-                         : "%rbx"
-                         );
-
-    if((~ret & tmp_msr.value) == 0) {
-        __asm__ __volatile__ (
-                             "movq %0, %%cr4;"
-                             :
-                             : "q"(ret)
-                             );
-    } else {
-        PrintError("Invalid CR4 Settings!\n");
-        return;
+    if (cpu_id == 0) {
+       if (v3_init_vmx_hw(&hw_info) == -1) {
+           PrintError("Could not initialize VMX hardware features on cpu %d\n", cpu_id);
+           return;
+       }
     }
-      __asm__ __volatile__ (
-                           "movq %%cr0, %%rbx; "
-                           "orq  $0x00000020,%%rbx; "
-                           "movq %%rbx, %%cr0;"
-                           :
-                           :
-                           : "%rbx"
-                           );
-      //
-    // Should check and return Error here.... 
+
+    enable_vmx();
+
 
     // Setup VMXON Region
-    vmxon_ptr_phys = allocate_vmcs();
-    PrintDebug("VMXON pointer: 0x%p\n", (void*)vmxon_ptr_phys);
+    vmx_on_region = allocate_vmcs();
+
 
-    if (v3_enable_vmx(vmxon_ptr_phys) == VMX_SUCCESS) {
-        PrintDebug("VMX Enabled\n");
+    if (vmx_on(vmx_on_region) == VMX_SUCCESS) {
+        V3_Print("VMX Enabled\n");
+       host_vmcs_ptrs[cpu_id] = vmx_on_region;
     } else {
-        PrintError("VMX initialization failure\n");
-        return;
+        V3_Print("VMX already enabled\n");
+       V3_FreePages((void *)vmx_on_region, 1);
     }
-       
 
-    if (has_vmx_nested_paging() == 1) {
-        v3_cpu_type = V3_VMX_EPT_CPU;
-    } else {
-        v3_cpu_type = V3_VMX_CPU;
+    PrintDebug("VMXON pointer: 0x%p\n", (void *)host_vmcs_ptrs[cpu_id]);    
+
+    {
+       struct vmx_sec_proc_ctrls sec_proc_ctrls;
+       sec_proc_ctrls.value = v3_vmx_get_ctrl_features(&(hw_info.sec_proc_ctrls));
+       
+       if (sec_proc_ctrls.enable_ept == 0) {
+           V3_Print("VMX EPT (Nested) Paging not supported\n");
+           v3_cpu_types[cpu_id] = V3_VMX_CPU;
+       } else if (sec_proc_ctrls.unrstrct_guest == 0) {
+           V3_Print("VMX EPT (Nested) Paging supported\n");
+           v3_cpu_types[cpu_id] = V3_VMX_EPT_CPU;
+       } else {
+           V3_Print("VMX EPT (Nested) Paging + Unrestricted guest supported\n");
+           v3_cpu_types[cpu_id] = V3_VMX_EPT_UG_CPU;
+       }
     }
+}
+
+
+void v3_deinit_vmx_cpu(int cpu_id) {
+    extern v3_cpu_arch_t v3_cpu_types[];
+    v3_cpu_types[cpu_id] = V3_INVALID_CPU;
 
-    // Setup the VMX specific vmm operations
-    vm_ops->init_guest = &init_vmx_guest;
-    vm_ops->start_guest = &start_vmx_guest;
-    vm_ops->has_nested_paging = &has_vmx_nested_paging;
+    if (host_vmcs_ptrs[cpu_id] != 0) {
+       V3_Print("Disabling VMX\n");
 
+       if (vmx_off() != VMX_SUCCESS) {
+           PrintError("Error executing VMXOFF\n");
+       }
+
+       V3_FreePages((void *)host_vmcs_ptrs[cpu_id], 1);
+
+       host_vmcs_ptrs[cpu_id] = 0;
+    }
 }