Merge branch 'master' into corlewis/set-handler-params

.github/workflows/build.yml

@@ -16,7 +16,7 @@ jobs:
     name: Language Spec PDF
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v2
+    - uses: actions/checkout@v4
     - name: Install texlive and pandoc
       run: |
         sudo apt-get update
@@ -31,32 +31,31 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        python-version: [ '2.x', '3.9' ]
+        python-version: [ '3.9', '3.x' ]
       fail-fast: false
     steps:
-    - uses: actions/checkout@v2
-    - uses: actions/setup-python@v2
+    - uses: actions/checkout@v4
+    - uses: actions/setup-python@v5
       with:
         python-version: ${{ matrix.python-version }}
     - name: Install python packages
       run: |
         cd python-capdl-tool
-        pip install -r requirements.txt
-        pip install nose future
+        pip3 install -r requirements.txt
     - name: Run tests
       run: |
         cd python-capdl-tool/tests
-        nosetests --exe
+        PYTHONPATH=../ ./runall.py
 
   capDL-tool:
     name: capDL-tool (ghc)
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v2
+    - uses: actions/checkout@v4
     - run: |
         sudo apt-get update
         sudo apt-get install libxml2-utils
-    - uses: actions/setup-haskell@v1.1.4
+    - uses: haskell/actions/setup@v2
       with:
         enable-stack: true
         stack-setup-ghc: true

capDL-tool/CapDL/MakeModel.hs

@@ -479,6 +479,7 @@ objectOf n obj =
         Obj RTReply_T [] [] -> RTReply
         Obj ARMSID_T [] [] -> ARMSID
         Obj ARMCB_T ps [] -> ARMCB (getCBExtraInfo ps)
+        Obj ARMSMC_T [] [] -> ARMSMC
         Obj _ _ (_:_) ->
           error $ "Only untyped caps can have objects as content: " ++
                   n ++ " = " ++ show obj
@@ -603,6 +604,8 @@ validCapPars (Endpoint {}) ps =
     subsetConstrs (removeConstr (Rights undefined) ps) [Badge undefined]
 validCapPars (Notification {}) ps =
     subsetConstrs (removeConstr (Rights undefined) ps) [Badge undefined]
+validCapPars (ARMSMC {}) ps =
+    subsetConstrs ps [Badge undefined]
 validCapPars (TCB {}) ps =
     subsetConstrs ps [Reply, MasterReply] &&
     (not (containsConstr Reply ps) || not (containsConstr MasterReply ps))
@@ -655,6 +658,7 @@ objCapOf containerName obj objRef params =
         ARMIrq {} -> ARMIRQHandlerCap objRef
         ARMSID {} -> ARMSIDCap objRef
         ARMCB {} -> ARMCBCap objRef
+        ARMSMC -> ARMSMCCap objRef (getBadge params)
     else error ("Incorrect params for cap to " ++ printID objRef ++ " in " ++
                 printID containerName ++ "; got " ++ show params)
 

capDL-tool/CapDL/Model.hs

@@ -118,6 +118,9 @@ data Cap
         | ARMIRQHandlerCap { capObj :: ObjID }
         | ARMSIDCap        { capObj :: ObjID }
         | ARMCBCap         { capObj :: ObjID }
+        | ARMSMCCap        {
+            capObj :: ObjID,
+            capBadge :: Word }
 
         -- X86 specific caps
         | IOPortsCap {
@@ -209,6 +212,8 @@ data KernelObject a
     | ARMSID
     | ARMCB { bankNumber :: Maybe Word }
 
+    | ARMSMC
+
 -- X86 specific objects
     | IOPorts { ports :: (Word, Word) }
     | IODevice {
@@ -249,6 +254,7 @@ data KOType
     | ARMIrqSlot_T
     | ARMSID_T
     | ARMCB_T
+    | ARMSMC_T
     | ASIDPool_T
     | PT_T
     | PD_T
@@ -414,6 +420,7 @@ objID = capObj
 hasRights :: Cap -> Bool
 hasRights (NotificationCap {})   = True
 hasRights (EndpointCap {})        = True
+hasRights (ARMSMCCap {})          = True
 hasRights (FrameCap {})           = True
 hasRights _                       = False
 

capDL-tool/CapDL/ParserUtils.hs

@@ -137,6 +137,7 @@ object_type =
     <|> keyw "rtreply" RTReply_T
     <|> keyw "streamid" ARMSID_T
     <|> keyw "contextbank" ARMCB_T
+    <|> keyw "smc" ARMSMC_T
 
 obj_bit_size :: MapParser ObjParam
 obj_bit_size = do

capDL-tool/CapDL/PrintC.hs

@@ -158,6 +158,11 @@ showCap objs (ARMSIDCap id) _ is_orig _ =
 showCap objs (ARMCBCap id) _ is_orig _ =
     "{.type = CDL_CBCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ "}"
 
+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 (PTCap id _) _ is_orig _ =
     "{.type = CDL_PTCap, .obj_id = " ++ showObjID objs id ++
     ", .is_orig = " ++ is_orig ++ "}"
@@ -379,6 +384,7 @@ showObjectFields _ _ (SC info size_bits) _ _ _ =
 showObjectFields _ _ (RTReply {}) _ _ _ = ".type = CDL_RTReply,"
 showObjectFields _ _ (ARMSID {}) _ _ _ = ".type = CDL_SID,"
 showObjectFields _ _ (ARMCB {}) _ _ _ = ".type = CDL_CB,"
+showObjectFields _ _ ARMSMC _ _ _ = ".type = CDL_SMC,"
 showObjectFields _ _ x _ _ _ = assert False $
     "UNSUPPORTED OBJECT TYPE: " ++ show x
 

capDL-tool/CapDL/PrintUtils.hs

@@ -215,6 +215,7 @@ prettyObjParams obj = case obj of
     ARMIrq _ trigger target -> text "arm_irq" <+> maybeParensList[prettyARMIRQTrigger trigger, prettyARMIRQTarget target]
     ARMSID {} -> text "streamid"
     ARMCB {} -> text "contextbank"
+    ARMSMC {} -> text "smc"
 
 capParams [] = empty
 capParams xs = parens (hsep $ punctuate comma xs)
@@ -305,6 +306,8 @@ maybeCapParams cap = case cap of
         capParams (maybeBadge badge ++ maybeRights False rights)
     NotificationCap _ badge rights ->
         capParams (maybeBadge badge ++ maybeRights False rights)
+    ARMSMCCap _ badge ->
+        capParams (maybeBadge badge)
     ReplyCap _ -> capParams [text "reply"]
     MasterReplyCap _ -> capParams [text "master_reply"]
     CNodeCap _ guard gsize ->
@@ -335,6 +338,8 @@ sameParams cap1 cap2 =
     ((EndpointCap _ b1 r1), (EndpointCap _ b2 r2)) -> b1 == b2 && r1 == r2
     ((NotificationCap _ b1 r1), (NotificationCap _ b2 r2)) ->
         b1 == b2 && r1 == r2
+    ((ARMSMCCap _ b1), (ARMSMCCap _ b2)) ->
+        b1 == b2
     ((CNodeCap _ g1 gs1), (CNodeCap _ g2 gs2)) ->
         g1 == g2 && gs1 == gs2
     ((FrameCap _ r1 a1 c1 m1), (FrameCap _ r2 a2 c2 m2)) -> r1 == r2 && a1 == a2 && c1 == c2 && m1 == m2

capDL-tool/CapDL/PrintXml.hs

@@ -119,6 +119,7 @@ showObjectName MSIIrq {} = "MSIIrq"
 showObjectName ARMIrq {} = "ARMIrq"
 showObjectName ARMSID {} = "ARMSID"
 showObjectName ARMCB {} = "ARMCB"
+showObjectName ARMSMC = "ARMSMC"
 
 --
 -- Get a cap's name.
@@ -158,10 +159,12 @@ showCapName RTReplyCap {} = "RTReplyCap"
 showCapName SchedControlCap {} = "SchedControlCap"
 showCapName ARMSIDCap {} = "ARMSIDCap"
 showCapName ARMCBCap {} = "ARMCBCap"
+showCapName ARMSMCCap {} = "ARMSMCCap"
 
 showExtraCapAttributes :: Cap -> [(String, String)]
 showExtraCapAttributes (EndpointCap _ capBadge _) = [("badge", show capBadge)]
 showExtraCapAttributes (NotificationCap _ capBadge _) = [("badge", show capBadge)]
+showExtraCapAttributes (ARMSMCCap _ capBadge) = [("badge", show capBadge)]
 showExtraCapAttributes (CNodeCap _ guard guardSize) =
     [("guard", show guard), ("guardSize", show guardSize)]
 showExtraCapAttributes (FrameCap _ _ _ False _) = [("cached", "False")]

capDL-tool/CapDL/State.hs

@@ -321,6 +321,7 @@ koType (MSIIrq {}) = MSIIrqSlot_T
 koType (ARMIrq {}) = ARMIrqSlot_T
 koType (ARMSID {}) = ARMSID_T
 koType (ARMCB {}) = ARMCB_T
+koType ARMSMC = ARMSMC_T
 
 objAt :: (KernelObject Word -> Bool) -> ObjID -> Model Word -> Bool
 objAt p ref = maybe False p . maybeObject ref
@@ -357,6 +358,7 @@ capTyp (IRQMSIHandlerCap {}) = MSIIrqSlot_T
 capTyp (ARMIRQHandlerCap {}) = ARMIrqSlot_T
 capTyp (ARMSIDCap {}) = ARMSID_T
 capTyp (ARMCBCap {}) = ARMCB_T
+capTyp (ARMSMCCap {}) = ARMSMC_T
 capTyp _ = error "cap has no object"
 
 checkTypAt :: Cap -> Model Word -> ObjID -> Word -> Logger Bool
@@ -406,10 +408,12 @@ validCapArch X86_64 (IOPTCap {}) = True
 validCapArch ARM11 (ARMIOSpaceCap {}) = True
 validCapArch ARM11 (ARMIRQHandlerCap {}) = 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 _ _ = False
 
 checkCapArch :: Arch -> Cap -> ObjID -> Word -> Logger Bool
@@ -466,6 +470,8 @@ validObjArch AARCH64 (PUD {}) = True
 validObjArch AARCH64 (PGD {}) = True
 validObjArch AARCH64 (ARMSID {}) = True
 validObjArch AARCH64 (ARMCB {}) = True
+validObjArch AARCH64 (ARMSMC {}) = True
+validObjArch AARCH64 (ARMIODevice {}) = True
 validObjArch _ _ = False
 
 checkObjArch :: Arch -> KernelObject Word -> ObjID -> Logger Bool

capDL-tool/Main.hs

@@ -164,6 +164,7 @@ genObjectSizeMap m =
                       , ("seL4_ARMIRQ",              ARMIrqSlot_T)
                       , ("seL4_ARMSID",              ARMSID_T)
                       , ("seL4_ARMCB",               ARMCB_T)
+                      , ("seL4_ARMSMC",              ARMSMC_T)
                       ]
 
 -- Abort with an error message if 'isFullyAllocated' fails.

capDL-tool/capDL-tool.cabal

@@ -17,8 +17,8 @@ copyright:           Data61, CSIRO
 category:            Development
 build-type:          Simple
 extra-source-files:  README.md
-cabal-version:       >=1.18
-tested-with:         GHC == 8.8.4, GHC == 9.0.2
+cabal-version:       1.18
+tested-with:         GHC == 9.2.8
 
 executable parse-capDL
   main-is:             Main.hs
@@ -32,15 +32,15 @@ executable parse-capDL
   build-depends:
                        -- Included libraries
                        array >=0.5 && <0.6,
-                       base >= 4.13 && <4.16,
+                       base >= 4.16,
                        containers >=0.6 && <0.7,
                        filepath >=1.4 && <1.5,
                        mtl >=2.2 && <2.3,
                        parsec >=3.1 && <3.2,
                        unix >=2.7 && <3,
 
                        -- Other libraries
-                       base-compat >= 0.11 && <0.12,
+                       base-compat == 0.12.*,
                        lens >= 4.15,
                        MissingH >=1.4 && <1.6,
                        pretty >=1.1 && <1.2,
@@ -59,3 +59,5 @@ executable parse-capDL
 
   ghc-options:         -O2 -Werror -Wall -fno-warn-name-shadowing
                        -fno-warn-missing-signatures -fno-warn-type-defaults
+                       -fno-warn-incomplete-uni-patterns
+                       -fno-warn-incomplete-record-updates

capDL-tool/stack.yaml

@@ -4,7 +4,7 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-# Stackage LTS Haskell 19.12 (ghc-9.0.2)
-resolver: lts-19.12
+# Stackage LTS Haskell 20.25 (ghc-9.2.8)
+resolver: lts-20.25
 
 local-bin-path: .

capdl-loader-app/include/capdl.h

@@ -83,6 +83,9 @@ typedef enum {
     CDL_ARMIOSpaceCap,
     CDL_SIDCap,
     CDL_CBCap,
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    CDL_SMCCap,
+#endif
 #endif
 #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
     CDL_VCPUCap,
@@ -169,8 +172,10 @@ typedef enum {
     CDL_Frame         = seL4_ARM_SmallPageObject,
 #ifdef CONFIG_ARCH_AARCH64
     CDL_PUD           = seL4_ARM_PageUpperDirectoryObject,
+#if !(defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined (CONFIG_ARM_PA_SIZE_BITS_40))
     CDL_PGD           = seL4_ARM_PageGlobalDirectoryObject,
 #endif
+#endif
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
     CDL_VCPU          = seL4_ARM_VCPUObject,
 #endif
@@ -208,6 +213,9 @@ typedef enum {
     CDL_ARMInterrupt = seL4_ObjectTypeCount + 11,
     CDL_SID = seL4_ObjectTypeCount + 12,
     CDL_CB = seL4_ObjectTypeCount + 13,
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    CDL_SMC = seL4_ObjectTypeCount + 14,
+#endif
 #endif
 #ifdef CONFIG_ARCH_RISCV
     CDL_Frame = seL4_RISCV_4K_Page,

capdl-loader-app/src/main.c

@@ -663,6 +663,12 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_
     }
 #endif
 
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    if (CDL_Obj_Type(obj) == CDL_SMC) {
+        return seL4_NoError;
+    }
+#endif
+
 #if !CONFIG_CAPDL_LOADER_STATIC_ALLOC
     if (isDeviceObject(obj)) {
         seL4_Word paddr = CDL_Obj_Paddr(obj);
@@ -1790,6 +1796,12 @@ static void init_cnode_slot(CDL_Model *spec, init_cnode_mode mode, CDL_ObjID cno
         src_index = seL4_CapASIDControl;
         move_cap = false;
         break;
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    case CDL_SMCCap:
+        src_index = seL4_CapSMC;
+        move_cap = false;
+        break;
+#endif
     default:
         src_index = orig_caps(target_cap_obj);
         break;
@@ -1906,12 +1918,12 @@ static void init_copy_addr(seL4_BootInfo *bi)
      * the next 16mb alignment where we can map in a pagetable.
      */
     uintptr_t bi_start = (uintptr_t)bi;
-    copy_addr = ROUND_UP(bi_start + PAGE_SIZE_4K + bi->extraLen, 0x1000000);
+    copy_addr = ROUND_UP(bi_start + seL4_BootInfoFrameSize + bi->extraLen, 0x1000000);
 }
 
 static void cache_extended_bootinfo_headers(seL4_BootInfo *bi)
 {
-    uintptr_t cur = (uintptr_t)bi + PAGE_SIZE_4K;
+    uintptr_t cur = (uintptr_t)bi + seL4_BootInfoFrameSize;
     uintptr_t end = cur + bi->extraLen;
 
     while (cur < end) {

object_sizes/object_sizes.yaml

@@ -3,6 +3,7 @@
 #include <autoconf.h>
 #include <sel4/constants.h>
 #include <sel4/sel4_arch/constants.h>
+#include <sel4/sel4_arch/deprecated.h>
 #include <sel4/mode/types.h>
 seL4_TCBObject: seL4_TCBBits
 seL4_EndpointObject: seL4_EndpointBits
@@ -65,3 +66,4 @@ seL4_MSIIRQ: 0
 seL4_ARMIRQ: 0
 seL4_ARMSID: 0
 seL4_ARMCB: 0
+seL4_ARMSMC: 0

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
+    DomainControl, is_aligned, ARMIRQMode, ARMIRQ, ContextBank, StreamID, SMC
 from capdl.util import ctz
 from .Spec import Spec
 
@@ -168,6 +168,8 @@ def alloc(self, type, name=None, label=None, **kwargs):
             o = StreamID(name)
         elif type == ObjectType.seL4_ARMCB:
             o = ContextBank(name)
+        elif type == ObjectType.seL4_ARMSMC:
+            o = SMC(name)
         else:
             raise Exception('Invalid object type %s' % type)
         self.spec.add_object(o)