tool: enforce the protected procedure priorities

As per the Microkit manual,

> A protected call is only possible if the callee has strictly higher
> priority than the caller.

Due to the change to specify `pp="true"` in the SDF in the previous
commit, we can now verify that the priority invariant holds true,
instead of it being possible to create a system with this behaviour.

Signed-off-by: julia <[email protected]>
Signed-off-by: Ivan-Velickovic <[email protected]>

tool/microkit/src/sdf.rs

@@ -1201,6 +1201,22 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result<SystemDescrip
             ));
         }
 
+        let pd_a = &pds[ch.end_a.pd];
+        let pd_b = &pds[ch.end_b.pd];
+        if ch.end_a.pp && pd_a.priority >= pd_b.priority {
+            return Err(format!(
+                "Error: PPCs must be to protection domains of strictly higher priorities; \
+                        channel with PPC exists from pd {} (priority: {}) to pd {} (priority: {})",
+                pd_a.name, pd_a.priority, pd_b.name, pd_b.priority
+            ));
+        } else if ch.end_b.pp && pd_b.priority >= pd_a.priority {
+            return Err(format!(
+                "Error: PPCs must be to protection domains of strictly higher priorities; \
+                        channel with PPC exists from pd {} (priority: {}) to pd {} (priority: {})",
+                pd_b.name, pd_b.priority, pd_a.name, pd_a.priority
+            ));
+        }
+
         ch_ids[ch.end_a.pd].push(ch.end_a.id);
         ch_ids[ch.end_b.pd].push(ch.end_b.id);
     }

tool/microkit/tests/sdf/ch_ppcall_priority.xml

@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="test1" priority="2">
+        <program_image path="test" />
+    </protection_domain>
+    <protection_domain name="test2" priority="1">
+        <program_image path="test" />
+    </protection_domain>
+
+    <channel>
+        <end pd="test1" id="0" pp="true" />
+        <end pd="test2" id="0" />
+    </channel>
+</system>

tool/microkit/tests/test.rs

@@ -368,6 +368,14 @@ mod channel {
             "Error: cannot ppc bidirectionally on element 'channel': ",
         )
     }
+
+    #[test]
+    fn test_ppcall_priority() {
+        check_error(
+            "ch_ppcall_priority.xml",
+            "Error: PPCs must be to protection domains of strictly higher priorities; channel with PPC exists from pd test1 (priority: 2) to pd test2 (priority: 1)",
+        )
+    }
 }
 
 #[cfg(test)]