save->base = vmcs_readl(sf->base);
save->limit = vmcs_read32(sf->limit);
save->ar = vmcs_read32(sf->ar_bytes);
- vmcs_write16(sf->selector, vmcs_readl(sf->base) >> 4);
+ vmcs_write16(sf->selector, save->base >> 4);
+ vmcs_write32(sf->base, save->base & 0xfffff);
vmcs_write32(sf->limit, 0xffff);
vmcs_write32(sf->ar_bytes, 0xf3);
}