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

{-# OPTIONS_GHC -fno-warn-unused-binds #-}

module CapDL.MakeModel where

import CapDL.Model
import CapDL.AST
import CapDL.State

import Prelude ()
import Prelude.Compat
import Data.Maybe
import Data.List.Compat
import qualified Data.Either as Either
import Data.Data
import Data.Word
import Data.Bits
import Data.Function (on)
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Control.Monad.State as ST
import Control.Monad
import Control.Monad.Writer (tell)
import Text.PrettyPrint (text)

-- | A spec can place objects in explicit slots, or not.
-- This keeps track of the most recently used slot, and returns
-- the next slot when needed.
type SlotState = ST.State Word

getSlot :: SlotState Word
getSlot = do
    slot <- ST.get
    return $ slot + 1

putSlot :: Word -> SlotState ()
putSlot = ST.put

evalSlotState :: SlotState a -> a
evalSlotState = (`ST.evalState` maxBound) -- HACK: `getSlot maxBound` wraps to slot 0

isUntyped :: KernelObject Word -> Bool
isUntyped Untyped{} = True
isUntyped _ = False

emptyModel arch = Model arch Map.empty Map.empty
emptyIdents = Idents Map.empty

printID :: ObjID -> String
printID (name, Nothing) = name
printID (name, Just num) = name ++ "[" ++ show num ++ "]"

baseName :: QName -> NameRef
baseName = last

qNames :: QName -> [NameRef]
qNames = init

sameName :: ObjID -> ObjID -> Bool
sameName (first, _) (second, _) = first == second

numObject :: Map.Map ObjID a -> Name -> Word
numObject objs name =
    if Map.member (name, Just 0) objs
    then fromIntegral $ length $ filter (sameName (name, Nothing)) $ Map.keys objs
    else error $ "Unknown reference: " ++ name

refToID :: NameRef -> ObjID
refToID (name, []) = (name, Nothing)
refToID (name, [Only n]) = (name, Just n)
refToID names = error ("A unique identifer was expected at " ++ show names)

unrange :: Word -> Range -> [Maybe Word]
unrange num range = case range of
    Only id -> [Just id]
    FromTo first last -> map Just list
        where list = if first <= last
                     then [first..last]
                     else [first,first-1..last]
    From first -> map Just [first..num - 1]
    To last -> map Just [0..last]
    All -> map Just [0..num - 1]

refToIDs :: Map.Map ObjID a -> NameRef -> [ObjID]
refToIDs _ (name, []) = [(name, Nothing)]
refToIDs objs (name, ranges) =
    zip (repeat name) $ concatMap (unrange (numObject objs name)) ranges

makeIDs :: Name -> Maybe Word -> [ObjID]
makeIDs name Nothing = [(name,Nothing)]
makeIDs name (Just num) = zip (repeat name) (map Just [0..(num - 1)])

members :: Ord k => [k] -> Map.Map k a -> Bool
members names objs = all (`Map.member` objs) names

addCovered :: ObjMap Word -> [ObjID] -> [ObjID] -> [ObjID]
addCovered objs names cov =
    if members names objs
    then cov ++ names -- FIXME: needed to preserve order, but inefficient
    else error ("At least one object reference is unknown: " ++ show names)

addUTCover :: ObjMap Word -> CoverMap -> [ObjID] -> ObjID -> CoverMap
addUTCover objs covers names ut =
    Map.insertWith (addCovered objs) ut names covers

addUTCovers :: ObjMap Word -> CoverMap -> [ObjID] -> [ObjID] -> CoverMap
addUTCovers _ covers _ [] = covers
addUTCovers objs covers n [ut] = addUTCover objs covers n ut
addUTCovers objs covers n (ut:uts) =
    addUTCovers objs (addUTCover objs covers n ut) [ut] uts

addUTDecl ::  ObjMap Word -> ObjID -> CoverMap -> NameRef -> CoverMap
addUTDecl objs ut covers names = addUTCover objs covers (refToIDs objs names) ut

addUTDecls ::  ObjMap Word -> ObjID -> CoverMap -> [NameRef] -> CoverMap
addUTDecls objs ut = foldl' (addUTDecl objs ut)

getUntypedCover :: Maybe NameRef -> ObjMap Word -> CoverMap -> Decl -> CoverMap
getUntypedCover prevName objs covers (ObjDecl (KODecl objName obj)) =
    if null (objDecls obj)
    then
        let (name, num) = refToID $ baseName objName
            qns = qNames objName
        in addUTCovers objs covers (makeIDs name num)
                       (map refToID (reverse (maybeCons prevName qns)))
    else
        let name = refToID $ baseName objName
            qns = qNames objName
            covers' = addUTCovers objs covers [name]
                                  (map refToID (reverse (maybeCons prevName qns)))
            covers'' = addUTDecls objs name covers' (Either.rights (objDecls obj))
        in getUntypedCovers (Just (baseName objName)) objs covers''
                            (map ObjDecl (Either.lefts (objDecls obj)))
    where maybeCons (Just x) xs = x:xs
          maybeCons Nothing xs = xs
getUntypedCover _ _ covers _ = covers

getUntypedCovers :: Maybe NameRef -> ObjMap Word -> CoverMap -> [Decl] -> CoverMap
getUntypedCovers prevName objs =
    foldl' (getUntypedCover prevName objs)

-- A child of an untyped may be mentioned multiple times in the spec.
-- When parsing, this creates multiple entries in the cover list.
-- We normalise the untyped cover by removing duplicates.
--
-- This feature is deprecated; generate warnings when we encounter it.
dedupCoverIDs :: CoverMap -> Logger CoverMap
dedupCoverIDs = sequenceA . Map.mapWithKey (dedup Set.empty Set.empty)
  where dedup _ _ _ [] = return [] :: Logger [ObjID]
                         -- constrain monad type; otherwise we need FlexibleContexts
        dedup seen reported utID (x:xs)
          | Set.member x seen = do
              when (Set.notMember x reported) $ do
                tell $ text $ "warning: specifying untyped child multiple times is deprecated: " ++
                              "ut = " ++ printID utID ++ ", child = " ++ printID x ++ "\n"
              dedup seen (Set.insert x reported) utID xs
          | otherwise = (x:) <$> dedup (Set.insert x seen) reported utID xs

emptyUntyped :: KernelObject Word
emptyUntyped = Untyped Nothing Nothing

getUTObj :: ObjMap Word -> ObjID -> KernelObject Word
getUTObj objs ut =
    case Map.lookup ut objs of
        Nothing -> emptyUntyped
        Just obj ->
            if isUntyped obj
            then obj
            else error ("Untyped object expected at \""++ printID ut ++
                        "\", but found instead: " ++ show obj)

addUTName :: ObjMap Word -> ObjID -> ObjMap Word
addUTName objs ut = Map.insert ut (getUTObj objs ut) objs

addUTNames :: ObjMap Word -> [ObjID] -> ObjMap Word
addUTNames objs [] = objs
addUTNames objs [ut] = addUTName objs ut
addUTNames objs (ut:uts) = addUTNames (addUTName objs ut) uts

addUntyped :: ObjMap Word -> Decl -> ObjMap Word
addUntyped objs (ObjDecl (KODecl objName obj)) =
    if null (objDecls obj)
    then
        let qns = qNames objName
        in addUTNames objs (map refToID qns)
    else
        let qns = qNames objName
            objs' = addUTNames objs (map refToID qns)
        in addUntypeds objs' (map ObjDecl (Either.lefts (objDecls obj)))
addUntyped objs _ = objs

addUntypeds :: ObjMap Word -> [Decl] -> ObjMap Word
addUntypeds = foldl' addUntyped

getTCBAddr :: [ObjParam] -> Maybe Word
getTCBAddr [] = Nothing
getTCBAddr (TCBExtraParam (Addr addr) : _) = Just addr
getTCBAddr (_ : xs ) = getTCBAddr xs

getTCBip :: [ObjParam] -> Maybe Word
getTCBip [] = Nothing
getTCBip (TCBExtraParam (IP ip) : _) = Just ip
getTCBip (_ : xs ) = getTCBip xs

getTCBsp :: [ObjParam] -> Maybe Word
getTCBsp [] = Nothing
getTCBsp (TCBExtraParam (SP sp) : _) = Just sp
getTCBsp (_ : xs ) = getTCBsp xs

getTCBprio :: [ObjParam] -> Maybe Integer
getTCBprio [] = Nothing
getTCBprio (TCBExtraParam (Prio prio) : _) = Just prio
getTCBprio (_ : xs) = getTCBprio xs

getTCBmax_prio :: [ObjParam] -> Maybe Integer
getTCBmax_prio [] = Nothing
getTCBmax_prio (TCBExtraParam (MaxPrio max_prio) : _) = Just max_prio
getTCBmax_prio (_ : xs) = getTCBmax_prio xs

getTCBaffinity :: [ObjParam] -> Maybe Integer
getTCBaffinity [] = Nothing
getTCBaffinity (TCBExtraParam (Affinity affinity) : _) = Just affinity
getTCBaffinity (_ : xs) = getTCBaffinity xs

getTCBresume :: [ObjParam] -> Maybe Bool
getTCBresume [] = Nothing
getTCBresume (TCBExtraParam (Resume resume) : _) = Just resume
getTCBresume (_ : xs) = getTCBresume xs

getExtraInfo :: Name -> [ObjParam] -> Maybe TCBExtraInfo
getExtraInfo n params =
    -- FIXME: This is really hacky hardcoding the acceptable combinations of attributes.
    case (getTCBAddr params, getTCBip params, getTCBsp params, getTCBprio params, getTCBmax_prio params, getTCBaffinity params, getTCBresume params) of
        (Just addr, Just ip, Just sp, Just prio, Just max_prio, Just affinity, resume) ->
            Just $ TCBExtraInfo addr (Just ip) (Just sp) (Just prio) (Just max_prio) (Just affinity) resume
        (Just addr, Nothing, Nothing, Nothing, Nothing, Just affinity, resume) ->
            Just $ TCBExtraInfo addr Nothing Nothing Nothing Nothing (Just affinity) resume
        (Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing) -> Nothing
        params -> error $ "Incorrect extra tcb parameters: " ++ n ++ show params

getCNodeHasUntyped :: [ObjParam] -> Maybe Bool
getCNodeHasUntyped [] = Nothing
getCNodeHasUntyped (CNodeExtraParam (HasUntyped untyped) : _) = Just untyped
getCNodeHasUntyped (_ : xs) = getCNodeHasUntyped xs

getCNodeExtraInfo :: [ObjParam] -> CNodeExtraInfo
getCNodeExtraInfo params = CNodeExtraInfo (getCNodeHasUntyped params)

getTCBDom :: [ObjParam] -> Integer
getTCBDom [] = 0
getTCBDom (Dom dom : _) = dom
getTCBDom (_ : xs) = getTCBDom xs

getFaultEP :: [ObjParam] -> Maybe Word
getFaultEP [] = Nothing
getFaultEP (FaultEP fault_ep : _) = Just fault_ep
getFaultEP (_ : xs) = getFaultEP xs

getInitArguments :: [ObjParam] -> [Word]
getInitArguments [] = []
getInitArguments (InitArguments init : _) = init
getInitArguments (_ : xs) = getInitArguments xs

getSCPeriod :: [ObjParam] -> Maybe Word64
getSCPeriod [] = Nothing
getSCPeriod (SCExtraParam (Period period) : _) = Just period
getSCPeriod (_ : xs) = getSCPeriod xs

getSCBudget :: [ObjParam] -> Maybe Word64
getSCBudget [] = Nothing
getSCBudget (SCExtraParam (Budget budget) : _) = Just budget
getSCBudget (_ : xs) = getSCBudget xs

getSCData :: [ObjParam] -> Maybe Word
getSCData [] = Nothing
getSCData (SCExtraParam (SCData scData) : _) = Just scData
getSCData (_ : xs) = getSCData xs

getCBExtraInfo :: [ObjParam] -> Maybe Word
getCBExtraInfo [] = Nothing
getCBExtraInfo (CBExtraParam (CBNumber x) : _) = Just x
getCBExtraInfo (_ : xs) = getCBExtraInfo xs

getSCExtraInfo :: Name -> [ObjParam] -> Maybe SCExtraInfo
getSCExtraInfo n params =
    -- FIXME: This is really hacky hardcoding the acceptable combinations of attributes.
    case (getSCPeriod params, getSCBudget params, getSCData params) of
        (Just period, Just budget, Just scData) ->
            Just $ SCExtraInfo (Just period) (Just budget) (Just scData)
        (Just period, Just budget, Nothing) ->
            Just $ SCExtraInfo (Just period) (Just budget) Nothing
        (Nothing, Nothing, Nothing) -> Nothing
        params -> error $ "Incorrect extra sc parameters: " ++ n ++ show params

getIOAPICIrqIoapic :: [ObjParam] -> Word
getIOAPICIrqIoapic [] = error $ "Incorrect ioapic irq parameters"
getIOAPICIrqIoapic (IOAPICIRQExtraParam (IOAPIC ioapic) : _) = ioapic
getIOAPICIrqIoapic (_ : xs) = getIOAPICIrqIoapic xs

getIOAPICIrqPin :: [ObjParam] -> Word
getIOAPICIrqPin [] = error $ "Incorrect ioapic irq parameters"
getIOAPICIrqPin (IOAPICIRQExtraParam (Pin pin) : _) = pin
getIOAPICIrqPin (_ : xs) = getIOAPICIrqPin xs

getIOAPICIrqLevel :: [ObjParam] -> Word
getIOAPICIrqLevel [] = error $ "Incorrect ioapic irq parameters"
getIOAPICIrqLevel (IOAPICIRQExtraParam (Level level) : _) = level
getIOAPICIrqLevel (_ : xs) = getIOAPICIrqLevel xs

getIOAPICIrqPolarity :: [ObjParam] -> Word
getIOAPICIrqPolarity [] = error $ "Incorrect ioapic irq parameters"
getIOAPICIrqPolarity (IOAPICIRQExtraParam (Polarity polarity) : _) = polarity
getIOAPICIrqPolarity (_ : xs) = getIOAPICIrqPolarity xs

getMSIIrqHandle :: [ObjParam] -> Word
getMSIIrqHandle [] = error $ "Incorrect msi irq parameters"
getMSIIrqHandle (MSIIRQExtraParam (MSIHandle handle) : _) = handle
getMSIIrqHandle (_ : xs) = getMSIIrqHandle xs

getMSIIrqPCIBus :: [ObjParam] -> Word
getMSIIrqPCIBus [] = error $ "Incorrect msi irq parameters"
getMSIIrqPCIBus (MSIIRQExtraParam (MSIPCIBus bus) : _) = bus
getMSIIrqPCIBus (_ : xs) = getMSIIrqPCIBus xs

getMSIIrqPCIDev :: [ObjParam] -> Word
getMSIIrqPCIDev [] = error $ "Incorrect msi irq parameters"
getMSIIrqPCIDev (MSIIRQExtraParam (MSIPCIDev dev) : _) = dev
getMSIIrqPCIDev (_ : xs) = getMSIIrqPCIDev xs

getMSIIrqPCIFun :: [ObjParam] -> Word
getMSIIrqPCIFun [] = error $ "Incorrect msi irq parameters"
getMSIIrqPCIFun (MSIIRQExtraParam (MSIPCIFun fun) : _) = fun
getMSIIrqPCIFun (_ : xs) = getMSIIrqPCIFun xs

getARMIrqTrigger :: Name -> [ObjParam] -> Word
getARMIrqTrigger n [] = error ("Incorrect Arm irq parameters: missing 'trigger': " ++ n)
getARMIrqTrigger _ (ARMIRQExtraParam (ARMIRQTrigger trigger) : _) = trigger
getARMIrqTrigger n (_ : xs) = getARMIrqTrigger n xs

getARMIrqTarget :: Name -> [ObjParam] -> Word
getARMIrqTarget n [] = error ("Incorrect Arm irq parameters: missing 'target': " ++ n)
getARMIrqTarget _ (ARMIRQExtraParam (ARMIRQTarget target) : _) = target
getARMIrqTarget n (_ : xs) = getARMIrqTarget n xs

getMaybeBitSize :: [ObjParam] -> Maybe Word
getMaybeBitSize [] = Nothing
getMaybeBitSize (BitSize x : _) = Just x
getMaybeBitSize (_ : xs) = getMaybeBitSize xs

getBitSize :: Name -> [ObjParam] -> Word
getBitSize n xs =
    case getMaybeBitSize xs of
        Nothing -> error ("Needs bitsize parameter: " ++ n)
        Just sz -> sz

getVMSize :: Name -> [ObjParam] -> Word
getVMSize n [] = error ("Needs vmsize parameter: " ++ n)
getVMSize n (VMSize 0 : _) = error ("Cannot make a frame object that has size 0: " ++ n)
getVMSize _ (VMSize x : _) = x
getVMSize n (_ : xs) = getVMSize n xs

getMaybePaddr :: [ObjParam] -> Maybe Word
getMaybePaddr [] = Nothing
getMaybePaddr (Paddr x : _) = Just x
getMaybePaddr (_ : xs) = getMaybePaddr xs

getMaybeFill :: [ObjParam] -> Maybe [[String]]
getMaybeFill [] = Nothing
getMaybeFill (FrameExtraParam (Fill f) : _) = Just f
getMaybeFill(_ : xs) = getMaybeFill xs

getLevel :: Name -> [ObjParam] -> Word
getLevel n [] = error ("Needs level parameter: " ++ n)
getLevel _ (IOPTLevel l : _) = l
getLevel n (_ : xs) = getLevel n xs

getDomainID :: Name -> [ObjParam] -> Word
getDomainID n [] = error ("Needs domainID parameter: " ++ n)
getDomainID _ (DomainID x : _) = x
getDomainID n (_ : xs) = getDomainID n xs

getPCIDevice :: Name -> [ObjParam] -> (Word, Word, Word)
getPCIDevice n [] = error ("Needs pciDevice parameter: " ++ n)
getPCIDevice _ (PCIDevice x : _) = x
getPCIDevice n (_ : xs) = getPCIDevice n xs

getARMIODevice :: Name -> [ObjParam] -> Word
getARMIODevice n [] = error ("Needs iospace parameter: " ++ n)
getARMIODevice _ (ARMIOSpace x : _) = x
getARMIODevice n (_ : xs) = getARMIODevice n xs

getPorts :: Name -> [ObjParam] -> (Word, Word)
getPorts n [] = error ("Needs ports parameter: " ++ n)
getPorts _ (Ports x : _) = x
getPorts n (_ : xs) = getPorts n xs

getMaybeAsidHigh :: [ObjParam] -> Maybe Word
getMaybeAsidHigh [] = Nothing
getMaybeAsidHigh (AsidHigh asidHigh : _) = Just asidHigh
getMaybeAsidHigh (_ : ps) = getMaybeAsidHigh ps

-- need this hack because 'Constr' isn't 'Ord'. "Ord a" must group by constrs!
sortConstrs :: (Data a, Ord a) => [a] -> [a]
sortConstrs = sortBy (\x y -> if toConstr x == toConstr y then EQ else compare x y)

subsetConstrs :: (Ord a, Data a) => [a] -> [a] -> Bool
subsetConstrs = isSubsequenceOf `on` (map toConstr . sortConstrs)

containsConstr :: (Data a) => a -> [a] -> Bool
containsConstr x xs = toConstr x `elem` map toConstr xs

numConstrs :: (Data a) => a -> Int
numConstrs x = length $ dataTypeConstrs $ dataTypeOf x

removeConstr :: Data a => a -> [a] -> [a]
removeConstr x xs = filter (\y -> toConstr x /= toConstr y) xs

validObjPars :: KO -> Bool
validObjPars (Obj TCB_T ps []) =
  subsetConstrs ps (replicate (numConstrs (Addr undefined)) (TCBExtraParam undefined)
                    ++ [InitArguments undefined, Dom undefined, FaultEP undefined])
validObjPars (Obj CNode_T ps []) =
  subsetConstrs ps [BitSize undefined, CNodeExtraParam $ HasUntyped undefined]
validObjPars (Obj Untyped_T ps _) = subsetConstrs ps [BitSize undefined, Paddr undefined]
validObjPars (Obj Frame_T ps []) =
  subsetConstrs ps [VMSize undefined, Paddr undefined, FrameExtraParam undefined] &&
  (not (containsConstr (Paddr undefined) ps) || containsConstr (VMSize undefined) ps)
validObjPars (Obj ASIDPool_T ps []) = subsetConstrs ps [AsidHigh undefined]
validObjPars (Obj IOPT_T ps []) = subsetConstrs ps [IOPTLevel undefined]
validObjPars (Obj IOPorts_T ps []) = subsetConstrs ps [Ports undefined]
validObjPars (Obj IODevice_T ps []) = subsetConstrs ps [DomainID undefined, PCIDevice undefined]
validObjPars (Obj ARMIODevice_T ps []) = subsetConstrs ps [ARMIOSpace undefined]
validObjPars (Obj SC_T ps []) =
  subsetConstrs ps (replicate (numConstrs (Addr undefined)) (SCExtraParam undefined)
                    ++ [BitSize undefined])
validObjPars (Obj IOAPICIrqSlot_T ps []) =
  subsetConstrs ps (replicate (numConstrs (Addr undefined)) (IOAPICIRQExtraParam undefined))
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 ARMCB_T ps []) =
  subsetConstrs ps (replicate (numConstrs (Addr undefined)) (CBExtraParam undefined))
validObjPars obj = null (params obj)

-- For converting frame sizes to size bits
wordLog2 :: Word -> Int
wordLog2 w = finiteBitSize w - 1 - countLeadingZeros w

objectOf :: Name -> KO -> KernelObject Word
objectOf n obj =
    if validObjPars obj
    then case obj of
        Obj Endpoint_T [] [] -> Endpoint
        Obj Notification_T [] [] -> Notification
        Obj TCB_T ps [] ->
            TCB Map.empty (getFaultEP ps) (getExtraInfo n ps) (getTCBDom ps) (getInitArguments ps)
        Obj CNode_T ps [] -> CNode Map.empty (getBitSize n ps) (getCNodeExtraInfo ps)
        Obj Untyped_T ps _ -> Untyped (getMaybeBitSize ps) (getMaybePaddr ps)
        Obj ASIDPool_T ps [] -> ASIDPool Map.empty (getMaybeAsidHigh ps)
        Obj PT_T _ [] -> PT Map.empty
        Obj PD_T _ [] -> PD Map.empty
        Obj PML4_T _ [] -> PML4 Map.empty
        Obj PDPT_T _ [] -> PDPT Map.empty
        Obj PUD_T _ [] -> PUD Map.empty
        Obj PGD_T _ [] -> PGD Map.empty
        Obj Frame_T ps [] ->
            let size = getVMSize n ps
                bits = wordLog2 size
            in if bits < 0 || 2^bits /= size
               then error $ "Frame size not power of 2: " ++ n ++ " = " ++ show obj
               else Frame (fromIntegral bits) (getMaybePaddr ps) (getMaybeFill ps)
        Obj IOPT_T ps [] -> IOPT Map.empty (getLevel n ps)
        Obj IOPorts_T ps [] -> IOPorts (getPorts n ps)
        Obj IODevice_T ps [] -> IODevice Map.empty (getDomainID n ps) (getPCIDevice n ps)
        Obj ARMIODevice_T ps [] -> ARMIODevice Map.empty (getARMIODevice n ps)
        Obj IrqSlot_T [] [] -> CNode Map.empty 0 (CNodeExtraInfo Nothing)
        Obj IOAPICIrqSlot_T ps [] -> IOAPICIrq Map.empty (getIOAPICIrqIoapic ps) (getIOAPICIrqPin ps) (getIOAPICIrqLevel ps) (getIOAPICIrqPolarity ps)
        Obj MSIIrqSlot_T ps [] -> MSIIrq Map.empty (getMSIIrqHandle ps) (getMSIIrqPCIBus ps) (getMSIIrqPCIDev ps) (getMSIIrqPCIFun ps)
        Obj ARMIrqSlot_T ps [] -> ARMIrq Map.empty (getARMIrqTrigger n ps) (getARMIrqTarget n ps)
        Obj VCPU_T [] [] -> VCPU
        Obj SC_T ps [] -> SC (getSCExtraInfo n ps) (getMaybeBitSize ps)
        Obj RTReply_T [] [] -> RTReply
        Obj ARMSID_T [] [] -> ARMSID
        Obj ARMCB_T ps [] -> ARMCB (getCBExtraInfo ps)
        Obj _ _ (_:_) ->
          error $ "Only untyped caps can have objects as content: " ++
                  n ++ " = " ++ show obj
        _ -> error ("Could not convert: " ++ n ++ " = " ++ show obj)
    else error ("Incorrect params for " ++ n)

insertObjects :: [ObjID] -> KernelObject Word -> ObjMap Word -> ObjMap Word
insertObjects ids obj objs = foldl' (\map id->Map.insert id obj map) objs ids

isMember :: Name -> ObjMap Word -> Bool
isMember name objs =
    Map.member (name, Nothing) objs || Map.member (name, Just 0) objs

addObject :: ObjMap Word -> Decl -> ObjMap Word
addObject objs (ObjDecl (KODecl objName obj)) =
    if not $ CapDL.AST.koType obj == Untyped_T && isMember name objs
    then if isMember name objs
        then error ("Duplicate name declaration: " ++ name)
        else let
            objs' = insertObjects (makeIDs name num) (objectOf name obj) objs
        in addObjects objs' (map ObjDecl (Either.lefts (objDecls obj)))
    else objs
    where (name, num) = refToID $ baseName objName
addObject s _ = s

addObjects :: ObjMap Word -> [Decl] -> ObjMap Word
addObjects = foldl' addObject

addIRQ :: IRQMap -> (Word, ObjID) -> IRQMap
addIRQ irqNode (slot, irq) =
    if Map.member slot irqNode
    then error ("IRQ already mapped: " ++ show slot)
    else Map.insert slot irq irqNode

addIRQs :: IRQMap -> [(Word, ObjID)] -> IRQMap
addIRQs = foldl' addIRQ

getSlotIRQs :: ObjMap Word -> CapMapping -> SlotState [(Word, ObjID)]
getSlotIRQs objs (IRQMapping slot nameRef) = do
    slot' <- checkSlot slot
    let irqs = refToIDs objs nameRef
        lastSlot = slot' + fromIntegral (length irqs - 1)
    putSlot lastSlot
    return $ zip [slot'..lastSlot] irqs
getSlotIRQs _ _ = error "not an IRQMapping"

addIRQMapping :: ObjMap Word -> SlotState IRQMap -> CapMapping -> SlotState IRQMap
addIRQMapping objs irqNode cm = do
    slotIRQs <- getSlotIRQs objs cm
    node <- irqNode
    return $ addIRQs node slotIRQs

addIRQMappings :: ObjMap Word -> IRQMap -> [CapMapping] -> SlotState IRQMap
addIRQMappings objs irqNode =
    foldl' (addIRQMapping objs) (return irqNode)

addIRQNode :: ObjMap Word -> IRQMap -> Decl -> IRQMap
addIRQNode objs irqNode (IRQDecl irqs) =
    if Map.null irqNode
    then evalSlotState (addIRQMappings objs irqNode irqs)
    else error "Duplicate IRQ node declaration"
addIRQNode _ irqNode _ = irqNode

addIRQNodes :: ObjMap Word -> IRQMap -> [Decl] -> IRQMap
addIRQNodes objs = foldl' (addIRQNode objs)

insertMapping :: KernelObject Word -> (Word, Cap) -> KernelObject Word
insertMapping obj (slot, cap) =
    if hasSlots obj
    then let mappings = slots obj
        in if Map.member slot mappings
        then error ("Slot already filled: " ++ show slot)
        else obj {slots = Map.insert slot cap mappings}
    else error ("This object does not support cap mappings: " ++ show obj)

insertMappings :: KernelObject Word -> [(Word, Cap)] -> KernelObject Word
insertMappings = foldl' insertMapping

getBadge :: [CapParam] -> Word
getBadge [] = 0
getBadge (Badge n : _) = n
getBadge (_ : xs) = getBadge xs

getRights :: [CapParam] -> CapRights
getRights [] = Set.empty
getRights (Rights r : ps) = r `Set.union` getRights ps
getRights (_ : ps) = getRights ps

getGuard :: [CapParam] -> Word
getGuard [] = 0
getGuard (Guard n : _) = n
getGuard (_ : ps) = getGuard ps

getGuardSize :: [CapParam] -> Word
getGuardSize [] = 0
getGuardSize (GuardSize n : _) = n
getGuardSize (_ : ps) = getGuardSize ps

getReplys :: [CapParam] -> [CapParam]
getReplys [] = []
getReplys (Reply : ps) = Reply : getReplys ps
getReplys (MasterReply : ps) = MasterReply : getReplys ps
getReplys (_ : ps) = getReplys ps

getMaybeAsid :: [CapParam] -> Maybe Asid
getMaybeAsid [] = Nothing
getMaybeAsid (Asid asid : _) = Just asid
getMaybeAsid (_ : ps) = getMaybeAsid ps

getCached :: [CapParam] -> Bool
getCached [] = True
getCached (Cached c : _) = c
getCached (_ : ps) = getCached ps

getMaybeMapping :: [CapParam] -> Maybe (ObjID, Word)
getMaybeMapping [] = Nothing
getMaybeMapping (FrameMapping c s : _) = Just (refToID c, s)
getMaybeMapping (_ : ps) = getMaybeMapping ps

validCapPars :: KernelObject Word -> [CapParam] -> Bool
validCapPars (Endpoint {}) ps =
    subsetConstrs (removeConstr (Rights undefined) ps) [Badge undefined]
validCapPars (Notification {}) ps =
    subsetConstrs (removeConstr (Rights undefined) ps) [Badge undefined]
validCapPars (TCB {}) ps =
    subsetConstrs ps [Reply, MasterReply] &&
    (not (containsConstr Reply ps) || not (containsConstr MasterReply ps))
validCapPars (CNode {}) ps = subsetConstrs ps [Guard undefined, GuardSize undefined]
validCapPars (Frame {}) ps =
    subsetConstrs (removeConstr (Rights undefined) ps) [Asid undefined, Cached undefined,
                                                        FrameMapping undefined undefined]
validCapPars (RTReply {}) ps = subsetConstrs ps [Rights undefined]
validCapPars (PD {}) ps = subsetConstrs ps [Asid undefined]
validCapPars (PT {}) ps = subsetConstrs ps [Asid undefined]
validCapPars (PML4 {}) ps = subsetConstrs ps [Asid undefined]
validCapPars (PDPT {}) ps = subsetConstrs ps [Asid undefined]
validCapPars (PUD {}) ps = subsetConstrs ps [Asid undefined]
validCapPars (PGD {}) ps = subsetConstrs ps [Asid undefined]
validCapPars _ ps = null ps

objCapOf :: ObjID -> KernelObject Word -> ObjID -> [CapParam] -> Cap
objCapOf containerName obj objRef params =
    if validCapPars obj params
    then case obj of
        Endpoint -> EndpointCap objRef (getBadge params) (getRights params)
        Notification ->
            NotificationCap objRef (getBadge params) (getRights params)
        RTReply -> RTReplyCap objRef (getRights params)
        TCB {} ->
            case getReplys params of
                [] -> TCBCap objRef
                [Reply] -> ReplyCap objRef
                [MasterReply] -> MasterReplyCap objRef
                _ -> error "invalid cap"
        Untyped {} -> UntypedCap objRef
        CNode _ 0 _ -> IRQHandlerCap objRef --FIXME: This should check if the obj is in the irqNode
        CNode {} -> CNodeCap objRef (getGuard params) (getGuardSize params)
        Frame {} -> FrameCap objRef (getRights params) (getMaybeAsid params) (getCached params)
                                    (getMaybeMapping params)
        PML4 {} -> PML4Cap objRef (getMaybeAsid params)
        PDPT {} -> PDPTCap objRef (getMaybeAsid params)
        PD {} -> PDCap objRef (getMaybeAsid params)
        PT {} -> PTCap objRef (getMaybeAsid params)
        PUD {} -> PUDCap objRef (getMaybeAsid params)
        PGD {} -> PGDCap objRef (getMaybeAsid params)
        ASIDPool {} -> ASIDPoolCap objRef
        IOPT {} -> IOPTCap objRef
        IOPorts {} -> IOPortsCap objRef
        IODevice {} -> IOSpaceCap objRef
        ARMIODevice  {} -> ARMIOSpaceCap objRef
        VCPU {} -> VCPUCap objRef
        SC {} -> SCCap objRef
        IOAPICIrq {} -> IRQIOAPICHandlerCap objRef
        MSIIrq {} -> IRQMSIHandlerCap objRef
        ARMIrq {} -> ARMIRQHandlerCap objRef
        ARMSID {} -> ARMSIDCap objRef
        ARMCB {} -> ARMCBCap objRef
    else error ("Incorrect params for cap to " ++ printID objRef ++ " in " ++
                printID containerName ++ "; got " ++ show params)

capOf :: ObjMap Word -> ObjID -> [CapParam] -> ObjID -> Cap
capOf objs containerName xs id =
    case Map.lookup id objs of
        Nothing ->
            error ("Unknown object \"" ++ printID id ++
                   "\" for cap in " ++ printID containerName)
        Just obj -> objCapOf containerName obj id xs

capsOf :: ObjMap Word -> ObjID -> [ObjID] -> [CapParam] -> [Cap]
capsOf objs name ids xs = map (capOf objs name xs) ids

checkSlot :: Maybe Word -> SlotState Word
checkSlot (Just slot) = return slot
checkSlot Nothing = getSlot

validCapPars' :: Name -> [CapParam] -> Bool
validCapPars' name ps
    | name == schedControl = subsetConstrs ps [Core undefined]
    | otherwise = null ps

getCore :: ObjID -> [CapParam] -> Word
getCore containerName [] =
    error ("Needs core parameter for sched_control cap in " ++ printID containerName)
getCore _ (Core n:_) = n
getCore containerName (_:ps) = getCore containerName ps

capOf' :: ObjID -> Name -> [CapParam] -> Cap
capOf' containerName capName ps
    | capName == ioSpaceMaster = IOSpaceMasterCap
    | capName == asidControl = ASIDControlCap
    | capName == irqControl = IRQControlCap
    | capName == domain = DomainCap
    | capName == schedControl = SchedControlCap (getCore containerName ps)
    | otherwise =
        error ("capOf' called with a name it doesn't know about: " ++ capName)

slotsAndCapsOf :: ObjMap Word-> ObjID -> CapMapping -> SlotState [(Word, Cap)]
slotsAndCapsOf objs objName (CapMapping slot _ nameRef params _)
    | fst nameRef `elem` capStrings && null (snd nameRef) = do
        let (name, []) = nameRef
        if validCapPars' name params
            then do
                slot' <- checkSlot slot
                putSlot slot'
                return [(slot', capOf' objName name params)]
            else error ("Incorrect params for cap to " ++ name ++
                        " in " ++ printID objName)
    | otherwise = do
        slot' <- checkSlot slot
        let caps = capsOf objs objName (refToIDs objs nameRef) params
            lastSlot = slot' + fromIntegral (length caps - 1)
        putSlot lastSlot
        return $ zip [slot'..lastSlot] caps
slotsAndCapsOf _ _ (CopyOf slot _ _ _ _) = do
    slot' <- checkSlot slot
    putSlot slot'
    return [(slot', NullCap)]
slotsAndCapsOf _ _ _ = error "IRQ or ASID mapping"

addMapping :: ObjMap Word -> ObjID -> KernelObject Word -> CapMapping
              -> SlotState (KernelObject Word)
addMapping objs n obj cm = do
    slotCaps <- slotsAndCapsOf objs n cm
    return $ insertMappings obj slotCaps

addMappings :: ObjMap Word -> ObjID -> KernelObject Word -> [CapMapping]
               -> SlotState (KernelObject Word)
addMappings objs n =
    foldM (addMapping objs n)

hasUnnumbered :: [CapMapping] -> Bool
hasUnnumbered [] = False
hasUnnumbered (x:xs) =
    case slot x of
        Nothing -> True
        _ -> hasUnnumbered xs

hasCopy :: [CapMapping] -> Bool
hasCopy [] = False
hasCopy (CopyOf {}:_) = True
hasCopy (_:xs) = hasCopy xs

validMapping :: [CapMapping] -> Bool
validMapping mappings = not $ hasCopy mappings && hasUnnumbered mappings

addCap :: Model Word -> (ObjID, [CapMapping]) -> Model Word
addCap (Model arch objs irqNode cdt untypedCovers) (id, mappings) =
    case Map.lookup id objs of
        Nothing -> error ("Unknown cap container: " ++ printID id)
        Just obj ->
            if validMapping mappings
            then Model arch (Map.insert id mapped objs) irqNode cdt untypedCovers
            else error $ printID id ++
                                " uses both copies of caps and unnumbered slots"
            where mapped = evalSlotState (addMappings objs id obj mappings)

addCapDecl :: Model Word -> Decl -> Model Word
addCapDecl m@(Model _ objs _ _ _) (CapDecl names mappings) =
    foldl' addCap m (zip (refToIDs objs names) (repeat mappings))
addCapDecl s _ = s

addCapDecls :: [Decl] -> Model Word -> Model Word
addCapDecls decls m = foldl' addCapDecl m decls

insertCapIdentMapping :: ObjID -> Idents CapName -> CapName -> Word
                         -> Idents CapName
insertCapIdentMapping obj (Idents ids) name slot =
    Idents (Map.insert name (obj,slot) ids)

addCapIdentMapping' :: ObjMap Word -> ObjID -> Idents CapName -> Word -> NameRef
                       -> NameRef -> Idents CapName
addCapIdentMapping' m obj ids slot (names, range) ref =
    let len = length $ refToIDs m ref
        names' = case range of
            [] -> if len == 1
                then [(names, Nothing)]
                else error ("Cannot give a unique name to an array of caps: "
                            ++ names)
            [All] -> zip (repeat names) (map Just [0..fromIntegral len - 1])
            _ -> error "invalid range"
        lastSlot = slot + fromIntegral len - 1
        slots = [slot..lastSlot]
    in foldl' (\ids' (name, s) -> insertCapIdentMapping obj ids' name s)
                                                        ids (zip names' slots)

addCapIdentMapping :: ObjMap Word -> ObjID -> Idents CapName -> CapMapping
                      -> Idents CapName
addCapIdentMapping m obj ids (CapMapping (Just slot) (Just names) ref _ _) =
    addCapIdentMapping' m obj ids slot names ref
addCapIdentMapping m obj ids (CopyOf (Just slot) (Just names) ref _ _) =
    addCapIdentMapping' m obj ids slot names ref
addCapIdentMapping _ _ i _ = i

addCapIdentMappings :: ObjMap Word -> NameRef -> Idents CapName -> [CapMapping]
                       -> Idents CapName
addCapIdentMappings m obj =
    foldl' (addCapIdentMapping m (head (refToIDs m obj)))

addCapIdent :: ObjMap Word -> Idents CapName -> Decl -> Idents CapName
addCapIdent _ (Idents ids) (CapNameDecl name target slot) =
    Idents (Map.insert (name, Nothing) (target', slot) ids)
    where
        target' = refToID target
addCapIdent m i (CapDecl obj mappings) = addCapIdentMappings m obj i mappings
addCapIdent _ i _ = i

capIdents :: ObjMap Word -> [Decl] -> Idents CapName
capIdents m = foldl' (addCapIdent m) emptyIdents

-- FIXME: inefficient, use a proper data structure for this
type CapRefMappings = CapRef -> Maybe CapRef

-- Follow a mapping transitively to the end
transMapping :: (Show a, Eq a) => (a -> Maybe a) -> a -> a
transMapping = transMappingE []

-- FIXME: I'm sure there is a library function for this somewhere
transMappingE :: (Show a, Eq a) => [a] -> (a -> Maybe a) -> a -> a
transMappingE seen m x =
    if x `elem` seen
        then error ("Cyclic reference: " ++ show x)
        else
            case m x of
                Nothing -> x
                Just l -> transMappingE (x:seen) m l

funUpd :: Eq a => (a -> b) -> a -> b -> a -> b
funUpd f x y z = if z == x then y else f z

empty :: a -> Maybe b
empty _ = Nothing

addCapCopyRef :: Idents CapName -> ObjID -> CapRefMappings ->
                 CapMapping -> CapRefMappings
addCapCopyRef (Idents ids) obj m (CopyOf (Just slot) _ target _ _) =
    funUpd m (obj, slot) (Map.lookup (refToID target) ids)
addCapCopyRef _ _ m _ = m

addCapCopyRefs :: ObjMap Word -> Idents CapName -> CapRefMappings -> Decl
                  -> CapRefMappings
addCapCopyRefs map ids m (CapDecl objs mappings) =
    foldl' (\m' obj -> foldl' (addCapCopyRef ids obj) m' mappings)
                                                          m (refToIDs map objs)
addCapCopyRefs _ _ m _ = m

capCopyGraph :: ObjMap Word -> Idents CapName -> [Decl] -> CapRefMappings
capCopyGraph m ids = foldl' (addCapCopyRefs m ids) empty

getMasked :: [CapParam] -> CapRights
getMasked [] = allRights
getMasked (Masked r : ps) = Set.intersection r (getMasked ps)
getMasked (_ : ps) = getMasked ps

copyCapParams :: [CapParam] -> Cap -> Cap
copyCapParams params cap
    | hasRights cap = cap {capRights = Set.intersection rights $ capRights cap}
    | otherwise = cap
    where rights = getMasked params

getSrcCap :: Idents CapName -> CapRefMappings -> Model Word -> ObjID -> Cap
getSrcCap (Idents ids) refs m src =
    case Map.lookup src ids of
        Nothing -> error ("Unknown cap reference: " ++ printID src)
        Just srcRef ->
            case maybeSlotCap (transMapping refs srcRef) m of
                Nothing -> error ("Could not resolve cap reference: "++
                                  show (transMapping refs srcRef))
                Just cap -> cap

addCapCopy :: Idents CapName -> CapRefMappings -> ObjID ->
              Model Word -> CapMapping -> Model Word
addCapCopy ids refs obj m (CopyOf (Just slot) _ src params _) =
    let caps = map (getSrcCap ids refs m) (refToIDs (cap_ids ids) src)
        slots = [slot..(slot + fromIntegral (length caps))]
        caps' = map (copyCapParams params) caps
    in foldl' (\m' (cap, slot') -> ST.execState (setCap (obj,slot') cap) m')
              m (zip caps' slots)
addCapCopy _ _ _ m _ = m

-- FIXME: this recursion pattern over all mappings is duplicated all over
-- the place. factor out.
addCapCopies :: Idents CapName -> CapRefMappings -> NameRef ->
              Model Word -> CapMapping -> Model Word
addCapCopies ids refs names m@(Model _ map _ _ _) copy =
    foldl' (\model obj -> addCapCopy ids refs obj model copy) m
          (refToIDs map names)

addCapCopyDecl :: Idents CapName -> CapRefMappings -> Model Word -> Decl ->
                  Model Word
addCapCopyDecl ids refs m (CapDecl obj mappings) =
    foldl' (addCapCopies ids refs obj) m mappings
addCapCopyDecl _ _ m _ = m

addCapCopyDecls :: Idents CapName -> CapRefMappings -> Model Word -> [Decl] ->
                   Model Word
addCapCopyDecls ids refs = foldl' (addCapCopyDecl ids refs)

getCapCopy :: Idents CapName -> ObjMap Word -> ObjID -> CopyMap ->
              CapMapping -> CopyMap
getCapCopy ids _ obj copies (CopyOf (Just slot) _ src _ _) =
    let capNames = refToIDs (cap_ids ids) src
        capRefs = zip (repeat obj) [slot..(slot + fromIntegral (length capNames))]
    in foldl' (\copies' (capRef, capName) -> Map.insert capRef capName copies')
                                                   copies (zip capRefs capNames)
getCapCopy _ _ _ m _ = m

getCapCopies :: Idents CapName -> ObjMap Word -> NameRef -> CopyMap ->
                CapMapping -> CopyMap
getCapCopies ids m names copies copy =
    foldl' (\copies obj -> getCapCopy ids m obj copies copy) copies
          (refToIDs m names)

getCapCopyDecl :: Idents CapName -> ObjMap Word -> CopyMap -> Decl -> CopyMap
getCapCopyDecl ids m copies (CapDecl obj mappings) =
    foldl' (getCapCopies ids m obj) copies mappings
getCapCopyDecl _ _ copies _ = copies

getCapCopyDecls :: Idents CapName -> ObjMap Word -> [Decl] -> CopyMap
getCapCopyDecls ids m = foldl' (getCapCopyDecl ids m) Map.empty

slotRefToCapRef :: Idents CapName -> SlotRef -> CapRef
slotRefToCapRef _ (Left (obj, slot)) = (refToID obj, slot)
slotRefToCapRef ids (Right name) =
    case Map.lookup (refToID name) (cap_ids ids) of
        Just capRef -> capRef
        Nothing -> error $ "Unknown cap reference: " ++ printID (refToID name)

insertCDT :: CapRef -> CapRef -> CDT -> CDT
insertCDT child parent cdt =
    if isNothing (Map.lookup child cdt)
    then Map.insert child parent cdt
    else error $ show child ++ " has multiple parents"

getDeclOrSlotRef :: Idents CapName -> CapRef -> CDT -> Either Decl SlotRef -> CDT
getDeclOrSlotRef ids parent cdt (Left decl@(CDTDecl child _)) =
    let child' = slotRefToCapRef ids child
        cdt' = insertCDT child' parent cdt
    in getCDTDecl ids cdt' decl
getDeclOrSlotRef _ _ _ (Left _) = error "not a CDTDecl"
getDeclOrSlotRef ids parent cdt (Right child) =
    let child' = slotRefToCapRef ids child
    in insertCDT child' parent cdt

getCDTDecl :: Idents CapName -> CDT -> Decl -> CDT
getCDTDecl ids cdt (CDTDecl parent children) =
    foldl' (getDeclOrSlotRef ids parent') cdt children
    where parent' = slotRefToCapRef ids parent
getCDTDecl _ cdt _ = cdt

getCDTDecls :: Idents CapName -> [Decl] -> CDT
getCDTDecls ids = foldl' (getCDTDecl ids) Map.empty

addCDTMapping :: Idents CapName -> ObjID -> CDT -> CapMapping -> SlotState CDT
addCDTMapping ids obj cdt mapping
    | isJust (maybeParent mapping) = do
        slot' <- checkSlot (slot mapping)
        putSlot slot'
        let parent = slotRefToCapRef ids $ fromJust $ maybeParent mapping
            child = (obj, slot')
        return $ insertCDT child parent cdt
    | otherwise = return cdt

addCDTMappings :: Idents CapName -> CDT -> (ObjID, [CapMapping]) -> SlotState CDT
addCDTMappings ids cdt (obj, mappings) =
    foldM (addCDTMapping ids obj) cdt mappings

addCDTCapDecl :: ObjMap Word -> Idents CapName -> CDT -> Decl -> CDT
addCDTCapDecl objs ids cdt (CapDecl names mappings) =
    foldl' (\cdt capDecl -> evalSlotState (addCDTMappings ids cdt capDecl))
           cdt (zip (refToIDs objs names) (repeat mappings))
addCDTCapDecl _ _ cdt _ = cdt

addCDTCapDecls :: ObjMap Word -> Idents CapName -> CDT -> [Decl] -> CDT
addCDTCapDecls objs ids = foldl' (addCDTCapDecl objs ids)

makeModel :: Module -> Logger (Model Word, Idents CapName, CopyMap)
makeModel (Module arch decls) = do
    let objs = addObjects Map.empty decls
        objs' = addUntypeds objs decls
        irqs = addIRQNodes objs' Map.empty decls
        ids = capIdents objs' decls
        refs = capCopyGraph objs' ids decls
        copies = getCapCopyDecls ids objs' decls
        cdt = getCDTDecls ids decls
        cdt' = addCDTCapDecls objs' ids cdt decls
    covers <- dedupCoverIDs $ getUntypedCovers Nothing objs' Map.empty decls
    return (flip (addCapCopyDecls ids refs) decls .
                  addCapDecls decls $
              Model arch objs' irqs cdt' covers,
            ids, copies)