VMX is working for a 32-bit Linux kernel. It should also work for a 64-bit kernel...

[palacios.git] / palacios / src / palacios / svm_handler.c

diff --git a/palacios/src/palacios/svm_handler.c b/palacios/src/palacios/svm_handler.c
index a70b0dd..5736234 100644 (file)
--- a/palacios/src/palacios/svm_handler.c
+++ b/palacios/src/palacios/svm_handler.c
@@ -24,16 +24,18 @@
 #include <palacios/vmm_decoder.h>
 #include <palacios/vmm_ctrl_regs.h>
 #include <palacios/svm_io.h>
-#include <palacios/svm_halt.h>
+#include <palacios/vmm_halt.h>
 #include <palacios/svm_pause.h>
 #include <palacios/svm_wbinvd.h>
 #include <palacios/vmm_intr.h>
 #include <palacios/vmm_emulator.h>
 #include <palacios/svm_msr.h>
-#include <palacios/vmm_profiler.h>
 #include <palacios/vmm_hypercall.h>
 #include <palacios/vmm_direct_paging.h>
 
+#ifdef CONFIG_TELEMETRY
+#include <palacios/vmm_telemetry.h>
+#endif
 
 
 int v3_handle_svm_exit(struct guest_info * info) {
@@ -97,9 +99,9 @@ int v3_handle_svm_exit(struct guest_info * info) {
     }
 
 
-#ifdef CONFIG_PROFILE_VMM
-    if (info->enable_profiler) {
-       rdtscll(info->profiler.start_time);
+#ifdef CONFIG_TELEMETRY
+    if (info->enable_telemetry) {
+       v3_telemetry_start_exit(info);
     }
 #endif
 
@@ -262,7 +264,7 @@ int v3_handle_svm_exit(struct guest_info * info) {
 #ifdef CONFIG_DEBUG_HALT
            PrintDebug("Guest halted\n");
 #endif
-           if (v3_handle_svm_halt(info) == -1) {
+           if (v3_handle_halt(info) == -1) {
                return -1;
            }
            break;
@@ -320,10 +322,9 @@ int v3_handle_svm_exit(struct guest_info * info) {
     }
     // END OF SWITCH (EXIT_CODE)
 
-#ifdef CONFIG_PROFILE_VMM
-    if (info->enable_profiler) {
-       rdtscll(info->profiler.end_time);
-       v3_profile_exit(info, exit_code);
+#ifdef CONFIG_TELEMETRY
+    if (info->enable_telemetry) {
+       v3_telemetry_end_exit(info, exit_code);
     }
 #endif