diff --git a/.reuse/dep5 b/.reuse/dep5 index 94b4b27b..0ca4cd11 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -9,6 +9,7 @@ Files: capDL-tool/camkes-adder-arm.thy.right capDL-tool/cap-dist-elf-simpleserver.right capDL-tool/example-arm.right + capDL-tool/example-aarch64.right capDL-tool/example-ia32.right capDL-tool/hello-dump.right python-capdl-tool/tests/resources/arm-hello.bin diff --git a/CHANGES.md b/CHANGES.md index e0a4bd9f..522952c2 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -15,13 +15,19 @@ ### Changes * Add support for fpu_disabled flag on TCBs for platforms with CONFIG_HAVE_FPU. -* remove `pyaml` python dependency and use `pyyaml` (import `yaml`) directly. +* Add support for SGISignal capability. SGISignal capabilities in capDL point + to an `arm_sgi_signal` object with `(irg: , target: )` properties + that define the destination of the SGI. +* Remove `pyaml` python dependency and use `pyyaml` (import `yaml`) directly. ### Upgrade Notes +* existing capDL specs should continue to work without change + --- ## 0.3 2024-07-01 + Using seL4 version 13.0.0 ### Changes diff --git a/capDL-tool/CapDL/AST.hs b/capDL-tool/CapDL/AST.hs index f04af63a..7a4fc65f 100644 --- a/capDL-tool/CapDL/AST.hs +++ b/capDL-tool/CapDL/AST.hs @@ -117,6 +117,8 @@ data ObjParam = msi_irq_extraParam :: MSIIRQExtraParam } | ARMIRQExtraParam { arm_irq_extraParam :: ARMIRQExtraParam } + | ARMSGISignalIrq { + sgi_irq :: Word } | InitArguments { arguments :: [Word] } | DomainID { diff --git a/capDL-tool/CapDL/MakeModel.hs b/capDL-tool/CapDL/MakeModel.hs index 33130802..8e544bbc 100644 --- a/capDL-tool/CapDL/MakeModel.hs +++ b/capDL-tool/CapDL/MakeModel.hs @@ -344,6 +344,17 @@ getARMIrqTarget n [] = error ("Incorrect Arm irq parameters: missing 'target': " getARMIrqTarget _ (ARMIRQExtraParam (ARMIRQTarget target) : _) = target getARMIrqTarget n (_ : xs) = getARMIrqTarget n xs +getSGISignalIrq :: Name -> [ObjParam] -> Word +getSGISignalIrq n [] = error ("Incorrect Arm sgi_signal parameters: missing 'irq': " ++ n) +getSGISignalIrq _ (ARMSGISignalIrq irq : _) = irq +getSGISignalIrq n (_ : xs) = getSGISignalIrq n xs + +getARMSGISignalTarget :: Name -> [ObjParam] -> Word +getARMSGISignalTarget n [] = error ("Incorrect Arm sgi_signal parameters: missing 'target': " ++ n) +getARMSGISignalTarget _ (ARMIRQExtraParam (ARMIRQTarget target) : _) = target +getARMSGISignalTarget n (_ : xs) = getARMSGISignalTarget n xs + + getMaybeBitSize :: [ObjParam] -> Maybe Word getMaybeBitSize [] = Nothing getMaybeBitSize (BitSize x : _) = Just x @@ -442,6 +453,7 @@ validObjPars (Obj ARMIrqSlot_T ps []) = subsetConstrs ps (replicate (numConstrs (ARMIRQTrigger undefined)) (ARMIRQExtraParam undefined)) validObjPars (Obj ARMCB_T ps []) = subsetConstrs ps (replicate (numConstrs (CBNumber undefined)) (CBExtraParam undefined)) +validObjPars (Obj ARMSGISignal_T ps []) = length ps == 2 validObjPars obj = null (params obj) -- For converting frame sizes to size bits @@ -485,6 +497,7 @@ objectOf n obj = Obj ARMSID_T [] [] -> ARMSID Obj ARMCB_T ps [] -> ARMCB (getCBExtraInfo ps) Obj ARMSMC_T [] [] -> ARMSMC + Obj ARMSGISignal_T ps [] -> ARMSGISignal (getSGISignalIrq n ps) (getARMSGISignalTarget n ps) Obj _ _ (_:_) -> error $ "Only untyped caps can have objects as content: " ++ n ++ " = " ++ show obj @@ -664,6 +677,7 @@ objCapOf containerName obj objRef params = ARMSID {} -> ARMSIDCap objRef ARMCB {} -> ARMCBCap objRef ARMSMC -> ARMSMCCap objRef (getBadge params) + ARMSGISignal {} -> ARMSGISignalCap objRef else error ("Incorrect params for cap to " ++ printID objRef ++ " in " ++ printID containerName ++ "; got " ++ show params) diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs index acc52a17..c7450fae 100644 --- a/capDL-tool/CapDL/Model.hs +++ b/capDL-tool/CapDL/Model.hs @@ -121,6 +121,7 @@ data Cap | ARMSMCCap { capObj :: ObjID, capBadge :: Word } + | ARMSGISignalCap { capObj :: ObjID } -- X86 specific caps | IOPortsCap { @@ -208,6 +209,9 @@ data KernelObject a slots :: CapMap a, trigger :: Word, target :: Word } + | ARMSGISignal { + irq :: Word, + target :: Word } -- fake kernel objects for smmu | ARMSID @@ -256,6 +260,7 @@ data KOType | ARMSID_T | ARMCB_T | ARMSMC_T + | ARMSGISignal_T | ASIDPool_T | PT_T | PD_T diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs index 051fcdce..7fc519aa 100644 --- a/capDL-tool/CapDL/ParserUtils.hs +++ b/capDL-tool/CapDL/ParserUtils.hs @@ -138,6 +138,7 @@ object_type = <|> keyw "streamid" ARMSID_T <|> keyw "contextbank" ARMCB_T <|> keyw "smc" ARMSMC_T + <|> keyw "arm_sgi_signal" ARMSGISignal_T obj_bit_size :: MapParser ObjParam obj_bit_size = do @@ -411,6 +412,12 @@ arm_irq_extra_param = do <|> arm_irq_target) return $ ARMIRQExtraParam param +arm_sgi_signal_irq :: MapParser ObjParam +arm_sgi_signal_irq = do + reserved "irq" + colon + n <- number + return $ ARMSGISignalIrq n fill_param :: MapParser FrameExtraParam fill_param = do @@ -466,6 +473,7 @@ object_param = <|> ports_param <|> asid_high_param <|> cb_extra_param + <|> arm_sgi_signal_irq object_params :: MapParser [ObjParam] object_params = diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index a4dc9516..d0c766eb 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -162,6 +162,8 @@ showCap objs (ARMSMCCap id badge) _ is_orig _ = "{.type = CDL_SMCCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ ", .data = { .tag = CDL_CapData_Badge, .badge = " ++ show badge ++ "}}" +showCap objs (ARMSGISignalCap id) _ is_orig _ = + "{.type = CDL_SGISignalCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ "}" showCap objs (PTCap id _) _ is_orig _ = "{.type = CDL_PTCap, .obj_id = " ++ showObjID objs id ++ @@ -388,6 +390,12 @@ showObjectFields _ _ (RTReply {}) _ _ _ = ".type = CDL_RTReply," showObjectFields _ _ (ARMSID {}) _ _ _ = ".type = CDL_SID," showObjectFields _ _ (ARMCB {}) _ _ _ = ".type = CDL_CB," showObjectFields _ _ ARMSMC _ _ _ = ".type = CDL_SMC," +showObjectFields _ _ (ARMSGISignal irq target) _ _ _ = + ".type = CDL_SGISignal," +++ + ".sgisignal_extra = {" +++ + ".irq = " ++ show irq ++ "," +++ + ".target = " ++ show target ++ "," +++ + "}," showObjectFields _ _ x _ _ _ = assert False $ "UNSUPPORTED OBJECT TYPE: " ++ show x diff --git a/capDL-tool/CapDL/PrintUtils.hs b/capDL-tool/CapDL/PrintUtils.hs index 7424a164..41d8413f 100644 --- a/capDL-tool/CapDL/PrintUtils.hs +++ b/capDL-tool/CapDL/PrintUtils.hs @@ -168,14 +168,17 @@ prettyMSIPCIFun :: Word -> Doc prettyMSIPCIFun fun = text "msi_pci_fun:" <+> (text $ show fun) prettyARMIRQTrigger :: Word -> Doc -prettyARMIRQTrigger trigger = text "irq_trigger:" <+> (text $ show trigger) +prettyARMIRQTrigger trigger = text "trigger:" <+> (text $ show trigger) prettyARMIRQTarget :: Word -> Doc -prettyARMIRQTarget target = text "irq_target:" <+> (text $ show target) +prettyARMIRQTarget target = text "target:" <+> (text $ show target) prettyARMIODevice :: Word -> Doc prettyARMIODevice iospace = text "iospace:" <+> (text $ show iospace) +prettyARMIRQ :: Word -> Doc +prettyARMIRQ irq = text "irq:" <+> (text $ show irq) + prettyFills :: Maybe [[String]] -> Doc prettyFills (Just fills) = text "fill:" <+> brackets (hsep (punctuate comma (map (braces . text . unwords) fills))) prettyFills Nothing = empty @@ -220,6 +223,8 @@ prettyObjParams obj = case obj of ARMSID {} -> text "streamid" ARMCB {} -> text "contextbank" ARMSMC {} -> text "smc" + ARMSGISignal irq target -> text "arm_sgi_signal" <+> + maybeParensList [prettyARMIRQ irq, prettyARMIRQTarget target] capParams [] = empty capParams xs = parens (hsep $ punctuate comma xs) diff --git a/capDL-tool/CapDL/PrintXml.hs b/capDL-tool/CapDL/PrintXml.hs index ee6c90e9..0c2c8c42 100644 --- a/capDL-tool/CapDL/PrintXml.hs +++ b/capDL-tool/CapDL/PrintXml.hs @@ -88,6 +88,7 @@ showObjectAttrs (IOPorts sz) = [("size", show sz)] showObjectAttrs (IODevice _ dom pci) = [("domain", show dom), ("device", show pci)] showObjectAttrs (ARMIODevice _ iospace) = [("iospace", show iospace)] showObjectAttrs (IOPT _ level) = [("level", show level)] +showObjectAttrs (ARMSGISignal irq target) = [("irq", show irq), ("target", show target)] showObjectAttrs _ = [] -- @@ -120,6 +121,7 @@ showObjectName ARMIrq {} = "ARMIrq" showObjectName ARMSID {} = "ARMSID" showObjectName ARMCB {} = "ARMCB" showObjectName ARMSMC = "ARMSMC" +showObjectName ARMSGISignal {} = "ARMSGISignal" -- -- Get a cap's name. @@ -160,6 +162,7 @@ showCapName SchedControlCap {} = "SchedControlCap" showCapName ARMSIDCap {} = "ARMSIDCap" showCapName ARMCBCap {} = "ARMCBCap" showCapName ARMSMCCap {} = "ARMSMCCap" +showCapName ARMSGISignalCap {} = "ARMSGISignalCap" showExtraCapAttributes :: Cap -> [(String, String)] showExtraCapAttributes (EndpointCap _ capBadge _) = [("badge", show capBadge)] diff --git a/capDL-tool/CapDL/State.hs b/capDL-tool/CapDL/State.hs index 6d4caa48..5c4b67a7 100644 --- a/capDL-tool/CapDL/State.hs +++ b/capDL-tool/CapDL/State.hs @@ -322,6 +322,7 @@ koType (ARMIrq {}) = ARMIrqSlot_T koType (ARMSID {}) = ARMSID_T koType (ARMCB {}) = ARMCB_T koType ARMSMC = ARMSMC_T +koType (ARMSGISignal {}) = ARMSGISignal_T objAt :: (KernelObject Word -> Bool) -> ObjID -> Model Word -> Bool objAt p ref = maybe False p . maybeObject ref @@ -359,6 +360,7 @@ capTyp (ARMIRQHandlerCap {}) = ARMIrqSlot_T capTyp (ARMSIDCap {}) = ARMSID_T capTyp (ARMCBCap {}) = ARMCB_T capTyp (ARMSMCCap {}) = ARMSMC_T +capTyp (ARMSGISignalCap {}) = ARMSGISignal_T capTyp _ = error "cap has no object" checkTypAt :: Cap -> Model Word -> ObjID -> Word -> Logger Bool @@ -407,6 +409,7 @@ validCapArch X86_64 (IOSpaceCap {}) = True validCapArch X86_64 (IOPTCap {}) = True validCapArch ARM11 (ARMIOSpaceCap {}) = True validCapArch ARM11 (ARMIRQHandlerCap {}) = True +validCapArch ARM11 (ARMSGISignalCap {}) = True validCapArch AARCH64 (ARMIRQHandlerCap {}) = True validCapArch AARCH64 (ARMIOSpaceCap {}) = True validCapArch AARCH64 (PUDCap {}) = True @@ -414,6 +417,7 @@ validCapArch AARCH64 (PGDCap {}) = True validCapArch AARCH64 (ARMSIDCap {}) = True validCapArch AARCH64 (ARMCBCap {}) = True validCapArch AARCH64 (ARMSMCCap {}) = True +validCapArch AARCH64 (ARMSGISignalCap {}) = True validCapArch _ _ = False checkCapArch :: Arch -> Cap -> ObjID -> Word -> Logger Bool @@ -453,6 +457,7 @@ validObjArch RISCV (VCPU {}) = False validObjArch _ (VCPU {}) = True validObjArch ARM11 (ARMIODevice {}) = True validObjArch ARM11 (ARMIrq {}) = True +validObjArch ARM11 (ARMSGISignal {}) = True validObjArch IA32 (IOPorts {}) = True validObjArch IA32 (IODevice {}) = True validObjArch IA32 (IOPT {}) = True @@ -472,6 +477,7 @@ validObjArch AARCH64 (ARMSID {}) = True validObjArch AARCH64 (ARMCB {}) = True validObjArch AARCH64 (ARMSMC {}) = True validObjArch AARCH64 (ARMIODevice {}) = True +validObjArch AARCH64 (ARMSGISignal {}) = True validObjArch _ _ = False checkObjArch :: Arch -> KernelObject Word -> ObjID -> Logger Bool @@ -505,7 +511,7 @@ validObjCap :: Arch -> KernelObject Word -> Word -> Cap -> Bool validObjCap arch (TCB {}) slot cap = validTCBSlotCap arch slot cap validObjCap _ (CNode _ 0) slot cap = slot == 0 && is _NotificationCap cap -- FIXME: we should add a separate IRQObject validObjCap _ (CNode {}) _ _ = True -validObjCap _ (ASIDPool {}) _ cap = is _PDCap cap +validObjCap arch (ASIDPool {}) _ cap = validTCBSlotCap arch tcbVTableSlot cap validObjCap RISCV (PT {}) _ cap = is _FrameCap cap || is _PTCap cap validObjCap _ (PT {}) _ cap = is _FrameCap cap validObjCap _ (PD {}) _ cap = is _FrameCap cap || is _PTCap cap diff --git a/capDL-tool/Main.hs b/capDL-tool/Main.hs index ffe0baca..9d6460f3 100644 --- a/capDL-tool/Main.hs +++ b/capDL-tool/Main.hs @@ -165,6 +165,7 @@ genObjectSizeMap m = , ("seL4_ARMSID", ARMSID_T) , ("seL4_ARMCB", ARMCB_T) , ("seL4_ARMSMC", ARMSMC_T) + , ("seL4_ARMSGI_Signal", ARMSGISignal_T) ] -- Abort with an error message if 'isFullyAllocated' fails. diff --git a/capDL-tool/Makefile b/capDL-tool/Makefile index 50462108..fca15a79 100644 --- a/capDL-tool/Makefile +++ b/capDL-tool/Makefile @@ -10,7 +10,9 @@ TARGET=parse-capDL all: $(TARGET) .PHONY: tests -tests: example-arm.test-OK example-ia32.test-OK hello-dump.test-OK cap-dist-elf-simpleserver.test-OK camkes-adder-arm.test-OK camkes-adder-arm.test-thy-OK +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 \ + camkes-adder-arm.test-thy-OK %.parse %.dot %.xml: %.cdl $(TARGET) stack exec $(TARGET) -- -t $*.parse -x $*.xml -d $*.dot $< || rm -f $*.parse $*.dot $*.xml diff --git a/capDL-tool/capdl.dtd b/capDL-tool/capdl.dtd index 447db2b4..56183660 100644 --- a/capDL-tool/capdl.dtd +++ b/capDL-tool/capdl.dtd @@ -17,6 +17,8 @@ + + diff --git a/capDL-tool/example-aarch64.cdl b/capDL-tool/example-aarch64.cdl new file mode 100644 index 00000000..fee51f71 --- /dev/null +++ b/capDL-tool/example-aarch64.cdl @@ -0,0 +1,146 @@ +/* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +arch aarch64 + +objects { + +rm_ut = ut { + rm_tcb = tcb (init: [10], dom: 5, fault_ep: 0xF) + something = ut (8 bits) { + rm_cn = cnode (10 bits) + } + rm_pd = pgd + rm_ap = asid_pool (asid_high: 0x1) + + linux_pd = pt + + rm_ut_small[50] = ut (12 bits) + rm_ut_big[100] = ut (20 bits) + + frame_nic1[64] = frame (4k) + -- io space?? + + frame_nic2[64] = frame (4k) + -- io space?? + + frame_nic3[4] = frame (4k) + -- io space?? + + timer = notification + control = ep + test[5] = cnode (8 bits) +} + +rm_ut_small[0] = ut { + name_b +} + +rm_ut_small[0]/g = tcb + +irq_handler[3] = irq +nic1_notification = notification + +cnode_booter = cnode (8 bits) + +name_b/name = ut (8 bits) { y[..2], z } + +name_b = ut (10 bits) +name/name2/name3/x = tcb +y[5] = ep +z = ep + +sgi2 = arm_sgi_signal (target: 0, irq: 1) + +} + +caps { + +rm_cn { + 001: rm_tcb + 002: rm_cn (guard: 0, guard_size: 0) + 003: rm_pd (asid: (0x1, 0x1)) + 006: rm_ap +0x00b: linux_pd; +0x00c: rm_ut_small[3..5]; +0x00f: rm_ut_small[7..20, 23, 27..]; +0x03e: rm_ut_big[]; + +0x0a3: irq_handler[0]; +0x0a4: name[] = frame_nic1[]; + +0x0e5: irq_handler[1]; +0x0e6: frame_nic2[] (RW, asid: (0x1, 0x1)); +-- 126: iospace + +0x126: sgi2 + +0x127: irq_handler[2]; +0x128: frame_nic3[]; +-- 12c: iospace + +0x12d: timer (G) +0x12e: control (badge: 10) + +0x12f: name2 = (masked: R); + 304: test[0] + 305: test[1] + 306: test[1,2] + 308: +0x200: - child_of name2 +0x201: - child_of (rm_cn, 0x12f) +0x202: +} + +rm_tcb { + vspace: rm_pd + cspace: rm_cn +} + +cap_name = (rm_tcb, cspace) +cap_name2 = (irq_table, 0) + +cnode_booter { + 001: rm_ut + sched_control (core: 0) +} + +test[2..] { + 001: name3 = name_b + 0x200: rm_cn +} + +test[1] { + 001: name_b + 2: g (reply) + 0x200: rm_cn +} + +cap_test = (test[1],0x200) + +test[0] { + 1: +} + +rm_ap { + 1: rm_pd +} + +} irq maps { + + irq_handler[] + +} cdt { + +(cnode_booter, 1) { + (rm_cn, 0x12d) +} + +cap_test { + (rm_cn, 0x12e) +} + +} diff --git a/capDL-tool/example-aarch64.right b/capDL-tool/example-aarch64.right new file mode 100644 index 00000000..644df3e3 --- /dev/null +++ b/capDL-tool/example-aarch64.right @@ -0,0 +1,104 @@ +arch aarch64 + +objects { + + cnode_booter = cnode (8 bits) + control = ep + frame_nic1[64] = frame (4k) + frame_nic2[64] = frame (4k) + frame_nic3[4] = frame (4k) + g = tcb (dom: 0) + irq_handler[3] = irq + linux_pd = pt + nic1_notification = notification + rm_ap = asid_pool (asid_high: 0x1) + rm_cn = cnode (10 bits) + rm_pd = pgd + rm_tcb = tcb (fault_ep: 15, dom: 5, init: [10]) + sgi2 = arm_sgi_signal (irq: 1, target: 0) + test[5] = cnode (8 bits) + timer = notification + x = tcb (dom: 0) + y[5] = ep + z = ep + + name = ut (8 bits) {y[0..2], z, name2} + name2 = ut {name3} + name3 = ut {x} + name_b = ut (10 bits) {name} + rm_ut = ut {rm_tcb, something, rm_pd, rm_ap, linux_pd, + rm_ut_small[0..49], rm_ut_big[0..99], frame_nic1[0..63], + frame_nic2[0..63], frame_nic3[0..3], timer, control, test[0..4]} + rm_ut_big[100] = ut (20 bits) + rm_ut_small[50] = ut (12 bits) + rm_ut_small[0] = ut (12 bits) {name_b, g} + something = ut (8 bits) {rm_cn} + +} caps { + + cnode_booter { + 1: rm_ut + 2: sched_control (core: 0) + } + + rm_ap {1: rm_pd} + + rm_cn { + 1: rm_tcb + 2: rm_cn + 3: rm_pd + 6: rm_ap + 11: linux_pd + 12: rm_ut_small[3..5, 7..20, 23, 27..49] + 62: rm_ut_big[0..99] + 163: irq_handler[0] + 164: frame_nic1[0..63] + 229: irq_handler[1] + 230: frame_nic2[0..63] (RW, asid: (0x1, 0x1)) + 294: sgi2 + 295: irq_handler[2] + 296: frame_nic3[0..3] + 301: timer (G) + 302: control (badge: 10) + 303: rm_cn + 304: test[0..1, 1..2] + 308: name_b + 512: rm_cn + 513: rm_cn + 514: frame_nic1[0..63] + } + + rm_tcb { + 0: rm_cn + 1: rm_pd + } + + test[0] {1: rm_cn} + + test[1] { + 1: name_b + 2: g (reply) + 512: rm_cn + } + + test[2..4] { + 1: name_b + 512: rm_cn + } + +} cdt { + + (cnode_booter, 1) {(rm_cn, 301)} + + (test[1], 512) {(rm_cn, 302)} + + (rm_cn, 303) { + (rm_cn, 512) + (rm_cn, 513) + } + +} irq maps { + + 0: irq_handler[0..2] + +} \ No newline at end of file diff --git a/capDL-tool/example-arm.cdl b/capDL-tool/example-arm.cdl index 329eb4fb..4cfc9918 100644 --- a/capDL-tool/example-arm.cdl +++ b/capDL-tool/example-arm.cdl @@ -53,6 +53,8 @@ name/b = tcb y[5] = ep z = ep +sgi1 = arm_sgi_signal(irq: 10, target: 2) + } caps { rm_cn { @@ -72,6 +74,8 @@ rm_cn { 0x0e6: frame_nic2[] (RW, asid: (0x1, 0x1)); -- 126: iospace +0x126: sgi1; + 0x127: irq_handler[2]; 0x128: frame_nic3[]; -- 12c: iospace diff --git a/capDL-tool/example-arm.right b/capDL-tool/example-arm.right index 0f62c12e..d7430657 100644 --- a/capDL-tool/example-arm.right +++ b/capDL-tool/example-arm.right @@ -17,6 +17,7 @@ objects { rm_cn = cnode (10 bits) rm_pd = pd rm_tcb = tcb (fault_ep: 15, dom: 5, init: [10]) + sgi1 = arm_sgi_signal (irq: 10, target: 2) test[5] = cnode (8 bits) timer = notification x = tcb (dom: 0) @@ -56,6 +57,7 @@ objects { 164: frame_nic1[0..63] 229: irq_handler[1] 230: frame_nic2[0..63] (RW, asid: (0x1, 0x1)) + 294: sgi1 295: irq_handler[2] 296: frame_nic3[0..3] 301: timer (G) diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h index 27f963f5..dafc96b0 100644 --- a/capdl-loader-app/include/capdl.h +++ b/capdl-loader-app/include/capdl.h @@ -83,6 +83,9 @@ typedef enum { CDL_ARMIOSpaceCap, CDL_SIDCap, CDL_CBCap, +#ifndef CONFIG_ENABLE_SMP_SUPPORT + CDL_SGISignalCap, +#endif #ifdef CONFIG_ALLOW_SMC_CALLS CDL_SMCCap, #endif @@ -216,6 +219,9 @@ typedef enum { #ifdef CONFIG_ALLOW_SMC_CALLS CDL_SMC = seL4_ObjectTypeCount + 14, #endif +#ifndef CONFIG_ENABLE_SMP_SUPPORT + CDL_SGISignal = seL4_ObjectTypeCount + 15, +#endif #endif #ifdef CONFIG_ARCH_RISCV CDL_Frame = seL4_RISCV_4K_Page, @@ -311,6 +317,12 @@ typedef struct { int target; } CDL_ARMIRQExtraInfo; +typedef struct { + seL4_Word irq; + seL4_Word target; +} CDL_SGISignalExtraInfo; + + typedef enum { CDL_FrameFill_None = 0, CDL_FrameFill_BootInfo, @@ -368,6 +380,7 @@ typedef struct { CDL_FrameExtraInfo frame_extra; seL4_Word paddr; /* Physical address; only relevant for untyped objects. */ seL4_Word asid_high; /* for ASID pools */ + CDL_SGISignalExtraInfo sgisignal_extra; struct { seL4_Word start; seL4_Word end; diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index ac1df4fa..a8cbff7e 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -663,6 +663,15 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_ } #endif +#if defined(CONFIG_ARCH_ARM) && !defined(CONFIG_ENABLE_SMP_SUPPORT) + if (CDL_Obj_Type(obj) == CDL_SGISignal) { + err = seL4_IRQControl_IssueSGISignal(seL4_CapIRQControl, obj->sgisignal_extra.irq, obj->sgisignal_extra.target, + seL4_CapInitThreadCNode, free_slot, CONFIG_WORD_SIZE); + ZF_LOGF_IF(err != seL4_NoError, "Failed to allocate SGISignal cap"); + return seL4_NoError; + } +#endif + #ifdef CONFIG_ALLOW_SMC_CALLS if (CDL_Obj_Type(obj) == CDL_SMC) { return seL4_NoError; diff --git a/object_sizes/object_sizes.yaml b/object_sizes/object_sizes.yaml index 90da4e5c..cb3ab6db 100644 --- a/object_sizes/object_sizes.yaml +++ b/object_sizes/object_sizes.yaml @@ -67,3 +67,4 @@ seL4_ARMIRQ: 0 seL4_ARMSID: 0 seL4_ARMCB: 0 seL4_ARMSMC: 0 +seL4_ARMSGI_Signal: 0 diff --git a/python-capdl-tool/capdl/Allocator.py b/python-capdl-tool/capdl/Allocator.py index 0b25d0c2..10ecbceb 100644 --- a/python-capdl-tool/capdl/Allocator.py +++ b/python-capdl-tool/capdl/Allocator.py @@ -19,7 +19,7 @@ Notification, TCB, Untyped, IOPageTable, Object, IRQ, IOPorts, IODevice, \ ARMIODevice, VCPU, ASIDPool, SC, SchedControl, RTReply, ObjectType, \ ObjectRights, IOAPICIRQ, MSIIRQ, IRQControl, get_object_size, ASIDControl, \ - DomainControl, is_aligned, ARMIRQMode, ARMIRQ, ContextBank, StreamID, SMC + DomainControl, is_aligned, ARMIRQMode, ARMIRQ, ContextBank, StreamID, SMC, ARMSGISignal from capdl.util import ctz from .Spec import Spec @@ -88,7 +88,7 @@ def alloc(self, type, name=None, label=None, **kwargs): if type == ObjectType.seL4_UntypedObject: size_bits = kwargs.get('size_bits', 12) paddr = kwargs.get('paddr', None) - assert(paddr != 0) + assert (paddr != 0) o = Untyped(name, size_bits, paddr) elif type == ObjectType.seL4_TCBObject: o = TCB(name) @@ -147,6 +147,8 @@ def alloc(self, type, name=None, label=None, **kwargs): if notification is not None: o.set_notification(notification) + elif type == ObjectType.seL4_ARM_SGI_Signal: + o = ARMSGISignal(name, **kwargs) elif type == ObjectType.seL4_IRQControl: o = IRQControl(name) elif type == ObjectType.seL4_ASID_Control: @@ -360,7 +362,7 @@ def allocate(self, spec): Therefore, we raise AllocatorException if the spec's asid_high numbers cannot be obtained by the C loader. """ - assert(isinstance(spec, Spec)) + assert (isinstance(spec, Spec)) num_asid_high = get_object_size(ObjectType.seL4_ASID_Table) free_asid_highs = SortedSet(range(num_asid_high)) @@ -434,7 +436,7 @@ def allocate(self, spec): class AllocQueue: def __init__(self, s): - assert(isinstance(s, Spec)) + assert (isinstance(s, Spec)) # dict of unfungible objects, sorted by paddr. self.unfun_objects = SortedDict(lambda x: -x) # dict of lists of fungible objects, indexed by size_bits @@ -517,7 +519,7 @@ def __init__(self): def _overlap(before, after): assert isinstance(before, Untyped) assert isinstance(after, Untyped) - assert(before.paddr <= after.paddr) + assert (before.paddr <= after.paddr) return not (before.paddr < after.paddr and ((before.paddr + before.get_size()) < (after.paddr + after.get_size()))) @staticmethod @@ -566,8 +568,8 @@ def _fill_from_objects(self, objects, untyped, size_bits, spec): # no objects of the size we were looking for -- try for two of a smaller size first = self._fill_from_objects(objects, untyped, size_bits - 1, spec) second = self._fill_from_objects(objects, untyped, size_bits - 1, spec) - assert(first == 0 or first == size_bits - 1) - assert(second == 0 or second == size_bits - 1) + assert (first == 0 or first == size_bits - 1) + assert (second == 0 or second == size_bits - 1) if first == second: if first == 0: # we successfully allocated all of the space @@ -583,7 +585,7 @@ def _fill_from_objects(self, objects, untyped, size_bits, spec): return 0 def _use_untyped(self, objects, untyped, size_bytes, is_device, spec): - assert(untyped.remaining() >= size_bytes) + assert (untyped.remaining() >= size_bytes) while size_bytes: # size_bits is calculated from the minimum alignment between the goal @@ -600,7 +602,7 @@ def _use_untyped(self, objects, untyped, size_bytes, is_device, spec): # we failed to fill from objects at all self._add_placeholder(untyped, size_bits, spec) size_bytes -= (1 << size_bits) - assert(size_bytes >= 0) + assert (size_bytes >= 0) def _next_ut(self): if not self.ut_iter: @@ -611,7 +613,7 @@ def _next_ut(self): raise AllocatorException("Out of untyped memory to allocate from") def allocate(self, s): - assert(isinstance(s, Spec)) + assert (isinstance(s, Spec)) if not len(s.objs): # nothing to do diff --git a/python-capdl-tool/capdl/Object.py b/python-capdl-tool/capdl/Object.py index 07584434..ec3ba023 100644 --- a/python-capdl-tool/capdl/Object.py +++ b/python-capdl-tool/capdl/Object.py @@ -106,6 +106,8 @@ class ObjectType(Enum): # Only used by ASIDTableAllocator. Note: this counts slots, not bytes. seL4_ASID_Table = auto() + seL4_ARM_SGI_Signal = auto() + class ObjectRights(Flag): _order_ = 'seL4_NoRights seL4_CanRead seL4_CanWrite seL4_CanGrant seL4_CanGrantReply seL4_AllRights' @@ -566,6 +568,19 @@ def __repr__(self): return '%s = arm_irq (trigger:%s, target:%d)' % (self.name, "level" if self.trigger == ARMIRQMode.seL4_ARM_IRQ_LEVEL else "edge", self.target) +class ARMSGISignal(Object): + def __init__(self, name, irq, target): + super(ARMSGISignal, self).__init__(name) + self.irq = irq + self.target = target + + def get_size_bits(self): + return None + + def __repr__(self): + return '%s = arm_sgi_signal (irq:%s, target:%s)' % (self.name, hex(self.irq), hex(self.target)) + + class VCPU(Object): def __repr__(self): return '%s = vcpu' % self.name