tool: add tests for parsing virtual machines

Signed-off-by: Ivan-Velickovic <[email protected]>
seL4 · Oct 30, 2024 · f8ddfbb · f8ddfbb
1 parent cf833e9
commit f8ddfbb
Show file tree

Hide file tree

Showing 10 changed files with 196 additions and 3 deletions.
diff --git a/tool/microkit/tests/sdf/pd_duplicate_child_id_vcpu.xml 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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")