data = vmcs_read32(GUEST_SYSENTER_CS);
                break;
        case MSR_IA32_SYSENTER_EIP:
-               data = vmcs_read32(GUEST_SYSENTER_EIP);
+               data = vmcs_readl(GUEST_SYSENTER_EIP);
                break;
        case MSR_IA32_SYSENTER_ESP:
-               data = vmcs_read32(GUEST_SYSENTER_ESP);
+               data = vmcs_readl(GUEST_SYSENTER_ESP);
                break;
        default:
                msr = find_msr_entry(vcpu, msr_index);
                vmcs_write32(GUEST_SYSENTER_CS, data);
                break;
        case MSR_IA32_SYSENTER_EIP:
-               vmcs_write32(GUEST_SYSENTER_EIP, data);
+               vmcs_writel(GUEST_SYSENTER_EIP, data);
                break;
        case MSR_IA32_SYSENTER_ESP:
-               vmcs_write32(GUEST_SYSENTER_ESP, data);
+               vmcs_writel(GUEST_SYSENTER_ESP, data);
                break;
        case MSR_IA32_TIME_STAMP_COUNTER:
                guest_write_tsc(data);