Skip to content

SGI support for capDL-tool #77

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
lsf37 merged 6 commits into from
Nov 19, 2025
Merged

SGI support for capDL-tool #77

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
03e66a6
capDL-tool: fix printing for ARM irq handler caps
lsf37 Nov 17, 2025
0e2f236
SGI support for capDL-tool + loader + python
kent-mcleod Sep 16, 2022
78efc72
capDL-tool: fix ASIDPool check
lsf37 Nov 17, 2025
ff2e6ab
capDL-tool: add an AArch64 test example
lsf37 Nov 17, 2025
280b0ca
CHANGES: add SGISignal cap entry
lsf37 Nov 17, 2025
36085a4
trivial: style update
lsf37 Nov 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .reuse/dep5
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 7 additions & 1 deletion CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: <num>, target: <num>)` 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
Expand Down
2 changes: 2 additions & 0 deletions capDL-tool/CapDL/AST.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,8 @@ data ObjParam =
msi_irq_extraParam :: MSIIRQExtraParam }
| ARMIRQExtraParam {
arm_irq_extraParam :: ARMIRQExtraParam }
| ARMSGISignalIrq {
sgi_irq :: Word }
| InitArguments {
arguments :: [Word] }
| DomainID {
Expand Down
14 changes: 14 additions & 0 deletions capDL-tool/CapDL/MakeModel.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Comment thread
lsf37 marked this conversation as resolved.

getMaybeBitSize :: [ObjParam] -> Maybe Word
getMaybeBitSize [] = Nothing
getMaybeBitSize (BitSize x : _) = Just x
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)

Expand Down
5 changes: 5 additions & 0 deletions capDL-tool/CapDL/Model.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,7 @@ data Cap
| ARMSMCCap {
capObj :: ObjID,
capBadge :: Word }
| ARMSGISignalCap { capObj :: ObjID }
Copy link
Copy Markdown
Contributor

@Indanz Indanz Nov 18, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So this is where the model deviates from reality and the properties are not part of the cap, but instead we pretend here they are elsewhere?

I don't understand what the advantage of that is, wouldn't that confuse object creation code when it creates zero sized SGI caps? Those won't be derivates of the UT cap either, so revoking the UT won't automatically clean up the SGI cap, which breaks normally valid assumptions. With this in mind, I really don't like pretending it's an object while it isn't.

Copy link
Copy Markdown
Member Author

@lsf37 lsf37 Nov 18, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree with you, for these caps it'd be conceptually nicer not to do that. Since capDL already deals with the issue for a lot of other cap types, there is infrastructure for fake objects, but no infrastructure for caps with content but without objects (only the control caps have no object in capDL).

For the concrete concerns, they are both fine and dealt with by the existing infrastructure for fake objects: the caps are not created from Untypeds and the loader knows that, so their derivation tree is not confused and revocation on UT is not supposed to clean up the object (the sgi_signal objects should not be under any untyped cover in the spec -- maybe I should add an explicit check for that). You can still specify an original cap and a derived cap (there are only two levels for SGISignalCap) and that works fine in the loader as well, it has an explicit is_original flag that is used for this.

SGISignal caps can be revoked either by revoking on the IRQControl cap (which removes all of them, including IRQHandlers), or individually (that's what the second level is useful for) -- that's not specific to capDL, though, that's just how the IRQ-related caps work in the kernel.

So it does work fine with the right semantics, and in terms of capDL it does actually fit with how the rest is treated. It is awkward in the formalisation, because for other fake objects there is some kind of state in the kernel I can tie them to, but for these ones there is not, the data is only in the cap. So the indirection is going to be annoying in the proof. But it's better dealing with that only once than trying to build and debug a whole lot of infrastructure for creating caps in a different way to what the rest of the tools are used to.


-- X86 specific caps
| IOPortsCap {
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -256,6 +260,7 @@ data KOType
| ARMSID_T
| ARMCB_T
| ARMSMC_T
| ARMSGISignal_T
| ASIDPool_T
| PT_T
| PD_T
Expand Down
8 changes: 8 additions & 0 deletions capDL-tool/CapDL/ParserUtils.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -466,6 +473,7 @@ object_param =
<|> ports_param
<|> asid_high_param
<|> cb_extra_param
<|> arm_sgi_signal_irq

object_params :: MapParser [ObjParam]
object_params =
Expand Down
8 changes: 8 additions & 0 deletions capDL-tool/CapDL/PrintC.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ++
Expand Down Expand Up @@ -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

Expand Down
9 changes: 7 additions & 2 deletions capDL-tool/CapDL/PrintUtils.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
3 changes: 3 additions & 0 deletions capDL-tool/CapDL/PrintXml.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ = []

--
Expand Down Expand Up @@ -120,6 +121,7 @@ showObjectName ARMIrq {} = "ARMIrq"
showObjectName ARMSID {} = "ARMSID"
showObjectName ARMCB {} = "ARMCB"
showObjectName ARMSMC = "ARMSMC"
showObjectName ARMSGISignal {} = "ARMSGISignal"

--
-- Get a cap's name.
Expand Down Expand Up @@ -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)]
Expand Down
8 changes: 7 additions & 1 deletion capDL-tool/CapDL/State.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -407,13 +409,15 @@ 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
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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Comment thread
lsf37 marked this conversation as resolved.
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
Expand Down
1 change: 1 addition & 0 deletions capDL-tool/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion capDL-tool/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions capDL-tool/capdl.dtd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@
<!ATTLIST object level CDATA #IMPLIED>
<!ATTLIST object domain CDATA #IMPLIED>
<!ATTLIST object device CDATA #IMPLIED>
<!ATTLIST object irq CDATA #IMPLIED>
<!ATTLIST object target CDATA #IMPLIED>

<!ELEMENT cap EMPTY>
<!ATTLIST cap id CDATA #REQUIRED>
Expand Down
Loading