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, GeneralizedNewtypeDeriving #-}
14
15\end{impdetails}
16
17This module defines the low-level ARM hardware interface.
18
19> module SEL4.Machine.Hardware.ARM where
20
21\begin{impdetails}
22
23> import Prelude hiding (Word)
24> import SEL4.Machine.RegisterSet
25
26> import Control.Monad.Reader
27> import Data.Bits
28> import Data.Word(Word8, Word32)
29> import Data.Ix
30
31\end{impdetails}
32
33The ARM-specific register set definitions are qualified with the "ARM" prefix, and the platform-specific hardware access functions are qualified with the "Platform" prefix. The latter module is outside the scope of the reference manual; for the executable model, it is specific to the external simulator used for user-level code.
34
35> import qualified SEL4.Machine.RegisterSet.TARGET as ARM
36> import qualified SEL4.Machine.Hardware.TARGET.Callbacks as Platform
37> import qualified SEL4.Machine.Hardware.TARGET.PLATFORM as Platform
38
39\subsection{Data Types}
40
41The machine monad contains a platform-specific opaque pointer, used by the external simulator interface.
42
43> type MachineData = Platform.MachineData
44
45> type MachineMonad = ReaderT MachineData IO
46
47> type IRQ = Platform.IRQ
48
49> newtype HardwareASID = HardwareASID { fromHWASID :: Word8 }
50>     deriving (Num, Enum, Bounded, Ord, Ix, Eq, Show)
51
52> toPAddr = Platform.PAddr
53
54\subsubsection{Virtual Memory}
55
56ARM hardware-defined pages come in four sizes: 4k, 64k, 1M and 16M. The 16M page size only has hardware support on some ARMv6 CPUs, such as the ARM1136; the kernel will simulate them using 16 1M mappings on other CPUs.
57
58> data VMPageSize
59>     = ARMSmallPage
60>     | ARMLargePage
61>     | ARMSection
62>     | ARMSuperSection
63>     deriving (Show, Eq, Ord, Enum, Bounded)
64
65ARM virtual memory faults are handled by one of two trap handlers: one for data aborts, and one for instruction aborts.
66
67> data VMFaultType
68>     = ARMDataAbort
69>     | ARMPrefetchAbort
70>     deriving Show
71
72\subsection{Hypervisor}
73
74> data HypFaultType
75#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
76>     = ARMVCPUFault Word32 -- HSR
77#else
78>     = ARMNoHypFaults
79#endif
80>     deriving Show
81
82\subsubsection{Physical Memory}
83
84The ARM MMU does not allow access to physical addresses while translation is enabled; the kernel must access its objects via virtual addresses. Depending on the platform, these virtual addresses may either be the same as the physical addresses, or offset by a constant.
85
86> type PAddr = Platform.PAddr
87
88> ptrFromPAddr :: PAddr -> PPtr a
89> ptrFromPAddr = Platform.ptrFromPAddr
90
91> addrFromPPtr :: PPtr a -> PAddr
92> addrFromPPtr = Platform.addrFromPPtr
93
94> fromPAddr :: PAddr -> Word
95> fromPAddr = Platform.fromPAddr
96
97> addPAddr :: PAddr -> Word -> PAddr
98> addPAddr p w = toPAddr (fromPAddr p + w)
99
100\subsection{Hardware Access}
101
102The following functions define the ARM-specific interface between the kernel and the hardware. Most of them depend on the simulator in use, and are therefore defined in the platform module.
103
104> pageBits :: Int
105> pageBits = 12
106
107> pageBitsForSize :: VMPageSize -> Int
108> pageBitsForSize ARMSmallPage = 12
109> pageBitsForSize ARMLargePage = 16
110#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
111> pageBitsForSize ARMSection = 20
112> pageBitsForSize ARMSuperSection = 24
113#else
114> pageBitsForSize ARMSection = 21
115> pageBitsForSize ARMSuperSection = 25
116#endif
117
118> getMemoryRegions :: MachineMonad [(PAddr, PAddr)]
119> getMemoryRegions = do
120>     cpbtr <- ask
121>     liftIO $ Platform.getMemoryRegions cpbtr
122
123> getDeviceRegions :: MachineMonad [(PAddr, PAddr)]
124> getDeviceRegions = do
125>     cbptr <- ask
126>     liftIO $ Platform.getDeviceRegions cbptr
127
128> getKernelDevices :: MachineMonad [(PAddr, PPtr Word)]
129> getKernelDevices = do
130>     cbptr <- ask
131>     liftIO $ Platform.getKernelDevices cbptr
132
133> loadWord :: PPtr Word -> MachineMonad Word
134> loadWord ptr = do
135>     cbptr <- ask
136>     liftIO $ Platform.loadWordCallback cbptr $ addrFromPPtr ptr
137
138> storeWord :: PPtr Word -> Word -> MachineMonad ()
139> storeWord ptr val = do
140>     cbptr <- ask
141>     liftIO $ Platform.storeWordCallback cbptr (addrFromPPtr ptr) val
142
143> storeWordVM :: PPtr Word -> Word -> MachineMonad ()
144> storeWordVM ptr val = storeWord ptr val
145
146> pageColourBits :: Int
147> pageColourBits = Platform.pageColourBits
148
149> getActiveIRQ :: Bool -> MachineMonad (Maybe IRQ)
150> getActiveIRQ _ = do
151>     cbptr <- ask
152>     liftIO $ Platform.getActiveIRQ cbptr
153
154> ackInterrupt :: IRQ -> MachineMonad ()
155> ackInterrupt irq = do
156>     cbptr <- ask
157>     liftIO $ Platform.ackInterrupt cbptr irq
158
159> maskInterrupt :: Bool -> IRQ -> MachineMonad ()
160> maskInterrupt maskI irq = do
161>     cbptr <- ask
162>     liftIO $ Platform.maskInterrupt cbptr maskI irq
163
164> configureTimer :: MachineMonad IRQ
165> configureTimer = do
166>     cbptr <- ask
167>     liftIO $ Platform.configureTimer cbptr
168
169> initIRQController :: MachineMonad ()
170> initIRQController = do
171>     cbptr <- ask
172>     liftIO $ Platform.initIRQController cbptr
173
174> setIRQTrigger :: IRQ -> Bool -> MachineMonad ()
175> setIRQTrigger irq trigger = error "ARM machine callback unimplemented"
176
177> resetTimer :: MachineMonad ()
178> resetTimer = do
179>     cbptr <- ask
180>     liftIO $ Platform.resetTimer cbptr
181
182> debugPrint :: String -> MachineMonad ()
183> debugPrint str = liftIO $ putStrLn str
184
185> getRestartPC = getRegister (Register ARM.FaultInstruction)
186> setNextPC = setRegister (Register ARM.LR_svc)
187
188\subsection{ARM Memory Management}
189
190There are several operations used by the ARM memory management code to access relevant hardware registers.
191
192\subsubsection{Cleaning Memory}
193
194This function is called before a region of user-memory is recycled.
195It zeros every word to ensure that user tasks cannot access any private data
196that might previously have been stored in the region and
197then flushes the kernel's mapping from the virtually-indexed caches.
198
199> clearMemory :: PPtr Word -> Int -> MachineMonad ()
200> clearMemory ptr byteLength = do
201>     let wordSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8
202>     let ptr' = PPtr $ fromPPtr ptr
203>     let ptrs = [ptr', ptr' + wordSize .. ptr' + fromIntegral byteLength - 1]
204>     mapM_ (\p -> storeWord p 0) ptrs
205>     cleanCacheRange_PoU (VPtr $ fromPPtr ptr)
206>                         (VPtr (fromPPtr (ptr + fromIntegral byteLength - 1)))
207>                         (toPAddr $ fromPPtr ptr)
208
209This function is called before a region of memory is made user-accessible.
210Though in Haskell, it is implemented as "clearMemory",
211we draw the logical distinction to gain more freedom for its interpretation
212in the Isabelle formalization.
213
214> initMemory :: PPtr Word -> Int -> MachineMonad ()
215> initMemory = clearMemory
216
217This function is called to free a region of user-memory after use.
218In Haskell, this operation does not do anything.
219We just use it as a stub for the Isabelle formalization.
220
221> freeMemory :: PPtr Word -> Int -> MachineMonad ()
222> freeMemory _ _ = return ()
223
224Same as "clearMemory", but uses storeWordVM to write to memory.
225To be used when creating mapping objects (page tables and -dirs)
226Flushing the kernel's mapping from the virtually-indexed
227caches must be done separately.
228
229> clearMemoryVM :: PPtr Word -> Int -> MachineMonad ()
230> clearMemoryVM ptr bits = do
231>     let wordSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8
232>     let ptr' = PPtr $ fromPPtr ptr
233>     let ptrs = [ptr', ptr' + wordSize .. ptr' + 1 `shiftL` bits - 1]
234>     mapM_ (\p -> storeWordVM p 0) ptrs
235
236\subsubsection{Address Space Setup}
237
238> writeTTBR0 :: Word -> MachineMonad ()
239> writeTTBR0 w = do
240>     cbptr <- ask
241>     liftIO $ Platform.writeTTBR0 cbptr w
242
243> writeTTBR0Ptr :: PAddr -> MachineMonad ()
244> writeTTBR0Ptr pd = writeTTBR0 ((fromPAddr pd .&. 0xffffe000) .|. 0x18)
245
246> setCurrentPD :: PAddr -> MachineMonad ()
247> setCurrentPD pd = do
248#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
249>     setCurrentPDPL2 pd
250#else
251>     dsb
252>     writeTTBR0Ptr pd
253>     isb
254#endif
255
256> setHardwareASID :: HardwareASID -> MachineMonad ()
257> setHardwareASID (HardwareASID hw_asid) = do
258>     cbptr <- ask
259>     liftIO $ Platform.setHardwareASID cbptr hw_asid
260
261#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
262
263> setCurrentPDPL2 :: PAddr -> MachineMonad ()
264> setCurrentPDPL2 = error "FIXME ARMHYP machine callback unimplemented"
265
266> writeContextIDAndPD :: HardwareASID -> PAddr -> MachineMonad ()
267> writeContextIDAndPD = error "FIXME ARMHYP  machine callback unimplemented"
268
269#endif
270
271\subsubsection{Memory Barriers}
272
273> isb :: MachineMonad ()
274> isb = do
275>     cbptr <- ask
276>     liftIO $ Platform.isbCallback cbptr
277
278> dsb :: MachineMonad ()
279> dsb = do
280>     cbptr <- ask
281>     liftIO $ Platform.dsbCallback cbptr
282
283> dmb :: MachineMonad ()
284> dmb = do
285>     cbptr <- ask
286>     liftIO $ Platform.dmbCallback cbptr
287
288\subsubsection{Cache Cleaning and TLB Flushes}
289
290> invalidateLocalTLB :: MachineMonad ()
291> invalidateLocalTLB = do
292>     cbptr <- ask
293>     liftIO $ Platform.invalidateLocalTLBCallback cbptr
294
295> invalidateLocalTLB_ASID :: HardwareASID -> MachineMonad ()
296> invalidateLocalTLB_ASID (HardwareASID hw_asid) = do
297>     cbptr <- ask
298>     liftIO $ Platform.invalidateLocalTLB_ASIDCallback cbptr hw_asid
299
300> invalidateLocalTLB_VAASID :: Word -> MachineMonad ()
301> invalidateLocalTLB_VAASID mva_plus_asid = do
302>     cbptr <- ask
303>     liftIO $ Platform.invalidateLocalTLB_VAASIDCallback cbptr mva_plus_asid
304
305> cleanByVA :: VPtr -> PAddr -> MachineMonad ()
306> cleanByVA mva pa = do
307>     cbptr <- ask
308>     liftIO $ Platform.cacheCleanByVACallback cbptr mva pa
309
310> cleanByVA_PoU :: VPtr -> PAddr -> MachineMonad ()
311> cleanByVA_PoU mva pa = do
312>     cbptr <- ask
313>     liftIO $ Platform.cacheCleanByVA_PoUCallback cbptr mva pa
314
315> invalidateByVA :: VPtr -> PAddr -> MachineMonad ()
316> invalidateByVA mva pa = do
317>     cbptr <- ask
318>     liftIO $ Platform.cacheInvalidateByVACallback cbptr mva pa
319
320> invalidateByVA_I :: VPtr -> PAddr -> MachineMonad ()
321> invalidateByVA_I mva pa = do
322>     cbptr <- ask
323>     liftIO $ Platform.cacheInvalidateByVA_ICallback cbptr mva pa
324
325> invalidate_I_PoU :: MachineMonad ()
326> invalidate_I_PoU = do
327>     cbptr <- ask
328>     liftIO $ Platform.cacheInvalidate_I_PoUCallback cbptr
329
330> cleanInvalByVA :: VPtr -> PAddr -> MachineMonad ()
331> cleanInvalByVA mva pa = do
332>     cbptr <- ask
333>     liftIO $ Platform.cacheCleanInvalidateByVACallback cbptr mva pa
334
335> branchFlush :: VPtr -> PAddr -> MachineMonad ()
336> branchFlush mva pa = do
337>     cbptr <- ask
338>     liftIO $ Platform.branchFlushCallback cbptr mva pa
339
340> clean_D_PoU :: MachineMonad ()
341> clean_D_PoU = do
342>     cbptr <- ask
343>     liftIO $ Platform.cacheClean_D_PoUCallback cbptr
344
345> cleanInvalidate_D_PoC :: MachineMonad ()
346> cleanInvalidate_D_PoC = do
347>     cbptr <- ask
348>     liftIO $ Platform.cacheCleanInvalidate_D_PoCCallback cbptr
349
350> cleanInvalidate_D_PoU :: MachineMonad ()
351> cleanInvalidate_D_PoU = do
352>     cbptr <- ask
353>     liftIO $ Platform.cacheCleanInvalidate_D_PoUCallback cbptr
354
355> cleanInvalidateL2Range :: PAddr -> PAddr -> MachineMonad ()
356> cleanInvalidateL2Range start end = do
357>     cbptr <- ask
358>     liftIO $ Platform.cacheCleanInvalidateL2RangeCallback cbptr start end
359
360> invalidateL2Range :: PAddr -> PAddr -> MachineMonad ()
361> invalidateL2Range start end = do
362>     cbptr <- ask
363>     liftIO $ Platform.cacheInvalidateL2RangeCallback cbptr start end
364
365> cleanL2Range :: PAddr -> PAddr -> MachineMonad ()
366> cleanL2Range start end = do
367>     cbptr <- ask
368>     liftIO $ Platform.cacheCleanL2RangeCallback cbptr start end
369
370> lineStart addr = (addr `shiftR` cacheLineBits) `shiftL` cacheLineBits
371
372Performs the given operation on every cache line that intersects the
373supplied range.
374
375> cacheRangeOp :: (VPtr -> PAddr -> MachineMonad ()) ->
376>                 VPtr -> VPtr -> PAddr -> MachineMonad ()
377> cacheRangeOp operation vstart vend pstart = do
378>     let pend = pstart + (toPAddr $ fromVPtr (vend - vstart))
379>     let vptrs = [lineStart vstart, lineStart vstart + fromIntegral cacheLine .. lineStart vend]
380>     let pptrs = [lineStart pstart, lineStart pstart + fromIntegral cacheLine .. lineStart pend]
381>     mapM_ (\(v,p) -> operation v p) (zip vptrs pptrs)
382
383> cleanCacheRange_PoC :: VPtr -> VPtr -> PAddr -> MachineMonad ()
384> cleanCacheRange_PoC vstart vend pstart =
385>     cacheRangeOp cleanByVA vstart vend pstart
386
387> cleanInvalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
388> cleanInvalidateCacheRange_RAM vstart vend pstart = do
389>     cleanCacheRange_PoC vstart vend pstart
390>     dsb
391>     cleanInvalidateL2Range pstart (pstart + (toPAddr $ fromVPtr $ vend - vstart))
392>     cacheRangeOp cleanInvalByVA vstart vend pstart
393>     dsb
394
395> cleanCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
396> cleanCacheRange_RAM vstart vend pstart = do
397>     cleanCacheRange_PoC vstart vend pstart
398>     dsb
399>     cleanL2Range pstart (pstart + (toPAddr $ fromVPtr $ vend - vstart))
400
401> cleanCacheRange_PoU :: VPtr -> VPtr -> PAddr -> MachineMonad ()
402> cleanCacheRange_PoU vstart vend pstart =
403>     cacheRangeOp cleanByVA_PoU vstart vend pstart
404
405> invalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
406> invalidateCacheRange_RAM vstart vend pstart = do
407>     when (vstart /= lineStart vstart) $
408>         cleanCacheRange_RAM vstart vstart pstart
409>     when (vend + 1 /= lineStart (vend + 1)) $
410>         cleanCacheRange_RAM (lineStart vend) (lineStart vend)
411>             (pstart + (toPAddr $ fromVPtr $ lineStart vend - vstart))
412>     invalidateL2Range pstart
413>         (pstart + (toPAddr $ fromVPtr $ vend - vstart))
414>     cacheRangeOp invalidateByVA vstart vend pstart
415>     dsb
416
417> invalidateCacheRange_I :: VPtr -> VPtr -> PAddr -> MachineMonad ()
418> invalidateCacheRange_I vstart vend pstart =
419>     cacheRangeOp invalidateByVA_I vstart vend pstart
420
421> branchFlushRange :: VPtr -> VPtr -> PAddr -> MachineMonad ()
422> branchFlushRange vstart vend pstart =
423>     cacheRangeOp branchFlush vstart vend pstart
424
425> cleanCaches_PoU :: MachineMonad ()
426> cleanCaches_PoU = do
427>     dsb
428>     clean_D_PoU
429>     dsb
430>     invalidate_I_PoU
431>     dsb
432
433> cleanInvalidateL1Caches :: MachineMonad ()
434> cleanInvalidateL1Caches = do
435>     dsb
436>     cleanInvalidate_D_PoC
437>     dsb
438>     invalidate_I_PoU
439>     dsb
440
441This function is used to clear the load exclusive monitor. This dummy
442implementation assumes the monitor is not modelled in our simulator.
443
444> clearExMonitor :: MachineMonad ()
445> clearExMonitor = return ()
446
447\subsubsection{Fault Status Registers}
448
449> getIFSR :: MachineMonad Word
450> getIFSR = do
451>     cbptr <- ask
452>     liftIO $ Platform.getIFSR cbptr
453
454> getDFSR :: MachineMonad Word
455> getDFSR = do
456>     cbptr <- ask
457>     liftIO $ Platform.getDFSR cbptr
458
459> getFAR :: MachineMonad VPtr
460> getFAR = do
461>     cbptr <- ask
462>     liftIO $ Platform.getFAR cbptr
463
464#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
465
466\subsection{Hypervisor-specific status/control registers}
467
468> getHSR :: MachineMonad Word
469> getHSR = error "FIXME ARMHYP machine callback unimplemented"
470
471> setHCR :: Word -> MachineMonad ()
472> setHCR _hcr = error "FIXME ARMHYP machine callback unimplemented"
473
474> getHDFAR :: MachineMonad VPtr
475> getHDFAR = error "FIXME ARMHYP machine callback unimplemented"
476
477> addressTranslateS1CPR :: VPtr -> MachineMonad VPtr
478> addressTranslateS1CPR = error "FIXME ARMHYP machine callback unimplemented"
479
480> getSCTLR :: MachineMonad Word
481> getSCTLR = error "FIXME ARMHYP machine callback unimplemented"
482
483> setSCTLR :: Word -> MachineMonad ()
484> setSCTLR _sctlr = error "FIXME ARMHYP machine callback unimplemented"
485
486\subsection{Hypervisor banked registers}
487
488Rather than a line-for-line copy of every hypervisor register storage and
489retrieval function from the C code, we abstract the concept into one function
490each. Some special registers, like SCTLR, still get their own load/store
491functions due to being operated on separately.
492
493> readVCPUHardwareReg :: ARM.VCPUReg -> MachineMonad Word
494> readVCPUHardwareReg reg = error "FIXME ARMHYP machine callback unimplemented"
495
496> writeVCPUHardwareReg :: ARM.VCPUReg -> Word -> MachineMonad ()
497> writeVCPUHardwareReg reg val = error "FIXME ARMHYP machine callback unimplemented"
498
499#endif
500
501\subsubsection{Page Table Structure}
502
503The ARM architecture defines a two-level hardware-walked page table. The kernel must write entries to this table in the defined format to construct address spaces for user-level tasks.
504
505#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
506
507The following types are Haskell representations of an entry in an ARMv6 page table. The "PDE" (page directory entry) type is an entry in the first level, and the "PTE" (page table entry) type is an entry in the second level. Note that "SuperSectionPDE" is an extension provided by some ARMv6 cores.
508
509> data PDE
510>     = InvalidPDE
511>     | PageTablePDE {
512>         pdeTable :: PAddr,
513>         pdeParity :: Bool,
514>         pdeDomain :: Word }
515>     | SectionPDE {
516>         pdeFrame :: PAddr,
517>         pdeParity :: Bool,
518>         pdeDomain :: Word,
519>         pdeCacheable :: Bool,
520>         pdeGlobal :: Bool,
521>         pdeExecuteNever :: Bool,
522>         pdeRights :: VMRights }
523>     | SuperSectionPDE {
524>         pdeFrame :: PAddr,
525>         pdeParity :: Bool,
526>         pdeCacheable :: Bool,
527>         pdeGlobal :: Bool,
528>         pdeExecuteNever :: Bool,
529>         pdeRights :: VMRights }
530>     deriving (Show, Eq)
531
532> wordFromPDE :: PDE -> Word
533> wordFromPDE InvalidPDE = 0
534> wordFromPDE (PageTablePDE table parity domain) = 1 .|.
535>     (fromIntegral table .&. 0xfffffc00) .|.
536>     (if parity then bit 9 else 0) .|.
537>     ((domain .&. 0xf) `shiftL` 5)
538> wordFromPDE (SectionPDE frame parity domain cacheable global xn rights) = 2 .|.
539>     (fromIntegral frame .&. 0xfff00000) .|.
540>     (if parity then bit 9 else 0) .|.
541>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
542>     (if xn then bit 4 else 0) .|.
543>     ((domain .&. 0xf) `shiftL` 5) .|.
544>     (if global then 0 else bit 17) .|.
545>     (fromIntegral $ fromEnum rights `shiftL` 10)
546> wordFromPDE (SuperSectionPDE frame parity cacheable global xn rights) = 2 .|.
547>     bit 18 .|.
548>     (fromIntegral frame .&. 0xff000000) .|.
549>     (if parity then bit 9 else 0) .|.
550>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
551>     (if xn then bit 4 else 0) .|.
552>     (if global then 0 else bit 17) .|.
553>     (fromIntegral $ fromEnum rights `shiftL` 10)
554
555> data PTE
556>     = InvalidPTE
557>     | LargePagePTE {
558>         pteFrame :: PAddr,
559>         pteCacheable :: Bool,
560>         pteGlobal :: Bool,
561>         pteExecuteNever :: Bool,
562>         pteRights :: VMRights }
563>     | SmallPagePTE {
564>         pteFrame :: PAddr,
565>         pteCacheable :: Bool,
566>         pteGlobal :: Bool,
567>         pteExecuteNever :: Bool,
568>         pteRights :: VMRights }
569>     deriving (Show, Eq)
570
571> wordFromPTE :: PTE -> Word
572> wordFromPTE InvalidPTE = 0
573> wordFromPTE (LargePagePTE frame cacheable global xn rights) = 1 .|.
574>     (fromIntegral frame .&. 0xffff0000) .|.
575>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
576>     (if global then 0 else bit 11) .|.
577>     (if xn then bit 15 else 0) .|.
578>     (fromIntegral $ fromEnum rights `shiftL` 4)
579> wordFromPTE (SmallPagePTE frame cacheable global xn rights) = 2 .|.
580>     (fromIntegral frame .&. 0xfffff000) .|.
581>     (if xn then 1 else 0) .|.
582>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
583>     (if global then 0 else bit 11) .|.
584>     (fromIntegral $ fromEnum rights `shiftL` 4)
585
586#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */
587
588Hypervisor extensions use long page table descriptors (64-bit) for the stage 2
589translation (host-to-hypervisor). This is a three-level table system, but the
590hardware can be configured to omit the first level entirely if all second
591levels are stored contiguously. We use this configuration to preserve the usual
592page table/directory nomenclature.
593
594> -- FIXME ARMHYP global (SH) is never used so I don't know what a global page's SH would look like
595
596seL4 does not use hardware domains or parity on ARM hypervisor systems.
597
598> data PDE
599>     = InvalidPDE
600>     | PageTablePDE {
601>         pdeTable :: PAddr }
602>     | SectionPDE {
603>         pdeFrame :: PAddr,
604>         pdeCacheable :: Bool,
605>         pdeExecuteNever :: Bool,
606>         pdeRights :: VMRights }
607>     | SuperSectionPDE {
608>         pdeFrame :: PAddr,
609>         pdeCacheable :: Bool,
610>         pdeExecuteNever :: Bool,
611>         pdeRights :: VMRights }
612>     deriving (Show, Eq)
613
614> hapFromVMRights :: VMRights -> Word
615> hapFromVMRights VMKernelOnly = 0
616> hapFromVMRights VMNoAccess = 0
617> hapFromVMRights VMReadOnly = 1
618> hapFromVMRights VMReadWrite = 3
619
620> wordsFromPDE :: PDE -> [Word]
621> wordsFromPDE InvalidPDE = [0, 0]
622> wordsFromPDE (PageTablePDE table) = [w0, 0]
623>     where w0 = 3 .|. (fromIntegral table .&. 0xfffff000)
624> wordsFromPDE (SectionPDE frame cacheable xn rights) = [w0, w1]
625>     where w1 = 0 .|. (if xn then bit 22 else 0) -- no contig. hint
626>           w0 = 1 .|.
627>                (fromIntegral frame .&. 0xfffff000) .|.
628>                bit 10 .|. -- AF
629>                (hapFromVMRights rights `shiftL` 6) .|.
630>                (if cacheable then 0xf `shiftL` 2 else 0)
631> wordsFromPDE (SuperSectionPDE frame cacheable xn rights) = [w0, w1]
632>     where w1 = 0 .|. (if xn then bit 22 else 0) .|. bit 20 -- contig. hint
633>           w0 = 1 .|.
634>                (fromIntegral frame .&. 0xfffff000) .|.
635>                bit 10 .|. -- AF
636>                (hapFromVMRights rights `shiftL` 6) .|.
637>                (if cacheable then 0xf `shiftL` 2 else 0)
638
639> data PTE
640>     = InvalidPTE
641>     | LargePagePTE {
642>         pteFrame :: PAddr,
643>         pteCacheable :: Bool,
644>         pteExecuteNever :: Bool,
645>         pteRights :: VMRights }
646>     | SmallPagePTE {
647>         pteFrame :: PAddr,
648>         pteCacheable :: Bool,
649>         pteExecuteNever :: Bool,
650>         pteRights :: VMRights }
651>     deriving (Show, Eq)
652
653> wordsFromPTE :: PTE -> [Word]
654> wordsFromPTE InvalidPTE = [0, 0]
655> wordsFromPTE (SmallPagePTE frame cacheable xn rights) = [w0, w1]
656>     where w1 = 0 .|. (if xn then bit 22 else 0) .|. bit 20 -- contig. hint
657>           w0 = 3 .|.
658>                (fromIntegral frame .&. 0xfffff000) .|.
659>                bit 10 .|. -- AF
660>                (hapFromVMRights rights `shiftL` 6) .|.
661>                (if cacheable then 0xf `shiftL` 2 else 0)
662> wordsFromPTE (LargePagePTE frame cacheable xn rights) = [w0, w1]
663>     where w1 = 0 .|. (if xn then bit 22 else 0) -- no contig. hint
664>           w0 = 3 .|.
665>                (fromIntegral frame .&. 0xfffff000) .|.
666>                bit 10 .|. -- AF
667>                (hapFromVMRights rights `shiftL` 6) .|.
668>                (if cacheable then 0xf `shiftL` 2 else 0)
669
670#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
671
672> data VMRights
673>     = VMNoAccess
674>     | VMKernelOnly
675>     | VMReadOnly
676>     | VMReadWrite
677>     deriving (Show, Eq, Enum)
678
679> data VMAttributes = VMAttributes {
680>     armPageCacheable, armParityEnabled, armExecuteNever :: Bool }
681
682Convenient references to size and log of size of PDEs and PTEs.
683
684#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
685
686With hypervisor extensions enabled, page table and page directory entries occupy
6878 bytes. Page directories occupy four frames, and page tables occupy a frame.
688
689> pteBits = (3 :: Int)
690> pdeBits = (3 :: Int)
691> pdBits = (11 :: Int) + pdeBits
692> ptBits = (9 :: Int) + pteBits
693> vcpuBits = pageBits
694
695#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */
696
697ARM page directories and page tables occupy four frames and one quarter of a frame, respectively.
698
699> pteBits = (2 :: Int)
700> pdeBits = (2 :: Int)
701> pdBits = (12 :: Int) + pdeBits
702> ptBits = (8 :: Int) + pteBits
703
704#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
705
706> pteSize :: Int
707> pteSize = bit pteBits
708> pdeSize :: Int
709> pdeSize = bit pdeBits
710
711> cacheLineBits = Platform.cacheLineBits
712> cacheLine = Platform.cacheLine
713
714#ifdef CONFIG_ARM_SMMU
715
716\subsubsection{IO Page Table Structure}
717
718> ioptBits :: Int
719> ioptBits = pageBits
720
721FIXME ARMHYP this is really platform code (TK1), move there
722
723Note that InvalidIOPDE and InvalidPTE do not exist in C, as there is no valid bit. What actually happens is that a non-read, non-write entry is considered invalid. In pracice, the kernel writes an IOPTE/IOPDE of all zeros here.
724
725> data IOPDE
726>     = InvalidIOPDE
727>     | PageTableIOPDE {
728>         iopdeFrame :: PAddr,
729>         iopdeRead :: Bool,
730>         iopdeWrite :: Bool,
731>         iopdeNonsecure :: Bool }
732>     | SectionIOPDE {
733>         iopdeFrame :: PAddr,
734>         iopdeRead :: Bool,
735>         iopdeWrite :: Bool,
736>         iopdeNonsecure :: Bool }
737>     deriving (Show, Eq)
738
739> iopteBits = 2 :: Int
740> iopdeBits = 2 :: Int
741> iopteSize = bit iopteBits :: Int
742> iopdeSize = bit iopdeBits :: Int
743
744> wordFromIOPDE :: IOPDE -> Word
745> wordFromIOPDE InvalidIOPDE = 0
746> wordFromIOPDE (PageTableIOPDE addr r w ns) = bit 28 .|.
747>         ((fromIntegral addr .&. 0xfffffc00) `shiftR` 10) .|.
748>         (if r then bit 31 else 0) .|.
749>         (if w then bit 30 else 0) .|.
750>         (if ns then bit 29 else 0)
751> wordFromIOPDE (SectionIOPDE addr r w ns) = 0 .|.
752>         ((fromIntegral addr .&. 0xffc00000) `shiftR` 12) .|.
753>         (if r then bit 31 else 0) .|.
754>         (if w then bit 30 else 0) .|.
755>         (if ns then bit 29 else 0)
756
757> data IOPTE
758>     = InvalidIOPTE
759>     | PageIOPTE {
760>         iopteFrame :: PAddr,
761>         iopteRead :: Bool,
762>         iopteWrite :: Bool,
763>         iopteNonsecure :: Bool }
764>     deriving (Show, Eq)
765
766> wordFromIOPTE :: IOPTE -> Word
767> wordFromIOPTE InvalidIOPTE = 0
768> wordFromIOPTE (PageIOPTE addr r w ns) = 0 .|.
769>         ((fromIntegral addr .&. 0xfffff000) `shiftR` 12) .|.
770>         (if r then bit 31 else 0) .|.
771>         (if w then bit 30 else 0) .|.
772>         (if ns then bit 29 else 0)
773
774#endif /* CONFIG_ARM_SMMU */
775
776#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
777
778\subsection{GIC VCPU interface}
779
780FIXME ARMHYP consider moving to platform code?
781
782> vgicIRQActive :: Word
783> vgicIRQActive = 2 `shiftL` 28
784
785> vgicIRQMask :: Word
786> vgicIRQMask = 3 `shiftL` 28
787
788> get_gic_vcpu_ctrl_hcr :: MachineMonad Word
789> get_gic_vcpu_ctrl_hcr = error "FIXME ARMHYP Unimplemented callback"
790
791> set_gic_vcpu_ctrl_hcr :: Word -> MachineMonad ()
792> set_gic_vcpu_ctrl_hcr = error "FIXME ARMHYP Unimplemented callback"
793
794> get_gic_vcpu_ctrl_vmcr :: MachineMonad Word
795> get_gic_vcpu_ctrl_vmcr = error "FIXME ARMHYP Unimplemented callback"
796
797> set_gic_vcpu_ctrl_vmcr :: Word -> MachineMonad ()
798> set_gic_vcpu_ctrl_vmcr = error "FIXME ARMHYP Unimplemented callback"
799
800> get_gic_vcpu_ctrl_apr :: MachineMonad Word
801> get_gic_vcpu_ctrl_apr = error "FIXME ARMHYP Unimplemented callback"
802
803> set_gic_vcpu_ctrl_apr :: Word -> MachineMonad ()
804> set_gic_vcpu_ctrl_apr = error "FIXME ARMHYP Unimplemented callback"
805
806> get_gic_vcpu_ctrl_vtr :: MachineMonad Word
807> get_gic_vcpu_ctrl_vtr = error "FIXME ARMHYP Unimplemented callback"
808
809> get_gic_vcpu_ctrl_eisr0 :: MachineMonad Word
810> get_gic_vcpu_ctrl_eisr0 = error "FIXME ARMHYP Unimplemented callback"
811
812> get_gic_vcpu_ctrl_eisr1 :: MachineMonad Word
813> get_gic_vcpu_ctrl_eisr1 = error "FIXME ARMHYP Unimplemented callback"
814
815> get_gic_vcpu_ctrl_misr :: MachineMonad Word
816> get_gic_vcpu_ctrl_misr = error "FIXME ARMHYP Unimplemented callback"
817
818> get_gic_vcpu_ctrl_lr :: Word -> MachineMonad Word
819> get_gic_vcpu_ctrl_lr = error "FIXME ARMHYP Unimplemented callback"
820
821> set_gic_vcpu_ctrl_lr :: Word -> Word -> MachineMonad ()
822> set_gic_vcpu_ctrl_lr = error "FIXME ARMHYP Unimplemented callback"
823
824#endif
825
826\subsection{Constants}
827
828> physBase :: PAddr
829> physBase = toPAddr Platform.physBase
830
831> kernelBase :: VPtr
832> kernelBase = Platform.kernelBase
833
834#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
835
836> hcrVCPU =  (0x87039 :: Word) -- HCR_VCPU
837> hcrNative = (0xfe8703b :: Word) -- HCR_NATIVE
838> vgicHCREN = (0x1 :: Word) -- VGIC_HCR_EN
839> sctlrDefault = (0xc5187c :: Word) -- SCTLR_DEFAULT
840> actlrDefault = (0x40 :: Word) -- ACTLR_DEFAULT
841> gicVCPUMaxNumLR = (64 :: Int)
842
843#endif
844
845