Add support for XN vm attributes

capDL-tool/CapDL/AST.hs

@@ -166,6 +166,8 @@ data CapParam
         asid :: Asid }
     | Cached {
         cached :: Bool }
+    | Executable {
+        executable :: Bool }
     | FrameMapping {
         container :: NameRef,
         slotIndex :: Word }

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)

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,

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

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 ++

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

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

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 _ = []
 
 --

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]
     _ -> []
 

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

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)
 }
 }