* __vmx_vcpu_run - Run a vCPU via a transition to VMX guest mode
  * @vmx:       struct vcpu_vmx *
  * @regs:      unsigned long * (to guest registers)
- * %RBX:       VMCS launched status (non-zero indicates already launched)
+ * @launched:  %true if the VMCS has been launched
  *
  * Returns:
  *     %RBX is 0 on VM-Exit, 1 on VM-Fail
         */
        push %_ASM_ARG2
 
+       /* Copy @launched to BL, _ASM_ARG3 is volatile. */
+       mov %_ASM_ARG3B, %bl
+
        /* Adjust RSP to account for the CALL to vmx_vmenter(). */
        lea -WORD_SIZE(%_ASM_SP), %_ASM_ARG2
        call vmx_update_host_rsp
 
                "call __vmx_vcpu_run \n\t"
              : ASM_CALL_CONSTRAINT, "=b"(vmx->fail),
 #ifdef CONFIG_X86_64
-               "=D"((int){0}), "=S"((int){0})
-             : "D"(vmx), "S"(&vcpu->arch.regs),
+               "=D"((int){0}), "=S"((int){0}), "=d"((int){0})
+             : "D"(vmx), "S"(&vcpu->arch.regs), "d"(vmx->loaded_vmcs->launched)
 #else
-               "=a"((int){0}), "=d"((int){0})
-             : "a"(vmx), "d"(&vcpu->arch.regs),
+               "=a"((int){0}), "=d"((int){0}), "=c"((int){0})
+             : "a"(vmx), "d"(&vcpu->arch.regs), "c"(vmx->loaded_vmcs->launched)
 #endif
-               "b"(vmx->loaded_vmcs->launched)
              : "cc", "memory"
 #ifdef CONFIG_X86_64
-               , "rax", "rcx", "rdx"
+               , "rax", "rcx"
                , "r8", "r9", "r10", "r11", "r12", "r13", "r14", "r15"
 #else
-               , "ecx", "edi", "esi"
+               , "edi", "esi"
 #endif
              );