From c46a641f7fb638b096c4407548988b9c99546058 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 19 Jul 2019 10:41:51 +1000 Subject: [PATCH] riscv haskell: globalPT is at maxPTLevel --- spec/haskell/src/SEL4/Kernel/VSpace/RISCV64.hs | 4 ---- spec/haskell/src/SEL4/Model/StateData/RISCV64.hs | 7 ++++++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/spec/haskell/src/SEL4/Kernel/VSpace/RISCV64.hs b/spec/haskell/src/SEL4/Kernel/VSpace/RISCV64.hs index 8155b22d3..054371966 100644 --- a/spec/haskell/src/SEL4/Kernel/VSpace/RISCV64.hs +++ b/spec/haskell/src/SEL4/Kernel/VSpace/RISCV64.hs @@ -39,10 +39,6 @@ import SEL4.API.Invocation.RISCV64 as ArchInv {- Constants -} --- counting from 0, i.e. number of levels = maxPTLevel + 1 = top-level table -maxPTLevel :: Int -maxPTLevel = 2 - ipcBufferSizeBits :: Int ipcBufferSizeBits = 10 diff --git a/spec/haskell/src/SEL4/Model/StateData/RISCV64.hs b/spec/haskell/src/SEL4/Model/StateData/RISCV64.hs index 782ecf31f..242c4df13 100644 --- a/spec/haskell/src/SEL4/Model/StateData/RISCV64.hs +++ b/spec/haskell/src/SEL4/Model/StateData/RISCV64.hs @@ -32,8 +32,13 @@ data KernelState = RISCVKernelState { riscvKSKernelVSpace :: PPtr Word -> RISCVVSpaceRegionUse } +-- counting from 0 at bottom, i.e. number of levels = maxPTLevel + 1; +-- maxPTLevel = level of top-level root table +maxPTLevel :: Int +maxPTLevel = 2 + riscvKSGlobalPT :: KernelState -> PPtr PTE -riscvKSGlobalPT s = head (riscvKSGlobalPTs s 0) +riscvKSGlobalPT s = head (riscvKSGlobalPTs s maxPTLevel) newKernelState :: PAddr -> (KernelState, [PAddr]) newKernelState _ = error "No initial state defined for RISC-V"