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

aarch64 haskell: fill in updateASIDPoolEntry 

This refactors getASIDPoolEntry to extract code that is shared between
lookup and update, and should make conversion to reader monad later
easier.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-02-09 16:40:44 +11:00 committed by Gerwin Klein
parent b1370585fe
commit c9d224d79a
1 changed files with 21 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -40,7 +40,7 @@ import Data.Array
import Data.List
import Data.Word (Word32)
-- The RISC-V-specific invocations are imported with the "ArchInv" prefix. This
-- The AArch64-specific invocations are imported with the "ArchInv" prefix. This
-- is necessary to avoid namespace conflicts with the generic invocations.
import SEL4.API.Invocation.AARCH64 as ArchInv
@ -75,12 +75,17 @@ lookupIPCBuffer isReceiver thread = do
{- ASID Lookups -}
-- FIXME AARCH64: make this a Reader Monad
getASIDPoolEntry :: ASID -> Kernel (Maybe ASIDPoolEntry)
getASIDPoolEntry asid = do
getPoolPtr :: ASID -> Kernel (Maybe (PPtr ASIDPool))
getPoolPtr asid = do
assert (asid > 0) "ASID 0 is used for objects that are not mapped"
assert (asid <= snd asidRange) "ASID out of range"
asidTable <- gets (armKSASIDTable . ksArchState)
let poolPtr = asidTable!(asidHighBitsOf asid)
return $ asidTable!(asidHighBitsOf asid)
-- FIXME AARCH64: make this a Reader Monad
getASIDPoolEntry :: ASID -> Kernel (Maybe ASIDPoolEntry)
getASIDPoolEntry asid = do
poolPtr <- getPoolPtr asid
maybePool <- case poolPtr of
Just ptr -> liftM Just $ getObject ptr
Nothing -> return Nothing
@ -88,10 +93,16 @@ getASIDPoolEntry asid = do
Just (ASIDPool pool) -> return $ pool!(asid .&. mask asidLowBits)
Nothing -> return Nothing
updateASIDPoolEntry :: ASID -> (ASIDPoolEntry -> Maybe ASIDPoolEntry) -> Kernel ()
updateASIDPoolEntry asid f = error "FIXME AARCH64: TODO"
-- TODO: should assert that ASID exists (resolve to not-Nothing)
-- TODO: swap parameter order?
updateASIDPoolEntry :: (ASIDPoolEntry -> Maybe ASIDPoolEntry) -> ASID -> Kernel ()
updateASIDPoolEntry f asid = do
maybePoolPtr <- getPoolPtr asid
assert (isJust maybePoolPtr) "ASID pool pointer must exist"
let poolPtr = fromJust maybePoolPtr
ASIDPool pool <- getObject poolPtr
let maybeEntry = pool!(asid .&. mask asidLowBits)
assert (isJust maybeEntry) "ASID pool entry must exist"
let pool' = pool//[(asid .&. mask asidLowBits, f $ fromJust maybeEntry)]
setObject poolPtr $ ASIDPool pool'
findVSpaceForASID :: ASID -> KernelF LookupFailure (PPtr PTE)
findVSpaceForASID asid = do
@ -313,7 +324,7 @@ setVMRoot tcb = do
-- FIXME AARCH64: naming
storeHWASID :: ASID -> VMID -> Kernel ()
storeHWASID asid hw_asid = do
updateASIDPoolEntry asid (\entry -> Just $ entry { apVMID = Just hw_asid })
updateASIDPoolEntry (\entry -> Just $ entry { apVMID = Just hw_asid }) asid
hwASIDTable <- gets (armKSHWASIDTable . ksArchState)
let hwASIDTable' = hwASIDTable//[(hw_asid, Just asid)]
modify (\s -> s {
@ -332,8 +343,7 @@ loadHWASID asid = do
-- FIXME AARCH64: naming
invalidateASID :: ASID -> Kernel ()
invalidateASID asid = do
updateASIDPoolEntry asid (\entry -> Just $ entry { apVMID = Nothing })
invalidateASID = updateASIDPoolEntry (\entry -> Just $ entry { apVMID = Nothing })
-- FIXME AARCH64: naming
invalidateHWASIDEntry :: VMID -> Kernel ()