From 17e82be984c8a6b0c71779c54c940add0efea675 Mon Sep 17 00:00:00 2001 From: Alex Pavey Date: Tue, 25 Jan 2022 16:22:06 -0500 Subject: [PATCH] smmuv2: Add ability to specify sid and cb numbers Add a mandatory `sid:` parameter to `streamid` objects. python-capdl-tool now takes the stream ID and bank number as allocation arguments. `streamid` objects without a `sid:` parameter are now rejected. An example CDL file is provided for reference. Signed-off-by: Alex Pavey (cherry picked from commit 0c0871c82d5aea25ed3d423335f5fcaeaa3aaf30) Signed-off-by: Tyler Doiron --- .reuse/dep5 | 6 +++++ capDL-tool/CapDL/AST.hs | 7 ++++++ capDL-tool/CapDL/MakeModel.hs | 9 +++++++- capDL-tool/CapDL/Model.hs | 2 +- capDL-tool/CapDL/ParserUtils.hs | 13 +++++++++++ capDL-tool/CapDL/PrintC.hs | 16 +++++++++++-- capDL-tool/CapDL/PrintUtils.hs | 5 +++- capDL-tool/Makefile | 4 +++- capDL-tool/example-aarch64-smmu.cdl | 26 +++++++++++++++++++++ capDL-tool/example-aarch64-smmu.right | 23 +++++++++++++++++++ capdl-loader-app/include/capdl.h | 10 ++++++++ capdl-loader-app/src/main.c | 13 +++-------- python-capdl-tool/capdl/Allocator.py | 4 ++-- python-capdl-tool/capdl/Object.py | 15 +++++++----- python-capdl-tool/examples/smmu.py | 33 +++++++++++++++++++++++++++ 15 files changed, 162 insertions(+), 24 deletions(-) create mode 100644 capDL-tool/example-aarch64-smmu.cdl create mode 100644 capDL-tool/example-aarch64-smmu.right create mode 100644 python-capdl-tool/examples/smmu.py diff --git a/.reuse/dep5 b/.reuse/dep5 index 0ca4cd11..6eaf80d1 100644 --- a/.reuse/dep5 +++ b/.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 diff --git a/capDL-tool/CapDL/AST.hs b/capDL-tool/CapDL/AST.hs index c1aa8d99..ebc9cd42 100644 --- a/capDL-tool/CapDL/AST.hs +++ b/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 { diff --git a/capDL-tool/CapDL/MakeModel.hs b/capDL-tool/CapDL/MakeModel.hs index 5d20231a..8e77986d 100644 --- a/capDL-tool/CapDL/MakeModel.hs +++ b/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) diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs index 91edd71f..064a6711 100644 --- a/capDL-tool/CapDL/Model.hs +++ b/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 diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs index 7fc519aa..25a882ca 100644 --- a/capDL-tool/CapDL/ParserUtils.hs +++ b/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 diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index e06f07a0..7b55ce79 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/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," +++ diff --git a/capDL-tool/CapDL/PrintUtils.hs b/capDL-tool/CapDL/PrintUtils.hs index 41d8413f..30bec43a 100644 --- a/capDL-tool/CapDL/PrintUtils.hs +++ b/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" <+> diff --git a/capDL-tool/Makefile b/capDL-tool/Makefile index fca15a79..5ef03071 100644 --- a/capDL-tool/Makefile +++ b/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 diff --git a/capDL-tool/example-aarch64-smmu.cdl b/capDL-tool/example-aarch64-smmu.cdl new file mode 100644 index 00000000..fa7cdd89 --- /dev/null +++ b/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 { + +} diff --git a/capDL-tool/example-aarch64-smmu.right b/capDL-tool/example-aarch64-smmu.right new file mode 100644 index 00000000..132726c6 --- /dev/null +++ b/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 { + +} diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h index 0589a908..a96ea02d 100644 --- a/capdl-loader-app/include/capdl.h +++ b/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; diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index c54dd465..1c42d5de 100644 --- a/capdl-loader-app/src/main.c +++ b/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 diff --git a/python-capdl-tool/capdl/Allocator.py b/python-capdl-tool/capdl/Allocator.py index eb49967d..b04c79ee 100644 --- a/python-capdl-tool/capdl/Allocator.py +++ b/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: diff --git a/python-capdl-tool/capdl/Object.py b/python-capdl-tool/capdl/Object.py index 03e384c5..f8d8ef5d 100644 --- a/python-capdl-tool/capdl/Object.py +++ b/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): diff --git a/python-capdl-tool/examples/smmu.py b/python-capdl-tool/examples/smmu.py new file mode 100644 index 00000000..6bae253a --- /dev/null +++ b/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))