From f8ddfbb60d6959c6ddede307b1e392abe1d1d1aa Mon Sep 17 00:00:00 2001
From: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Date: Wed, 30 Oct 2024 22:03:17 +1100
Subject: [PATCH] tool: add tests for parsing virtual machines

Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
---
 .../tests/sdf/pd_duplicate_child_id_vcpu.xml  | 17 +++++
 tool/microkit/tests/sdf/vm_duplicate_name.xml | 20 ++++++
 .../tests/sdf/vm_invalid_vcpu_cpu.xml         | 13 ++++
 .../microkit/tests/sdf/vm_invalid_vcpu_id.xml | 13 ++++
 tool/microkit/tests/sdf/vm_missing_mr.xml     | 15 +++++
 tool/microkit/tests/sdf/vm_missing_vcpu.xml   | 12 ++++
 .../microkit/tests/sdf/vm_missing_vcpu_id.xml | 13 ++++
 tool/microkit/tests/sdf/vm_not_child.xml      | 11 +++
 .../tests/sdf/vm_overlapping_maps.xml         | 18 +++++
 tool/microkit/tests/test.rs                   | 67 ++++++++++++++++++-
 10 files changed, 196 insertions(+), 3 deletions(-)
 create mode 100644 tool/microkit/tests/sdf/pd_duplicate_child_id_vcpu.xml
 create mode 100644 tool/microkit/tests/sdf/vm_duplicate_name.xml
 create mode 100644 tool/microkit/tests/sdf/vm_invalid_vcpu_cpu.xml
 create mode 100644 tool/microkit/tests/sdf/vm_invalid_vcpu_id.xml
 create mode 100644 tool/microkit/tests/sdf/vm_missing_mr.xml
 create mode 100644 tool/microkit/tests/sdf/vm_missing_vcpu.xml
 create mode 100644 tool/microkit/tests/sdf/vm_missing_vcpu_id.xml
 create mode 100644 tool/microkit/tests/sdf/vm_not_child.xml
 create mode 100644 tool/microkit/tests/sdf/vm_overlapping_maps.xml

diff --git a/tool/microkit/tests/sdf/pd_duplicate_child_id_vcpu.xml b/tool/microkit/tests/sdf/pd_duplicate_child_id_vcpu.xml
new file mode 100644
index 00000000..b1be0db4
--- /dev/null
+++ b/tool/microkit/tests/sdf/pd_duplicate_child_id_vcpu.xml
@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="parent">
+        <program_image path="parent.elf" />
+        <protection_domain name="child1" id="0">
+            <program_image path="child.elf" />
+        </protection_domain>
+        <virtual_machine name="guest1">
+            <vcpu id="0" />
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_duplicate_name.xml b/tool/microkit/tests/sdf/vm_duplicate_name.xml
new file mode 100644
index 00000000..d7343cb5
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_duplicate_name.xml
@@ -0,0 +1,20 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2021, Breakaway Consulting Pty. Ltd.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="hello1">
+        <program_image path="hello.elf" />
+        <virtual_machine name="guest">
+            <vcpu id="0" />
+        </virtual_machine>
+    </protection_domain>
+    <protection_domain name="hello2">
+        <program_image path="hello.elf" />
+        <virtual_machine name="guest">
+            <vcpu id="0" />
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_invalid_vcpu_cpu.xml b/tool/microkit/tests/sdf/vm_invalid_vcpu_cpu.xml
new file mode 100644
index 00000000..ea4c0c35
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_invalid_vcpu_cpu.xml
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="pd">
+        <virtual_machine name="guest">
+            <vcpu id="0" cpu="300" />
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_invalid_vcpu_id.xml b/tool/microkit/tests/sdf/vm_invalid_vcpu_id.xml
new file mode 100644
index 00000000..44a262e7
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_invalid_vcpu_id.xml
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="pd">
+        <virtual_machine name="guest">
+            <vcpu id="300" />
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_missing_mr.xml b/tool/microkit/tests/sdf/vm_missing_mr.xml
new file mode 100644
index 00000000..75829a25
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_missing_mr.xml
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2021, Breakaway Consulting Pty. Ltd.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="hello" priority="254">
+        <program_image path="hello.elf" />
+        <virtual_machine name="guest">
+            <vcpu id="0" />
+            <map mr="mr1" perms="rw" vaddr="0x1_000_000" />
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_missing_vcpu.xml b/tool/microkit/tests/sdf/vm_missing_vcpu.xml
new file mode 100644
index 00000000..f0e24b61
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_missing_vcpu.xml
@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="pd">
+        <virtual_machine name="guest">
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_missing_vcpu_id.xml b/tool/microkit/tests/sdf/vm_missing_vcpu_id.xml
new file mode 100644
index 00000000..b36d8d4a
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_missing_vcpu_id.xml
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="pd">
+        <virtual_machine name="guest">
+            <vcpu />
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_not_child.xml b/tool/microkit/tests/sdf/vm_not_child.xml
new file mode 100644
index 00000000..9d6a128f
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_not_child.xml
@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2024, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <virtual_machine name="guest">
+        <vcpu id="0" />
+    </virtual_machine>
+</system>
diff --git a/tool/microkit/tests/sdf/vm_overlapping_maps.xml b/tool/microkit/tests/sdf/vm_overlapping_maps.xml
new file mode 100644
index 00000000..c4273001
--- /dev/null
+++ b/tool/microkit/tests/sdf/vm_overlapping_maps.xml
@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2021, Breakaway Consulting Pty. Ltd.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <memory_region name="mr1" size="0x1000" />
+    <memory_region name="mr2" size="0x1000" />
+    <protection_domain name="hello" priority="254">
+        <program_image path="hello.elf" />
+        <virtual_machine name="guest">
+            <vcpu id="0" />
+            <map mr="mr1" perms="rw" vaddr="0x1_000_000" />
+            <map mr="mr2" perms="rw" vaddr="0x1_000_000" />
+        </virtual_machine>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs
index 90b5811d..0ed4c448 100644
--- a/tool/microkit/tests/test.rs
+++ b/tool/microkit/tests/test.rs
@@ -253,6 +253,14 @@ mod protection_domain {
         )
     }
 
+    #[test]
+    fn test_duplicate_child_id_vcpu() {
+        check_error(
+            "pd_duplicate_child_id_vcpu.xml",
+            "Error: duplicate id: 0 clashes with virtual machine vcpu id in protection domain: 'parent' @",
+        )
+    }
+
     #[test]
     fn test_small_stack_size() {
         check_error(
@@ -279,14 +287,67 @@ mod protection_domain {
 }
 
 #[cfg(test)]
-mod channel {
+mod virtual_machine {
     use super::*;
 
     #[test]
-    fn test_missing_pd() {
-        check_missing("ch_missing_pd.xml", "pd", "end")
+    fn test_vm_not_child() {
+        check_error(
+            "vm_not_child.xml",
+            "Error: virtual machine must be a child of a protection domain",
+        )
+    }
+
+    #[test]
+    fn test_duplicate_name() {
+        check_error(
+            "vm_duplicate_name.xml",
+            "Error: duplicate virtual machine name 'guest'",
+        )
     }
 
+    #[test]
+    fn test_missing_vcpu() {
+        check_error(
+            "vm_missing_vcpu.xml",
+            "Error: missing 'vcpu' element on virtual_machine: ",
+        )
+    }
+
+    #[test]
+    fn test_missing_vcpu_id() {
+        check_missing("vm_missing_vcpu_id.xml", "id", "vcpu")
+    }
+
+    #[test]
+    fn test_invalid_vcpu_id() {
+        check_error(
+            "vm_invalid_vcpu_id.xml",
+            "Error: id must be < 62 on element 'vcpu'",
+        )
+    }
+
+    #[test]
+    fn test_overlapping_maps() {
+        check_error(
+            "vm_overlapping_maps.xml",
+            "Error: map for 'mr2' has virtual address range [0x1000000..0x1001000) which overlaps with map for 'mr1' [0x1000000..0x1001000) in virtual machine 'guest' @"
+        )
+    }
+
+    #[test]
+    fn test_missing_mr() {
+        check_error(
+            "vm_missing_mr.xml",
+            "Error: invalid memory region name 'mr1' on 'map' @",
+        )
+    }
+}
+
+#[cfg(test)]
+mod channel {
+    use super::*;
+
     #[test]
     fn test_missing_id() {
         check_missing("ch_missing_id.xml", "id", "end")