vmm_handle_xsetbv
int vmm_handle_xsetbv(struct vcpu *, uint64_t *);
ret = vmm_handle_xsetbv(vcpu, rax);