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 the architecture-specific kernel global data for the ARM architecture.
12
13\begin{impdetails}
14
15> {-# LANGUAGE CPP #-}
16
17\end{impdetails}
18
19> module SEL4.Model.StateData.ARM where
20
21\begin{impdetails}
22
23> import Prelude hiding (Word)
24> import SEL4.Machine
25> import SEL4.Machine.Hardware.ARM
26>     (HardwareASID(..), PTE(..), PDE(..), ptBits, pdBits)
27> import SEL4.Object.Structures.ARM
28
29> import Data.Array
30> import Data.Bits
31> import Data.Helpers
32
33\end{impdetails}
34
35The datatype ArmVSpaceRegionUse is solely used to formulate invariants about the use of memory regions.
36Consider the data to be ghost state (only written, never read by the implementation).
37
38> data ArmVSpaceRegionUse
39>  = ArmVSpaceUserRegion
40>  | ArmVSpaceInvalidRegion
41>  | ArmVSpaceKernelWindow
42>  | ArmVSpaceDeviceWindow
43
44There are three ARM-specific global data elements:
45
46\begin{itemize}
47\item a pointer to the globals frame, which is used to map thread-local data --- such as the IPC buffer location --- into every user thread's address space;
48\item the root ASID table; and
49\item the global page directory, which is copied to initialise new page directories, and also as the hardware page table root when the current thread has no valid root.
50\end{itemize}
51
52seL4 stores the hardware ASID into the last (invalid) entry of a page
53directory, which the user cannot map. This allows fast changes to hardware
54ASIDs for a given address space.  To represent this, we use a ghost state
55armKSASIDMap to map from page directories to hardware ASIDs.
56
57armKSKernelVSpace is ghost state.
58
59FIXME ARMHYP_SMMU ARMHYP missing IO ASID to PD map for SMMU
60
61> data KernelState = ARMKernelState {
62>     armKSASIDTable :: Array ASID (Maybe (PPtr ASIDPool)),
63>     armKSHWASIDTable :: Array HardwareASID (Maybe ASID),
64>     armKSNextASID :: HardwareASID,
65>     armKSASIDMap :: Array ASID (Maybe (HardwareASID, PPtr PDE)),
66#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
67>     armKSGlobalPD :: PPtr PDE,
68>     armKSGlobalPTs :: [PPtr PTE],
69#else
70>     armHSCurVCPU :: Maybe (PPtr VCPU, Bool),
71>     armKSGICVCPUNumListRegs :: Int,
72>     armUSGlobalPD :: PPtr PDE,
73>     -- a page directory containing invalid mappings (no shared kernel region)
74#endif
75>     armKSKernelVSpace :: PPtr Word -> ArmVSpaceRegionUse}
76
77#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
78
79> newKernelState :: PAddr -> (KernelState, [PAddr])
80> newKernelState data_start = (state, frames)
81>     where
82>         alignToBits addr b = (((addr - 1) `shiftR` b) + 1) `shiftL` b
83>         globalsFrame = data_start `alignToBits` pageBits
84>         globalsFrameTop = globalsFrame + bit pageBits
85>         globalPTs = globalsFrameTop `alignToBits` pageBits
86>         globalPTsTop = globalPTs + bit pageBits
87>         globalPD = globalPTsTop `alignToBits` pdBits
88>         globalPDTop = globalPD + bit pdBits
89>         frames = globalsFrame :
90>             [globalPTs, globalPTs + bit pageBits .. globalPTsTop - 1] ++
91>             [globalPD, globalPD + bit pageBits .. globalPDTop - 1]
92>         state = ARMKernelState {
93>             armKSASIDTable = funPartialArray (const Nothing) (0, (1 `shiftL` asidHighBits) - 1),
94>             armKSHWASIDTable = funArray (const Nothing),
95>             armKSNextASID = minBound,
96>             armKSASIDMap = funPartialArray (const Nothing) asidRange,
97>             armKSGlobalPD = ptrFromPAddr globalPD,
98>             armKSGlobalPTs = map ptrFromPAddr
99>                 [globalPTs, globalPTs + bit ptBits .. globalPTsTop-1],
100>             armKSKernelVSpace =
101>                 (\vref -> if vref < mask 20 then ArmVSpaceKernelWindow
102>                                             else ArmVSpaceInvalidRegion) }
103
104#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */
105
106FIXME ARMHYP what is this thing, what is data_start? where is it getting data_start? what are these frames it is returning?
107
108FIXME ARMHYP not even sure if mask 20 is correct here
109
110FIXME ARMHYP ok, someone needs to explain how this actually works before it gets fixed
111
112> newKernelState :: PAddr -> (KernelState, [PAddr])
113> newKernelState data_start = (state, frames)
114>     where
115>         alignToBits addr b = (((addr - 1) `shiftR` b) + 1) `shiftL` b
116>         globalsFrame = data_start `alignToBits` pageBits
117>         globalsFrameTop = globalsFrame + bit pageBits
118>         frames = error "FIXME ARMHYP TODO"
119>         state = ARMKernelState {
120>             armKSASIDTable = funPartialArray (const Nothing) (0, (1 `shiftL` asidHighBits) - 1),
121>             armKSHWASIDTable = funArray (const Nothing),
122>             armKSNextASID = minBound,
123>             armKSASIDMap = funPartialArray (const Nothing) asidRange,
124>             armHSCurVCPU = Nothing,
125>             armKSGICVCPUNumListRegs = error "FIXME ARMHYP read from platform",
126>             armUSGlobalPD = error "FIXME ARMHYP address of C global constant",
127>             armKSKernelVSpace =
128>                 (\vref -> if vref < mask 20 then ArmVSpaceKernelWindow
129>                                             else ArmVSpaceInvalidRegion)
130>             }
131
132#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
133
134