1%
2% Copyright 2014, General Dynamics C4 Systems
3%
4% This software may be distributed and modified according to the terms of
5% the GNU General Public License version 2. Note that NO WARRANTY is provided.
6% See "LICENSE_GPLv2.txt" for details.
7%
8% @TAG(GD_GPL)
9%
10
11\begin{impdetails}
12
13> {-# LANGUAGE CPP, EmptyDataDecls, GeneralizedNewtypeDeriving #-}
14
15\end{impdetails}
16
17This module defines instances of "PSpaceStorable" for ARM-specific kernel objects. This includes page table and page directory entries, and ASID pools.
18
19> module SEL4.Object.Instances.ARM where
20
21\begin{impdetails}
22
23> import SEL4.Machine.Hardware.ARM(PTE(..), PDE(..))
24> import SEL4.Object.Structures
25> import SEL4.Model
26> import Data.Helpers
27#ifdef CONFIG_ARM_SMMU
28> import SEL4.Machine.Hardware.ARM(IOPTE(..), IOPDE(..))
29#endif
30
31\end{impdetails}
32
33> instance PSpaceStorable PDE where
34>     makeObject = InvalidPDE
35>     injectKO = KOArch . KOPDE
36>     projectKO o = case o of
37>                   KOArch (KOPDE p) -> return p
38>                   _ -> typeError "PDE" o
39
40> instance PSpaceStorable PTE where
41>     makeObject = InvalidPTE
42>     injectKO = KOArch . KOPTE
43>     projectKO o = case o of
44>                 KOArch (KOPTE p) -> return p
45>                 _ -> typeError "PTE" o
46
47#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
48> instance PSpaceStorable VCPU where
49>     makeObject = makeVCPUObject
50>     injectKO = KOArch . KOVCPU
51>     projectKO o = case o of
52>                 KOArch (KOVCPU p) -> return p
53>                 _ -> typeError "VCPU" o
54#endif
55
56#ifdef CONFIG_ARM_SMMU
57> instance PSpaceStorable IOPDE where
58>     makeObject = InvalidIOPDE
59>     injectKO = KOArch . KOIOPDE
60>     projectKO o = case o of
61>                   KOArch (KOIOPDE p) -> return p
62>                   _ -> typeError "IOPDE" o
63
64> instance PSpaceStorable IOPTE where
65>     makeObject = InvalidIOPTE
66>     injectKO = KOArch . KOIOPTE
67>     projectKO o = case o of
68>                 KOArch (KOIOPTE p) -> return p
69>                 _ -> typeError "IOPTE" o
70#endif
71
72> instance PSpaceStorable ASIDPool where
73>     makeObject = ASIDPool $
74>         funPartialArray (const Nothing) (0,1023)
75>     injectKO = KOArch . KOASIDPool
76>     projectKO o = case o of
77>         KOArch (KOASIDPool e) -> return e
78>         _ -> typeError "ASID pool" o
79
80