From d4d08d387a7a4e9e4d43d8aa8cc9b30ceba3869d Mon Sep 17 00:00:00 2001
From: julia <git.ts@trainwit.ch>
Date: Wed, 4 Sep 2024 10:56:16 +1000
Subject: [PATCH] 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 <git.ts@trainwit.ch>
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
---
 tool/microkit/src/sdf.rs                      | 16 ++++++++++++++++
 .../microkit/tests/sdf/ch_ppcall_priority.xml | 19 +++++++++++++++++++
 tool/microkit/tests/test.rs                   |  8 ++++++++
 3 files changed, 43 insertions(+)
 create mode 100644 tool/microkit/tests/sdf/ch_ppcall_priority.xml

diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 4933150c..73ee65c9 100644
--- a/tool/microkit/src/sdf.rs
+++ b/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);
     }
diff --git a/tool/microkit/tests/sdf/ch_ppcall_priority.xml b/tool/microkit/tests/sdf/ch_ppcall_priority.xml
new file mode 100644
index 00000000..6524fee5
--- /dev/null
+++ b/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>
diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs
index a281aa89..9c1a34de 100644
--- a/tool/microkit/tests/test.rs
+++ b/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)]