diff --git a/src/arch/x86/64/c_traps.c b/src/arch/x86/64/c_traps.c
index 97ede8dba..9f359db32 100644
--- a/src/arch/x86/64/c_traps.c
+++ b/src/arch/x86/64/c_traps.c
@@ -41,16 +41,10 @@ static void NORETURN restore_vmx(tcb_t *cur_thread, vcpu_t *vcpu)
 #ifdef CONFIG_X86_64_VTX_64BIT_GUESTS
     vcpu_restore_guest_msrs(vcpu);
 #endif /* CONFIG_X86_64_VTX_64BIT_GUESTS */
+
     /* attempt to do a vmlaunch/vmresume */
     asm volatile(
-        // Arguments are getting stored in general purpose registers that need to be used.
-        // Copy them to unused general purpose registers
-        "movq %[launched], %%rbx\n"
 #ifdef CONFIG_X86_64_VTX_64BIT_GUESTS
-        "movq %[host_msr], %%r8\n"
-        "movq %[guest_msr], %%r9\n"
-        "movq %[reg], %%r10\n"
-
         // Save host's GS, Shadow GS, and FS
         "mov $0xC0000101, %%ecx\n"
         "rdmsr\n"
@@ -67,7 +61,7 @@ static void NORETURN restore_vmx(tcb_t *cur_thread, vcpu_t *vcpu)
         "shl $0x20,%%rdx\n"
         "or %%rdx, %%rax\n"
         "mov %%rax, %%r13\n" // R13 has FS
-        "movq %%r8, %%rsp\n" // host_gs
+        "movq %[host_msr], %%rsp\n" // host_gs
         "pushq %%r13\n"
         "pushq %%r12\n"
         "pushq %%r11\n"
@@ -75,7 +69,7 @@ static void NORETURN restore_vmx(tcb_t *cur_thread, vcpu_t *vcpu)
         // Restore guest's GS and Shadow GS
         "mov $0xC0000101, %%ecx\n"
         "swapgs\n"
-        "movq %%r9, %%rsp\n" // guest_gs
+        "movq %[guest_msr], %%rsp\n" // guest_gs
         "popq %%rax\n"       // GS
         "mov %%rax,%%rdx\n"
         "shr $0x20,%%rdx\n"
@@ -91,12 +85,12 @@ static void NORETURN restore_vmx(tcb_t *cur_thread, vcpu_t *vcpu)
         "mov %%rax,%%rdx\n"
         "shr $0x20,%%rdx\n"
         "wrmsr\n"
-        "movq %%r10, %%rsp\n" // reg
+        "movq %[guest_regs], %%rsp\n"
 #else /* not CONFIG_X86_64_VTX_64BIT_GUESTS */
         // Set our stack pointer to the top of the tcb so we can efficiently pop
-        "movq %[reg], %%rsp\n"
+        "movq %[guest_regs], %%rsp\n"
 #endif /* CONFIG_X86_64_VTX_64BIT_GUESTS */
-        "cmpq $0x1, (%%rbx)\n" // is the VM launched already?
+        "cmpq $0x1, (%[launched])\n" // is the VM launched already?
         "jne launch\n"
         "popq %%rax\n"
         "popq %%rbx\n"
@@ -183,12 +177,12 @@ static void NORETURN restore_vmx(tcb_t *cur_thread, vcpu_t *vcpu)
         "leaq vmlaunch_failed(%%rip), %%rax\n"
         "jmp *%%rax\n"
         :
-        : [reg]"r"(&vcpu->gp_registers[VCPU_EAX]),
+        : [guest_regs]"r"(vcpu->gp_registers),
         [launched]"r"(&vcpu->launched),
 #ifdef CONFIG_X86_64_VTX_64BIT_GUESTS
         [stack_size]"i"(BIT(CONFIG_KERNEL_STACK_BITS)),
-        [guest_msr]"r"(&vcpu->guest_msr_registers[VCPU_GS]),
-        [host_msr]"r"(&vcpu->host_msr_registers[n_vcpu_msr_register])
+        [guest_msr]"r"(vcpu->guest_msr_registers),
+        [host_msr]"r"(vcpu->host_msr_registers)
 #else /* not CONFIG_X86_64_VTX_64BIT_GUESTS */
         [stack_size]"i"(BIT(CONFIG_KERNEL_STACK_BITS))
 #ifdef ENABLE_SMP_SUPPORT
@@ -196,8 +190,9 @@ static void NORETURN restore_vmx(tcb_t *cur_thread, vcpu_t *vcpu)
 #endif
 #endif /* CONFIG_X86_64_VTX_64BIT_GUESTS */
         // Clobber memory so the compiler is forced to complete all stores
-        // before running this assembler
-        : "memory"
+        // before running this assembler. Leave rbx, r8, r9 and r10 not clobbered
+        // so that the inputs get pinned to those general purpose registers.
+        : "memory", "cc", "rax", "rcx", "rdx", "r11", "r12", "r13", "r14", "r15"
     );
     UNREACHABLE();
 }