adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

riscv haskell: globalPT is at maxPTLevel

This commit is contained in:
Gerwin Klein 2019-07-19 10:41:51 +10:00
parent 939201f782
commit c46a641f7f
2 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spec/haskell/src/SEL4/Kernel/VSpace/RISCV64.hs
View File

@ -39,10 +39,6 @@ import SEL4.API.Invocation.RISCV64 as ArchInv
{- Constants -} {- Constants -}
-- counting from 0, i.e. number of levels = maxPTLevel + 1 = top-level table
maxPTLevel :: Int
maxPTLevel = 2
ipcBufferSizeBits :: Int ipcBufferSizeBits :: Int
ipcBufferSizeBits = 10 ipcBufferSizeBits = 10

7
spec/haskell/src/SEL4/Model/StateData/RISCV64.hs
View File

@ -32,8 +32,13 @@ data KernelState = RISCVKernelState {
riscvKSKernelVSpace :: PPtr Word -> RISCVVSpaceRegionUse 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 :: KernelState -> PPtr PTE
riscvKSGlobalPT s = head (riscvKSGlobalPTs s 0) riscvKSGlobalPT s = head (riscvKSGlobalPTs s maxPTLevel)
newKernelState :: PAddr -> (KernelState, [PAddr]) newKernelState :: PAddr -> (KernelState, [PAddr])
newKernelState _ = error "No initial state defined for RISC-V" newKernelState _ = error "No initial state defined for RISC-V"