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

aarch64 haskell: eliminate isValidNativeRoot 

Define isValidVTableRoot directly as on the other architectures.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-03-07 15:42:15 +11:00
parent 6461e9223c
commit 126fdfef77
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
1 changed files with 3 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
View File

@ -461,12 +461,10 @@ isVTableRoot :: Capability -> Bool
isVTableRoot (ArchObjectCap (PageTableCap { capPTType = VSRootPT_T })) = True
isVTableRoot _ = False
-- FIXME AARCH64: name indirection kept here for sync with C; both (C and
-- Haskell) should define isValidVTableRoot directly
isValidNativeRoot :: Capability -> Bool
isValidNativeRoot cap = isVTableRoot cap && isJust (capPTMappedAddress (capCap cap))
isValidVTableRoot :: Capability -> Bool
isValidVTableRoot cap = isVTableRoot cap && isJust (capPTMappedAddress (capCap cap))
-- if isValidNativeRoot holds, return VSpace and ASID, otherwise throw error
-- if isValidVTableRoot holds, return VSpace and ASID, otherwise throw error
checkVSpaceRoot :: Capability -> Int -> KernelF SyscallError (PPtr PTE, ASID)
checkVSpaceRoot vspaceCap argNo =
case vspaceCap of
@ -476,9 +474,6 @@ checkVSpaceRoot vspaceCap argNo =
-> return (vspace, asid)
_ -> throw $ InvalidCapability argNo
isValidVTableRoot :: Capability -> Bool
isValidVTableRoot = isValidNativeRoot
checkValidIPCBuffer :: VPtr -> Capability -> KernelF SyscallError ()
checkValidIPCBuffer vptr (ArchObjectCap (FrameCap {capFIsDevice = False})) = do
when (vptr .&. mask ipcBufferSizeBits /= 0) $ throw AlignmentError