smmuv2: Add ability to specify sid and cb numbers in a cdl file

capDL-tool/CapDL/AST.hs

@@ -58,6 +58,11 @@ data SCExtraParam =
       scData :: Word }
    deriving (Show, Eq, Ord, Typeable, Data)
 
+data SIDExtraParam =
+    SIDNumber {
+    sidNumber :: Word }
+    deriving (Eq, Show, Ord, Typeable, Data)
+
 data CBExtraParam = 
     CBNumber {
     cbNumber :: Word }
@@ -107,6 +112,8 @@ data ObjParam =
       frameExtraParam :: FrameExtraParam}
   | SCExtraParam {
       sc_extraParam :: SCExtraParam }
+  | SIDExtraParam {
+      sid_extraParam :: SIDExtraParam }
   | CBExtraParam {
       cb_extraParam :: CBExtraParam }
   | IOAPICIRQExtraParam {

capDL-tool/CapDL/MakeModel.hs

@@ -273,6 +273,11 @@ getSCData [] = Nothing
 getSCData (SCExtraParam (SCData scData) : _) = Just scData
 getSCData (_ : xs) = getSCData xs
 
+getSIDExtraInfo :: [ObjParam] -> Maybe Word
+getSIDExtraInfo [] = Nothing
+getSIDExtraInfo (SIDExtraParam (SIDNumber x) : _) = Just x
+getSIDExtraInfo (_ : xs) = getSIDExtraInfo xs
+
 getCBExtraInfo :: [ObjParam] -> Maybe Word
 getCBExtraInfo [] = Nothing
 getCBExtraInfo (CBExtraParam (CBNumber x) : _) = Just x
@@ -435,6 +440,8 @@ validObjPars (Obj MSIIrqSlot_T ps []) =
   subsetConstrs ps (replicate (numConstrs (Addr undefined)) (MSIIRQExtraParam undefined))
 validObjPars (Obj ARMIrqSlot_T ps []) =
   subsetConstrs ps (replicate (numConstrs (Addr undefined)) (ARMIRQExtraParam undefined))
+validObjPars (Obj ARMSID_T ps []) =
+  subsetConstrs ps (replicate (numConstrs (Addr undefined)) (SIDExtraParam undefined))
 validObjPars (Obj ARMCB_T ps []) =
   subsetConstrs ps (replicate (numConstrs (Addr undefined)) (CBExtraParam undefined))
 validObjPars obj = null (params obj)
@@ -477,7 +484,7 @@ objectOf n obj =
         Obj VCPU_T [] [] -> VCPU
         Obj SC_T ps [] -> SC (getSCExtraInfo n ps) (getMaybeBitSize ps)
         Obj RTReply_T [] [] -> RTReply
-        Obj ARMSID_T [] [] -> ARMSID
+        Obj ARMSID_T ps [] -> ARMSID (getSIDExtraInfo ps)
         Obj ARMCB_T ps [] -> ARMCB (getCBExtraInfo ps)
         Obj _ _ (_:_) ->
           error $ "Only untyped caps can have objects as content: " ++

capDL-tool/CapDL/Model.hs

@@ -206,7 +206,7 @@ data KernelObject a
         target :: Word }
 
 -- fake kernel objects for smmu
-    | ARMSID
+    | ARMSID { sidNumber :: Maybe Word }
     | ARMCB { bankNumber :: Maybe Word }
 
 -- X86 specific objects

capDL-tool/CapDL/ParserUtils.hs

@@ -278,6 +278,13 @@ sc_period = do
     n <- integer64
     return $ Period n
 
+sid_number :: MapParser SIDExtraParam
+sid_number = do
+    reserved "sid"
+    colon
+    n <- number
+    return $ SIDNumber n
+
 cb_number :: MapParser CBExtraParam
 cb_number = do
     reserved "bank"
@@ -306,6 +313,11 @@ sc_extra_param = do
             <|> sc_data)
     return $ SCExtraParam param
 
+sid_extra_param :: MapParser ObjParam
+sid_extra_param = do
+    param <- sid_number
+    return $ SIDExtraParam param
+
 cb_extra_param :: MapParser ObjParam
 cb_extra_param = do
     param <- cb_number
@@ -457,6 +469,7 @@ object_param =
     <|> arm_irq_extra_param
     <|> ports_param
     <|> asid_high_param
+    <|> sid_extra_param
     <|> cb_extra_param
 
 object_params :: MapParser [ObjParam]

capDL-tool/CapDL/PrintC.hs

@@ -377,8 +377,24 @@ showObjectFields _ _ (SC info size_bits) _ _ _ =
     sc_data   = fromMaybe 0 (maybe Nothing scData info)
     sizeBits  = fromMaybe 0 size_bits
 showObjectFields _ _ (RTReply {}) _ _ _ = ".type = CDL_RTReply,"
-showObjectFields _ _ (ARMSID {}) _ _ _ = ".type = CDL_SID,"
-showObjectFields _ _ (ARMCB {}) _ _ _ = ".type = CDL_CB,"
+showObjectFields _ _ (ARMSID sid_number) _ _ _ =
+    ".type = CDL_SID," +++
+    ".sid_extra = {" +++
+        ".sid = " ++ show (sid) +++
+    "}"
+    where
+    sid = case sid_number of
+        Just num -> num
+        _ -> 0
+showObjectFields _ _ (ARMCB cb_number) _ _ _ =
+    ".type = CDL_CB," +++
+    ".cb_extra = {" +++
+        ".bank = " ++ show (bank) +++
+    "}"
+    where
+    bank = case cb_number of
+        Just num -> num
+        _ -> 0
 showObjectFields _ _ x _ _ _ = assert False $
     "UNSUPPORTED OBJECT TYPE: " ++ show x
 

capdl-loader-app/include/capdl.h

@@ -279,6 +279,10 @@ typedef struct {
     seL4_Word data;
 } CDL_SCExtraInfo;
 
+typedef struct {
+    uint32_t sid;
+} CDL_SIDExtraInfo;
+
 typedef struct {
     uint8_t bank;
 } CDL_CBExtraInfo;
@@ -353,6 +357,7 @@ typedef struct {
         CDL_TCBExtraInfo tcb_extra;
         CDL_SCExtraInfo sc_extra;
         CDL_CBExtraInfo cb_extra;
+        CDL_SIDExtraInfo sid_extra;
         CDL_IOAPICIRQExtraInfo ioapicirq_extra;
         CDL_MSIIRQExtraInfo msiirq_extra;
         CDL_ARMIRQExtraInfo armirq_extra;
@@ -526,6 +531,11 @@ static inline uint8_t CDL_TCB_Priority(CDL_Object *obj)
     return obj->tcb_extra.priority;
 }
 
+static inline uint32_t CDL_SID_Sid(CDL_Object *obj)
+{
+    return obj->sid_extra.sid;
+}
+
 static inline uint8_t CDL_CB_Bank(CDL_Object *obj)
 {
     return obj->cb_extra.bank;

capdl-loader-app/src/main.c

@@ -52,8 +52,6 @@
 
 #define STACK_ALIGNMENT_BYTES 16
 
-#define MAX_STREAM_IDS 60
-
 static seL4_CPtr capdl_to_sel4_orig[CONFIG_CAPDL_LOADER_MAX_OBJECTS];
 static seL4_CPtr capdl_to_sel4_copy[CONFIG_CAPDL_LOADER_MAX_OBJECTS];
 static seL4_CPtr capdl_to_sel4_irq[CONFIG_CAPDL_LOADER_MAX_OBJECTS];
@@ -82,7 +80,6 @@ extern char _end[];
  * This is expected to be initialised by 'init_copy_addr' on system init */
 uintptr_t copy_addr;
 
-uint32_t sid_number = 0;
 /* In the case where we just want a 4K page and we cannot allocate
  * a page table ourselves, we use this pre allocated region that
  * is guaranteed to have a pagetable */
@@ -648,17 +645,14 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_
      */
 #ifdef CONFIG_ARM_SMMU
     if (CDL_Obj_Type(obj) == CDL_SID) {
-        err = seL4_ARM_SIDControl_GetSID(seL4_CapSMMUSIDControl, sid_number, seL4_CapInitThreadCNode, free_slot,
+        err = seL4_ARM_SIDControl_GetSID(seL4_CapSMMUSIDControl, CDL_SID_Sid(obj), seL4_CapInitThreadCNode, free_slot,
                                          CONFIG_WORD_SIZE);
         ZF_LOGF_IF(err != seL4_NoError, "Failed to allocate SID cap");
-        sid_number++;
-        ZF_LOGF_IF(sid_number > MAX_STREAM_IDS, "Stream ID numbers exhausted");
         return seL4_NoError;
     } else if (CDL_Obj_Type(obj) == CDL_CB) {
         err = seL4_ARM_CBControl_GetCB(seL4_CapSMMUCBControl, CDL_CB_Bank(obj), seL4_CapInitThreadCNode, free_slot,
                                        CONFIG_WORD_SIZE);
         ZF_LOGF_IF(err != seL4_NoError, "Failed to allocate CB cap");
-        sid_number = 0; //(1***)
         return seL4_NoError;
     }
 #endif

python-capdl-tool/capdl/Allocator.py

@@ -165,9 +165,9 @@ def alloc(self, type, name=None, label=None, **kwargs):
         elif type == ObjectType.seL4_RTReplyObject:
             o = RTReply(name)
         elif type == ObjectType.seL4_ARMSID:
-            o = StreamID(name)
+            o = StreamID(name, **kwargs)
         elif type == ObjectType.seL4_ARMCB:
-            o = ContextBank(name)
+            o = ContextBank(name, **kwargs)
         else:
             raise Exception('Invalid object type %s' % type)
         self.spec.add_object(o)

python-capdl-tool/capdl/Object.py

@@ -640,26 +640,26 @@ def get_size_bits(self):
 
 
 class StreamID(Object):
-    def __init__(self, name):
+    def __init__(self, name, streamid=0):
         super().__init__(name)
 
+        self.sid = streamid
+
     def __repr__(self):
-        return '%s = streamid' % self.name
+        return '%s = streamid (sid: %d)' % (self.name, self.sid)
 
     def get_size_bits(self):
         return None
 
 
 class ContextBank(Object):
-    def __init__(self, name):
+    def __init__(self, name, bank=0):
         super().__init__(name)
 
-        # Assignment of context bank numbers will evolve with use case
-        self.bank = 0
+        self.bank = bank
 
     def __repr__(self):
         s = '%s = contextbank (bank: %d)' % (self.name, self.bank)
-        self.bank += 1
         return s
 
     def get_size_bits(self):