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