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 contains the architecture-specific kernel global data for the 10-- RISCV 64bit architecture. 11 12module SEL4.Model.StateData.RISCV64 where 13 14import SEL4.Machine 15import SEL4.Machine.Hardware.RISCV64 (PTE(..)) 16import SEL4.Object.Structures.RISCV64 17 18import Data.Array 19 20-- used in proofs only 21data RISCVVSpaceRegionUse 22 = RISCVVSpaceUserRegion 23 | RISCVVSpaceInvalidRegion 24 | RISCVVSpaceKernelWindow 25 | RISCVVSpaceDeviceWindow 26 27data KernelState = RISCVKernelState { 28 riscvKSASIDTable :: Array ASID (Maybe (PPtr ASIDPool)), 29 riscvKSGlobalPT :: PPtr PTE } 30 31newKernelState :: PAddr -> (KernelState, [PAddr]) 32newKernelState _ = error "No initial state defined for RISC-V" 33