4486 	u32 vmx_msr_low, vmx_msr_high;  in adjust_vmx_controls()  local
4489 	rdmsr(msr, vmx_msr_low, vmx_msr_high);  in adjust_vmx_controls()
4491 	ctl &= vmx_msr_high; /* bit == 0 in high word ==> must be zero */  in adjust_vmx_controls()
4504 	u32 vmx_msr_low, vmx_msr_high;  in allow_1_setting()  local
4506 	rdmsr(msr, vmx_msr_low, vmx_msr_high);  in allow_1_setting()
4507 	return vmx_msr_high & ctl;  in allow_1_setting()
4512 	u32 vmx_msr_low, vmx_msr_high;  in setup_vmcs_config()  local
4636 	rdmsr(MSR_IA32_VMX_BASIC, vmx_msr_low, vmx_msr_high);  in setup_vmcs_config()
4639 	if ((vmx_msr_high & 0x1fff) > PAGE_SIZE)  in setup_vmcs_config()
4644 	if (vmx_msr_high & (1u<<16))  in setup_vmcs_config()
4649 	if (((vmx_msr_high >> 18) & 15) != 6)  in setup_vmcs_config()
4652 	vmcs_conf->size = vmx_msr_high & 0x1fff;  in setup_vmcs_config()
4654 	vmcs_conf->basic_cap = vmx_msr_high & ~0x1fff;  in setup_vmcs_config()