1% Copyright 2014, General Dynamics C4 Systems 2% 3% This software may be distributed and modified according to the terms of 4% the GNU General Public License version 2. Note that NO WARRANTY is provided. 5% See "LICENSE_GPLv2.txt" for details. 6% 7% @TAG(GD_GPL) 8% 9 10This module defines instances of "PSpaceStorable" for X64-specific kernel objects. This includes page table and page directory entries, and ASID pools. 11 12> module SEL4.Object.Instances.X64 where 13 14\begin{impdetails} 15 16> import SEL4.Machine.Hardware.X64(PTE(..), PDE(..), PDPTE(..), PML4E(..)) 17> import SEL4.Object.Structures 18> import SEL4.Model 19> import Data.Helpers 20 21\end{impdetails} 22 23> instance PSpaceStorable PDE where 24> makeObject = InvalidPDE 25> injectKO = KOArch . KOPDE 26> projectKO o = case o of 27> KOArch (KOPDE p) -> return p 28> _ -> typeError "PDE" o 29 30> instance PSpaceStorable PTE where 31> makeObject = InvalidPTE 32> injectKO = KOArch . KOPTE 33> projectKO o = case o of 34> KOArch (KOPTE p) -> return p 35> _ -> typeError "PTE" o 36 37> instance PSpaceStorable PDPTE where 38> makeObject = InvalidPDPTE 39> injectKO = KOArch . KOPDPTE 40> projectKO o = case o of 41> KOArch (KOPDPTE p) -> return p 42> _ -> typeError "PDPTE" o 43 44> instance PSpaceStorable PML4E where 45> makeObject = InvalidPML4E 46> injectKO = KOArch . KOPML4E 47> projectKO o = case o of 48> KOArch (KOPML4E p) -> return p 49> _ -> typeError "PML4E" o 50 51> instance PSpaceStorable ASIDPool where 52> makeObject = ASIDPool $ 53> funPartialArray (const Nothing) (0,1023) 54> injectKO = KOArch . KOASIDPool 55> projectKO o = case o of 56> KOArch (KOASIDPool e) -> return e 57> _ -> typeError "ASID pool" o 58 59>--instance PSpaceStorable IOPTE where 60>-- makeObject = InvalidIOPTE 61>-- injectKO = KOArch . KOIOPTE 62>-- projectKO o = case o of 63>-- KOArch (KOIOPTE p) -> return p 64>-- _ -> typeError "IOPTE" o 65 66>--instance PSpaceStorable IORTE where 67>-- makeObject = InvalidIORTE 68>-- injectKO = KOArch . KOIORTE 69>-- projectKO o = case o of 70>-- KOArch (KOIORTE p) -> return p 71>-- _ -> typeError "IORTE" o 72 73>--instance PSpaceStorable IOCTE where 74>-- makeObject = InvalidIOCTE 75>-- injectKO = KOArch . KOIOCTE 76>-- projectKO o = case o of 77>-- KOArch (KOIOCTE p) -> return p 78>-- _ -> typeError "IOCTE" o 79 80