pub const VMX_BASIC_VMCS_SIZE_SHIFT: u32 = 32;