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 defines instances of "PSpaceStorable" for X64-specific kernel objects. This includes page table and page directory entries, and ASID pools.
11
12> module SEL4.Object.Instances.X64 where
13
14\begin{impdetails}
15
16> import SEL4.Machine.Hardware.X64(PTE(..), PDE(..), PDPTE(..), PML4E(..))
17> import SEL4.Object.Structures
18> import SEL4.Model
19> import Data.Helpers
20
21\end{impdetails}
22
23> instance PSpaceStorable PDE where
24>     makeObject = InvalidPDE
25>     injectKO = KOArch . KOPDE
26>     projectKO o = case o of
27>                   KOArch (KOPDE p) -> return p
28>                   _ -> typeError "PDE" o
29
30> instance PSpaceStorable PTE where
31>     makeObject = InvalidPTE
32>     injectKO = KOArch . KOPTE
33>     projectKO o = case o of
34>                 KOArch (KOPTE p) -> return p
35>                 _ -> typeError "PTE" o
36
37> instance PSpaceStorable PDPTE where
38>     makeObject = InvalidPDPTE
39>     injectKO = KOArch . KOPDPTE
40>     projectKO o = case o of
41>                 KOArch (KOPDPTE p) -> return p
42>                 _ -> typeError "PDPTE" o
43
44> instance PSpaceStorable PML4E where
45>     makeObject = InvalidPML4E
46>     injectKO = KOArch . KOPML4E
47>     projectKO o = case o of
48>                 KOArch (KOPML4E p) -> return p
49>                 _ -> typeError "PML4E" o
50
51> instance PSpaceStorable ASIDPool where
52>     makeObject = ASIDPool $
53>         funPartialArray (const Nothing) (0,1023)
54>     injectKO = KOArch . KOASIDPool
55>     projectKO o = case o of
56>         KOArch (KOASIDPool e) -> return e
57>         _ -> typeError "ASID pool" o
58
59>--instance PSpaceStorable IOPTE where
60>--    makeObject = InvalidIOPTE
61>--    injectKO = KOArch . KOIOPTE
62>--    projectKO o = case o of
63>--                KOArch (KOIOPTE p) -> return p
64>--                _ -> typeError "IOPTE" o
65
66>--instance PSpaceStorable IORTE where
67>--    makeObject = InvalidIORTE
68>--    injectKO = KOArch . KOIORTE
69>--    projectKO o = case o of
70>--                KOArch (KOIORTE p) -> return p
71>--                _ -> typeError "IORTE" o
72
73>--instance PSpaceStorable IOCTE where
74>--    makeObject = InvalidIOCTE
75>--    injectKO = KOArch . KOIOCTE
76>--    projectKO o = case o of
77>--                KOArch (KOIOCTE p) -> return p
78>--                _ -> typeError "IOCTE" o
79
80