| -- |
| -- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) |
| -- |
| -- SPDX-License-Identifier: BSD-2-Clause |
| -- |
| |
| module CapDL.State where |
| |
| import CapDL.Model |
| |
| import Prelude () |
| import Prelude.Compat |
| import Control.Monad.State |
| import Control.Monad.Writer |
| import Data.Maybe |
| import Data.List.Compat |
| import qualified Data.Map as Map |
| import qualified Data.Set as Set |
| import Text.PrettyPrint (Doc, text) |
| import Control.Lens.Extras (is) |
| |
| type Kernel a = State (Model Word) a |
| |
| maybeObject :: ObjID -> Model Word -> Maybe (KernelObject Word) |
| maybeObject ref = Map.lookup ref . objects |
| |
| isObject :: ObjID -> Model Word -> Bool |
| isObject ref = isJust . maybeObject ref |
| |
| object :: ObjID -> Model Word -> KernelObject Word |
| object ref m = |
| case maybeObject ref m of |
| Just obj -> obj |
| Nothing -> error $ "Object does not exist: " ++ show ref |
| |
| modifyObject :: ObjID -> (KernelObject Word -> KernelObject Word) -> Kernel () |
| modifyObject ref f = |
| modify (\s -> s { objects = Map.update (Just . f) ref (objects s) }) |
| |
| setObject :: ObjID -> KernelObject Word -> Kernel () |
| setObject ref obj = modifyObject ref (const obj) |
| |
| objSlots :: KernelObject Word -> CapMap Word |
| objSlots obj = |
| if hasSlots obj then slots obj |
| else Map.empty |
| |
| slotsOfMaybe :: Maybe (KernelObject Word) -> CapMap Word |
| slotsOfMaybe = maybe Map.empty objSlots |
| |
| slotsOf :: ObjID -> Model Word -> CapMap Word |
| slotsOf ref = slotsOfMaybe . maybeObject ref |
| |
| getCovered :: ObjID -> Model Word -> [ObjID] |
| getCovered ut_ref = getUTCover ut_ref . untypedCovers |
| |
| setCovered :: ObjID -> [ObjID] -> Kernel () |
| setCovered ut_ref covers = |
| modify (\s -> s { untypedCovers = Map.insert ut_ref covers (untypedCovers s) }) |
| |
| type SlotsLookup = ObjID -> Model Word -> CapMap Word |
| |
| cNodeSlots :: SlotsLookup |
| cNodeSlots ref m = case maybeObject ref m of |
| Just (CNode slots _ _) -> slots |
| _ -> Map.empty |
| |
| pdSlots :: SlotsLookup |
| pdSlots ref m = case maybeObject ref m of |
| Just (PD slots) -> slots |
| Just (PT slots) -> slots |
| _ -> Map.empty |
| |
| ioptSlots :: SlotsLookup |
| ioptSlots ref m = case maybeObject ref m of |
| Just (IOPT slots _) -> slots |
| _ -> Map.empty |
| |
| maybeObjID :: Cap -> Maybe ObjID |
| maybeObjID cap = if hasObjID cap then Just (objID cap) else Nothing |
| |
| lookupOf :: Cap -> SlotsLookup -> Model Word -> CapMap Word |
| lookupOf cap lookup = maybe (const Map.empty) lookup (maybeObjID cap) |
| |
| type CapLookup = [([Word], Cap)] |
| |
| singleton :: a -> [a] |
| singleton x = [x] |
| |
| mapKeys :: (a -> b) -> [(a,c)] -> [(b,c)] |
| mapKeys f = map (\(a,b) -> (f a,b)) |
| |
| mapVals :: (b -> c) -> [(a,b)] -> [(a,c)] |
| mapVals f = map (\(a,b) -> (a,f b)) |
| |
| mapWithKey :: (a -> b -> c) -> [(a,b)] -> [c] |
| mapWithKey f = map (\(a,b) -> f a b) |
| |
| snoc :: [a] -> a -> [a] |
| snoc xs x = xs ++ [x] |
| |
| -- FIXME: ignoring guards |
| nextLookup :: Model Word -> SlotsLookup -> [Word] -> Cap -> CapLookup |
| nextLookup m lookup ws cap = |
| Map.toList $ Map.mapKeys (snoc ws) (lookupOf cap lookup m) |
| |
| -- FIXME: ignoring guards |
| nextLevel :: Model Word -> CapLookup -> SlotsLookup -> CapLookup |
| nextLevel m cl lookup = concat (mapWithKey (nextLookup m lookup) cl) |
| |
| allLevels :: CapLookup -> Int -> SlotsLookup -> Model Word -> CapLookup |
| allLevels [] _ _ _ = [] |
| allLevels _ 0 _ _ = [] |
| allLevels cl d lookup m = |
| cl ++ allLevels (nextLevel m cl lookup) (d - 1) lookup m |
| |
| maxDepth = 4 |
| |
| capSpaceLookup :: CapMap Word -> SlotsLookup -> Model Word -> CapLookup |
| capSpaceLookup caps lookup = |
| let firstLevel = Map.toList . Map.mapKeys singleton $ caps |
| in allLevels firstLevel maxDepth lookup |
| |
| capSpace :: CapMap Word -> SlotsLookup -> Model Word -> CapMap [Word] |
| capSpace caps lookup = Map.fromList . capSpaceLookup caps lookup |
| |
| cspaceCap :: ObjID -> Model Word -> Cap |
| cspaceCap tcb_ref = |
| fromJust . Map.lookup tcbCTableSlot . slots . object tcb_ref |
| |
| cspace :: ObjID -> Model Word -> CapMap [Word] |
| cspace tcb_ref m = |
| let cap = cspaceCap tcb_ref m |
| in capSpace (lookupOf cap cNodeSlots m) cNodeSlots m |
| |
| capLookup :: [Word] -> ObjID -> Model Word -> Maybe Cap |
| capLookup ref tcb_ref = Map.lookup ref . cspace tcb_ref |
| |
| flattenCnode :: KernelObject Word -> Model Word -> (ObjID, KernelObject [Word]) |
| flattenCnode tcb m = |
| let cnode_id = objID $ fromJust . Map.lookup tcbCTableSlot . slots $ tcb |
| cnode = object cnode_id m |
| in (cnode_id, cnode { slots = capSpace (slots cnode) cNodeSlots m }) |
| |
| flattenPD :: KernelObject Word -> Model Word -> KernelObject [Word] |
| flattenPD obj m = |
| let newSlots = capSpace (slots obj) pdSlots m |
| origSlots = Map.mapKeys singleton (slots obj) |
| in obj { slots = Map.difference newSlots origSlots } |
| |
| isFrame :: Cap -> Maybe Cap |
| isFrame cap = |
| case cap of |
| FrameCap {} -> Just cap |
| _ -> Nothing |
| |
| flattenIOPT :: KernelObject Word -> Model Word -> KernelObject [Word] |
| flattenIOPT obj m = |
| let newSlots = capSpace (slots obj) ioptSlots m |
| newSlots' = foldl (flip (Map.update isFrame)) newSlots $ |
| map fst (Map.toList newSlots) |
| in obj { slots = newSlots' } |
| |
| flatten' :: Model Word -> ObjMap [Word] -> (ObjID, KernelObject Word) -> |
| ObjMap [Word] |
| flatten' m objs (n, obj@(PD {})) = Map.insert n (flattenPD obj m) objs |
| flatten' m objs (n, obj@(IOPT _ 1)) = Map.insert n (flattenIOPT obj m) objs |
| flatten' m objs (n, obj@(TCB {})) = |
| let tcb = obj { slots = Map.mapKeys singleton (slots obj) } |
| objs' = Map.insert n tcb objs |
| (cnode_id, cnode) = flattenCnode obj m |
| in Map.insert cnode_id cnode objs' |
| flatten' _ objs (n, obj) |
| | hasSlots obj = |
| let obj' = obj { slots = Map.mapKeys singleton (slots obj) } |
| in Map.insertWith const n obj' objs |
| | otherwise = |
| let obj' = case obj of |
| Endpoint -> Endpoint |
| Notification -> Notification |
| Untyped msb paddr-> Untyped msb paddr |
| Frame vms p f -> Frame vms p f |
| IOPorts sz -> IOPorts sz |
| _ -> error "unmatched" |
| in Map.insert n obj' objs |
| |
| flatten :: Model Word -> Model [Word] |
| flatten m@(Model arch objs irqNode cdt untypedCovers) = |
| Model arch (foldl (flatten' m) Map.empty (Map.toList objs)) irqNode cdt untypedCovers |
| |
| -- slots of one object |
| getSlots :: ObjID -> Kernel (CapMap Word) |
| getSlots ref = gets $ slotsOf ref |
| |
| -- Caps |
| |
| maybeSlotCap :: CapRef -> Model Word -> Maybe Cap |
| maybeSlotCap (ref,slot) = Map.lookup slot . slotsOf ref |
| |
| slotCap :: CapRef -> Model Word -> Cap |
| slotCap cref = fromJust . maybeSlotCap cref |
| |
| setSlots :: ObjID -> CapMap Word -> Kernel () |
| setSlots ref sl = do |
| obj <- gets $ object ref |
| when (hasSlots obj) $ setObject ref $ obj {slots = sl} |
| |
| setCap :: CapRef -> Cap -> Kernel () |
| setCap (ref,slot) cap = do |
| slots <- gets $ slotsOf ref |
| case Map.lookup slot slots of |
| Just NullCap -> setSlots ref $ Map.insert slot cap slots |
| Nothing -> setSlots ref $ Map.insert slot cap slots |
| _ -> error ("Slot already filled: slot " ++ show slot ++ |
| " in " ++ show ref) |
| |
| removeCap :: CapRef -> Kernel () |
| removeCap (ref,slot) = do |
| slots <- gets $ slotsOf ref |
| setSlots ref $ Map.delete slot slots |
| |
| allObjs :: Model Word -> [(ObjID,KernelObject Word)] |
| allObjs = Map.toList . objects |
| |
| refSlots :: (ObjID,KernelObject Word) -> [(CapRef, Cap)] |
| refSlots (ref,obj) = |
| map (\(slot,cap) -> ((ref,slot),cap)) $ Map.toList $ objSlots obj |
| |
| allSlots :: Model Word -> [(CapRef,Cap)] |
| allSlots = concatMap refSlots . allObjs |
| |
| findSlotCapsWithRef :: (CapRef -> Cap -> Bool) -> Model Word -> [(CapRef, Cap)] |
| findSlotCapsWithRef p = filter (uncurry p) . allSlots |
| |
| findSlotCaps :: (Cap -> Bool) -> Model Word -> [(CapRef, Cap)] |
| findSlotCaps p = findSlotCapsWithRef (\_ -> p) |
| |
| findSlots :: (Cap -> Bool) -> Model Word -> [CapRef] |
| findSlots p = map fst . findSlotCaps p |
| |
| hasTarget :: ObjID -> Cap -> Bool |
| hasTarget ref cap = hasObjID cap && objID cap == ref |
| |
| -- validity |
| |
| type Logger a = Writer Doc a |
| |
| sameID :: ObjID -> Cap -> Bool |
| sameID id cap = hasObjID cap && id == objID cap |
| |
| isMapped :: ObjID -> KernelObject Word -> Bool |
| isMapped id obj |
| | hasSlots obj = any (sameID id) $ Map.elems (slots obj) |
| | otherwise = False |
| |
| allMappings :: ObjID -> Model Word -> [(ObjID, KernelObject Word)] |
| allMappings id m = filter (isMapped id . snd) (allObjs m) |
| |
| isASID :: KernelObject Word -> Bool |
| isASID (ASIDPool {}) = True |
| isASID _ = False |
| |
| uniqueASID :: ObjID -> Model Word -> Bool |
| uniqueASID id m = |
| let mappings = filter (isASID . snd) (allMappings id m) |
| in length mappings <= 1 |
| |
| checkASID :: ObjID -> Model Word -> Logger Bool |
| checkASID id m = do |
| let valid = uniqueASID id m |
| unless valid (tell $ text $ show id ++ " is mapped into multiple ASID's\n") |
| return valid |
| |
| isPD :: KernelObject Word -> Bool |
| isPD (PD {}) = True |
| isPD _ = False |
| |
| uniquePD :: ObjID -> Model Word -> Bool |
| uniquePD id m = |
| let mappings = filter (isPD . snd) (allMappings id m) |
| in length mappings <= 1 |
| |
| checkPD :: ObjID -> Model Word -> Logger Bool |
| checkPD id m = do |
| let valid = uniquePD id m |
| unless valid (tell $ text $ show id ++ " is mapped into multiple PD's\n") |
| return valid |
| |
| checkMapping :: Model Word -> (ObjID, KernelObject Word) -> Logger Bool |
| checkMapping m (id, obj) = |
| case obj of |
| PD {} -> checkASID id m |
| PT {} -> checkPD id m |
| _ -> return True |
| |
| checkMappings :: Model Word -> Logger Bool |
| checkMappings m = do |
| let objs = allObjs m |
| allM (checkMapping m) objs |
| |
| koType :: KernelObject Word -> KOType |
| koType Endpoint = Endpoint_T |
| koType Notification = Notification_T |
| koType (TCB {}) = TCB_T |
| koType (CNode {}) = CNode_T |
| koType (Untyped {}) = Untyped_T |
| koType (ASIDPool {}) = ASIDPool_T |
| koType (PML4 {}) = PML4_T |
| koType (PDPT {}) = PDPT_T |
| koType (PD {}) = PD_T |
| koType (PT {}) = PT_T |
| koType (PGD {}) = PGD_T |
| koType (PUD {}) = PUD_T |
| koType (Frame {}) = Frame_T |
| koType (IOPorts {}) = IOPorts_T |
| koType (IODevice {}) = IODevice_T |
| koType (ARMIODevice {}) = ARMIODevice_T |
| koType (IOPT {}) = IOPT_T |
| koType (VCPU {}) = VCPU_T |
| koType (SC {}) = SC_T |
| koType (RTReply {}) = RTReply_T |
| koType (IOAPICIrq {}) = IOAPICIrqSlot_T |
| koType (MSIIrq {}) = MSIIrqSlot_T |
| koType (ARMIrq {}) = ARMIrqSlot_T |
| koType (ARMSID {}) = ARMSID_T |
| koType (ARMCB {}) = ARMCB_T |
| |
| objAt :: (KernelObject Word -> Bool) -> ObjID -> Model Word -> Bool |
| objAt p ref = maybe False p . maybeObject ref |
| |
| typAt :: KOType -> ObjID -> Model Word -> Bool |
| typAt t = objAt $ (==) t . koType |
| |
| capTyp :: Cap -> KOType |
| capTyp (UntypedCap {}) = Untyped_T |
| capTyp (EndpointCap {}) = Endpoint_T |
| capTyp (NotificationCap {}) = Notification_T |
| capTyp (ReplyCap {}) = TCB_T |
| capTyp (MasterReplyCap {}) = TCB_T |
| capTyp (CNodeCap {}) = CNode_T |
| capTyp (TCBCap {}) = TCB_T |
| capTyp (IRQHandlerCap {}) = CNode_T |
| capTyp (FrameCap {}) = Frame_T |
| capTyp (PTCap {}) = PT_T |
| capTyp (PDCap {}) = PD_T |
| capTyp (PML4Cap {} ) = PML4_T |
| capTyp (PDPTCap {} ) = PDPT_T |
| capTyp (PUDCap {} ) = PUD_T |
| capTyp (PGDCap {} ) = PGD_T |
| capTyp (ASIDPoolCap {}) = ASIDPool_T |
| capTyp (IOPortsCap {}) = IOPorts_T |
| capTyp (IOSpaceCap {}) = IODevice_T |
| capTyp (ARMIOSpaceCap {}) = ARMIODevice_T |
| capTyp (IOPTCap {}) = IOPT_T |
| capTyp (VCPUCap {}) = VCPU_T |
| capTyp (SCCap {}) = SC_T |
| capTyp (RTReplyCap {}) = RTReply_T |
| capTyp (IRQIOAPICHandlerCap {}) = IOAPICIrqSlot_T |
| capTyp (IRQMSIHandlerCap {}) = MSIIrqSlot_T |
| capTyp (ARMIRQHandlerCap {}) = ARMIrqSlot_T |
| capTyp (ARMSIDCap {}) = ARMSID_T |
| capTyp (ARMCBCap {}) = ARMCB_T |
| capTyp _ = error "cap has no object" |
| |
| checkTypAt :: Cap -> Model Word -> ObjID -> Word -> Logger Bool |
| checkTypAt cap m contID slot = do |
| let valid = not (hasObjID cap) || typAt (capTyp cap) (objID cap) m |
| unless valid (tell $ text $ "The cap at slot " ++ show slot ++ " in " ++ |
| show contID ++ " refers to an object of the wrong type\n") |
| --FIXME:Needs better error message |
| return valid |
| |
| validCapArch :: Arch -> Cap -> Bool |
| validCapArch _ NullCap = True |
| validCapArch _ (UntypedCap {}) = True |
| validCapArch _ (EndpointCap {}) = True |
| validCapArch _ (NotificationCap {}) = True |
| validCapArch _ (ReplyCap {}) = True |
| validCapArch _ (MasterReplyCap {}) = True |
| validCapArch _ (CNodeCap {}) = True |
| validCapArch _ (TCBCap {}) = True |
| validCapArch _ IRQControlCap = True |
| validCapArch _ (IRQHandlerCap {}) = True |
| validCapArch _ (DomainCap {}) = True |
| validCapArch _ (FrameCap {}) = True |
| validCapArch _ (PTCap {}) = True |
| validCapArch _ (PDCap {}) = True |
| validCapArch _ (ASIDPoolCap {}) = True |
| validCapArch _ ASIDControlCap = True |
| validCapArch _ (SCCap {}) = True |
| validCapArch _ (RTReplyCap {}) = True |
| validCapArch _ (SchedControlCap {}) = True |
| validCapArch RISCV (VCPUCap {}) = False |
| validCapArch _ (VCPUCap {}) = True |
| validCapArch IA32 (IRQIOAPICHandlerCap {}) = True |
| validCapArch IA32 (IRQMSIHandlerCap {}) = True |
| validCapArch IA32 (IOPortsCap {}) = True |
| validCapArch IA32 IOSpaceMasterCap = True |
| validCapArch IA32 (IOSpaceCap {}) = True |
| validCapArch IA32 (IOPTCap {}) = True |
| validCapArch X86_64 (PML4Cap {}) = True |
| validCapArch X86_64 (PDPTCap {}) = True |
| validCapArch X86_64 (IRQIOAPICHandlerCap {}) = True |
| validCapArch X86_64 (IRQMSIHandlerCap {}) = True |
| validCapArch X86_64 (IOPortsCap {}) = True |
| validCapArch X86_64 IOSpaceMasterCap = True |
| validCapArch X86_64 (IOSpaceCap {}) = True |
| validCapArch X86_64 (IOPTCap {}) = True |
| validCapArch ARM11 (ARMIOSpaceCap {}) = True |
| validCapArch ARM11 (ARMIRQHandlerCap {}) = True |
| validCapArch AARCH64 (ARMIRQHandlerCap {}) = True |
| validCapArch AARCH64 (PUDCap {}) = True |
| validCapArch AARCH64 (PGDCap {}) = True |
| validCapArch AARCH64 (ARMSIDCap {}) = True |
| validCapArch AARCH64 (ARMCBCap {}) = True |
| validCapArch _ _ = False |
| |
| checkCapArch :: Arch -> Cap -> ObjID -> Word -> Logger Bool |
| checkCapArch arch cap contID slot = do |
| let valid = validCapArch arch cap |
| unless valid (tell $ text $ "The cap at slot " ++ show slot ++ " in " ++ |
| show contID ++ " is not valid for this architecture\n") |
| return valid |
| |
| checkValidCap :: Arch -> ObjID -> Model Word -> (Word, Cap) -> Logger Bool |
| checkValidCap arch contID m (slot, cap) = do |
| capArch <- checkCapArch arch cap contID slot |
| typ <- checkTypAt cap m contID slot |
| return $ capArch && typ |
| |
| checkValidCaps :: Arch -> KernelObject Word -> ObjID -> Model Word -> Logger Bool |
| checkValidCaps arch obj id m = |
| allM (checkValidCap arch id m) (Map.toList $ objSlots obj) |
| |
| allM f xs = do |
| bs <- mapM f xs |
| return $ and bs |
| |
| validObjArch :: Arch -> KernelObject Word -> Bool |
| validObjArch _ Endpoint = True |
| validObjArch _ Notification = True |
| validObjArch _ (TCB {}) = True |
| validObjArch _ (CNode {}) = True |
| validObjArch _ (Untyped {}) = True |
| validObjArch _ (ASIDPool {}) = True |
| validObjArch _ (PD {}) = True |
| validObjArch _ (PT {}) = True |
| validObjArch _ (Frame {}) = True |
| validObjArch _ (SC {}) = True |
| validObjArch _ (RTReply {}) = True |
| validObjArch RISCV (VCPU {}) = False |
| validObjArch _ (VCPU {}) = True |
| validObjArch ARM11 (ARMIODevice {}) = True |
| validObjArch ARM11 (ARMIrq {}) = True |
| validObjArch IA32 (IOPorts {}) = True |
| validObjArch IA32 (IODevice {}) = True |
| validObjArch IA32 (IOPT {}) = True |
| validObjArch IA32 (IOAPICIrq {}) = True |
| validObjArch IA32 (MSIIrq {}) = True |
| validObjArch X86_64 (PML4 {}) = True |
| validObjArch X86_64 (PDPT {}) = True |
| validObjArch X86_64 (IOPorts {}) = True |
| validObjArch X86_64 (IODevice {}) = True |
| validObjArch X86_64 (IOPT {}) = True |
| validObjArch X86_64 (IOAPICIrq {}) = True |
| validObjArch X86_64 (MSIIrq {}) = True |
| validObjArch AARCH64 (ARMIrq {}) = True |
| validObjArch AARCH64 (PUD {}) = True |
| validObjArch AARCH64 (PGD {}) = True |
| validObjArch AARCH64 (ARMSID {}) = True |
| validObjArch AARCH64 (ARMCB {}) = True |
| validObjArch _ _ = False |
| |
| checkObjArch :: Arch -> KernelObject Word -> ObjID -> Logger Bool |
| checkObjArch arch obj id = do |
| let valid = validObjArch arch obj |
| unless valid |
| (tell $ text $ show id ++ " is not a valid object for this architecture\n") |
| return valid |
| |
| validTCBSlotCap :: Arch -> Word -> Cap -> Bool |
| validTCBSlotCap arch slot cap |
| | slot == tcbCTableSlot = is _CNodeCap cap |
| | slot == tcbVTableSlot |
| = case arch of |
| IA32 -> is _PDCap cap |
| ARM11 -> is _PDCap cap |
| X86_64 -> is _PML4Cap cap |
| AARCH64 -> is _PGDCap cap || is _PUDCap cap |
| RISCV -> is _PTCap cap |
| | slot == tcbReplySlot = is _MasterReplyCap cap |
| | slot == tcbCallerSlot = is _ReplyCap cap |
| | slot == tcbIPCBufferSlot = is _FrameCap cap |
| | slot == tcbFaultEPSlot = is _EndpointCap cap |
| | slot == tcbSCSlot = is _SCCap cap |
| | slot == tcbTempFaultEPSlot = is _EndpointCap cap |
| | slot == tcbBoundVCPUSlot = arch /= RISCV && is _VCPUCap cap |
| | otherwise = cap == NullCap |
| |
| validObjCap :: Arch -> KernelObject Word -> Word -> Cap -> Bool |
| validObjCap arch (TCB {}) slot cap = validTCBSlotCap arch slot cap |
| validObjCap _ (CNode _ 0 _) slot cap = slot == 0 && is _NotificationCap cap -- FIXME: we should add a separate IRQObject |
| validObjCap _ (CNode {}) _ _ = True |
| validObjCap _ (ASIDPool {}) _ cap = is _PDCap cap |
| validObjCap RISCV (PT {}) _ cap = is _FrameCap cap || is _PTCap cap |
| validObjCap _ (PT {}) _ cap = is _FrameCap cap |
| validObjCap _ (PD {}) _ cap = is _FrameCap cap || is _PTCap cap |
| validObjCap _ (PDPT {}) _ cap = is _FrameCap cap || is _PDCap cap |
| validObjCap _ (PML4 {}) _ cap = is _PDPTCap cap |
| validObjCap _ (PUD {}) _ cap = is _FrameCap cap || is _PDCap cap |
| validObjCap _ (PGD {}) _ cap = is _PUDCap cap |
| validObjCap _ (ARMIODevice {}) _ _ = True -- FIXME: we should check IODevices properly |
| validObjCap _ (ARMIrq {}) slot cap = slot == 0 && is _NotificationCap cap |
| validObjCap _ (IODevice {}) _ _ = True -- FIXME: we should check IODevices properly |
| validObjCap _ (IOPT {}) _ cap = is _FrameCap cap || is _IOPTCap cap |
| validObjCap _ (IOAPICIrq {}) slot cap = slot == 0 && is _NotificationCap cap |
| validObjCap _ (MSIIrq {}) slot cap = slot == 0 && is _NotificationCap cap |
| validObjCap _ _ _ _ = False |
| |
| checkValidSlot :: Arch -> KernelObject Word -> ObjID -> (Word, Cap) -> Logger Bool |
| checkValidSlot arch obj contID (slot, cap) = do |
| let valid = validObjCap arch obj slot cap |
| unless valid (tell $ text $ "The cap at slot " ++ show slot ++ " in " ++ |
| show contID ++ " is not valid for this object\n") |
| return valid |
| |
| checkValidSlots :: Arch -> KernelObject Word -> ObjID -> Logger Bool |
| checkValidSlots arch obj id = |
| allM (checkValidSlot arch obj id) (Map.toList $ objSlots obj) |
| |
| -- FIXME: we should check that all irq objects are in the irqNode |
| checkObj :: Arch -> Model Word -> (ObjID, KernelObject Word) -> Logger Bool |
| checkObj arch m (id, obj) = do |
| objArch <- checkObjArch arch obj id |
| caps <- checkValidCaps arch obj id m |
| slots <- checkValidSlots arch obj id |
| return $ objArch && caps && slots |
| |
| checkObjs :: Arch -> Model Word -> Logger Bool |
| checkObjs arch m = do |
| let objs = allObjs m |
| allM (checkObj arch m) objs |
| |
| allCovers :: Model Word -> [[ObjID]] |
| allCovers (Model _ _ _ _ covMap) = |
| let covers = map snd (Map.toList covMap) |
| in filter (not . null) covers |
| |
| nullIntersections :: Ord a => [Set.Set a] -> Bool |
| nullIntersections [] = True |
| nullIntersections (x:xs) = check x xs |
| where check _ [] = True |
| check seen (x:xs) = |
| Set.null (x `Set.intersection` seen) && check (Set.union x seen) xs |
| |
| checkUntyped :: Model Word -> ObjID -> Logger Bool |
| checkUntyped m ref = do |
| let valid = |
| case object ref m of |
| Untyped _ _ -> True |
| _ -> False |
| unless valid |
| (tell $ text $ show ref ++ " covers objects but is not an untyped\n") |
| return valid |
| |
| checkUntypeds :: Model Word -> Logger Bool |
| checkUntypeds m@(Model _ _ _ _ covMap) = do |
| let objs = map fst (Map.toList covMap) |
| allM (checkUntyped m) objs |
| |
| checkUntypedCover :: Model Word -> (ObjID, [ObjID]) -> Logger Bool |
| checkUntypedCover m (id, objs) = do |
| let valid = allM (objAt (const True)) objs m |
| unless valid |
| (tell $ text $ show id ++ " covers a non-existant object\n") |
| return valid |
| |
| checkUntypedCovers :: Model Word -> Logger Bool |
| checkUntypedCovers m = |
| allM (checkUntypedCover m) $ Map.toList $ untypedCovers m |
| |
| checkCovers :: Model Word -> Logger Bool |
| checkCovers m = do |
| let valid = nullIntersections $ map Set.fromList $ allCovers m |
| unless valid (tell $ text $ "At least two untypeds have intersecting covers\n") |
| untypeds <- checkUntypeds m |
| covers <- checkUntypedCovers m |
| return $ valid && covers && untypeds |
| |
| isIRQ :: KernelObject Word -> Bool |
| isIRQ (CNode _ 0 _) = True --check irqNode |
| isIRQ IOAPICIrq{} = True |
| isIRQ MSIIrq{} = True |
| isIRQ ARMIrq{} = True |
| isIRQ _ = False |
| |
| validIRQ :: Model Word -> ObjID -> Bool |
| validIRQ m irq = isIRQ $ object irq m |
| |
| checkIRQ :: Model Word -> (Word, ObjID) -> Logger Bool |
| checkIRQ m (slot, irq) = do |
| let valid = validIRQ m irq |
| unless valid (tell $ text $ "The object mapped by irq " ++ show slot ++ --FIXME:rewrite |
| " in the irqNode is not a valid irq_slot\n") |
| return valid |
| |
| checkIRQNode :: Model Word -> Logger Bool |
| checkIRQNode m = allM (checkIRQ m) (Map.toList $ irqNode m) |
| |
| flattenCNodeSlots :: [(ObjID, KernelObject Word)] -> [Cap] |
| flattenCNodeSlots [] = [] |
| flattenCNodeSlots ((_, CNode slots _ _) : xs) = map snd (Map.toList slots) ++ flattenCNodeSlots xs |
| flattenCNodeSlots (_ : xs) = flattenCNodeSlots xs |
| |
| isMappedFrameCap :: Cap -> Bool |
| isMappedFrameCap (FrameCap _ _ _ _ (Just _)) = True |
| isMappedFrameCap _ = False |
| |
| -- Returns list containing each element in argument list occuring more than once. |
| -- There are no duplicates in the returned list. |
| findDuplicates :: Ord a => [a] -> [a] |
| findDuplicates = map head . filter ((>1) . length) . groupBy (==) . sort |
| |
| -- Checks that each mapping is specified by at most 1 frame cap |
| checkDuplicateMappedFrameCaps :: [(ObjID, Word)] -> Logger Bool |
| checkDuplicateMappedFrameCaps mappings = do |
| let duplicates = findDuplicates mappings |
| let valid = null duplicates |
| showCapSlot ((container, _), slot) = container ++ ", slot " ++ show slot |
| unless valid (tell $ text $ "Mappings referenced by multiple frame caps:\n" ++ |
| (intercalate "\n" $ map showCapSlot duplicates) |
| ++ "\n") |
| return valid |
| |
| checkMappingSlotSanity :: CapMap Word -> Word -> Logger Bool |
| checkMappingSlotSanity slots slot = |
| let cap = Map.lookup slot slots |
| in case cap of |
| Just (FrameCap {}) -> return True |
| Just _ -> do |
| tell $ text "Frame references mapping to object other than a frame\n" |
| return False |
| Nothing -> do |
| tell $ text "Frame references mapping in empty or non-existent slot\n" |
| return False |
| |
| checkMappingSanity :: (ObjID, KernelObject Word, Word) -> Logger Bool |
| checkMappingSanity (id, obj, slot) = |
| case obj of |
| PT slots -> checkMappingSlotSanity slots slot |
| PD slots -> checkMappingSlotSanity slots slot |
| _ -> do |
| tell $ text $ "Object specified in mapping(" ++ fst id ++ ", " ++ show slot ++ ") is neither page table nor page directory\n" |
| return False |
| |
| checkMappedFrameCapsSanity :: Model Word -> [(ObjID, Word)] -> Logger Bool |
| checkMappedFrameCapsSanity m mappings = do |
| let object_mappings = map (\(objID, slot) -> (objID, object objID m, slot)) mappings |
| allM checkMappingSanity object_mappings |
| |
| isCNode :: KernelObject Word -> Bool |
| isCNode (CNode _ _ _) = True |
| isCNode _ = False |
| |
| getSlotsFromKernelObject :: KernelObject Word -> Maybe (CapMap Word) |
| getSlotsFromKernelObject (TCB slots _ _ _ _) = Just slots |
| getSlotsFromKernelObject (CNode slots _ _) = Just slots |
| getSlotsFromKernelObject (ASIDPool slots _) = Just slots |
| getSlotsFromKernelObject (PT slots) = Just slots |
| getSlotsFromKernelObject (PD slots) = Just slots |
| getSlotsFromKernelObject (PML4 slots) = Just slots |
| getSlotsFromKernelObject (PDPT slots) = Just slots |
| getSlotsFromKernelObject (PUD slots) = Just slots |
| getSlotsFromKernelObject (PGD slots) = Just slots |
| getSlotsFromKernelObject (IODevice slots _ _) = Just slots |
| getSlotsFromKernelObject (ARMIODevice slots _) = Just slots |
| getSlotsFromKernelObject (IOPT slots _) = Just slots |
| getSlotsFromKernelObject _ = Nothing |
| |
| -- Checks that an object contains no frame caps with a specified mapping |
| checkObjectContainsNoMappedFrameCap :: (ObjID, KernelObject Word) -> Logger Bool |
| checkObjectContainsNoMappedFrameCap (id, obj) = |
| let maybe_slots = getSlotsFromKernelObject obj |
| in case maybe_slots of |
| Nothing -> return True |
| Just slots -> do |
| let valid = all (not . isMappedFrameCap) $ map snd $ Map.toList slots |
| unless valid $ tell $ text $ "Non-CNode object '" ++ fst id ++ "' contains frame cap with mapping\n" |
| return valid |
| |
| checkMappedFrameCapsOnlyInCNodes :: Model Word -> Logger Bool |
| checkMappedFrameCapsOnlyInCNodes m = |
| allM checkObjectContainsNoMappedFrameCap $ filter (not . isCNode . snd) $ allObjs m |
| |
| -- Checks that mappings specified by frame caps refer to valid slots in |
| -- container objects (page directories or page tables) which contain a |
| -- mapping to a frame. |
| checkMappedFrameCaps :: Model Word -> Logger Bool |
| checkMappedFrameCaps m = do |
| let mappings = map (\(FrameCap _ _ _ _ (Just x)) -> x) $ |
| filter isMappedFrameCap $ flattenCNodeSlots $ allObjs m |
| no_duplicates <- checkDuplicateMappedFrameCaps mappings |
| sane_mappings <- checkMappedFrameCapsSanity m mappings |
| only_in_cnodes <- checkMappedFrameCapsOnlyInCNodes m |
| return $ no_duplicates && sane_mappings && only_in_cnodes |
| |
| checkModel :: Model Word -> Logger Bool |
| checkModel m = do |
| objs <- checkObjs (arch m) m |
| covers <- checkCovers m |
| mappings <- checkMappings m |
| irq <- checkIRQNode m |
| mapped_frame_caps <- checkMappedFrameCaps m |
| tell $ text "" |
| return $ objs && covers && mappings && irq && mapped_frame_caps |
| |
| -- Utils for getting object sizes |
| lookupSizeMap :: KOType -> ObjectSizeMap -> Word |
| lookupSizeMap k objSizeMap = case Map.lookup k objSizeMap of |
| Just v -> v |
| Nothing -> error $ "missing size info for type: " ++ show k |
| |
| objSizeBits :: ObjectSizeMap -> KernelObject Word -> Word |
| -- 0-size CNodes are actually IRQ slots, and have no allocation size |
| objSizeBits _ (CNode { sizeBits = 0}) = 0 |
| -- variable sized objects |
| objSizeBits _ (Untyped { maybeSizeBits = Just b }) = b |
| objSizeBits _ (Frame { vmSizeBits = b }) = b |
| objSizeBits objSizeMap (CNode { sizeBits = b }) = |
| b + lookupSizeMap CNode_T objSizeMap |
| objSizeBits _ (SC { maybeSizeBits = Just b }) = b |
| -- everything else |
| objSizeBits objSizeMap ko = |
| lookupSizeMap (koType ko) objSizeMap |
| |
| {- |
| - Check that all objects belong to an untyped cover and all untyped |
| - covers have paddrs. This is required for generating Isabelle output. |
| -} |
| isFullyAllocated :: ObjectSizeMap -> ObjMap Word -> CoverMap -> Either (String, [ObjID]) () |
| isFullyAllocated sizeMap objs untypedCovers = |
| do |
| -- check untypeds |
| let missingPaddrs = [ utID | utID <- Map.keys untypedCovers |
| , isNothing $ maybePaddr $ objs Map.! utID ] |
| unless (null missingPaddrs) $ |
| Left ("Untyped(s) have children but don't have paddrs", missingPaddrs) |
| |
| -- check objects |
| let coveredObjs = Set.fromList $ concat $ Map.elems untypedCovers |
| missingObjs = [ objID | (objID, obj) <- Map.toList objs |
| , objID `Map.notMember` untypedCovers |
| , objSizeBits sizeMap obj /= 0 |
| , objID `Set.notMember` coveredObjs ] |
| unless (null missingObjs) $ |
| Left ("Object(s) are not allocated from any untyped", missingObjs) |
