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

riscv haskell: update PageMap to replace PageRemap (SELFOUR-161)

This commit is contained in:
Victor Phan 2019-09-26 12:14:30 +10:00
parent f284a0cb0e
commit 5d22c1d329
3 changed files with 6 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/haskell/src/SEL4/API/Invocation/RISCV64.hs
View File

@ -45,8 +45,6 @@ data PageTableInvocation
data PageInvocation
= PageGetAddr {
pageGetBasePtr :: PPtr Word }
| PageRemap {
pageRemapEntries :: (PTE, PPtr PTE) }
| PageMap {
pageMapCap :: Capability,
pageMapCTSlot :: PPtr CTE,

1
spec/haskell/src/SEL4/API/InvocationLabels/RISCV64.hs
View File

@ -16,7 +16,6 @@ data ArchInvocationLabel
= RISCVPageTableMap
| RISCVPageTableUnmap
| RISCVPageMap
| RISCVPageRemap
| RISCVPageUnmap
| RISCVPageGetAddress
| RISCVASIDControlMakePool

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

@ -328,7 +328,6 @@ checkSlot slot test = do
decodeRISCVFrameInvocationMap :: PPtr CTE -> ArchCapability -> VPtr -> Word ->
Word -> Capability -> KernelF SyscallError ArchInv.Invocation
decodeRISCVFrameInvocationMap cte cap vptr rightsMask attr vspaceCap = do
when (isJust $ capFMappedAddress cap) $ throw $ InvalidCapability 0
(vspace,asid) <- case vspaceCap of
ArchObjectCap (PageTableCap {
capPTMappedAddress = Just (asid, _),
@ -344,7 +343,12 @@ decodeRISCVFrameInvocationMap cte cap vptr rightsMask attr vspaceCap = do
(bitsLeft, slot) <- withoutFailure $ lookupPTSlot vspace vptr
unless (bitsLeft == pgBits) $ throw $
FailedLookup False $ MissingCapability bitsLeft
checkSlot slot (\pte -> pte == InvalidPTE)
case capFMappedAddress cap of
Just (asid', vaddr') -> do
when (asid' /= asid) $ throw $ InvalidCapability 1
when (vaddr' /= vptr) $ throw $ InvalidArgument 0
checkSlot slot (not . isPageTablePTE)
Nothing -> checkSlot slot (\pte -> pte == InvalidPTE)
let vmRights = maskVMRights (capFVMRights cap) $ rightsFromWord rightsMask
let framePAddr = addrFromPPtr (capFBasePtr cap)
let exec = not $ riscvExecuteNever (attribsFromWord attr)
@ -353,33 +357,6 @@ decodeRISCVFrameInvocationMap cte cap vptr rightsMask attr vspaceCap = do
pageMapCTSlot = cte,
pageMapEntries = (makeUserPTE framePAddr exec vmRights, slot) }
decodeRISCVFrameInvocationRemap :: PPtr CTE -> ArchCapability -> Word ->
Word -> Capability -> KernelF SyscallError ArchInv.Invocation
decodeRISCVFrameInvocationRemap cte cap rightsMask attr vspaceCap = do
(vspace,asid) <- case vspaceCap of
ArchObjectCap (PageTableCap {
capPTMappedAddress = Just (asid, _),
capPTBasePtr = vspace })
-> return (vspace, asid)
_ -> throw $ InvalidCapability 1
(asid',vaddr) <- case capFMappedAddress cap of
Just v -> return v
_ -> throw $ InvalidCapability 0
vspaceCheck <- lookupErrorOnFailure False $ findVSpaceForASID asid
when (vspaceCheck /= vspace || asid /= asid') $ throw $ InvalidCapability 1
checkVPAlignment (capFSize cap) vaddr
(bitsLeft, slot) <- withoutFailure $ lookupPTSlot vspace vaddr
let pgBits = pageBitsForSize $ capFSize cap
unless (bitsLeft == pgBits) $ throw $
FailedLookup False $ MissingCapability bitsLeft
checkSlot slot (not . isPageTablePTE)
let vmRights = maskVMRights (capFVMRights cap) $ rightsFromWord rightsMask
let framePAddr = addrFromPPtr (capFBasePtr cap)
let exec = not $ riscvExecuteNever (attribsFromWord attr)
return $ InvokePage $ PageRemap {
pageRemapEntries = (makeUserPTE framePAddr exec vmRights, slot) }
decodeRISCVFrameInvocation :: Word -> [Word] -> PPtr CTE ->
ArchCapability -> [(Capability, PPtr CTE)] ->
KernelF SyscallError ArchInv.Invocation
@ -389,9 +366,6 @@ decodeRISCVFrameInvocation label args cte (cap@FrameCap {}) extraCaps =
(ArchInvocationLabel RISCVPageMap, vaddr:rightsMask:attr:_, (vspaceCap,_):_) -> do
decodeRISCVFrameInvocationMap cte cap (VPtr vaddr) rightsMask attr vspaceCap
(ArchInvocationLabel RISCVPageMap, _, _) -> throw TruncatedMessage
(ArchInvocationLabel RISCVPageRemap, rightsMask:attr:_, (vspaceCap,_):_) -> do
decodeRISCVFrameInvocationRemap cte cap rightsMask attr vspaceCap
(ArchInvocationLabel RISCVPageRemap, _, _) -> throw TruncatedMessage
(ArchInvocationLabel RISCVPageUnmap, _, _) ->
return $ InvokePage $ PageUnmap {
pageUnmapCap = cap,
@ -547,10 +521,6 @@ performPageInvocation (PageMap cap ctSlot (pte,slot)) = do
storePTE slot pte
doMachineOp sfence
performPageInvocation (PageRemap (pte,slot)) = do
storePTE slot pte
doMachineOp sfence
performPageInvocation (PageUnmap cap ctSlot) = do
case capFMappedAddress cap of
Just (asid, vaddr) -> unmapPage (capFSize cap) asid vaddr (capFBasePtr cap)