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
11This module contains an instance of the machine-specific kernel API for the ARM architecture with hypervisor extensions.
12
13> {-# LANGUAGE CPP #-}
14
15> module SEL4.API.Types.ARM where
16
17> import SEL4.API.Types.Universal(APIObjectType, apiGetObjectSize)
18> import SEL4.Machine.Hardware.ARM
19> import Data.List (elemIndex)
20> import Data.Maybe (fromJust)
21
22There are three ARM-specific object types: virtual pages, page tables, and page directories.
23
24Hypervisor additions add VCPUs.
25
26I/O MMU additions add IO page table objects. Note that there is only one IO page directory created at kernel boot, which cannot be created or deleted. Hence IO page directories are not considered kernel objects.
27
28> data ObjectType
29>     = APIObjectType APIObjectType
30>     | SmallPageObject
31>     | LargePageObject
32>     | SectionObject
33>     | SuperSectionObject
34>     | PageTableObject
35>     | PageDirectoryObject
36#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
37>     | VCPUObject
38#endif
39#ifdef CONFIG_ARM_SMMU
40>     | IOPageTableObject
41#endif
42>     deriving (Show, Eq)
43
44> instance Bounded ObjectType where
45>     minBound = APIObjectType minBound
46>     maxBound = PageDirectoryObject
47
48> instance Enum ObjectType where
49>     fromEnum e =
50>       case e of
51>           APIObjectType a -> fromEnum a
52>           _ -> apiMax + 1 + archToIndex e
53>           where apiMax = fromEnum (maxBound :: APIObjectType)
54>                 archToIndex c = fromJust $ elemIndex c
55>                     [SmallPageObject
56>                     ,LargePageObject
57>                     ,SectionObject
58>                     ,SuperSectionObject
59>                     ,PageTableObject
60>                     ,PageDirectoryObject
61#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
62>                     ,VCPUObject
63#endif
64#ifdef CONFIG_ARM_SMMU
65>                     ,IOPageTableObject
66#endif
67>                     ]
68>     toEnum n
69>         | n <= apiMax = APIObjectType $ toEnum n
70>         | n == fromEnum SmallPageObject = SmallPageObject
71>         | n == fromEnum LargePageObject = LargePageObject
72>         | n == fromEnum SectionObject = SectionObject
73>         | n == fromEnum SuperSectionObject = SuperSectionObject
74>         | n == fromEnum PageTableObject = PageTableObject
75>         | n == fromEnum PageDirectoryObject = PageDirectoryObject
76#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
77>         | n == fromEnum VCPUObject = VCPUObject
78#endif
79#ifdef CONFIG_ARM_SMMU
80>         | n == fromEnum IOPageTableObject = IOPageTableObject
81#endif
82>         | otherwise = error "toEnum out of range for ARM.ObjectType"
83>         where apiMax = fromEnum (maxBound :: APIObjectType)
84
85> fromAPIType = APIObjectType
86
87> toAPIType (APIObjectType a) = Just a
88> toAPIType _ = Nothing
89
90> pageType = SmallPageObject
91
92> getObjectSize :: ObjectType -> Int -> Int
93> getObjectSize SmallPageObject _ = pageBitsForSize ARMSmallPage
94> getObjectSize LargePageObject _ = pageBitsForSize ARMLargePage
95> getObjectSize SectionObject _ = pageBitsForSize ARMSection
96> getObjectSize SuperSectionObject _ = pageBitsForSize ARMSuperSection
97> getObjectSize PageTableObject _ = ptBits
98> getObjectSize PageDirectoryObject _ = pdBits
99#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
100> getObjectSize VCPUObject _ = vcpuBits
101#endif
102#ifdef CONFIG_ARM_SMMU
103> getObjectSize IOPageTableObject _ = ioptBits
104#endif
105> getObjectSize (APIObjectType apiObjectType) size = apiGetObjectSize apiObjectType size
106
107
108> isFrameType :: ObjectType -> Bool
109> isFrameType SmallPageObject = True
110> isFrameType LargePageObject = True
111> isFrameType SectionObject = True
112> isFrameType SuperSectionObject = True
113> isFrameType _ = False
114
115