1-- Copyright 2018, Data61, CSIRO
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(DATA61_GPL)
8
9-- This module defines instances of "PSpaceStorable" for architecture-specific
10-- kernel objects. This includes page table and page directory entries, and
11-- ASID pools.
12
13module SEL4.Object.Instances.RISCV64 where
14
15import SEL4.Machine.Hardware.RISCV64(PTE(..))
16import SEL4.Object.Structures
17import SEL4.Model
18import Data.Helpers
19import Data.Bits
20
21instance PSpaceStorable PTE where
22    makeObject = InvalidPTE
23    injectKO = KOArch . KOPTE
24    projectKO o = case o of
25                KOArch (KOPTE p) -> return p
26                _ -> typeError "PTE" o
27
28instance PSpaceStorable ASIDPool where
29    makeObject = ASIDPool $
30        funPartialArray (const Nothing) (0,bit asidLowBits - 1)
31    injectKO = KOArch . KOASIDPool
32    projectKO o = case o of
33        KOArch (KOASIDPool e) -> return e
34        _ -> typeError "ASID pool" o
35