1% Copyright 2014, General Dynamics C4 Systems 2% 3% This software may be distributed and modified according to the terms of 4% the GNU General Public License version 2. Note that NO WARRANTY is provided. 5% See "LICENSE_GPLv2.txt" for details. 6% 7% @TAG(GD_GPL) 8% 9 10This module contains the architecture-specific kernel global data for the X86-64bit architecture. 11 12> module SEL4.Model.StateData.X64 where 13 14\begin{impdetails} 15 16> import Prelude hiding (Word) 17> import SEL4.Machine 18> import SEL4.Machine.Hardware.X64 (PML4E(..),PDPTE(..),PDE(..),PTE(..),IOPort) 19> import SEL4.Object.Structures.X64 20 21> import Data.Array 22 23\end{impdetails} 24 25%FIXME x64: potential C bug: the gdt entry structure in C only has 32 bits for addresses 26 27> data X64VSpaceRegionUse 28> = X64VSpaceUserRegion 29> | X64VSpaceInvalidRegion 30> | X64VSpaceKernelWindow 31> | X64VSpaceDeviceWindow 32 33 34> gdteBits :: Int 35> gdteBits = 3 36 37> data KernelState = X64KernelState { 38> x64KSASIDTable :: Array ASID (Maybe (PPtr ASIDPool)), 39> x64KSSKIMPML4 :: PPtr PML4E, 40> x64KSSKIMPDPTs :: [PPtr PDPTE], 41> x64KSSKIMPDs :: [PPtr PDE], 42> x64KSSKIMPTs :: [PPtr PTE], 43> x64KSCurrentUserCR3 :: CR3, 44> x64KSKernelVSpace :: PPtr Word -> X64VSpaceRegionUse, 45> x64KSAllocatedIOPorts :: Array IOPort Bool, 46> x64KSNumIOAPICs :: Word, 47> x64KSIRQState :: Array IRQ X64IRQState} 48 49> newKernelState :: PAddr -> (KernelState, [PAddr]) 50> newKernelState _ = error "No initial state defined for x64" 51 52