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

.reuse/dep5

@@ -19,3 +19,9 @@ Files:
   object_sizes/object_sizes.yaml
 Copyright: 2020, Data61, CSIRO (ABN 41 687 119 230)
 License: BSD-2-Clause
+
+Files:
+  VERSION
+  capDL-tool/example-aarch64-smmu.right
+Copyright: 2026, DornerWorks
+License: BSD-2-Clause

capDL-tool/CapDL/AST.hs

@@ -60,6 +60,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 }
@@ -109,6 +114,8 @@ data ObjParam =
       frameExtraParam :: FrameExtraParam}
   | SCExtraParam {
       sc_extraParam :: SCExtraParam }
+  | SIDExtraParam {
+      sid_extraParam :: SIDExtraParam }
   | CBExtraParam {
       cb_extraParam :: CBExtraParam }
   | IOAPICIRQExtraParam {

capDL-tool/CapDL/MakeModel.hs

@@ -278,6 +278,11 @@ getSCData [] = Nothing
 getSCData (SCExtraParam (SCData scData) : _) = Just scData
 getSCData (_ : xs) = getSCData xs
 
+getSIDExtraInfo :: Name -> [ObjParam] -> Word
+getSIDExtraInfo n [] = error ("Incorrect streamid parameters: missing 'sid': " ++ n)
+getSIDExtraInfo _ (SIDExtraParam (SIDNumber x) : _) = x
+getSIDExtraInfo n (_ : xs) = getSIDExtraInfo n xs
+
 getCBExtraInfo :: [ObjParam] -> Maybe Word
 getCBExtraInfo [] = Nothing
 getCBExtraInfo (CBExtraParam (CBNumber x) : _) = Just x
@@ -451,6 +456,8 @@ validObjPars (Obj MSIIrqSlot_T ps []) =
   subsetConstrs ps (replicate (numConstrs (MSIHandle undefined)) (MSIIRQExtraParam undefined))
 validObjPars (Obj ARMIrqSlot_T ps []) =
   subsetConstrs ps (replicate (numConstrs (ARMIRQTrigger undefined)) (ARMIRQExtraParam undefined))
+validObjPars (Obj ARMSID_T ps []) =
+  subsetConstrs ps (replicate (numConstrs (SIDNumber undefined)) (SIDExtraParam undefined))
 validObjPars (Obj ARMCB_T ps []) =
   subsetConstrs ps (replicate (numConstrs (CBNumber undefined)) (CBExtraParam undefined))
 validObjPars (Obj ARMSGISignal_T ps []) = length ps == 2
@@ -494,7 +501,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 n ps)
         Obj ARMCB_T ps [] -> ARMCB (getCBExtraInfo ps)
         Obj ARMSMC_T [] [] -> ARMSMC
         Obj ARMSGISignal_T ps [] -> ARMSGISignal (getSGISignalIrq n ps) (getARMSGISignalTarget n ps)

capDL-tool/CapDL/Model.hs

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

capDL-tool/CapDL/ParserUtils.hs

@@ -287,6 +287,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"
@@ -315,6 +322,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
@@ -472,6 +484,7 @@ object_param =
     <|> arm_irq_extra_param
     <|> ports_param
     <|> asid_high_param
+    <|> sid_extra_param
     <|> cb_extra_param
     <|> arm_sgi_signal_irq
 

capDL-tool/CapDL/PrintC.hs

@@ -387,8 +387,20 @@ 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) _ _ _ =
+    ".type = CDL_SID," +++
+    ".sid_extra = {" +++
+        ".sid = " ++ show sid +++
+    "}"
+showObjectFields _ _ (ARMCB cb_number) _ _ _ =
+    ".type = CDL_CB," +++
+    ".cb_extra = {" +++
+        ".bank = " ++ show (bank) +++
+    "}"
+    where
+    bank = case cb_number of
+        Just num -> num
+        _ -> 0
 showObjectFields _ _ ARMSMC _ _ _ = ".type = CDL_SMC,"
 showObjectFields _ _ (ARMSGISignal irq target) _ _ _ =
     ".type = CDL_SGISignal," +++

capDL-tool/CapDL/PrintUtils.hs

@@ -173,6 +173,9 @@ prettyARMIRQTrigger trigger = text "trigger:" <+> (text $ show trigger)
 prettyARMIRQTarget :: Word -> Doc
 prettyARMIRQTarget target = text "target:" <+> (text $ show target)
 
+prettySID :: Word -> Doc
+prettySID sid = text "sid:" <+> (text $ show sid)
+
 prettyARMIODevice :: Word -> Doc
 prettyARMIODevice iospace = text "iospace:" <+> (text $ show iospace)
 
@@ -220,7 +223,7 @@ prettyObjParams obj = case obj of
     IOAPICIrq _ ioapic pin level polarity -> text "ioapic_irq" <+> maybeParensList[prettyIOAPICNum ioapic, prettyIOAPICPin pin, prettyIOAPICLevel level, prettyIOAPICPolarity polarity]
     MSIIrq _ handle bus dev fun -> text "msi_irq" <+> maybeParensList[prettyMSIHandle handle, prettyMSIPCIBus bus, prettyMSIPCIDev dev, prettyMSIPCIFun fun]
     ARMIrq _ trigger target -> text "arm_irq" <+> maybeParensList[prettyARMIRQTrigger trigger, prettyARMIRQTarget target]
-    ARMSID {} -> text "streamid"
+    ARMSID sid -> text "streamid" <+> maybeParensList [prettySID sid]
     ARMCB {} -> text "contextbank"
     ARMSMC {} -> text "smc"
     ARMSGISignal irq target -> text "arm_sgi_signal" <+>

capDL-tool/Makefile

@@ -11,7 +11,8 @@ all: $(TARGET)
 
 .PHONY: tests
 tests: example-arm.test-OK example-ia32.test-OK example-aarch64.test-OK \
-       hello-dump.test-OK cap-dist-elf-simpleserver.test-OK camkes-adder-arm.test-OK \
+       example-aarch64-smmu.test-OK \
+	   hello-dump.test-OK cap-dist-elf-simpleserver.test-OK camkes-adder-arm.test-OK \
 			 camkes-adder-arm.test-thy-OK
 
 %.parse %.dot %.xml: %.cdl $(TARGET)
@@ -36,6 +37,7 @@ camkes-adder-arm.test-thy-OK: $(TARGET) camkes-adder-arm.cdl camkes-adder-arm.th
 # https://stackoverflow.com/questions/27090032
 .SECONDARY: example-arm.parse example-arm.dot example-arm.xml \
   example-ia32.parse example-ia32.dot example-ia32.xml \
+  example-aarch64-smmu.parse example-aarch64-smmu.dot example-aarch64-smmu.xml \
   hello-dump.parse hello-dump.dot hello-dump.xml \
   cap-dist-elf-simpleserver.parse cap-dist-elf-simpleserver.dot cap-dist-elf-simpleserver.xml \
   camkes-adder-arm.parse camkes-adder-arm.dot camkes-adder-arm.xml camkes-adder-arm.thy

capDL-tool/example-aarch64-smmu.cdl

@@ -0,0 +1,26 @@
+/*
+* Copyright 2026, DornerWorks
+*
+* SPDX-License-Identifier: BSD-2-Clause
+*/
+
+arch aarch64
+
+objects {
+sid_a = streamid (sid: 4)
+sid_b = streamid (sid: 9)
+sid_c = streamid (sid: 12)
+smmu_cnode = cnode (4 bits)
+}
+
+caps {
+smmu_cnode {
+0x1: sid_a
+0x2: sid_b
+0x3: sid_c
+}
+}
+
+irq maps {
+
+}

capDL-tool/example-aarch64-smmu.right

@@ -0,0 +1,23 @@
+arch aarch64
+
+objects {
+
+  sid_a = streamid (sid: 4)
+  sid_b = streamid (sid: 9)
+  sid_c = streamid (sid: 12)
+  smmu_cnode = cnode (4 bits)
+
+
+} caps {
+
+  smmu_cnode {
+    1: sid_a
+    2: sid_b
+    3: sid_c
+  }
+
+} cdt {
+
+} irq maps {
+
+}

capdl-loader-app/include/capdl.h

@@ -294,6 +294,10 @@ typedef struct {
     seL4_Word data;
 } CDL_SCExtraInfo;
 
+typedef struct {
+    uint32_t sid;
+} CDL_SIDExtraInfo;
+
 typedef struct {
     uint8_t bank;
 } CDL_CBExtraInfo;
@@ -374,6 +378,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;
@@ -589,6 +594,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 */
@@ -642,23 +639,19 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_
 #endif
 
     /* There can be multiple sids per context bank, currently only 1 sid per cb is implemented for the vms.
-     * When this gets extended we need to decide to add sid number -> cb number map into the haskell / python tool
-     * or generate the capdl spec so that the order remains correct here e.g a list a stream ids followed by the cb they
-     * are mapped to, the cb condition here (1***) will the reset the stream id number back to 0 for the next context bank.
+     * The sid and cb numbers are taken from the capdl spec, so the order of the objects in the spec does not matter.
+     * Stream IDs are fixed by the hardware and must always be specified while a cb without a bank number gets bank 0.
      */
 #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

@@ -163,9 +163,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)
         elif type == ObjectType.seL4_ARMSMC:
             o = SMC(name)
         else:

python-capdl-tool/capdl/Object.py

@@ -671,26 +671,29 @@ def get_size_bits(self):
 
 
 class StreamID(Object):
-    def __init__(self, name):
+    def __init__(self, name, streamid=None):
         super().__init__(name)
 
+        # Require Stream IDs to be provided as they are fixed by the hardware
+        if streamid is None:
+            raise ValueError('streamid %s requires a sid' % 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):

python-capdl-tool/examples/smmu.py

@@ -0,0 +1,33 @@
+#
+# Copyright 2026, DornerWorks
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+# Add the root directory of this repository to your PYTHONPATH environment
+# variable to enable the following import.
+import capdl
+
+# Create an allocator for kernel objects.
+obj_allocator = capdl.ObjectAllocator()
+
+# Let's create a CNode for the SMMU driver.
+smmu_cnode = obj_allocator.alloc(capdl.ObjectType.seL4_CapTableObject,
+                                 name='smmu_cnode', size_bits=4)
+
+# Let's create some SMMU stream IDs. These are fixed by the hardware, so
+# each one must be given its stream ID when it is allocated.
+sids = [obj_allocator.alloc(capdl.ObjectType.seL4_ARMSID, name, streamid=sid)
+        for name, sid in [('sid_a', 4), ('sid_b', 9), ('sid_c', 12)]]
+
+# Let's give the CNode a cap to each stream ID.
+cap_allocator = capdl.CSpaceAllocator(smmu_cnode)
+for sid in sids:
+    cap_allocator.alloc(sid)
+
+# Now create a spec and print it out to show what we did.
+spec = capdl.Spec(arch='aarch64')
+spec.add_object(smmu_cnode)
+for sid in sids:
+    spec.add_object(sid)
+print(str(spec))