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

aarch64 haskell: sync flush decode with aspec 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-03-17 14:51:29 +11:00 committed by Gerwin Klein
parent ac7491610b
commit 6d8134ef7a
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -570,8 +570,8 @@ decodeARMFrameInvocationFlush label args cap = case (args, capFMappedAddress cap
vspaceRoot <- lookupErrorOnFailure False $ findVSpaceForASID asid
when (end <= start) $ throw $ InvalidArgument 1
let pageSize = bit (pageBitsForSize (capFSize cap))
let pageBase = addrFromPPtr $ capFBasePtr cap
when (start >= pageSize || end > pageSize) $ throw $ InvalidArgument 0
let pageBase = addrFromPPtr $ capFBasePtr cap
let pstart = pageBase + toPAddr start
when (pstart < paddrBase || ((end - start) + fromPAddr pstart > fromPAddr paddrTop)) $
throw IllegalOperation
@ -616,7 +616,7 @@ decodeARMPageTableInvocationMap :: PPtr CTE -> ArchCapability -> VPtr ->
decodeARMPageTableInvocationMap cte cap vptr attr vspaceCap = do
when (isJust $ capPTMappedAddress cap) $ throw $ InvalidCapability 0
(vspace,asid) <- checkVSpaceRoot vspaceCap 1
when (vptr >= pptrUserTop) $ throw $ InvalidArgument 0
when (vptr > pptrUserTop) $ throw $ InvalidArgument 0
vspaceCheck <- lookupErrorOnFailure False $ findVSpaceForASID asid
when (vspaceCheck /= vspace) $ throw $ InvalidCapability 1
(bitsLeft, slot) <- withoutFailure $ lookupPTSlot vspace vptr
@ -664,14 +664,14 @@ decodeARMVSpaceInvocation label args cap@(PageTableCap { capPTisVSpace = True })
case frameInfo of
-- Ignore call if there is nothing mapped here
Nothing -> return $ InvokeVSpace VSpaceNothing
Just frameInfo -> do
withoutFailure $ checkValidMappingSize (fst frameInfo)
let baseStart = pageBase (VPtr start) (fst frameInfo)
let baseEnd = pageBase (VPtr end - 1) (fst frameInfo)
Just (bitsLeft, pAddr) -> do
withoutFailure $ checkValidMappingSize bitsLeft
let baseStart = pageBase (VPtr start) bitsLeft
let baseEnd = pageBase (VPtr end - 1) bitsLeft
when (baseStart /= baseEnd) $
throw $ RangeError start $ fromVPtr $ baseStart + mask (fst frameInfo)
let offset = start .&. mask (fst frameInfo)
let pStart = snd frameInfo + toPAddr offset
throw $ RangeError start $ fromVPtr $ baseStart + mask bitsLeft
let offset = start .&. mask bitsLeft
let pStart = pAddr + toPAddr offset
return $ InvokeVSpace $ VSpaceFlush {
vsFlushType = labelToFlushType label,
vsFlushStart = VPtr start,