Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2,887 changes: 98 additions & 2,789 deletions tool/microkit/src/sdf.rs

Large diffs are not rendered by default.

136 changes: 136 additions & 0 deletions tool/microkit/src/sdf/channels.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,136 @@
//
// Copyright 2025, UNSW
//
// SPDX-License-Identifier: BSD-2-Clause
//

use super::consts::*;
use super::pd_vm::ProtectionDomain;
use super::util::{check_attributes, checked_lookup, loc_string, value_error};
use super::{SdfNode, XmlSystemDescription};

use crate::util::str_to_bool;

#[derive(Debug, Clone)]
pub struct ChannelEnd {
pub pd: usize,
pub id: u64,
pub notify: bool,
pub pp: bool,
pub setvar_id: Option<String>,
}

#[derive(Debug)]
pub struct Channel {
pub end_a: ChannelEnd,
pub end_b: ChannelEnd,
}

impl ChannelEnd {
fn from_xml<'a>(
xml_sdf: &'a XmlSystemDescription,
node: &'a dyn SdfNode,
pds: &[ProtectionDomain],
) -> Result<ChannelEnd, String> {
let node_name = node.tag_name();
if node_name != "end" {
let pos = node.range().start;
return Err(format!(
"Error: invalid XML element '{}': {}",
node_name,
loc_string(xml_sdf, pos)
));
}

check_attributes(xml_sdf, node, &["pd", "id", "pp", "notify", "setvar_id"])?;
let end_pd = checked_lookup(xml_sdf, node, "pd")?;
let end_id = checked_lookup(xml_sdf, node, "id")?.parse::<i64>().unwrap();

if end_id > PD_MAX_ID as i64 {
return Err(value_error(
xml_sdf,
node,
format!("id must be < {}", PD_MAX_ID + 1),
));
}

if end_id < 0 {
return Err(value_error(xml_sdf, node, "id must be >= 0".to_string()));
}

let notify = node
.attribute("notify")
.map(str_to_bool)
.unwrap_or(Some(true))
.ok_or_else(|| {
value_error(
xml_sdf,
node,
"notify must be 'true' or 'false'".to_string(),
)
})?;

let pp = node
.attribute("pp")
.map(str_to_bool)
.unwrap_or(Some(false))
.ok_or_else(|| {
value_error(xml_sdf, node, "pp must be 'true' or 'false'".to_string())
})?;

if let Some(pd_idx) = pds.iter().position(|pd| pd.name == end_pd) {
let setvar_id = node.attribute("setvar_id").map(ToOwned::to_owned);
Ok(ChannelEnd {
pd: pd_idx,
id: end_id.try_into().unwrap(),
notify,
pp,
setvar_id,
})
} else {
Err(value_error(
xml_sdf,
node,
format!("invalid PD name '{end_pd}'"),
))
}
}
}

impl Channel {
/// It should be noted that this function assumes that `pds` is populated
/// with all the Protection Domains that could potentially be connected with
/// the channel.
pub(super) fn from_xml<'a>(
xml_sdf: &'a XmlSystemDescription,
node: &'a dyn SdfNode,
pds: &[ProtectionDomain],
) -> Result<Channel, String> {
check_attributes(xml_sdf, node, &[])?;

let [ref end_a, ref end_b] = node
.children()
.map(|node| ChannelEnd::from_xml(xml_sdf, &*node, pds))
.collect::<Result<Vec<_>, _>>()?[..]
else {
return Err(value_error(
xml_sdf,
node,
"exactly two end elements must be specified".to_string(),
));
};

if end_a.pp && end_b.pp {
return Err(value_error(
xml_sdf,
node,
"cannot ppc bidirectionally".to_string(),
));
}

Ok(Channel {
end_a: end_a.clone(),
end_b: end_b.clone(),
})
}
}
39 changes: 39 additions & 0 deletions tool/microkit/src/sdf/consts.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
//
// Copyright 2025, UNSW
//
// SPDX-License-Identifier: BSD-2-Clause
//

/// Events that come through entry points (e.g notified or protected) are given an
/// identifier that is used as the badge at runtime.
/// On 64-bit platforms, this badge has a limit of 64-bits which means that we are
/// limited in how many IDs a Microkit protection domain has since each ID represents
/// a unique bit.
/// Currently the first bit is used to determine whether or not the event is a PPC
/// or notification. The second bit is used to determine whether a fault occurred.
/// This means we are left with 62 bits for the ID.
/// IDs start at zero.
pub const PD_MAX_ID: u64 = 61;
pub const VCPU_MAX_ID: u64 = PD_MAX_ID;

/// This is the maximum slot allowed for cap maps. This can change if you wish,
/// but also update the MICROKIT_MAX_USER_CAPS define in `microkit.h`.
pub const CAP_MAP_MAX_SLOT: u64 = 128;

pub const MONITOR_PRIORITY: u8 = 255;
pub const PD_MAX_PRIORITY: u8 = 254;
/// In microseconds
pub const BUDGET_DEFAULT: u64 = 1000;

pub const MONITOR_PD_NAME: &str = "monitor";
pub const MONITOR_DOMAIN: u8 = 0;

/// Default to a stack size of 8KiB
pub const PD_DEFAULT_STACK_SIZE: u64 = 0x2000;
pub const PD_MIN_STACK_SIZE: u64 = 0x1000;
pub const PD_MAX_STACK_SIZE: u64 = 1024 * 1024 * 16;

/// Maximum x86 IRQ vector value. Inclusive.
/// This value is calculated by the kernel as `irq_user_max - irq_user_min` in
/// `src/arch/x86/object/interrupt.c`
pub const X86_IRQ_VECTOR_MAX: i64 = 107;
113 changes: 113 additions & 0 deletions tool/microkit/src/sdf/cspace.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
//
// Copyright 2025, UNSW
//
// SPDX-License-Identifier: BSD-2-Clause
//

use super::consts::*;
use super::util::{check_attributes, checked_lookup, loc_string, sdf_parse_number, value_error};
use super::{SdfLocation, SdfNode, XmlSystemDescription};

#[derive(Debug, PartialEq, Eq, Copy, Clone, Hash)]
pub enum CapMapType {
Tcb,
Sc,
VSpace,
}

#[derive(Debug, PartialEq, Eq)]
pub struct CapMap {
pub cap_type: CapMapType,
// FIXME: This is quite a hack. Basically, we need to be able to reference
// arbitrary PDs, but to gather the index, we need to know all the PDs.
// However, at the time of parsing the cap maps, we are in the process
// of parsing all the PDs. In lieu of something better (in my - @midnightveil's
// opinion, making everything think in terms of PD names, and something
// that was necessary to do for the multikernel changes); the pd idx will
// be filled out later during SDF parse process.
pub pd_name: String,
pub pd: Option<usize>,
// The destination "slot" in the CSpace: note that this is "opaque" and
// can be shifted depending on the location in the CSpace to work as the CPtr,
// but here it is given as the index into the CNode.
pub slot: u64,
/// Location in the parsed SDF file
pub text_pos: SdfLocation,
}

#[derive(Debug)]
pub struct CSpace {
pub cap_maps: Vec<CapMap>,
}

impl CapMap {
fn from_xml(
cap_type: CapMapType,
xml_sdf: &XmlSystemDescription,
node: &dyn SdfNode,
) -> Result<CapMap, String> {
// At the moment the four cap maps we support all have the 'pd' element,
// so we can include it here. When that stops being the case we will
// have to rework this a bit.
check_attributes(xml_sdf, node, &["slot", "pd"])?;

let pd_name = checked_lookup(xml_sdf, node, "pd")?.to_string();

let slot = sdf_parse_number(checked_lookup(xml_sdf, node, "slot")?, node)?;

if slot == 0 {
return Err(value_error(
xml_sdf,
node,
("The destination slot 0 has been reserved for Microkit CNode").to_string(),
));
}

// TODO: Rework this so that we don't have a fixed upper limit.
if slot >= CAP_MAP_MAX_SLOT {
return Err(value_error(
xml_sdf,
node,
format!("There are only {CAP_MAP_MAX_SLOT} destination cspace slots available."),
));
}

Ok(CapMap {
cap_type,
pd_name,
// FIXME: Hack, filled out later.
pd: None,
slot,
text_pos: node.range().start,
})
}
}

impl CSpace {
pub(super) fn from_xml(
xml_sdf: &XmlSystemDescription,
node: &dyn SdfNode,
) -> Result<Self, String> {
check_attributes(xml_sdf, node, &[])?;

let mut cap_maps = vec![];

for child in node.children() {
cap_maps.push(match child.tag_name() {
"cap_tcb" => CapMap::from_xml(CapMapType::Tcb, xml_sdf, &*child)?,
"cap_sc" => CapMap::from_xml(CapMapType::Sc, xml_sdf, &*child)?,
"cap_vspace" => CapMap::from_xml(CapMapType::VSpace, xml_sdf, &*child)?,
child_name => {
let location = loc_string(xml_sdf, child.range().start);
if let Some(type_name) = child_name.strip_prefix("cap_") {
return Err(format!("Cap type: '{type_name}' is not supported at '{location}'"));
} else {
return Err(format!("Element '{child_name}' is not supported in a <cspace> element at '{location}'"));
}
}
})
}

Ok(CSpace { cap_maps })
}
}
Loading
Loading