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