tool: use kernel config instead of feature flag

Signed-off-by: James Archer <[email protected]>
seL4 · Jul 26, 2024 · ed49ef8 · ed49ef8
1 parent fdad16f
commit ed49ef8
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 13 deletions.
diff --git a/build_sdk.py b/build_sdk.py
@@ -239,11 +239,10 @@ def test_tool() -> None:
     assert r == 0
 
 
-def build_tool(tool_target: Path, target_triple: str, experimental_domain_support: bool = False) -> None:
-    build_cmd = f"cd tool/microkit && cargo build --release --target {target_triple}"
-    if experimental_domain_support:
-        build_cmd = f"{build_cmd} --features experimental-domain-support"
-    r = system(build_cmd)
+def build_tool(tool_target: Path, target_triple: str) -> None:
+    r = system(
+        f"cd tool/microkit && cargo build --release --target {target_triple}"
+    )
     assert r == 0
 
     tool_output = f"./tool/microkit/target/{target_triple}/release/microkit"
@@ -502,7 +501,7 @@ def main() -> None:
     if not args.skip_tool:
         tool_target = root_dir / "bin" / "microkit"
         test_tool()
-        build_tool(tool_target, args.tool_target_triple, args.experimental_domain_support)
+        build_tool(tool_target, args.tool_target_triple)
 
     if not args.skip_docs:
         build_doc(root_dir)

diff --git a/tool/microkit/Cargo.toml b/tool/microkit/Cargo.toml
@@ -13,9 +13,6 @@ edition = "2021"
 name = "microkit"
 path = "src/main.rs"
 
-[features]
-experimental-domain-support = []
-
 [dependencies]
 roxmltree = "0.19.0"
 serde = "1.0.203"

diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs
@@ -2906,6 +2906,7 @@ fn main() -> Result<(), String> {
         fan_out_limit: json_str_as_u64(&kernel_config_json, "RETYPE_FAN_OUT_LIMIT")?,
         arm_pa_size_bits: 40,
         hypervisor: json_str_as_bool(&kernel_config_json, "ARM_HYPERVISOR_SUPPORT")?,
+        domain_scheduler: json_str_as_u64(&kernel_config_json, "NUM_DOMAINS")? != 1,
     };
 
     match kernel_config.arch {

diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs
@@ -48,6 +48,7 @@ pub struct Config {
     pub fan_out_limit: u64,
     pub hypervisor: bool,
     pub arm_pa_size_bits: usize,
+    pub domain_scheduler: bool,
 }
 
 pub enum Arch {

diff --git a/tool/microkit/src/sysxml.rs b/tool/microkit/src/sysxml.rs
@@ -75,6 +75,7 @@ fn loc_string(xml_sdf: &XmlSystemDescription, pos: roxmltree::TextPos) -> String
 pub struct PlatformDescription {
     /// Note that we have the invariant that page sizes are be ordered by size
     page_sizes: [u64; 2],
+    domain_scheduler: bool,
 }
 
 impl PlatformDescription {
@@ -83,7 +84,10 @@ impl PlatformDescription {
             Arch::Aarch64 => [0x1000, 0x200_000],
         };
 
-        PlatformDescription { page_sizes }
+        PlatformDescription {
+            page_sizes,
+            domain_scheduler: kernel_config.domain_scheduler,
+        }
     }
 }
 
@@ -291,6 +295,7 @@ impl ProtectionDomain {
         node: &roxmltree::Node,
         is_child: bool,
         domain_schedule: &Option<DomainSchedule>,
+        plat_desc: &PlatformDescription,
     ) -> Result<ProtectionDomain, String> {
         let mut attrs = vec![
             "name", "priority", "pp", "budget", "period", "passive", "domain",
@@ -375,7 +380,7 @@ impl ProtectionDomain {
                 return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name))
             }
             (_, Ok(domain)) => {
-                if cfg!(feature = "experimental-domain-support") {
+                if plat_desc.domain_scheduler {
                     return Err(format!("Protection domain {} specifies a domain {} but system does not specify a domain schedule", name, domain));
                 } else {
                     return Err(format!("Assigning PDs to domains is only supported if SDK is built with --experimental-domain-support"));
@@ -498,6 +503,7 @@ impl ProtectionDomain {
                     &child,
                     true,
                     &domain_schedule,
+                    &plat_desc,
                 )?),
                 "virtual_machine" => {
                     if virtual_machine.is_some() {
@@ -1050,7 +1056,7 @@ pub fn parse(
     // then parse the channels.
     let mut channel_nodes = Vec::new();
 
-    if cfg!(feature = "experimental-domain-support") {
+    if plat_desc.domain_scheduler {
         if let Some(domain_schedule_node) = system
             .children()
             .filter(|&child| child.is_element())
@@ -1072,11 +1078,12 @@ pub fn parse(
                 &child,
                 false,
                 &domain_schedule,
+                &plat_desc,
             )?),
             "channel" => channel_nodes.push(child),
             "memory_region" => mrs.push(SysMemoryRegion::from_xml(&xml_sdf, &child, plat_desc)?),
             "domain_schedule" => {
-                if !cfg!(feature = "experimental-domain-support") {
+                if !plat_desc.domain_scheduler {
                     let pos = xml_sdf.doc.text_pos_at(child.range().start);
                     return Err(format!("Domain schedule is only supported if SDK is built with --experimental-domain-support: {}", loc_string(&xml_sdf, pos)));
                 }

diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs
@@ -17,6 +17,7 @@ const DEFAULT_KERNEL_CONFIG: sel4::Config = sel4::Config {
     fan_out_limit: 256,
     hypervisor: true,
     arm_pa_size_bits: 40,
+    domain_scheduler: false,
 };
 
 const DEFAULT_PLAT_DESC: sysxml::PlatformDescription =