capDL-tool/CapDL/PrintC.hs

--
-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
--
-- SPDX-License-Identifier: BSD-2-Clause
--

-- Printer for C source format to be consumed by the CapDL initialiser.
-- Note: corresponds to the -c/--code argument.

module CapDL.PrintC where

import CapDL.Model
import CapDL.PrintUtils (sortObjects)

import Prelude ()
import Prelude.Compat
import Control.Exception (assert)
import Data.Ord (comparing)
import Data.List.Compat
import Data.List.Utils
import Data.Maybe (fromJust, fromMaybe)
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.Bits
import Numeric (showHex)
import Text.PrettyPrint

-- What we print depends on whether objects are pre-allocated.
data AllocationType =
       StaticAlloc
     | DynamicAlloc ObjectSizeMap

(+++) :: String -> String -> String
s1 +++ s2 = s1 ++ "\n" ++ s2

joinBy :: String -> [String] -> String
joinBy = intercalate

hex :: Word -> String
hex x = "0x" ++ showHex x ""

-- This prints paddrs in hex, except that Nothing (no fixed address)
-- is simply "0" for clarity.
pointerOfPAddr :: Maybe Word -> String
pointerOfPAddr p = fromMaybe "0" (hex <$> p)

maxObjects :: Int -> String
maxObjects count = "#define MAX_OBJECTS " ++ show count

memberArch :: Arch -> String
memberArch arch =
    "#if !defined(CONFIG_ARCH_" ++ a ++ ")" +++
    "#    error \"invalid target architecture; expecting " ++ a ++ "\"" +++
    "#endif"
    where
        a = case arch of
            IA32 -> "IA32"
            ARM11 -> "ARM"
            X86_64 -> "X86_64"
            AARCH64 -> "AARCH64"
            RISCV -> "RISCV"

memberNum :: Int -> String
memberNum n = ".num = " ++ show n ++ ","

showObjID :: Map ObjID Int -> ObjID -> String
showObjID xs id = (case Map.lookup id xs of
    Just w -> show w
    _ -> "INVALID_SLOT") ++ " /* " ++ fst id ++ " */"

rightConst :: Rights -> String
rightConst = ("CDL_Can"++) . show

showRights :: CapRights -> String
showRights rights
  | Set.null rights = "0"
  | otherwise =
      "(" ++ joinBy "|" (rightConst <$> Set.toList rights) ++ ")"

showPCI :: Word -> (Word, Word, Word) -> String
showPCI domainID (pciBus, pciDev, pciFun) =
    hex $ shift domainID 16 .|. shift pciBus 8 .|. shift pciDev 3 .|. pciFun

-- Lookup-by-value on a dictionary. I feel like I need a shower.
lookupByValue :: (a -> Bool) -> Map k a -> k
lookupByValue f m = head $ Map.keys $ Map.filter f m

showCap :: Map ObjID Int -> Cap -> IRQMap -> String -> ObjMap Word -> String
showCap _ NullCap _ _ _ = "{.type = CDL_NullCap}"
showCap objs (UntypedCap id) _ _ _ =
    "{.type = CDL_UntypedCap, .obj_id = " ++ showObjID objs id ++ "}"
showCap objs (EndpointCap id badge rights) _ is_orig _ =
    "{.type = CDL_EPCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++
    ", .rights = " ++ showRights rights ++
    ", .data = { .tag = CDL_CapData_Badge, .badge = " ++ show badge ++ "}}"
showCap objs (NotificationCap id badge rights) _ is_orig _ =
    "{.type = CDL_NotificationCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++
    ", .rights = " ++ showRights rights ++
    ", .data = { .tag = CDL_CapData_Badge, .badge = " ++ show badge ++
    "}}"
showCap objs (ReplyCap id) _ _ _ =
    "{.type = CDL_ReplyCap, .obj_id = " ++ showObjID objs id ++ "}"
    -- XXX: Does it even make sense to give out a reply cap? How does init fake this?
showCap objs (MasterReplyCap id) _ _ _ =
    "{.type = CDL_MasterReplyCap, .obj_id = " ++ showObjID objs id ++ "}"
    -- XXX: As above.
showCap objs (CNodeCap id guard guard_size) _ is_orig _ =
    "{.type = CDL_CNodeCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++
    ", .rights = CDL_AllRights, .data = CDL_CapData_MakeGuard(" ++
    show guard_size ++ ", " ++ show guard ++ ")}"
showCap objs (TCBCap id) _ is_orig _ =
    "{.type = CDL_TCBCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++
    ", .rights = CDL_AllRights}"
showCap _ IRQControlCap _ _ _ = "{.type = CDL_IRQControlCap}"
showCap _ DomainCap _ _ _ = "{.type = CDL_DomainCap}"
showCap _ (IRQHandlerCap id) irqNode is_orig _ =
    "{.type = CDL_IRQHandlerCap, .obj_id = INVALID_OBJ_ID" ++
    ", .is_orig = " ++ is_orig ++
    ", .irq = " ++ show (lookupByValue (== id) irqNode) ++ "}"
    -- Caps have obj_ids, or IRQs, but not both.
showCap _ (IRQIOAPICHandlerCap id) irqNode is_orig _ =
    "{.type = CDL_IRQHandlerCap, .obj_id = INVALID_OBJ_ID" ++
    ", .is_orig = " ++ is_orig ++
    ", .irq = " ++ show (lookupByValue (== id) irqNode) ++ "}"
    -- Caps have obj_ids, or IRQs, but not both.
showCap _ (IRQMSIHandlerCap id) irqNode is_orig _ =
    "{.type = CDL_IRQHandlerCap, .obj_id = INVALID_OBJ_ID" ++
    ", .is_orig = " ++ is_orig ++
    ", .irq = " ++ show (lookupByValue (== id) irqNode) ++ "}"
showCap _ (ARMIRQHandlerCap id) irqNode is_orig _ =
    "{.type = CDL_IRQHandlerCap, .obj_id = INVALID_OBJ_ID" ++
    ", .is_orig = " ++ is_orig ++
    ", .irq = " ++ show (lookupByValue (== id) irqNode) ++ "}"
    -- Caps have obj_ids, or IRQs, but not both.
showCap objs (FrameCap id rights _ cached maybe_mapping) _ is_orig _ =
    "{.type = CDL_FrameCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++
    ", .rights = " ++ showRights rights ++
    ", .vm_attribs = " ++
          (if cached then "seL4_ARCH_Default_VMAttributes" else "CDL_VM_CacheDisabled") ++
    ", .mapping_container_id = " ++
          (case maybe_mapping of
               Just (mapping_container, _) -> showObjID objs mapping_container;
               _ -> "INVALID_OBJ_ID") ++
    ", .mapping_slot = " ++
          (case maybe_mapping of
               Just (_, mapping_slot) -> show mapping_slot;
               _ -> "0") ++
    "}"
    -- FIXME: I feel like I should be doing something with the ASID data here...
showCap objs (ARMSIDCap id) _ is_orig _ =
    "{.type = CDL_SIDCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ "}"
showCap objs (ARMCBCap id) _ is_orig _ =
    "{.type = CDL_CBCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ "}"

showCap objs (PTCap id _) _ is_orig _ =
    "{.type = CDL_PTCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"
showCap objs (PDCap id _) _ is_orig _ =
    "{.type = CDL_PDCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"

showCap objs (PDPTCap id _) _ is_orig _ =
    "{.type = CDL_PDPTCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"
showCap objs (PML4Cap id _) _ is_orig _ =
    "{.type = CDL_PML4Cap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"
showCap objs (PUDCap id _) _ is_orig _ =
    "{.type = CDL_PUDCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"
showCap objs (PGDCap id _) _ is_orig _ =
    "{.type = CDL_PGDCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"
showCap _ ASIDControlCap _ _ _ =
    "{.type = CDL_ASIDControlCap}"
showCap objs (ASIDPoolCap id) _ _ _ =
    "{.type = CDL_ASIDPoolCap, .obj_id = " ++ showObjID objs id ++ "}"
showCap objs (IOPortsCap id) _ is_orig _ =
    "{.type = CDL_IOPortsCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"
showCap objs (IOSpaceCap id) _ is_orig ms =
    "{.type = CDL_IOSpaceCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++
    ", .data = { .tag = CDL_CapData_Raw, .data = " ++ showPCI dom pci ++ "}}"
    where pci = pciDevice $ fromJust $ Map.lookup id ms
          dom = domainID $ fromJust $ Map.lookup id ms
showCap objs (ARMIOSpaceCap id) _ is_orig ms =
    "{.type = CDL_ARMIOSpaceCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++
    ", .data = { .tag = CDL_CapData_Raw, .data = " ++ show iospace ++ "}}"
    where iospace = armiospace $ fromJust $ Map.lookup id ms
showCap objs (VCPUCap id) _ _ _ = "{.type = CDL_VCPUCap, .obj_id = " ++ showObjID objs id ++ "}"
showCap _ (SchedControlCap affinity) _ _ _ =
    "{.type = CDL_SchedControlCap, .obj_id = " ++ (hex affinity) ++ " }"
showCap objs (RTReplyCap id rights) _ _ _ =
    "{.type = CDL_RTReplyCap, .obj_id = " ++ showObjID objs id ++
    ", .rights = " ++ showRights rights ++ "}"
showCap objs (SCCap id) _ is_orig _ =
    "{.type = CDL_SCCap, .obj_id = " ++ showObjID objs id ++
    ", .is_orig = " ++ is_orig ++ "}"
showCap _ x _ _ _ = assert False $
    "UNSUPPORTED CAP TYPE: " ++ show x
    -- These are not supported by the initialiser itself.

showSlots :: Map ObjID Int -> ObjID -> [(Word, Cap)] -> IRQMap -> CDT -> ObjMap Word -> String
showSlots _ _ [] _ _ _ = ""
showSlots objs obj_id (x:xs) irqNode cdt ms =
    "{" ++ show index ++ ", " ++ slot ++ "}," +++
    showSlots objs obj_id xs irqNode cdt ms
    where
        index = fst x
        slot = showCap objs (snd x) irqNode is_orig ms
        is_orig = if Map.notMember (obj_id, index) cdt then "true" else "false"

memberSlots :: Map ObjID Int -> ObjID -> CapMap Word -> IRQMap -> CDT -> ObjMap Word -> String
memberSlots objs obj_id slots irqNode cdt ms =
    ".slots.num = " ++ show slot_count ++ "," +++
    ".slots.slot = (CDL_CapSlot[]) {" +++
    showSlots objs obj_id (Map.toList slots) irqNode cdt ms +++
    "},"
    where
        slot_count = Map.size slots

printInit :: [Word] -> String
printInit argv =
    "{" ++ joinBy ", " (map show argv) ++ "}"

showFrameFill :: [String] -> String
showFrameFill (dest_offset:dest_len:info_type:extra)  =
    "{.type = " ++ info_type ++ "," +++
    ".dest_offset = " ++ dest_offset ++ "," +++
    ".dest_len = " ++ dest_len ++ "," +++
    case (info_type,extra) of
        ("CDL_FrameFill_BootInfo",(bi_type:src_offset:[])) ->
            ".bi_type = {.type = " ++ bi_type ++ "," +++
            ".src_offset = " ++ src_offset +++
            "}},"
        ("CDL_FrameFill_FileData",(filename:file_offset:[])) ->
            ".file_data_type = {.filename = " ++ filename ++ "," +++
            ".file_offset = " ++ file_offset +++
            "}},"
        _ -> "#error Bad CDL_FrameFill_BootInfo args"
showFrameFill _  = ""

showFrameFills :: Maybe [[String]] -> String
showFrameFills (Just fills)  =
    ".fill = { " ++ unwords (map showFrameFill fills) ++ "}"
showFrameFills _ = ""


showFramePaddr :: Maybe Word -> String
showFramePaddr paddr =
    ".paddr = " ++ pointerOfPAddr paddr ++ ","

showObjectFields :: Map ObjID Int -> ObjID -> KernelObject Word -> IRQMap -> CDT -> ObjMap Word -> String
showObjectFields _ _ Endpoint _ _ _ = ".type = CDL_Endpoint,"
showObjectFields _ _ Notification _ _ _ = ".type = CDL_Notification,"
showObjectFields objs obj_id (TCB slots faultEndpoint info domain argv) _ _ _ =
    ".type = CDL_TCB," +++
    ".tcb_extra = {" +++
    "#if (" ++ hex ipcbuffer_addr ++ " & ((1 << seL4_IPCBufferSizeBits) - 1)) != 0" +++
    "#    error \"IPC buffer not correctly aligned\"" +++
    "#endif" +++
    ".ipcbuffer_addr = " ++ hex ipcbuffer_addr ++ "," +++
    ".priority = " ++ show priority ++ "," +++
    ".max_priority = " ++ show max_priority ++ "," +++
    ".affinity = " ++ show affinity ++ "," +++
    ".pc = " ++ hex pc ++ "," +++
    ".sp = " ++ hex stack ++ "," +++
    ".init = (const seL4_Word[])" ++ printInit argv ++ "," +++
    ".init_sz = " ++ show (length argv) ++ "," +++
    ".domain = " ++ show domain ++ "," +++
    ".resume = " ++ show resume' ++ "," +++
    ".fault_ep = " ++ show fault_ep ++ "," +++
    "}," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
    where
        ipcbuffer_addr = case info of {Just i -> ipcBufferAddr i; _ -> 0}
        priority = case info of {Just i -> case prio i of {Just p -> p; _ -> 125}; _ -> 125}
        max_priority = case info of {Just i -> case max_prio i of {Just p -> p; _ -> 125}; _ -> 125}
        affinity = case info of {Just i -> case affin i of {Just p -> p; _ -> 0}; _ -> 0}
        resume' = case info of {Just i -> case resume i of {Just True -> 1; Just False -> 0; _ -> 1}; _ -> 1}
        pc = case info of {Just i -> case ip i of {Just v -> v; _ -> 0}; _ -> 0}
        stack = case info of {Just i -> case sp i of {Just v -> v; _ -> 0}; _ -> 0}
        fault_ep = case faultEndpoint of {Just w -> w; _ -> 0}
showObjectFields objs obj_id (CNode slots sizeBits info) irqNode cdt ms =
    ".type = " ++ t ++ "," +++
    ".size_bits = " ++ show sizeBits ++ "," +++
    cnode_extra ++
    memberSlots objs obj_id slots irqNode cdt ms
    where
        -- IRQs are represented in CapDL as 0-sized CNodes. This is fine for
        -- the model, but the initialiser needs to know what objects represent
        -- interrupts to avoid trying to create them at runtime. It's a bit of
        -- a hack to assume that any 0-sized CNode is an interrupt, but this is
        -- an illegal size for a valid CNode so everything should work out.
        t = if sizeBits == 0 then "CDL_Interrupt" else "CDL_CNode"

        -- CNode-only attributes:
        --   hasUntyped instructs the rootserver to hand-off UntypedMemory objects
        untyped = case hasUntyped info of {Just True -> 1; _ -> 0}
        cnode_extra = if sizeBits == 0 then "" else
            ".cnode_extra = {" +++
                ".has_untyped_memory = " ++ show untyped ++ "," +++
            "},\n"
showObjectFields objs obj_id (IOAPICIrq slots ioapic pin level polarity) irqNode cdt ms =
    ".type = CDL_IOAPICInterrupt, " +++
    memberSlots objs obj_id slots irqNode cdt ms +++
    ".ioapicirq_extra = {" +++
        ".ioapic = " ++ show ioapic ++ "," +++
        ".ioapic_pin = " ++ show pin ++ "," +++
        ".level = " ++ show level ++ "," +++
        ".polarity = " ++ show polarity ++ "," +++
    "},"
showObjectFields objs obj_id (MSIIrq slots handle bus dev fun) irqNode cdt ms =
    ".type = CDL_MSIInterrupt, " +++
    memberSlots objs obj_id slots irqNode cdt ms +++
    ".msiirq_extra = {" +++
        ".handle = " ++ show handle ++ "," +++
        ".pci_bus = " ++ show bus ++ "," +++
        ".pci_dev = " ++ show dev ++ "," +++
        ".pci_fun = " ++ show fun ++ "," +++
    "},"
showObjectFields objs obj_id (ARMIrq slots trigger target) irqNode cdt ms =
    ".type = CDL_ARMInterrupt, " +++
    memberSlots objs obj_id slots irqNode cdt ms +++
    ".armirq_extra = {" +++
        ".trigger = " ++ show trigger ++ "," +++
        ".target = " ++ show target ++ "," +++
    "},"
showObjectFields _ _ (Untyped size_bits paddr) _ _ _ =
    ".type = CDL_Untyped," +++
    ".size_bits = " ++ maybe "-1" show size_bits ++ "," +++
    ".paddr = " ++ pointerOfPAddr paddr ++ ","
showObjectFields objs obj_id (PT slots) _ _ _ =
    ".type = CDL_PT," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
showObjectFields objs obj_id (PD slots) _ _ _ =
    ".type = CDL_PD," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
showObjectFields objs obj_id (PDPT slots) _ _ _ =
    ".type = CDL_PDPT," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
showObjectFields objs obj_id (PML4 slots) _ _ _ =
    ".type = CDL_PML4," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
showObjectFields objs obj_id (PUD slots) _ _ _ =
    ".type = CDL_PUD," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
showObjectFields objs obj_id (PGD slots) _ _ _ =
    ".type = CDL_PGD," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
showObjectFields _ _ (Frame size paddr extra) _ _ _ =
    ".type = CDL_Frame," +++
    ".size_bits = " ++ show size ++ "," +++
    ".frame_extra = { " ++ showFramePaddr paddr ++ showFrameFills extra +++ " },"
showObjectFields _ _ (IOPorts (start, end)) _ _ _ =
    ".type = CDL_IOPorts," +++
    ".start = " ++ show start ++ "," ++
    ".end = " ++ show end ++ ","
showObjectFields objs obj_id (ASIDPool slots asidHigh) _ _ _ =
    ".type = CDL_ASIDPool," +++
    ".asid_high = " ++ maybe "-1" hex asidHigh ++ "," +++
    memberSlots objs obj_id slots Map.empty Map.empty Map.empty -- IRQ, cdt and obj map not required
showObjectFields _ _ IODevice{} _ _ _ =
    ".type = CDL_IODevice,"
showObjectFields _ _ ARMIODevice{} _ _ _ =
    ".type = CDL_ARMIODevice,"
showObjectFields _ _ VCPU _ _ _ = ".type = CDL_VCPU,"
showObjectFields _ _ (SC info size_bits) _ _ _ =
    ".type = CDL_SchedContext," +++
    ".sc_extra = {" +++
        ".period = " ++ show sc_period ++ "," +++
        ".budget = " ++ show sc_budget ++ "," +++
        ".data = " ++ show sc_data ++ "," +++
    "}," +++
    ".size_bits = " ++ show sizeBits ++ ","
    where
    sc_period = fromMaybe 0 (maybe Nothing period info)
    sc_budget = fromMaybe 0 (maybe Nothing budget info)
    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 _ _ x _ _ _ = assert False $
    "UNSUPPORTED OBJECT TYPE: " ++ show x

showObject :: Map ObjID Int -> (ObjID, KernelObject Word) -> IRQMap -> CDT -> ObjMap Word -> String
showObject objs obj irqNode cdt ms =
    "{" +++
    "#ifdef CONFIG_DEBUG_BUILD" +++ ".name = \"" ++ name ++ "\"," +++ "#endif" +++
    showObjectFields objs id (snd obj) irqNode cdt ms +++
    "}"
    where
        id = fst obj
        name = fst id ++ (case snd id of
            Just index -> "[" ++ show index ++ "]"
            _ -> "")

showObjects :: Map ObjID Int -> Int -> [(ObjID, KernelObject Word)] -> IRQMap -> CDT -> ObjMap Word -> String
showObjects _ _ [] _ _ _ = ""
showObjects objs counter (x:xs) irqNode cdt ms =
    "[" ++ show counter ++ "] = " ++ showObject objs x irqNode cdt ms ++ "," +++
    showObjects objs (counter + 1) xs irqNode cdt ms

memberObjects :: Map ObjID Int -> [(ObjID, KernelObject Word)] -> IRQMap -> CDT ->
                 ObjMap Word -> String
memberObjects obj_ids obj_list irqNode cdt objs =
    ".objects = (CDL_Object[]) {" +++
    showObjects obj_ids 0 obj_list irqNode cdt objs +++
    "},"

-- Emit an array where each entry represents a given interrupt. Each is -1 if
-- that interrupt has no handler or else the object ID of the interrupt
-- (0-sized CNode).
memberIRQs :: Map ObjID Int -> IRQMap -> Arch -> String
memberIRQs objs irqNode _ =
    let maxIrq = case Map.null irqNode of
            False -> fst $ Map.findMax irqNode
            True -> 0
    in
    ".num_irqs = " ++ show (maxIrq + 1) ++ "," +++
    ".irqs = (CDL_ObjID[]){" +++
    joinBy ", "
        [ case Map.lookup k irqNode of
              Just i -> show $ fromJust $ Map.lookup i objs
              _ -> "-1"
        | k <- [0 .. maxIrq]
        ] +++
    "},"

showUntypedDerivation :: Map ObjID Int -> ObjID -> [ObjID] -> String
showUntypedDerivation objs utID utChildren =
    "{" +++
    "  .untyped = " ++ showObjID objs utID ++ "," +++
    "  .num = " ++ show (length utChildren) ++ "," +++
    "  .children = (CDL_ObjID[]){" +++
    Data.List.Utils.join ",\n"
        ["    " ++ showObjID objs childID | childID <- utChildren] +++
    "  }" +++
    "}"

showUntypedDerivations :: AllocationType -> Map ObjID Int -> CoverMap -> String
showUntypedDerivations DynamicAlloc{} _ untypedCovers
  | all null (Map.elems untypedCovers) =
      ".num_untyped = 0," +++
      ".untyped = NULL,"
  | otherwise = error $
      "refusing to generate spec for dynamic allocation because the " ++
      "following untypeds already have children:\n" ++
      Data.List.Utils.join "\n"
        [ "  " ++ show utID
        | (utID, utChildren) <- Map.toList untypedCovers
        , not $ null utChildren ]
showUntypedDerivations StaticAlloc objs untypedCovers =
    ".num_untyped = " ++ show (Map.size untypedCovers) ++ "," +++
    ".untyped = (CDL_UntypedDerivation[]){" +++
    joinBy ",\n" (map (uncurry (showUntypedDerivation objs)) $
                  Map.toList untypedCovers) +++
    "},"

-- find all ASIDPools and prepare them for allocation wrt. asid_high.
getASIDPoolDerivations :: ObjMap Word -> [(Word, ObjID)]
getASIDPoolDerivations ms =
    let table =
          sortBy (comparing fst)
              [ (asidHigh, objID)
              | (objID, ASIDPool lowSlots maybeAsidHigh) <- Map.toList ms,
                -- sanity checks
                Map.null lowSlots
                    || can'tAllocate objID "it has nonempty low slots",
                maybeAsidHigh /= Nothing
                    || can'tAllocate objID "it has no assigned asid_high",
                let Just asidHigh = maybeAsidHigh
              ]
        asidHighs = map fst table
    in -- more sanity checks
       if asidHighs /= [1..fromIntegral (length asidHighs)]
       then error $ "ASID pools don't have slot numbers of the form [1..n]: " ++ show table
       else table
    where can'tAllocate objID reason =
              error $ "can't allocate ASID pool " ++ show objID ++ " because " ++ reason

showASIDPoolDerivations :: Map ObjID Int -> ObjMap Word -> String
showASIDPoolDerivations objs ms =
    let table = getASIDPoolDerivations ms
        -- include ignored slot 0
        array = "(CDL_ObjID)-1 /* slot reserved for root thread, ignored */"
                : map (showObjID objs . snd) table
    in ".num_asid_slots = " ++ show (length array) ++ "," +++
       ".asid_slots = (CDL_ObjID[]){" +++
           joinBy ",\n" ["    " ++ idStr | idStr <- array] +++
       "},"

printC :: AllocationType -> Model Word -> Idents CapName -> CopyMap -> Doc
printC allocType (Model arch objs irqNode cdt untypedCovers) _ _ =
    text $
    "/* Generated file. Your changes will be overwritten. */" +++
    "" +++
    "#include <capdl.h>" +++
    "#include <sel4/sel4.h>" +++
    "" +++
    "#ifndef INVALID_SLOT" +++
    "#define INVALID_SLOT (-1)" +++
    "#endif" +++
    "" +++
    maxObjects objs_sz +++ -- FIXME: I suspect this is not the right list to measure.
    "" +++
    "CDL_Model capdl_spec = {" +++
    memberArch arch +++
    memberNum objs_sz +++
    memberIRQs obj_ids irqNode arch +++
    memberObjects obj_ids obj_list irqNode cdt objs +++
    showUntypedDerivations allocType obj_ids untypedCovers +++
    showASIDPoolDerivations obj_ids objs +++
    "};"
    where objs_sz = length $ Map.toList objs
          obj_list = case allocType of
              StaticAlloc -> Map.toList objs
              DynamicAlloc objSizeMap -> sortObjects objSizeMap (Map.toList objs)
          obj_ids = Map.fromList $ flip zip [0..] $ map fst obj_list