%
% Copyright 2014, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%

\begin{impdetails}

> {-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-}

\end{impdetails}

This module defines the low-level ARM hardware interface.

> module SEL4.Machine.Hardware.ARM where

\begin{impdetails}

> import Prelude hiding (Word)
> import SEL4.Machine.RegisterSet

> import Control.Monad.Reader
> import Data.Bits
> import Data.Word(Word8, Word32)
> import Data.Ix

\end{impdetails}

The 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.

> import qualified SEL4.Machine.RegisterSet.TARGET as ARM
> import qualified SEL4.Machine.Hardware.TARGET.Callbacks as Platform
> import qualified SEL4.Machine.Hardware.TARGET.PLATFORM as Platform

\subsection{Data Types}

The machine monad contains a platform-specific opaque pointer, used by the external simulator interface.

> type MachineData = Platform.MachineData

> type MachineMonad = ReaderT MachineData IO

> type IRQ = Platform.IRQ

> newtype HardwareASID = HardwareASID { fromHWASID :: Word8 }
>     deriving (Num, Enum, Bounded, Ord, Ix, Eq, Show)

> toPAddr = Platform.PAddr

\subsubsection{Virtual Memory}

ARM 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.

> data VMPageSize
>     = ARMSmallPage
>     | ARMLargePage
>     | ARMSection
>     | ARMSuperSection
>     deriving (Show, Eq, Ord, Enum, Bounded)

ARM virtual memory faults are handled by one of two trap handlers: one for data aborts, and one for instruction aborts.

> data VMFaultType
>     = ARMDataAbort
>     | ARMPrefetchAbort
>     deriving Show

\subsection{Hypervisor}

> data HypFaultType
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
>     = ARMVCPUFault Word32 -- HSR
#else
>     = ARMNoHypFaults
#endif
>     deriving Show

\subsubsection{Physical Memory}

The 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.

> type PAddr = Platform.PAddr

> ptrFromPAddr :: PAddr -> PPtr a
> ptrFromPAddr = Platform.ptrFromPAddr

> addrFromPPtr :: PPtr a -> PAddr
> addrFromPPtr = Platform.addrFromPPtr

> fromPAddr :: PAddr -> Word
> fromPAddr = Platform.fromPAddr

> addPAddr :: PAddr -> Word -> PAddr
> addPAddr p w = toPAddr (fromPAddr p + w)

\subsection{Hardware Access}

The 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.

> pageBits :: Int
> pageBits = 12

> pageBitsForSize :: VMPageSize -> Int
> pageBitsForSize ARMSmallPage = 12
> pageBitsForSize ARMLargePage = 16
#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
> pageBitsForSize ARMSection = 20
> pageBitsForSize ARMSuperSection = 24
#else
> pageBitsForSize ARMSection = 21
> pageBitsForSize ARMSuperSection = 25
#endif

> getMemoryRegions :: MachineMonad [(PAddr, PAddr)]
> getMemoryRegions = do
>     cpbtr <- ask
>     liftIO $ Platform.getMemoryRegions cpbtr

> getDeviceRegions :: MachineMonad [(PAddr, PAddr)]
> getDeviceRegions = do
>     cbptr <- ask
>     liftIO $ Platform.getDeviceRegions cbptr

> getKernelDevices :: MachineMonad [(PAddr, PPtr Word)]
> getKernelDevices = do
>     cbptr <- ask
>     liftIO $ Platform.getKernelDevices cbptr

> loadWord :: PPtr Word -> MachineMonad Word
> loadWord ptr = do
>     cbptr <- ask
>     liftIO $ Platform.loadWordCallback cbptr $ addrFromPPtr ptr

> storeWord :: PPtr Word -> Word -> MachineMonad ()
> storeWord ptr val = do
>     cbptr <- ask
>     liftIO $ Platform.storeWordCallback cbptr (addrFromPPtr ptr) val

> storeWordVM :: PPtr Word -> Word -> MachineMonad ()
> storeWordVM ptr val = storeWord ptr val

> pageColourBits :: Int
> pageColourBits = Platform.pageColourBits

> getActiveIRQ :: Bool -> MachineMonad (Maybe IRQ)
> getActiveIRQ _ = do
>     cbptr <- ask
>     liftIO $ Platform.getActiveIRQ cbptr

> ackInterrupt :: IRQ -> MachineMonad ()
> ackInterrupt irq = do
>     cbptr <- ask
>     liftIO $ Platform.ackInterrupt cbptr irq

> maskInterrupt :: Bool -> IRQ -> MachineMonad ()
> maskInterrupt maskI irq = do
>     cbptr <- ask
>     liftIO $ Platform.maskInterrupt cbptr maskI irq

> configureTimer :: MachineMonad IRQ
> configureTimer = do
>     cbptr <- ask
>     liftIO $ Platform.configureTimer cbptr

> initIRQController :: MachineMonad ()
> initIRQController = do
>     cbptr <- ask
>     liftIO $ Platform.initIRQController cbptr

> setIRQTrigger :: IRQ -> Bool -> MachineMonad ()
> setIRQTrigger irq trigger = error "ARM machine callback unimplemented"

> resetTimer :: MachineMonad ()
> resetTimer = do
>     cbptr <- ask
>     liftIO $ Platform.resetTimer cbptr

> debugPrint :: String -> MachineMonad ()
> debugPrint str = liftIO $ putStrLn str

> getRestartPC = getRegister (Register ARM.FaultInstruction)
> setNextPC = setRegister (Register ARM.LR_svc)

\subsection{ARM Memory Management}

There are several operations used by the ARM memory management code to access relevant hardware registers.

\subsubsection{Cleaning Memory}

This function is called before a region of user-memory is recycled.
It zeros every word to ensure that user tasks cannot access any private data
that might previously have been stored in the region and
then flushes the kernel's mapping from the virtually-indexed caches.

> clearMemory :: PPtr Word -> Int -> MachineMonad ()
> clearMemory ptr byteLength = do
>     let wordSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8
>     let ptr' = PPtr $ fromPPtr ptr
>     let ptrs = [ptr', ptr' + wordSize .. ptr' + fromIntegral byteLength - 1]
>     mapM_ (\p -> storeWord p 0) ptrs
>     cleanCacheRange_PoU (VPtr $ fromPPtr ptr)
>                         (VPtr (fromPPtr (ptr + fromIntegral byteLength - 1)))
>                         (toPAddr $ fromPPtr ptr)

This function is called before a region of memory is made user-accessible.
Though in Haskell, it is implemented as "clearMemory",
we draw the logical distinction to gain more freedom for its interpretation
in the Isabelle formalization.

> initMemory :: PPtr Word -> Int -> MachineMonad ()
> initMemory = clearMemory

This function is called to free a region of user-memory after use.
In Haskell, this operation does not do anything.
We just use it as a stub for the Isabelle formalization.

> freeMemory :: PPtr Word -> Int -> MachineMonad ()
> freeMemory _ _ = return ()

Same as "clearMemory", but uses storeWordVM to write to memory.
To be used when creating mapping objects (page tables and -dirs)
Flushing the kernel's mapping from the virtually-indexed
caches must be done separately.

> clearMemoryVM :: PPtr Word -> Int -> MachineMonad ()
> clearMemoryVM ptr bits = do
>     let wordSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8
>     let ptr' = PPtr $ fromPPtr ptr
>     let ptrs = [ptr', ptr' + wordSize .. ptr' + 1 `shiftL` bits - 1]
>     mapM_ (\p -> storeWordVM p 0) ptrs

\subsubsection{Address Space Setup}

> writeTTBR0 :: Word -> MachineMonad ()
> writeTTBR0 w = do
>     cbptr <- ask
>     liftIO $ Platform.writeTTBR0 cbptr w

> writeTTBR0Ptr :: PAddr -> MachineMonad ()
> writeTTBR0Ptr pd = writeTTBR0 ((fromPAddr pd .&. 0xffffe000) .|. 0x18)

> setCurrentPD :: PAddr -> MachineMonad ()
> setCurrentPD pd = do
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
>     setCurrentPDPL2 pd
#else
>     dsb
>     writeTTBR0Ptr pd
>     isb
#endif

> setHardwareASID :: HardwareASID -> MachineMonad ()
> setHardwareASID (HardwareASID hw_asid) = do
>     cbptr <- ask
>     liftIO $ Platform.setHardwareASID cbptr hw_asid

#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

> setCurrentPDPL2 :: PAddr -> MachineMonad ()
> setCurrentPDPL2 = error "FIXME ARMHYP machine callback unimplemented"

> writeContextIDAndPD :: HardwareASID -> PAddr -> MachineMonad ()
> writeContextIDAndPD = error "FIXME ARMHYP  machine callback unimplemented"

#endif

\subsubsection{Memory Barriers}

> isb :: MachineMonad ()
> isb = do
>     cbptr <- ask
>     liftIO $ Platform.isbCallback cbptr

> dsb :: MachineMonad ()
> dsb = do
>     cbptr <- ask
>     liftIO $ Platform.dsbCallback cbptr

> dmb :: MachineMonad ()
> dmb = do
>     cbptr <- ask
>     liftIO $ Platform.dmbCallback cbptr

\subsubsection{Cache Cleaning and TLB Flushes}

> invalidateLocalTLB :: MachineMonad ()
> invalidateLocalTLB = do
>     cbptr <- ask
>     liftIO $ Platform.invalidateLocalTLBCallback cbptr

> invalidateLocalTLB_ASID :: HardwareASID -> MachineMonad ()
> invalidateLocalTLB_ASID (HardwareASID hw_asid) = do
>     cbptr <- ask
>     liftIO $ Platform.invalidateLocalTLB_ASIDCallback cbptr hw_asid

> invalidateLocalTLB_VAASID :: Word -> MachineMonad ()
> invalidateLocalTLB_VAASID mva_plus_asid = do
>     cbptr <- ask
>     liftIO $ Platform.invalidateLocalTLB_VAASIDCallback cbptr mva_plus_asid

> cleanByVA :: VPtr -> PAddr -> MachineMonad ()
> cleanByVA mva pa = do
>     cbptr <- ask
>     liftIO $ Platform.cacheCleanByVACallback cbptr mva pa

> cleanByVA_PoU :: VPtr -> PAddr -> MachineMonad ()
> cleanByVA_PoU mva pa = do
>     cbptr <- ask
>     liftIO $ Platform.cacheCleanByVA_PoUCallback cbptr mva pa

> invalidateByVA :: VPtr -> PAddr -> MachineMonad ()
> invalidateByVA mva pa = do
>     cbptr <- ask
>     liftIO $ Platform.cacheInvalidateByVACallback cbptr mva pa

> invalidateByVA_I :: VPtr -> PAddr -> MachineMonad ()
> invalidateByVA_I mva pa = do
>     cbptr <- ask
>     liftIO $ Platform.cacheInvalidateByVA_ICallback cbptr mva pa

> invalidate_I_PoU :: MachineMonad ()
> invalidate_I_PoU = do
>     cbptr <- ask
>     liftIO $ Platform.cacheInvalidate_I_PoUCallback cbptr

> cleanInvalByVA :: VPtr -> PAddr -> MachineMonad ()
> cleanInvalByVA mva pa = do
>     cbptr <- ask
>     liftIO $ Platform.cacheCleanInvalidateByVACallback cbptr mva pa

> branchFlush :: VPtr -> PAddr -> MachineMonad ()
> branchFlush mva pa = do
>     cbptr <- ask
>     liftIO $ Platform.branchFlushCallback cbptr mva pa

> clean_D_PoU :: MachineMonad ()
> clean_D_PoU = do
>     cbptr <- ask
>     liftIO $ Platform.cacheClean_D_PoUCallback cbptr

> cleanInvalidate_D_PoC :: MachineMonad ()
> cleanInvalidate_D_PoC = do
>     cbptr <- ask
>     liftIO $ Platform.cacheCleanInvalidate_D_PoCCallback cbptr

> cleanInvalidate_D_PoU :: MachineMonad ()
> cleanInvalidate_D_PoU = do
>     cbptr <- ask
>     liftIO $ Platform.cacheCleanInvalidate_D_PoUCallback cbptr

> cleanInvalidateL2Range :: PAddr -> PAddr -> MachineMonad ()
> cleanInvalidateL2Range start end = do
>     cbptr <- ask
>     liftIO $ Platform.cacheCleanInvalidateL2RangeCallback cbptr start end

> invalidateL2Range :: PAddr -> PAddr -> MachineMonad ()
> invalidateL2Range start end = do
>     cbptr <- ask
>     liftIO $ Platform.cacheInvalidateL2RangeCallback cbptr start end

> cleanL2Range :: PAddr -> PAddr -> MachineMonad ()
> cleanL2Range start end = do
>     cbptr <- ask
>     liftIO $ Platform.cacheCleanL2RangeCallback cbptr start end

> lineStart addr = (addr `shiftR` cacheLineBits) `shiftL` cacheLineBits

Performs the given operation on every cache line that intersects the
supplied range.

> cacheRangeOp :: (VPtr -> PAddr -> MachineMonad ()) ->
>                 VPtr -> VPtr -> PAddr -> MachineMonad ()
> cacheRangeOp operation vstart vend pstart = do
>     let pend = pstart + (toPAddr $ fromVPtr (vend - vstart))
>     let vptrs = [lineStart vstart, lineStart vstart + fromIntegral cacheLine .. lineStart vend]
>     let pptrs = [lineStart pstart, lineStart pstart + fromIntegral cacheLine .. lineStart pend]
>     mapM_ (\(v,p) -> operation v p) (zip vptrs pptrs)

> cleanCacheRange_PoC :: VPtr -> VPtr -> PAddr -> MachineMonad ()
> cleanCacheRange_PoC vstart vend pstart =
>     cacheRangeOp cleanByVA vstart vend pstart

> cleanInvalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
> cleanInvalidateCacheRange_RAM vstart vend pstart = do
>     cleanCacheRange_PoC vstart vend pstart
>     dsb
>     cleanInvalidateL2Range pstart (pstart + (toPAddr $ fromVPtr $ vend - vstart))
>     cacheRangeOp cleanInvalByVA vstart vend pstart
>     dsb

> cleanCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
> cleanCacheRange_RAM vstart vend pstart = do
>     cleanCacheRange_PoC vstart vend pstart
>     dsb
>     cleanL2Range pstart (pstart + (toPAddr $ fromVPtr $ vend - vstart))

> cleanCacheRange_PoU :: VPtr -> VPtr -> PAddr -> MachineMonad ()
> cleanCacheRange_PoU vstart vend pstart =
>     cacheRangeOp cleanByVA_PoU vstart vend pstart

> invalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
> invalidateCacheRange_RAM vstart vend pstart = do
>     when (vstart /= lineStart vstart) $
>         cleanCacheRange_RAM vstart vstart pstart
>     when (vend + 1 /= lineStart (vend + 1)) $
>         cleanCacheRange_RAM (lineStart vend) (lineStart vend)
>             (pstart + (toPAddr $ fromVPtr $ lineStart vend - vstart))
>     invalidateL2Range pstart
>         (pstart + (toPAddr $ fromVPtr $ vend - vstart))
>     cacheRangeOp invalidateByVA vstart vend pstart
>     dsb

> invalidateCacheRange_I :: VPtr -> VPtr -> PAddr -> MachineMonad ()
> invalidateCacheRange_I vstart vend pstart =
>     cacheRangeOp invalidateByVA_I vstart vend pstart

> branchFlushRange :: VPtr -> VPtr -> PAddr -> MachineMonad ()
> branchFlushRange vstart vend pstart =
>     cacheRangeOp branchFlush vstart vend pstart

> cleanCaches_PoU :: MachineMonad ()
> cleanCaches_PoU = do
>     dsb
>     clean_D_PoU
>     dsb
>     invalidate_I_PoU
>     dsb

> cleanInvalidateL1Caches :: MachineMonad ()
> cleanInvalidateL1Caches = do
>     dsb
>     cleanInvalidate_D_PoC
>     dsb
>     invalidate_I_PoU
>     dsb

This function is used to clear the load exclusive monitor. This dummy
implementation assumes the monitor is not modelled in our simulator.

> clearExMonitor :: MachineMonad ()
> clearExMonitor = return ()

\subsubsection{Fault Status Registers}

> getIFSR :: MachineMonad Word
> getIFSR = do
>     cbptr <- ask
>     liftIO $ Platform.getIFSR cbptr

> getDFSR :: MachineMonad Word
> getDFSR = do
>     cbptr <- ask
>     liftIO $ Platform.getDFSR cbptr

> getFAR :: MachineMonad VPtr
> getFAR = do
>     cbptr <- ask
>     liftIO $ Platform.getFAR cbptr

#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

\subsection{Hypervisor-specific status/control registers}

> getHSR :: MachineMonad Word
> getHSR = error "FIXME ARMHYP machine callback unimplemented"

> setHCR :: Word -> MachineMonad ()
> setHCR _hcr = error "FIXME ARMHYP machine callback unimplemented"

> getHDFAR :: MachineMonad VPtr
> getHDFAR = error "FIXME ARMHYP machine callback unimplemented"

> addressTranslateS1CPR :: VPtr -> MachineMonad VPtr
> addressTranslateS1CPR = error "FIXME ARMHYP machine callback unimplemented"

> getSCTLR :: MachineMonad Word
> getSCTLR = error "FIXME ARMHYP machine callback unimplemented"

> setSCTLR :: Word -> MachineMonad ()
> setSCTLR _sctlr = error "FIXME ARMHYP machine callback unimplemented"

\subsection{Hypervisor banked registers}

Rather than a line-for-line copy of every hypervisor register storage and
retrieval function from the C code, we abstract the concept into one function
each. Some special registers, like SCTLR, still get their own load/store
functions due to being operated on separately.

> readVCPUHardwareReg :: ARM.VCPUReg -> MachineMonad Word
> readVCPUHardwareReg reg = error "FIXME ARMHYP machine callback unimplemented"

> writeVCPUHardwareReg :: ARM.VCPUReg -> Word -> MachineMonad ()
> writeVCPUHardwareReg reg val = error "FIXME ARMHYP machine callback unimplemented"

#endif

\subsubsection{Page Table Structure}

The 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.

#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT

The 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.

> data PDE
>     = InvalidPDE
>     | PageTablePDE {
>         pdeTable :: PAddr,
>         pdeParity :: Bool,
>         pdeDomain :: Word }
>     | SectionPDE {
>         pdeFrame :: PAddr,
>         pdeParity :: Bool,
>         pdeDomain :: Word,
>         pdeCacheable :: Bool,
>         pdeGlobal :: Bool,
>         pdeExecuteNever :: Bool,
>         pdeRights :: VMRights }
>     | SuperSectionPDE {
>         pdeFrame :: PAddr,
>         pdeParity :: Bool,
>         pdeCacheable :: Bool,
>         pdeGlobal :: Bool,
>         pdeExecuteNever :: Bool,
>         pdeRights :: VMRights }
>     deriving (Show, Eq)

> wordFromPDE :: PDE -> Word
> wordFromPDE InvalidPDE = 0
> wordFromPDE (PageTablePDE table parity domain) = 1 .|.
>     (fromIntegral table .&. 0xfffffc00) .|.
>     (if parity then bit 9 else 0) .|.
>     ((domain .&. 0xf) `shiftL` 5)
> wordFromPDE (SectionPDE frame parity domain cacheable global xn rights) = 2 .|.
>     (fromIntegral frame .&. 0xfff00000) .|.
>     (if parity then bit 9 else 0) .|.
>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
>     (if xn then bit 4 else 0) .|.
>     ((domain .&. 0xf) `shiftL` 5) .|.
>     (if global then 0 else bit 17) .|.
>     (fromIntegral $ fromEnum rights `shiftL` 10)
> wordFromPDE (SuperSectionPDE frame parity cacheable global xn rights) = 2 .|.
>     bit 18 .|.
>     (fromIntegral frame .&. 0xff000000) .|.
>     (if parity then bit 9 else 0) .|.
>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
>     (if xn then bit 4 else 0) .|.
>     (if global then 0 else bit 17) .|.
>     (fromIntegral $ fromEnum rights `shiftL` 10)

> data PTE
>     = InvalidPTE
>     | LargePagePTE {
>         pteFrame :: PAddr,
>         pteCacheable :: Bool,
>         pteGlobal :: Bool,
>         pteExecuteNever :: Bool,
>         pteRights :: VMRights }
>     | SmallPagePTE {
>         pteFrame :: PAddr,
>         pteCacheable :: Bool,
>         pteGlobal :: Bool,
>         pteExecuteNever :: Bool,
>         pteRights :: VMRights }
>     deriving (Show, Eq)

> wordFromPTE :: PTE -> Word
> wordFromPTE InvalidPTE = 0
> wordFromPTE (LargePagePTE frame cacheable global xn rights) = 1 .|.
>     (fromIntegral frame .&. 0xffff0000) .|.
>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
>     (if global then 0 else bit 11) .|.
>     (if xn then bit 15 else 0) .|.
>     (fromIntegral $ fromEnum rights `shiftL` 4)
> wordFromPTE (SmallPagePTE frame cacheable global xn rights) = 2 .|.
>     (fromIntegral frame .&. 0xfffff000) .|.
>     (if xn then 1 else 0) .|.
>     (if cacheable then bit 2 .|. bit 3 else 0) .|.
>     (if global then 0 else bit 11) .|.
>     (fromIntegral $ fromEnum rights `shiftL` 4)

#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */

Hypervisor extensions use long page table descriptors (64-bit) for the stage 2
translation (host-to-hypervisor). This is a three-level table system, but the
hardware can be configured to omit the first level entirely if all second
levels are stored contiguously. We use this configuration to preserve the usual
page table/directory nomenclature.

> -- FIXME ARMHYP global (SH) is never used so I don't know what a global page's SH would look like

seL4 does not use hardware domains or parity on ARM hypervisor systems.

> data PDE
>     = InvalidPDE
>     | PageTablePDE {
>         pdeTable :: PAddr }
>     | SectionPDE {
>         pdeFrame :: PAddr,
>         pdeCacheable :: Bool,
>         pdeExecuteNever :: Bool,
>         pdeRights :: VMRights }
>     | SuperSectionPDE {
>         pdeFrame :: PAddr,
>         pdeCacheable :: Bool,
>         pdeExecuteNever :: Bool,
>         pdeRights :: VMRights }
>     deriving (Show, Eq)

> hapFromVMRights :: VMRights -> Word
> hapFromVMRights VMKernelOnly = 0
> hapFromVMRights VMNoAccess = 0
> hapFromVMRights VMReadOnly = 1
> hapFromVMRights VMReadWrite = 3

> wordsFromPDE :: PDE -> [Word]
> wordsFromPDE InvalidPDE = [0, 0]
> wordsFromPDE (PageTablePDE table) = [w0, 0]
>     where w0 = 3 .|. (fromIntegral table .&. 0xfffff000)
> wordsFromPDE (SectionPDE frame cacheable xn rights) = [w0, w1]
>     where w1 = 0 .|. (if xn then bit 22 else 0) -- no contig. hint
>           w0 = 1 .|.
>                (fromIntegral frame .&. 0xfffff000) .|.
>                bit 10 .|. -- AF
>                (hapFromVMRights rights `shiftL` 6) .|.
>                (if cacheable then 0xf `shiftL` 2 else 0)
> wordsFromPDE (SuperSectionPDE frame cacheable xn rights) = [w0, w1]
>     where w1 = 0 .|. (if xn then bit 22 else 0) .|. bit 20 -- contig. hint
>           w0 = 1 .|.
>                (fromIntegral frame .&. 0xfffff000) .|.
>                bit 10 .|. -- AF
>                (hapFromVMRights rights `shiftL` 6) .|.
>                (if cacheable then 0xf `shiftL` 2 else 0)

> data PTE
>     = InvalidPTE
>     | LargePagePTE {
>         pteFrame :: PAddr,
>         pteCacheable :: Bool,
>         pteExecuteNever :: Bool,
>         pteRights :: VMRights }
>     | SmallPagePTE {
>         pteFrame :: PAddr,
>         pteCacheable :: Bool,
>         pteExecuteNever :: Bool,
>         pteRights :: VMRights }
>     deriving (Show, Eq)

> wordsFromPTE :: PTE -> [Word]
> wordsFromPTE InvalidPTE = [0, 0]
> wordsFromPTE (SmallPagePTE frame cacheable xn rights) = [w0, w1]
>     where w1 = 0 .|. (if xn then bit 22 else 0) .|. bit 20 -- contig. hint
>           w0 = 3 .|.
>                (fromIntegral frame .&. 0xfffff000) .|.
>                bit 10 .|. -- AF
>                (hapFromVMRights rights `shiftL` 6) .|.
>                (if cacheable then 0xf `shiftL` 2 else 0)
> wordsFromPTE (LargePagePTE frame cacheable xn rights) = [w0, w1]
>     where w1 = 0 .|. (if xn then bit 22 else 0) -- no contig. hint
>           w0 = 3 .|.
>                (fromIntegral frame .&. 0xfffff000) .|.
>                bit 10 .|. -- AF
>                (hapFromVMRights rights `shiftL` 6) .|.
>                (if cacheable then 0xf `shiftL` 2 else 0)

#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */

> data VMRights
>     = VMNoAccess
>     | VMKernelOnly
>     | VMReadOnly
>     | VMReadWrite
>     deriving (Show, Eq, Enum)

> data VMAttributes = VMAttributes {
>     armPageCacheable, armParityEnabled, armExecuteNever :: Bool }

Convenient references to size and log of size of PDEs and PTEs.

#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

With hypervisor extensions enabled, page table and page directory entries occupy
8 bytes. Page directories occupy four frames, and page tables occupy a frame.

> pteBits = (3 :: Int)
> pdeBits = (3 :: Int)
> pdBits = (11 :: Int) + pdeBits
> ptBits = (9 :: Int) + pteBits
> vcpuBits = pageBits

#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */

ARM page directories and page tables occupy four frames and one quarter of a frame, respectively.

> pteBits = (2 :: Int)
> pdeBits = (2 :: Int)
> pdBits = (12 :: Int) + pdeBits
> ptBits = (8 :: Int) + pteBits

#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */

> pteSize :: Int
> pteSize = bit pteBits
> pdeSize :: Int
> pdeSize = bit pdeBits

> cacheLineBits = Platform.cacheLineBits
> cacheLine = Platform.cacheLine

#ifdef CONFIG_ARM_SMMU

\subsubsection{IO Page Table Structure}

> ioptBits :: Int
> ioptBits = pageBits

FIXME ARMHYP this is really platform code (TK1), move there

Note 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.

> data IOPDE
>     = InvalidIOPDE
>     | PageTableIOPDE {
>         iopdeFrame :: PAddr,
>         iopdeRead :: Bool,
>         iopdeWrite :: Bool,
>         iopdeNonsecure :: Bool }
>     | SectionIOPDE {
>         iopdeFrame :: PAddr,
>         iopdeRead :: Bool,
>         iopdeWrite :: Bool,
>         iopdeNonsecure :: Bool }
>     deriving (Show, Eq)

> iopteBits = 2 :: Int
> iopdeBits = 2 :: Int
> iopteSize = bit iopteBits :: Int
> iopdeSize = bit iopdeBits :: Int

> wordFromIOPDE :: IOPDE -> Word
> wordFromIOPDE InvalidIOPDE = 0
> wordFromIOPDE (PageTableIOPDE addr r w ns) = bit 28 .|.
>         ((fromIntegral addr .&. 0xfffffc00) `shiftR` 10) .|.
>         (if r then bit 31 else 0) .|.
>         (if w then bit 30 else 0) .|.
>         (if ns then bit 29 else 0)
> wordFromIOPDE (SectionIOPDE addr r w ns) = 0 .|.
>         ((fromIntegral addr .&. 0xffc00000) `shiftR` 12) .|.
>         (if r then bit 31 else 0) .|.
>         (if w then bit 30 else 0) .|.
>         (if ns then bit 29 else 0)

> data IOPTE
>     = InvalidIOPTE
>     | PageIOPTE {
>         iopteFrame :: PAddr,
>         iopteRead :: Bool,
>         iopteWrite :: Bool,
>         iopteNonsecure :: Bool }
>     deriving (Show, Eq)

> wordFromIOPTE :: IOPTE -> Word
> wordFromIOPTE InvalidIOPTE = 0
> wordFromIOPTE (PageIOPTE addr r w ns) = 0 .|.
>         ((fromIntegral addr .&. 0xfffff000) `shiftR` 12) .|.
>         (if r then bit 31 else 0) .|.
>         (if w then bit 30 else 0) .|.
>         (if ns then bit 29 else 0)

#endif /* CONFIG_ARM_SMMU */

#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

\subsection{GIC VCPU interface}

FIXME ARMHYP consider moving to platform code?

> vgicIRQActive :: Word
> vgicIRQActive = 2 `shiftL` 28

> vgicIRQMask :: Word
> vgicIRQMask = 3 `shiftL` 28

> get_gic_vcpu_ctrl_hcr :: MachineMonad Word
> get_gic_vcpu_ctrl_hcr = error "FIXME ARMHYP Unimplemented callback"

> set_gic_vcpu_ctrl_hcr :: Word -> MachineMonad ()
> set_gic_vcpu_ctrl_hcr = error "FIXME ARMHYP Unimplemented callback"

> get_gic_vcpu_ctrl_vmcr :: MachineMonad Word
> get_gic_vcpu_ctrl_vmcr = error "FIXME ARMHYP Unimplemented callback"

> set_gic_vcpu_ctrl_vmcr :: Word -> MachineMonad ()
> set_gic_vcpu_ctrl_vmcr = error "FIXME ARMHYP Unimplemented callback"

> get_gic_vcpu_ctrl_apr :: MachineMonad Word
> get_gic_vcpu_ctrl_apr = error "FIXME ARMHYP Unimplemented callback"

> set_gic_vcpu_ctrl_apr :: Word -> MachineMonad ()
> set_gic_vcpu_ctrl_apr = error "FIXME ARMHYP Unimplemented callback"

> get_gic_vcpu_ctrl_vtr :: MachineMonad Word
> get_gic_vcpu_ctrl_vtr = error "FIXME ARMHYP Unimplemented callback"

> get_gic_vcpu_ctrl_eisr0 :: MachineMonad Word
> get_gic_vcpu_ctrl_eisr0 = error "FIXME ARMHYP Unimplemented callback"

> get_gic_vcpu_ctrl_eisr1 :: MachineMonad Word
> get_gic_vcpu_ctrl_eisr1 = error "FIXME ARMHYP Unimplemented callback"

> get_gic_vcpu_ctrl_misr :: MachineMonad Word
> get_gic_vcpu_ctrl_misr = error "FIXME ARMHYP Unimplemented callback"

> get_gic_vcpu_ctrl_lr :: Word -> MachineMonad Word
> get_gic_vcpu_ctrl_lr = error "FIXME ARMHYP Unimplemented callback"

> set_gic_vcpu_ctrl_lr :: Word -> Word -> MachineMonad ()
> set_gic_vcpu_ctrl_lr = error "FIXME ARMHYP Unimplemented callback"

#endif

\subsection{Constants}

> physBase :: PAddr
> physBase = toPAddr Platform.physBase

> kernelBase :: VPtr
> kernelBase = Platform.kernelBase

#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

> hcrVCPU =  (0x87039 :: Word) -- HCR_VCPU
> hcrNative = (0xfe8703b :: Word) -- HCR_NATIVE
> vgicHCREN = (0x1 :: Word) -- VGIC_HCR_EN
> sctlrDefault = (0xc5187c :: Word) -- SCTLR_DEFAULT
> actlrDefault = (0x40 :: Word) -- ACTLR_DEFAULT
> gicVCPUMaxNumLR = (64 :: Int)

#endif