forked from Imagelibrary/seL4
3207abeeb7
TLS_BASE virtual register is replaced with FS_BASE and GS_BASE virtual registers. The FS_BASE and GS_BASE virtual registers are moved to the end of the context so they need not be considered in the kernel exit and entry implementation. Removed tracking of ES, DS, FS, and GS segment selectors on kernel entry and exit. ES and DS are clobbered on kernel entry with the RPL 3 selector for a DPL 3 linear data segment. FS is clobbered on exit with the RPL 3 selector for the DPL 3 segment with FS_BASE as the base. This is done on exit to reload the value from the GDT. GS is clobbered on exit with the RPL 3 selector for the DPL 3 segment with GS_BASE as the base. This is done on exit to reload the value from the GDT. Kernel entry and exit code is refactored, simplified, and improved in light of the above changes. x64: update verified config to use fsgsbase instr The verification platform for x64 relies on the fsgsbase instruction.