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