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