diff --git a/capDL-tool/CapDL/AST.hs b/capDL-tool/CapDL/AST.hs index 67147461..3fbf5f85 100644 --- a/capDL-tool/CapDL/AST.hs +++ b/capDL-tool/CapDL/AST.hs @@ -166,6 +166,8 @@ data CapParam asid :: Asid } | Cached { cached :: Bool } + | Executable { + executable :: Bool } | FrameMapping { container :: NameRef, slotIndex :: Word } diff --git a/capDL-tool/CapDL/MakeModel.hs b/capDL-tool/CapDL/MakeModel.hs index c6e24f7f..ccd0eab9 100644 --- a/capDL-tool/CapDL/MakeModel.hs +++ b/capDL-tool/CapDL/MakeModel.hs @@ -612,6 +612,11 @@ getCached [] = True getCached (Cached c : _) = c getCached (_ : ps) = getCached ps +getExecutable :: [CapParam] -> Bool +getExecutable [] = True +getExecutable (Executable e : _) = e +getExecutable (_ : ps) = getExecutable ps + getMaybeMapping :: [CapParam] -> Maybe (ObjID, Word) getMaybeMapping [] = Nothing getMaybeMapping (FrameMapping c s : _) = Just (refToID c, s) @@ -629,7 +634,7 @@ validCapPars (TCB {}) ps = (not (containsConstr Reply ps) || not (containsConstr MasterReply ps)) validCapPars (CNode {}) ps = subsetConstrs ps [Guard undefined, GuardSize undefined] validCapPars (Frame {}) ps = - subsetConstrs (removeConstr (Rights undefined) ps) [Asid undefined, Cached undefined, + subsetConstrs (removeConstr (Rights undefined) ps) [Asid undefined, Cached undefined, Executable undefined, FrameMapping undefined undefined] validCapPars (PD {}) ps = subsetConstrs ps [Asid undefined] validCapPars (PT {}) ps = subsetConstrs ps [Asid undefined] @@ -655,7 +660,7 @@ objCapOf containerName obj objRef params = Untyped {} -> UntypedCap objRef CNode _ 0 -> IRQHandlerCap objRef --FIXME: This should check if the obj is in the irqNode CNode {} -> CNodeCap objRef (getGuard params) (getGuardSize params) - Frame {} -> FrameCap objRef (getRights params) (getMaybeAsid params) (getCached params) + Frame {} -> FrameCap objRef (getRights params) (getMaybeAsid params) (getCached params) (getExecutable params) (getMaybeMapping params) PML4 {} -> PML4Cap objRef (getMaybeAsid params) PDPT {} -> PDPTCap objRef (getMaybeAsid params) diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs index a6c1476b..42346fe1 100644 --- a/capDL-tool/CapDL/Model.hs +++ b/capDL-tool/CapDL/Model.hs @@ -90,6 +90,7 @@ data Cap capRights :: CapRights, capMaybeAsid :: Maybe Asid, capCached :: Bool, + capExecutable :: Bool, capMaybeMapping :: Maybe (ObjID, Word) } | PTCap { capObj :: ObjID, diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs index 7fc519aa..5f88ac54 100644 --- a/capDL-tool/CapDL/ParserUtils.hs +++ b/capDL-tool/CapDL/ParserUtils.hs @@ -511,7 +511,6 @@ right = chr 'R' Read <|> chr 'W' Write <|> chr 'G' Grant - <|> chr 'X' Grant <|> chr 'P' GrantReply parse_rights :: MapParser CapRights @@ -600,6 +599,12 @@ cap_param = <|> do reserved "uncached" return $ Cached False + <|> do + reserved "executable" + return $ Executable True + <|> do + reserved "execute_never" + return $ Executable False <|> do reserved "mapping" colon diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index 17f3f3c8..da02723e 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -138,7 +138,7 @@ showCap _ (ARMIRQHandlerCap id) irqNode is_orig _ = ", .is_orig = " ++ is_orig ++ ", .irq = " ++ show (lookupByValue (== id) irqNode) ++ "}" -- Caps have obj_ids, or IRQs, but not both. -showCap objs (FrameCap id rights _ cached maybe_mapping) _ is_orig _ = +showCap objs (FrameCap id rights _ cached _ maybe_mapping) _ is_orig _ = "{.type = CDL_FrameCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ ", .rights = " ++ showRights rights ++ diff --git a/capDL-tool/CapDL/PrintIsabelle.hs b/capDL-tool/CapDL/PrintIsabelle.hs index acca1d2b..2dc48b85 100644 --- a/capDL-tool/CapDL/PrintIsabelle.hs +++ b/capDL-tool/CapDL/PrintIsabelle.hs @@ -254,12 +254,13 @@ printCap _ _ _ _ IRQControlCap = text "IrqControlCap" printCap _ irqNode _ _ (IRQHandlerCap id) = text "IrqHandlerCap" <+> num (fromJust (lookupElem id irqNode)) printCap _ _ _ _ DomainCap = text "DomainCap" -printCap ms _ _ real (FrameCap id rights asid cached _) = text "FrameCap" <+> +printCap ms _ _ real (FrameCap id rights asid cached executable _) = text "FrameCap" <+> -- is_device flag, assumed always false. FIXME: add to model? text "False" <+> printID id <+> printRights rights <+> printFrameSize id ms <+> printReal real <+> printMaybeAsid asid <+> - text (if cached then "" else isaComment "uncached") + text (if cached then "" else isaComment "uncached") <+> + text (if executable then "" else isaComment "execute_never") printCap _ _ _ real (PTCap id asid) = text "PageTableCap" <+> printID id <+> printReal real <+> printMaybeAsid asid diff --git a/capDL-tool/CapDL/PrintUtils.hs b/capDL-tool/CapDL/PrintUtils.hs index 41d8413f..de83cfe0 100644 --- a/capDL-tool/CapDL/PrintUtils.hs +++ b/capDL-tool/CapDL/PrintUtils.hs @@ -277,16 +277,15 @@ maybeNum t n = prettyParemNum t n maybeBadge = maybeNum "badge" -prettyRight _ Read = text "R" -prettyRight _ Write = text "W" -prettyRight True Grant = text "X" -prettyRight False Grant = text "G" -prettyRight _ GrantReply = text "P" +prettyRight Read = text "R" +prettyRight Write = text "W" +prettyRight Grant = text "G" +prettyRight GrantReply = text "P" -maybeRightsList _ [] = [] -maybeRightsList isFrame xs = [hcat (map (prettyRight isFrame) xs)] +maybeRightsList [] = [] +maybeRightsList xs = [hcat (map prettyRight xs)] -maybeRights isFrame r = maybeRightsList isFrame (Set.toList r) +maybeRights r = maybeRightsList (Set.toList r) maybeGuard = maybeNum "guard" maybeGSize = maybeNum "guard_size" @@ -312,17 +311,17 @@ maybeFrameMapping (Just mapping) = prettyFrameMapping mapping maybeCapParams :: Cap -> Doc maybeCapParams cap = case cap of EndpointCap _ badge rights -> - capParams (maybeBadge badge ++ maybeRights False rights) + capParams (maybeBadge badge ++ maybeRights rights) NotificationCap _ badge rights -> - capParams (maybeBadge badge ++ maybeRights False rights) + capParams (maybeBadge badge ++ maybeRights rights) ARMSMCCap _ badge -> capParams (maybeBadge badge) ReplyCap _ -> capParams [text "reply"] MasterReplyCap _ -> capParams [text "master_reply"] CNodeCap _ guard gsize -> capParams (maybeGuard guard ++ maybeGSize gsize) - FrameCap _ rights asid cached mapping -> capParams (maybeRights True rights ++ maybeAsid asid ++ - (if cached then [] else [text "uncached"]) ++ maybeFrameMapping mapping) + FrameCap _ rights asid cached executable mapping -> capParams (maybeRights rights ++ maybeAsid asid ++ + (if cached then [] else [text "uncached"]) ++ (if executable then [] else [text "execute_never"]) ++ maybeFrameMapping mapping) PTCap _ asid -> capParams (maybeAsid asid) PDCap _ asid -> capParams (maybeAsid asid) SchedControlCap core -> capParams (prettyCore core) @@ -351,7 +350,7 @@ sameParams cap1 cap2 = b1 == b2 ((CNodeCap _ g1 gs1), (CNodeCap _ g2 gs2)) -> g1 == g2 && gs1 == gs2 - ((FrameCap _ r1 a1 c1 m1), (FrameCap _ r2 a2 c2 m2)) -> r1 == r2 && a1 == a2 && c1 == c2 && m1 == m2 + ((FrameCap _ r1 a1 c1 e1 m1), (FrameCap _ r2 a2 c2 e2 m2)) -> r1 == r2 && a1 == a2 && c1 == c2 && e1 == e2 && m1 == m2 ((PTCap _ a1), (PTCap _ a2)) -> a1 == a2 ((PDCap _ a1), (PDCap _ a2)) -> a1 == a2 _ -> True diff --git a/capDL-tool/CapDL/PrintXml.hs b/capDL-tool/CapDL/PrintXml.hs index 42e3d9a3..35765844 100644 --- a/capDL-tool/CapDL/PrintXml.hs +++ b/capDL-tool/CapDL/PrintXml.hs @@ -170,7 +170,7 @@ showExtraCapAttributes (NotificationCap _ capBadge _) = [("badge", show capBadge showExtraCapAttributes (ARMSMCCap _ capBadge) = [("badge", show capBadge)] showExtraCapAttributes (CNodeCap _ guard guardSize) = [("guard", show guard), ("guardSize", show guardSize)] -showExtraCapAttributes (FrameCap _ _ _ False _) = [("cached", "False")] +showExtraCapAttributes (FrameCap _ _ _ cached executable _) = [ ("cached", "False") | not cached ] ++ [ ("executable", "False") | not executable ] showExtraCapAttributes _ = [] -- diff --git a/capDL-tool/CapDL/STCC.hs b/capDL-tool/CapDL/STCC.hs index ee51afaa..96b19732 100644 --- a/capDL-tool/CapDL/STCC.hs +++ b/capDL-tool/CapDL/STCC.hs @@ -32,7 +32,7 @@ projectEndpoint capset = projectNtfn capset = Set.fromList $ concat [[(r, capObj) | r <- Set.toList rights] | (NotificationCap capObj _ rights) <- Set.toList capset] projectFrame capset = - Set.fromList $ concat [[(r, capObj) | r <- Set.toList rights] | (FrameCap capObj rights Nothing True Nothing) <- Set.toList capset] + Set.fromList $ concat [[(r, capObj) | r <- Set.toList rights] | (FrameCap capObj rights Nothing True _ Nothing) <- Set.toList capset] somefn :: Model Word -> IO () somefn (Model _ objects _ _ _ _ _ _) = @@ -301,7 +301,7 @@ getFrames' objects visited cap = PTCap capObj _ | capObj `Set.member` visited -> [] | otherwise -> cap : getFrames'' objects visited capObj - FrameCap _ _ _ _ _ -> + FrameCap _ _ _ _ _ _ -> [cap] _ -> [] diff --git a/capDL-tool/CapDL/State.hs b/capDL-tool/CapDL/State.hs index d43bb872..3b312866 100644 --- a/capDL-tool/CapDL/State.hs +++ b/capDL-tool/CapDL/State.hs @@ -624,7 +624,7 @@ flattenCNodeSlots ((_, CNode slots _) : xs) = map snd (Map.toList slots) ++ flat flattenCNodeSlots (_ : xs) = flattenCNodeSlots xs isMappedFrameCap :: Cap -> Bool -isMappedFrameCap (FrameCap _ _ _ _ (Just _)) = True +isMappedFrameCap (FrameCap _ _ _ _ _ (Just _)) = True isMappedFrameCap _ = False -- Returns list containing each element in argument list occuring more than once. @@ -708,7 +708,7 @@ checkMappedFrameCapsOnlyInCNodes m = -- mapping to a frame. checkMappedFrameCaps :: Model Word -> Logger Bool checkMappedFrameCaps m = do - let mappings = map (\(FrameCap _ _ _ _ (Just x)) -> x) $ + let mappings = map (\(FrameCap _ _ _ _ _ (Just x)) -> x) $ filter isMappedFrameCap $ flattenCNodeSlots $ allObjs m no_duplicates <- checkDuplicateMappedFrameCaps mappings sane_mappings <- checkMappedFrameCapsSanity m mappings diff --git a/capDL-tool/camkes-adder-arm.cdl b/capDL-tool/camkes-adder-arm.cdl index 78575f91..27f0bcd5 100644 --- a/capDL-tool/camkes-adder-arm.cdl +++ b/capDL-tool/camkes-adder-arm.cdl @@ -266,31 +266,31 @@ client_group_bin_pd { 0x1: pt_client_group_bin_0003 } pt_adder_group_bin_0000 { -0x10: frame_adder_group_bin_0000 (RWX) -0x20: frame_adder_group_bin_0001 (RWX) -0x30: frame_adder_group_bin_0004 (RWX) -0x40: frame_adder_group_bin_0011 (RWX) -0x50: frame_adder_group_bin_0036 (RWX) -0x60: frame_adder_group_bin_0015 (RWX) -0x70: frame_adder_group_bin_0039 (RWX) -0x80: frame_adder_group_bin_0017 (RWX) -0x90: frame_adder_group_bin_0041 (RWX) -0xa0: frame_adder_group_bin_0019 (RWX) -0xb0: frame_adder_group_bin_0043 (RWX) -0xc0: frame_adder_group_bin_0021 (RWX) -0xd0: frame_adder_group_bin_0045 (RWX) -0xe0: frame_adder_group_bin_0023 (RWX) -0xf0: frame_adder_group_bin_0047 (RWX) +0x10: frame_adder_group_bin_0000 (RW) +0x20: frame_adder_group_bin_0001 (RW) +0x30: frame_adder_group_bin_0004 (RW) +0x40: frame_adder_group_bin_0011 (RW) +0x50: frame_adder_group_bin_0036 (RW) +0x60: frame_adder_group_bin_0015 (RW) +0x70: frame_adder_group_bin_0039 (RW) +0x80: frame_adder_group_bin_0017 (RW) +0x90: frame_adder_group_bin_0041 (RW) +0xa0: frame_adder_group_bin_0019 (RW) +0xb0: frame_adder_group_bin_0043 (RW) +0xc0: frame_adder_group_bin_0021 (RW) +0xd0: frame_adder_group_bin_0045 (RW) +0xe0: frame_adder_group_bin_0023 (RW) +0xf0: frame_adder_group_bin_0047 (RW) } pt_adder_group_bin_0003 { -0x0: frame_adder_group_bin_0025 (RWX) -0x10: frame_adder_group_bin_0049 (RWX) -0x20: frame_adder_group_bin_0027 (RWX) -0x30: frame_adder_group_bin_0002 (RWX) -0x40: frame_adder_group_bin_0029 (RWX) -0x41: frame_adder_group_bin_0013 (RWX) -0x42: frame_adder_group_bin_0014 (RWX) -0x43: frame_adder_group_bin_0016 (RWX) +0x0: frame_adder_group_bin_0025 (RW) +0x10: frame_adder_group_bin_0049 (RW) +0x20: frame_adder_group_bin_0027 (RW) +0x30: frame_adder_group_bin_0002 (RW) +0x40: frame_adder_group_bin_0029 (RW) +0x41: frame_adder_group_bin_0013 (RW) +0x42: frame_adder_group_bin_0014 (RW) +0x43: frame_adder_group_bin_0016 (RW) 0x45: stack__camkes_stack_adder_0_control_0_adder_obj (RW) 0x46: stack__camkes_stack_adder_0_control_1_adder_obj (RW) 0x47: stack__camkes_stack_adder_0_control_2_adder_obj (RW) @@ -306,30 +306,30 @@ pt_adder_group_bin_0003 { 0x59: stack__camkes_stack_adder_0_fault_handler_2_adder_obj (RW) 0x5a: stack__camkes_stack_adder_0_fault_handler_3_adder_obj (RW) 0x5d: adder_frame__camkes_ipc_buffer_adder_0_fault_handler (RW) -0x5f: s_data_0_obj (RWX, uncached) +0x5f: s_data_0_obj (RW, uncached, execute_never) } pt_client_group_bin_0000 { -0x10: frame_client_group_bin_0000 (RWX) -0x20: frame_client_group_bin_0001 (RWX) -0x30: frame_client_group_bin_0003 (RWX) -0x40: frame_client_group_bin_0004 (RWX) -0x50: frame_client_group_bin_0029 (RWX) -0x60: frame_client_group_bin_0008 (RWX) -0x70: frame_client_group_bin_0032 (RWX) -0x80: frame_client_group_bin_0010 (RWX) -0x90: frame_client_group_bin_0033 (RWX) -0xa0: frame_client_group_bin_0012 (RWX) -0xb0: frame_client_group_bin_0034 (RWX) -0xc0: frame_client_group_bin_0014 (RWX) -0xd0: frame_client_group_bin_0035 (RWX) -0xe0: frame_client_group_bin_0016 (RWX) -0xf0: frame_client_group_bin_0036 (RWX) +0x10: frame_client_group_bin_0000 (RW) +0x20: frame_client_group_bin_0001 (RW) +0x30: frame_client_group_bin_0003 (RW) +0x40: frame_client_group_bin_0004 (RW) +0x50: frame_client_group_bin_0029 (RW) +0x60: frame_client_group_bin_0008 (RW) +0x70: frame_client_group_bin_0032 (RW) +0x80: frame_client_group_bin_0010 (RW) +0x90: frame_client_group_bin_0033 (RW) +0xa0: frame_client_group_bin_0012 (RW) +0xb0: frame_client_group_bin_0034 (RW) +0xc0: frame_client_group_bin_0014 (RW) +0xd0: frame_client_group_bin_0035 (RW) +0xe0: frame_client_group_bin_0016 (RW) +0xf0: frame_client_group_bin_0036 (RW) } pt_client_group_bin_0003 { -0x0: frame_client_group_bin_0018 (RWX) -0x10: frame_client_group_bin_0037 (RWX) -0x20: frame_client_group_bin_0020 (RWX) -0x30: frame_client_group_bin_0002 (RWX) +0x0: frame_client_group_bin_0018 (RW) +0x10: frame_client_group_bin_0037 (RW) +0x20: frame_client_group_bin_0020 (RW) +0x30: frame_client_group_bin_0002 (RW) 0x41: stack__camkes_stack_client_0_control_0_client_obj (RW) 0x42: stack__camkes_stack_client_0_control_1_client_obj (RW) 0x43: stack__camkes_stack_client_0_control_2_client_obj (RW) @@ -340,7 +340,7 @@ pt_client_group_bin_0003 { 0x4c: stack__camkes_stack_client_0_fault_handler_2_client_obj (RW) 0x4d: stack__camkes_stack_client_0_fault_handler_3_client_obj (RW) 0x50: client_frame__camkes_ipc_buffer_client_0_fault_handler (RW) -0x52: s_data_0_obj (RWX, uncached) +0x52: s_data_0_obj (RW, uncached, execute_never) } } diff --git a/capDL-tool/camkes-adder-arm.right b/capDL-tool/camkes-adder-arm.right index c574bd64..e96a6382 100644 --- a/capDL-tool/camkes-adder-arm.right +++ b/capDL-tool/camkes-adder-arm.right @@ -265,32 +265,32 @@ objects { } pt_adder_group_bin_0000 { - 16: frame_adder_group_bin_0000 (RWX) - 32: frame_adder_group_bin_0001 (RWX) - 48: frame_adder_group_bin_0004 (RWX) - 64: frame_adder_group_bin_0011 (RWX) - 80: frame_adder_group_bin_0036 (RWX) - 96: frame_adder_group_bin_0015 (RWX) - 112: frame_adder_group_bin_0039 (RWX) - 128: frame_adder_group_bin_0017 (RWX) - 144: frame_adder_group_bin_0041 (RWX) - 160: frame_adder_group_bin_0019 (RWX) - 176: frame_adder_group_bin_0043 (RWX) - 192: frame_adder_group_bin_0021 (RWX) - 208: frame_adder_group_bin_0045 (RWX) - 224: frame_adder_group_bin_0023 (RWX) - 240: frame_adder_group_bin_0047 (RWX) + 16: frame_adder_group_bin_0000 (RW) + 32: frame_adder_group_bin_0001 (RW) + 48: frame_adder_group_bin_0004 (RW) + 64: frame_adder_group_bin_0011 (RW) + 80: frame_adder_group_bin_0036 (RW) + 96: frame_adder_group_bin_0015 (RW) + 112: frame_adder_group_bin_0039 (RW) + 128: frame_adder_group_bin_0017 (RW) + 144: frame_adder_group_bin_0041 (RW) + 160: frame_adder_group_bin_0019 (RW) + 176: frame_adder_group_bin_0043 (RW) + 192: frame_adder_group_bin_0021 (RW) + 208: frame_adder_group_bin_0045 (RW) + 224: frame_adder_group_bin_0023 (RW) + 240: frame_adder_group_bin_0047 (RW) } pt_adder_group_bin_0003 { - 0: frame_adder_group_bin_0025 (RWX) - 16: frame_adder_group_bin_0049 (RWX) - 32: frame_adder_group_bin_0027 (RWX) - 48: frame_adder_group_bin_0002 (RWX) - 64: frame_adder_group_bin_0029 (RWX) - 65: frame_adder_group_bin_0013 (RWX) - 66: frame_adder_group_bin_0014 (RWX) - 67: frame_adder_group_bin_0016 (RWX) + 0: frame_adder_group_bin_0025 (RW) + 16: frame_adder_group_bin_0049 (RW) + 32: frame_adder_group_bin_0027 (RW) + 48: frame_adder_group_bin_0002 (RW) + 64: frame_adder_group_bin_0029 (RW) + 65: frame_adder_group_bin_0013 (RW) + 66: frame_adder_group_bin_0014 (RW) + 67: frame_adder_group_bin_0016 (RW) 69: stack__camkes_stack_adder_0_control_0_adder_obj (RW) 70: stack__camkes_stack_adder_0_control_1_adder_obj (RW) 71: stack__camkes_stack_adder_0_control_2_adder_obj (RW) @@ -306,32 +306,32 @@ objects { 89: stack__camkes_stack_adder_0_fault_handler_2_adder_obj (RW) 90: stack__camkes_stack_adder_0_fault_handler_3_adder_obj (RW) 93: adder_frame__camkes_ipc_buffer_adder_0_fault_handler (RW) - 95: s_data_0_obj (RWX, uncached) + 95: s_data_0_obj (RW, uncached, execute_never) } pt_client_group_bin_0000 { - 16: frame_client_group_bin_0000 (RWX) - 32: frame_client_group_bin_0001 (RWX) - 48: frame_client_group_bin_0003 (RWX) - 64: frame_client_group_bin_0004 (RWX) - 80: frame_client_group_bin_0029 (RWX) - 96: frame_client_group_bin_0008 (RWX) - 112: frame_client_group_bin_0032 (RWX) - 128: frame_client_group_bin_0010 (RWX) - 144: frame_client_group_bin_0033 (RWX) - 160: frame_client_group_bin_0012 (RWX) - 176: frame_client_group_bin_0034 (RWX) - 192: frame_client_group_bin_0014 (RWX) - 208: frame_client_group_bin_0035 (RWX) - 224: frame_client_group_bin_0016 (RWX) - 240: frame_client_group_bin_0036 (RWX) + 16: frame_client_group_bin_0000 (RW) + 32: frame_client_group_bin_0001 (RW) + 48: frame_client_group_bin_0003 (RW) + 64: frame_client_group_bin_0004 (RW) + 80: frame_client_group_bin_0029 (RW) + 96: frame_client_group_bin_0008 (RW) + 112: frame_client_group_bin_0032 (RW) + 128: frame_client_group_bin_0010 (RW) + 144: frame_client_group_bin_0033 (RW) + 160: frame_client_group_bin_0012 (RW) + 176: frame_client_group_bin_0034 (RW) + 192: frame_client_group_bin_0014 (RW) + 208: frame_client_group_bin_0035 (RW) + 224: frame_client_group_bin_0016 (RW) + 240: frame_client_group_bin_0036 (RW) } pt_client_group_bin_0003 { - 0: frame_client_group_bin_0018 (RWX) - 16: frame_client_group_bin_0037 (RWX) - 32: frame_client_group_bin_0020 (RWX) - 48: frame_client_group_bin_0002 (RWX) + 0: frame_client_group_bin_0018 (RW) + 16: frame_client_group_bin_0037 (RW) + 32: frame_client_group_bin_0020 (RW) + 48: frame_client_group_bin_0002 (RW) 65: stack__camkes_stack_client_0_control_0_client_obj (RW) 66: stack__camkes_stack_client_0_control_1_client_obj (RW) 67: stack__camkes_stack_client_0_control_2_client_obj (RW) @@ -342,7 +342,7 @@ objects { 76: stack__camkes_stack_client_0_fault_handler_2_client_obj (RW) 77: stack__camkes_stack_client_0_fault_handler_3_client_obj (RW) 80: client_frame__camkes_ipc_buffer_client_0_fault_handler (RW) - 82: s_data_0_obj (RWX, uncached) + 82: s_data_0_obj (RW, uncached, execute_never) } } cdt { diff --git a/capDL-tool/camkes-adder-arm.thy.right b/capDL-tool/camkes-adder-arm.thy.right index cb8db3c7..3a1aa308 100644 --- a/capDL-tool/camkes-adder-arm.thy.right +++ b/capDL-tool/camkes-adder-arm.thy.right @@ -702,21 +702,21 @@ lemma client_client_0_fault_handler_tcb_object_slots: by (simp add: client_client_0_fault_handler_tcb_def object_slots_def) definition pt_adder_group_bin_0000_caps :: "cdl_cap_map" where -"pt_adder_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_adder_group_bin_0000_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_adder_group_bin_0001_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_adder_group_bin_0004_id {Read, Write, Grant} 16 Fake None , - 64 \ Types_D.FrameCap False frame_adder_group_bin_0011_id {Read, Write, Grant} 16 Fake None , - 80 \ Types_D.FrameCap False frame_adder_group_bin_0036_id {Read, Write, Grant} 16 Fake None , - 96 \ Types_D.FrameCap False frame_adder_group_bin_0015_id {Read, Write, Grant} 16 Fake None , - 112 \ Types_D.FrameCap False frame_adder_group_bin_0039_id {Read, Write, Grant} 16 Fake None , - 128 \ Types_D.FrameCap False frame_adder_group_bin_0017_id {Read, Write, Grant} 16 Fake None , - 144 \ Types_D.FrameCap False frame_adder_group_bin_0041_id {Read, Write, Grant} 16 Fake None , - 160 \ Types_D.FrameCap False frame_adder_group_bin_0019_id {Read, Write, Grant} 16 Fake None , - 176 \ Types_D.FrameCap False frame_adder_group_bin_0043_id {Read, Write, Grant} 16 Fake None , - 192 \ Types_D.FrameCap False frame_adder_group_bin_0021_id {Read, Write, Grant} 16 Fake None , - 208 \ Types_D.FrameCap False frame_adder_group_bin_0045_id {Read, Write, Grant} 16 Fake None , - 224 \ Types_D.FrameCap False frame_adder_group_bin_0023_id {Read, Write, Grant} 16 Fake None , - 240 \ Types_D.FrameCap False frame_adder_group_bin_0047_id {Read, Write, Grant} 16 Fake None ]" +"pt_adder_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_adder_group_bin_0000_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_adder_group_bin_0001_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_adder_group_bin_0004_id {Read, Write} 16 Fake None , + 64 \ Types_D.FrameCap False frame_adder_group_bin_0011_id {Read, Write} 16 Fake None , + 80 \ Types_D.FrameCap False frame_adder_group_bin_0036_id {Read, Write} 16 Fake None , + 96 \ Types_D.FrameCap False frame_adder_group_bin_0015_id {Read, Write} 16 Fake None , + 112 \ Types_D.FrameCap False frame_adder_group_bin_0039_id {Read, Write} 16 Fake None , + 128 \ Types_D.FrameCap False frame_adder_group_bin_0017_id {Read, Write} 16 Fake None , + 144 \ Types_D.FrameCap False frame_adder_group_bin_0041_id {Read, Write} 16 Fake None , + 160 \ Types_D.FrameCap False frame_adder_group_bin_0019_id {Read, Write} 16 Fake None , + 176 \ Types_D.FrameCap False frame_adder_group_bin_0043_id {Read, Write} 16 Fake None , + 192 \ Types_D.FrameCap False frame_adder_group_bin_0021_id {Read, Write} 16 Fake None , + 208 \ Types_D.FrameCap False frame_adder_group_bin_0045_id {Read, Write} 16 Fake None , + 224 \ Types_D.FrameCap False frame_adder_group_bin_0023_id {Read, Write} 16 Fake None , + 240 \ Types_D.FrameCap False frame_adder_group_bin_0047_id {Read, Write} 16 Fake None ]" definition pt_adder_group_bin_0000 :: "cdl_object" where "pt_adder_group_bin_0000 \ Types_D.PageTable \ cdl_page_table_caps = pt_adder_group_bin_0000_caps \" @@ -726,14 +726,14 @@ lemma pt_adder_group_bin_0000_object_slots: by (simp add: pt_adder_group_bin_0000_def object_slots_def) definition pt_adder_group_bin_0003_caps :: "cdl_cap_map" where -"pt_adder_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_adder_group_bin_0025_id {Read, Write, Grant} 16 Fake None , - 16 \ Types_D.FrameCap False frame_adder_group_bin_0049_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_adder_group_bin_0027_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_adder_group_bin_0002_id {Read, Write, Grant} 16 Fake None , - 64 \ Types_D.FrameCap False frame_adder_group_bin_0029_id {Read, Write, Grant} 12 Fake None , - 65 \ Types_D.FrameCap False frame_adder_group_bin_0013_id {Read, Write, Grant} 12 Fake None , - 66 \ Types_D.FrameCap False frame_adder_group_bin_0014_id {Read, Write, Grant} 12 Fake None , - 67 \ Types_D.FrameCap False frame_adder_group_bin_0016_id {Read, Write, Grant} 12 Fake None , +"pt_adder_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_adder_group_bin_0025_id {Read, Write} 16 Fake None , + 16 \ Types_D.FrameCap False frame_adder_group_bin_0049_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_adder_group_bin_0027_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_adder_group_bin_0002_id {Read, Write} 16 Fake None , + 64 \ Types_D.FrameCap False frame_adder_group_bin_0029_id {Read, Write} 12 Fake None , + 65 \ Types_D.FrameCap False frame_adder_group_bin_0013_id {Read, Write} 12 Fake None , + 66 \ Types_D.FrameCap False frame_adder_group_bin_0014_id {Read, Write} 12 Fake None , + 67 \ Types_D.FrameCap False frame_adder_group_bin_0016_id {Read, Write} 12 Fake None , 69 \ Types_D.FrameCap False stack__camkes_stack_adder_0_control_0_adder_obj_id {Read, Write} 12 Fake None , 70 \ Types_D.FrameCap False stack__camkes_stack_adder_0_control_1_adder_obj_id {Read, Write} 12 Fake None , 71 \ Types_D.FrameCap False stack__camkes_stack_adder_0_control_2_adder_obj_id {Read, Write} 12 Fake None , @@ -749,7 +749,7 @@ definition pt_adder_group_bin_0003_caps :: "cdl_cap_map" where 89 \ Types_D.FrameCap False stack__camkes_stack_adder_0_fault_handler_2_adder_obj_id {Read, Write} 12 Fake None , 90 \ Types_D.FrameCap False stack__camkes_stack_adder_0_fault_handler_3_adder_obj_id {Read, Write} 12 Fake None , 93 \ Types_D.FrameCap False adder_frame__camkes_ipc_buffer_adder_0_fault_handler_id {Read, Write} 12 Fake None , - 95 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write, Grant} 12 Fake None \ \uncached\]" + 95 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write} 12 Fake None \ \uncached\ \ \execute_never\]" definition pt_adder_group_bin_0003 :: "cdl_object" where "pt_adder_group_bin_0003 \ Types_D.PageTable \ cdl_page_table_caps = pt_adder_group_bin_0003_caps \" @@ -759,21 +759,21 @@ lemma pt_adder_group_bin_0003_object_slots: by (simp add: pt_adder_group_bin_0003_def object_slots_def) definition pt_client_group_bin_0000_caps :: "cdl_cap_map" where -"pt_client_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_client_group_bin_0000_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_client_group_bin_0001_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_client_group_bin_0003_id {Read, Write, Grant} 16 Fake None , - 64 \ Types_D.FrameCap False frame_client_group_bin_0004_id {Read, Write, Grant} 16 Fake None , - 80 \ Types_D.FrameCap False frame_client_group_bin_0029_id {Read, Write, Grant} 16 Fake None , - 96 \ Types_D.FrameCap False frame_client_group_bin_0008_id {Read, Write, Grant} 16 Fake None , - 112 \ Types_D.FrameCap False frame_client_group_bin_0032_id {Read, Write, Grant} 16 Fake None , - 128 \ Types_D.FrameCap False frame_client_group_bin_0010_id {Read, Write, Grant} 16 Fake None , - 144 \ Types_D.FrameCap False frame_client_group_bin_0033_id {Read, Write, Grant} 16 Fake None , - 160 \ Types_D.FrameCap False frame_client_group_bin_0012_id {Read, Write, Grant} 16 Fake None , - 176 \ Types_D.FrameCap False frame_client_group_bin_0034_id {Read, Write, Grant} 16 Fake None , - 192 \ Types_D.FrameCap False frame_client_group_bin_0014_id {Read, Write, Grant} 16 Fake None , - 208 \ Types_D.FrameCap False frame_client_group_bin_0035_id {Read, Write, Grant} 16 Fake None , - 224 \ Types_D.FrameCap False frame_client_group_bin_0016_id {Read, Write, Grant} 16 Fake None , - 240 \ Types_D.FrameCap False frame_client_group_bin_0036_id {Read, Write, Grant} 16 Fake None ]" +"pt_client_group_bin_0000_caps \ [16 \ Types_D.FrameCap False frame_client_group_bin_0000_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_client_group_bin_0001_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_client_group_bin_0003_id {Read, Write} 16 Fake None , + 64 \ Types_D.FrameCap False frame_client_group_bin_0004_id {Read, Write} 16 Fake None , + 80 \ Types_D.FrameCap False frame_client_group_bin_0029_id {Read, Write} 16 Fake None , + 96 \ Types_D.FrameCap False frame_client_group_bin_0008_id {Read, Write} 16 Fake None , + 112 \ Types_D.FrameCap False frame_client_group_bin_0032_id {Read, Write} 16 Fake None , + 128 \ Types_D.FrameCap False frame_client_group_bin_0010_id {Read, Write} 16 Fake None , + 144 \ Types_D.FrameCap False frame_client_group_bin_0033_id {Read, Write} 16 Fake None , + 160 \ Types_D.FrameCap False frame_client_group_bin_0012_id {Read, Write} 16 Fake None , + 176 \ Types_D.FrameCap False frame_client_group_bin_0034_id {Read, Write} 16 Fake None , + 192 \ Types_D.FrameCap False frame_client_group_bin_0014_id {Read, Write} 16 Fake None , + 208 \ Types_D.FrameCap False frame_client_group_bin_0035_id {Read, Write} 16 Fake None , + 224 \ Types_D.FrameCap False frame_client_group_bin_0016_id {Read, Write} 16 Fake None , + 240 \ Types_D.FrameCap False frame_client_group_bin_0036_id {Read, Write} 16 Fake None ]" definition pt_client_group_bin_0000 :: "cdl_object" where "pt_client_group_bin_0000 \ Types_D.PageTable \ cdl_page_table_caps = pt_client_group_bin_0000_caps \" @@ -783,10 +783,10 @@ lemma pt_client_group_bin_0000_object_slots: by (simp add: pt_client_group_bin_0000_def object_slots_def) definition pt_client_group_bin_0003_caps :: "cdl_cap_map" where -"pt_client_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_client_group_bin_0018_id {Read, Write, Grant} 16 Fake None , - 16 \ Types_D.FrameCap False frame_client_group_bin_0037_id {Read, Write, Grant} 16 Fake None , - 32 \ Types_D.FrameCap False frame_client_group_bin_0020_id {Read, Write, Grant} 16 Fake None , - 48 \ Types_D.FrameCap False frame_client_group_bin_0002_id {Read, Write, Grant} 16 Fake None , +"pt_client_group_bin_0003_caps \ [0 \ Types_D.FrameCap False frame_client_group_bin_0018_id {Read, Write} 16 Fake None , + 16 \ Types_D.FrameCap False frame_client_group_bin_0037_id {Read, Write} 16 Fake None , + 32 \ Types_D.FrameCap False frame_client_group_bin_0020_id {Read, Write} 16 Fake None , + 48 \ Types_D.FrameCap False frame_client_group_bin_0002_id {Read, Write} 16 Fake None , 65 \ Types_D.FrameCap False stack__camkes_stack_client_0_control_0_client_obj_id {Read, Write} 12 Fake None , 66 \ Types_D.FrameCap False stack__camkes_stack_client_0_control_1_client_obj_id {Read, Write} 12 Fake None , 67 \ Types_D.FrameCap False stack__camkes_stack_client_0_control_2_client_obj_id {Read, Write} 12 Fake None , @@ -797,7 +797,7 @@ definition pt_client_group_bin_0003_caps :: "cdl_cap_map" where 76 \ Types_D.FrameCap False stack__camkes_stack_client_0_fault_handler_2_client_obj_id {Read, Write} 12 Fake None , 77 \ Types_D.FrameCap False stack__camkes_stack_client_0_fault_handler_3_client_obj_id {Read, Write} 12 Fake None , 80 \ Types_D.FrameCap False client_frame__camkes_ipc_buffer_client_0_fault_handler_id {Read, Write} 12 Fake None , - 82 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write, Grant} 12 Fake None \ \uncached\]" + 82 \ Types_D.FrameCap False s_data_0_obj_id {Read, Write} 12 Fake None \ \uncached\ \ \execute_never\]" definition pt_client_group_bin_0003 :: "cdl_object" where "pt_client_group_bin_0003 \ Types_D.PageTable \ cdl_page_table_caps = pt_client_group_bin_0003_caps \" diff --git a/capDL-tool/cap-dist-elf-simpleserver.cdl b/capDL-tool/cap-dist-elf-simpleserver.cdl index e24d3268..d09968b1 100644 --- a/capDL-tool/cap-dist-elf-simpleserver.cdl +++ b/capDL-tool/cap-dist-elf-simpleserver.cdl @@ -24,7 +24,7 @@ cnode { tcb ep (RWG) cnode (guard: 0, guard_size: 28) - frame[5] (RWG) + frame[5] (RW) } ap { pd1 } @@ -32,7 +32,7 @@ ap { pd1 } pd1 { 0: pt1 } pt1 { - 0x10: frame[] (RWG) + 0x10: frame[] (RW) } cnode2 { 5: cnode (guard: 1, guard_size: 28) } @@ -40,6 +40,6 @@ cnode2 { 5: cnode (guard: 1, guard_size: 28) } tcb { cspace: cnode2 (guard: 0, guard_size: 28) vspace: pd1 - ipc_buffer_slot: frame[5] (RWG) + ipc_buffer_slot: frame[5] (RW) } } diff --git a/capDL-tool/cap-dist-elf-simpleserver.right b/capDL-tool/cap-dist-elf-simpleserver.right index a0798f88..c2fba984 100644 --- a/capDL-tool/cap-dist-elf-simpleserver.right +++ b/capDL-tool/cap-dist-elf-simpleserver.right @@ -20,19 +20,19 @@ objects { 0: tcb 1: ep (RWG) 2: cnode (guard_size: 28) - 3: frame[5] (RWX) + 3: frame[5] (RW) } cnode2 {5: cnode (guard: 1, guard_size: 28)} pd1 {0: pt1} - pt1 {16: frame[0..5] (RWX)} + pt1 {16: frame[0..5] (RW)} tcb { 0: cnode2 (guard_size: 28) 1: pd1 - 4: frame[5] (RWX) + 4: frame[5] (RW) } } cdt { diff --git a/capDL-tool/capdl.dtd b/capDL-tool/capdl.dtd index 88aa2a42..b9998ac8 100644 --- a/capDL-tool/capdl.dtd +++ b/capDL-tool/capdl.dtd @@ -30,6 +30,7 @@ + diff --git a/capDL-tool/doc/capDL.md b/capDL-tool/doc/capDL.md index 09063fb6..c8b42557 100644 --- a/capDL-tool/doc/capDL.md +++ b/capDL-tool/doc/capDL.md @@ -128,8 +128,10 @@ in section [Modules](#modules). | 'asid' ':' asid | 'cached' | 'uncached' + | 'executable' + | 'execute_never' - right ::= 'R' | 'W' | 'G' | 'X' + right ::= 'R' | 'W' | 'G' | 'P' asid ::= '(' number ',' number ')' parent ::= '- child_of' slot_ref diff --git a/capDL-tool/tools/capdl.vim b/capDL-tool/tools/capdl.vim index 8f727393..fe2b96f7 100644 --- a/capDL-tool/tools/capdl.vim +++ b/capDL-tool/tools/capdl.vim @@ -20,7 +20,7 @@ syn keyword CapDLKeyword arch caps objects arm11 ia32 syn match CapDLIRQMap "\" syn match CapDLIRQ "\\( maps\)\@!" syn keyword CapDLObject notification asid_pool cnode ep frame io_device io_ports io_pt pd pt tcb ut -syn keyword CapDLAttribute addr affinity badge dom fault_ep G guard guard_size init ip max_prio prio sp R RG RX RW RWG RWX W WG WX paddr cached uncached +syn keyword CapDLAttribute addr affinity badge dom fault_ep G guard guard_size init ip max_prio prio sp R RG RX RW RWG W WG WX paddr cached uncached execute execute_never syn match CapDLCPP "[ \t]*#.*$" syn match CapDLLiteral "\<\(0x\)\?[0-9]\+\(k\|M\)\?\( bits\)\?\>" syn match CapDLLiteral "\<0x[0-f]\+\>" diff --git a/python-capdl-tool/capdl/Cap.py b/python-capdl-tool/capdl/Cap.py index 89965331..51be28cd 100644 --- a/python-capdl-tool/capdl/Cap.py +++ b/python-capdl-tool/capdl/Cap.py @@ -27,6 +27,7 @@ def __init__(self, referent, **kwargs): self.guard_size = 0 self.badge = None self.cached = True + self.executable = True self.ports = None self.mapping_container = None self.mapping_slot = None @@ -92,14 +93,15 @@ def __repr__(self): rights = [sym for sym, flag in [('R', self.read), ('W', self.write), - ('X', is_frame and self.grant), - ('G', not is_frame and self.grant), + ('G', self.grant), ('P', self.grantreply)] if flag] extra.append(''.join(rights)) if isinstance(self.referent, Frame) and not self.cached: extra.append('uncached') + if isinstance(self.referent, Frame) and not self.executable: + extra.append('execute_never') if isinstance(self.referent, Frame) and \ self.mapping_container is not None: extra.append('mapping: (%s, %d)' % (self.mapping_container.name, self.mapping_slot)) diff --git a/python-capdl-tool/capdl/PageCollection.py b/python-capdl-tool/capdl/PageCollection.py index 2be2fc5a..5c239cd1 100644 --- a/python-capdl-tool/capdl/PageCollection.py +++ b/python-capdl-tool/capdl/PageCollection.py @@ -86,7 +86,7 @@ def _get_page_cap(self, existing_frames, page, page_vaddr, page_counter, spec): page['size']) spec.add_object(frame) return Cap(frame, read=page['read'], write=page['write'], - grant=page['execute']) + executable=page['execute']) def get_spec(self, existing_frames={}): if self._spec is not None: