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, EmptyDataDecls, GeneralizedNewtypeDeriving #-} 14 15\end{impdetails} 16 17This module defines instances of "PSpaceStorable" for ARM-specific kernel objects. This includes page table and page directory entries, and ASID pools. 18 19> module SEL4.Object.Instances.ARM where 20 21\begin{impdetails} 22 23> import SEL4.Machine.Hardware.ARM(PTE(..), PDE(..)) 24> import SEL4.Object.Structures 25> import SEL4.Model 26> import Data.Helpers 27#ifdef CONFIG_ARM_SMMU 28> import SEL4.Machine.Hardware.ARM(IOPTE(..), IOPDE(..)) 29#endif 30 31\end{impdetails} 32 33> instance PSpaceStorable PDE where 34> makeObject = InvalidPDE 35> injectKO = KOArch . KOPDE 36> projectKO o = case o of 37> KOArch (KOPDE p) -> return p 38> _ -> typeError "PDE" o 39 40> instance PSpaceStorable PTE where 41> makeObject = InvalidPTE 42> injectKO = KOArch . KOPTE 43> projectKO o = case o of 44> KOArch (KOPTE p) -> return p 45> _ -> typeError "PTE" o 46 47#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 48> instance PSpaceStorable VCPU where 49> makeObject = makeVCPUObject 50> injectKO = KOArch . KOVCPU 51> projectKO o = case o of 52> KOArch (KOVCPU p) -> return p 53> _ -> typeError "VCPU" o 54#endif 55 56#ifdef CONFIG_ARM_SMMU 57> instance PSpaceStorable IOPDE where 58> makeObject = InvalidIOPDE 59> injectKO = KOArch . KOIOPDE 60> projectKO o = case o of 61> KOArch (KOIOPDE p) -> return p 62> _ -> typeError "IOPDE" o 63 64> instance PSpaceStorable IOPTE where 65> makeObject = InvalidIOPTE 66> injectKO = KOArch . KOIOPTE 67> projectKO o = case o of 68> KOArch (KOIOPTE p) -> return p 69> _ -> typeError "IOPTE" o 70#endif 71 72> instance PSpaceStorable ASIDPool where 73> makeObject = ASIDPool $ 74> funPartialArray (const Nothing) (0,1023) 75> injectKO = KOArch . KOASIDPool 76> projectKO o = case o of 77> KOArch (KOASIDPool e) -> return e 78> _ -> typeError "ASID pool" o 79 80