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

arch ia32

objects

-- following 2 could be implicit
ioport = ioport
irqtable = cnode (8 bits)

rm_ut = ut {
  rm_tcb = tcb
  name2 = ut {
    rm_cn = cnode (10 bits)
  }
  rm_pd = page_directory [ 10 -> frame_name_x, .. ]
  rm_ap = asid_pool (asid_high: 0x0)

  linux_pd = page_directory

  rm_ut_small[50] = untyped (12 bits)
  rm_ut_big[101] = untyped (20 bits)

  frame_nic1[64] = frame (4k)
  -- io space??

  frame_nic2[64] = frame (4k)
  -- io space??

  frame_nic3[4] = frame (4k)
  -- io space??

  timer = notification
  control = ep
}

name: ut { x, y, z }

name: ut
name/name2/name3/x = tcb ..
name/y =
name/z =

caps

name {
  opt num: obj_name parameters
}

rm_cn {
  001: rm_tcb;
  002: rm_cn (0, 0, mask: R, rights: W);
  003: rm_pd;
  006: rm_ap;
  007: ioport;
  00b: linux_pd;
  00c: rm_ut_small[3..7];
  00x: rm_ut_small[7..200, 232, 237..];
  03e: rm_ut_big[];

  0a3: IRQHandler nic1;
  0a4: name = frame_nic1[];
  0e4: iospace;

  0e5: IRQHandler nic2
  0e6: frame_nic2[]
  126: iospace

  127: IRQHandler nic3
  128: frame_nic3[]
  12c: iospace

  12d: timer
  12e: control
  12f: name2 = name (masked: R)
}

rm_tcb {
  vspace: rm_pd
  cspace: rm_cn
}

cap_name = (rm_tcb, cspace)
cap_name2 = (irqtable, 0)

irqtable { 0: notification_cap nic1 }

cnode_booter {
  001: rm_ut
}

CDT: {
  rm_ut parent_of timer
}