29 lines
1.2 KiB
Diff
29 lines
1.2 KiB
Diff
--- src/kernel/sel4/src/arch/x86/object/vcpu.c
|
|
+++ src/kernel/sel4/src/arch/x86/object/vcpu.c
|
|
@@ -377,6 +379,12 @@ check_vtx_fixed_values(bool_t useTrueMsrs)
|
|
uint32_t local_cr4_high = x86_rdmsr_low(IA32_VMX_CR4_FIXED0_MSR);
|
|
uint32_t local_cr4_low = x86_rdmsr_low(IA32_VMX_CR4_FIXED1_MSR);
|
|
|
|
+ /* if UG was switched on on boot CPU, do it also on all other CPUs */
|
|
+ if (secondary_control_low & BIT(7)) {
|
|
+ local_secondary_control_high &= BIT(7);
|
|
+ local_cr0_high &= ~(BIT(31) | BIT(0));
|
|
+ }
|
|
+
|
|
/* We want to check that any bits that there are no bits that this core
|
|
* requires to be high, that the BSP did not require to be high. This can
|
|
* be checked with 'local_high & high == local_high'.
|
|
@@ -1067,6 +1075,12 @@ vtx_init(void)
|
|
printf("vt-x: lack of required features\n");
|
|
return false;
|
|
}
|
|
+
|
|
+ /* enable unrestricted guest support if available */
|
|
+ if (secondary_control_low & BIT(7)) {
|
|
+ secondary_control_high |= BIT(7);
|
|
+ cr0_high &= ~(BIT(31) | BIT(0));
|
|
+ }
|
|
}
|
|
if (!check_vtx_fixed_values(vmx_basic_msr_get_true_msrs(vmx_basic))) {
|
|
printf("vt-x: cores have inconsistent features\n");
|