x86: Add new minimal_64 test

Add a new VM app to demonstrate/test the new x86_64 virtualization support. Signed-off-by: Jingyao Zhou <[email protected]>
seL4 · May 2, 2023 · 72f2c83 · 72f2c83
1 parent 9f0a534
commit 72f2c83
Show file tree

Hide file tree

Showing 3 changed files with 88 additions and 0 deletions.
diff --git a/apps/x86/minimal_64/CMakeLists.txt b/apps/x86/minimal_64/CMakeLists.txt
@@ -0,0 +1,39 @@
+#
+# Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+cmake_minimum_required(VERSION 3.8.2)
+
+project(minimal_64)
+
+# Include CAmkES VM helper functions
+include(${CAMKES_VM_HELPERS_PATH})
+find_package(camkes-vm-linux REQUIRED)
+include(${CAMKES_VM_LINUX_HELPERS_PATH})
+# message(WARNING "${CAMKES_VM_HELPERS_PATH}")
+
+# message(FATAL_ERROR "${CAMKES_VM_LINUX_HELPERS_PATH}")
+
+# Declare VM component: Init0
+DeclareCAmkESVM(Init0)
+
+# Get Default Linux VM files
+GetArchDefaultLinuxKernelFile("64" kernel_file)
+GetArchDefaultLinuxRootfsFile("64" rootfs_file)
+
+# Decompress Linux Kernel image and add to file server
+DecompressLinuxKernel(extract_linux_kernel decompressed_kernel ${kernel_file})
+AddToFileServer("bzimage" ${decompressed_kernel} DEPENDS extract_linux_kernel)
+
+# Add rootfs images into file server
+AddToFileServer("rootfs.cpio" ${rootfs_file})
+
+# Initialise CAmkES Root Server with addition CPP includes
+DeclareCAmkESVMRootServer(minimal_64.camkes)
+
+if(SIMULATION)
+	include(simulation)
+    GenerateSimulateScript()
+endif()
diff --git a/apps/x86/minimal_64/app_settings.cmake b/apps/x86/minimal_64/app_settings.cmake
@@ -0,0 +1,12 @@
+#
+# Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+cmake_minimum_required(VERSION 3.8.2)
+
+# Define kernel config options
+set(KernelSel4Arch "x86_64" CACHE STRING "" FORCE)
+set(KernelMaxNumNodes 1 CACHE STRING "" FORCE)
+set(KernelX86_64VTX64BitGuests ON CACHE BOOL "" FORCE)
diff --git a/apps/x86/minimal_64/minimal_64.camkes b/apps/x86/minimal_64/minimal_64.camkes
@@ -0,0 +1,37 @@
+/*
+ * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ */
+
+import <VM/vm.camkes>;
+
+#include <configurations/vm.h>
+
+#define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \
+i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem"
+
+component Init0 {
+    VM_INIT_DEF()
+}
+
+assembly {
+    composition {
+        VM_COMPOSITION_DEF()
+        VM_PER_VM_COMP_DEF(0)
+    }
+
+    configuration {
+        VM_CONFIGURATION_DEF()
+        VM_PER_VM_CONFIG_DEF(0)
+
+        vm0.simple_untyped23_pool = 20;
+        vm0.heap_size = 0x2000000;
+        vm0.guest_ram_mb = 128;
+        vm0.kernel_cmdline = VM_GUEST_CMDLINE;
+        vm0.kernel_image = "bzimage";
+        vm0.kernel_relocs = "bzimage";
+        vm0.initrd_image = "rootfs.cpio";
+        vm0.iospace_domain = 0x0f;
+    }
+}