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