diff --git a/capDL-tool/CapDL/AST.hs b/capDL-tool/CapDL/AST.hs index 5f237503..ef43f67c 100644 --- a/capDL-tool/CapDL/AST.hs +++ b/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 { diff --git a/capDL-tool/CapDL/MakeModel.hs b/capDL-tool/CapDL/MakeModel.hs index 021cf2c8..416057d6 100644 --- a/capDL-tool/CapDL/MakeModel.hs +++ b/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: " ++ diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs index 6a2c0af6..2ec43a7a 100644 --- a/capDL-tool/CapDL/Model.hs +++ b/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 diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs index b67cea62..8adecc20 100644 --- a/capDL-tool/CapDL/ParserUtils.hs +++ b/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] diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index b4ff3ca5..b1b6fbe0 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/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 diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h index f6f05855..4f2d1adb 100644 --- a/capdl-loader-app/include/capdl.h +++ b/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; diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index c543faa2..23d81423 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 */ @@ -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 diff --git a/python-capdl-tool/capdl/Allocator.py b/python-capdl-tool/capdl/Allocator.py index 1ce613e8..6cdcf0dd 100644 --- a/python-capdl-tool/capdl/Allocator.py +++ b/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) diff --git a/python-capdl-tool/capdl/Object.py b/python-capdl-tool/capdl/Object.py index ba506957..e138d279 100644 --- a/python-capdl-tool/capdl/Object.py +++ b/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):