Add initial refactored simple single guest example

This example has two build systems now, a Makefile as well as the Zig
build system for educational purposes.

Documentation to follow.

.gitignore

@@ -1,3 +1,5 @@
 build/
 *.pdf
+zig-out/
+zig-cache/
 

examples/simple/Makefile

@@ -0,0 +1,143 @@
+#
+# Copyright 2021, Breakaway Consulting Pty. Ltd.
+# Copyright 2022, UNSW (ABN 57 195 873 179)
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(SEL4CP_SDK)),)
+$(error SEL4CP_SDK must be specified)
+endif
+
+ifeq ($(strip $(BOARD)),)
+$(error BOARD must be specified)
+endif
+
+ifeq ($(strip $(CONFIG)),)
+$(error CONFIG must be specified)
+endif
+
+ifeq ($(strip $(SYSTEM)),)
+$(error SYSTEM must be specified)
+endif
+
+# @ivanv: Check for dependencies and make sure they are installed/in the path
+
+# @ivanv: check that all dependencies exist
+# Specify that we use bash for all shell commands
+SHELL=/bin/bash
+# All dependencies needed to compile the VMM
+QEMU := qemu-system-aarch64
+DTC := dtc
+
+ifndef TOOLCHAIN
+	# Get whether the common toolchain triples exist
+	TOOLCHAIN_AARCH64_LINUX_GNU := $(shell command -v aarch64-linux-gnu-gcc 2> /dev/null)
+	TOOLCHAIN_AARCH64_UNKNOWN_LINUX_GNU := $(shell command -v aarch64-unknown-linux-gnu-gcc 2> /dev/null)
+	# Then check if they are defined and select the appropriate one
+	ifdef TOOLCHAIN_AARCH64_LINUX_GNU
+		TOOLCHAIN := aarch64-linux-gnu
+	else ifdef TOOLCHAIN_AARCH64_UNKNOWN_LINUX_GNU
+		TOOLCHAIN := aarch64-unknown-linux-gnu
+	else
+		$(error "Could not find an AArch64 cross-compiler")
+	endif
+endif
+
+CC := $(TOOLCHAIN)-gcc
+LD := $(TOOLCHAIN)-ld
+AS := $(TOOLCHAIN)-as
+SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
+
+# @ivanv: need to have a step for putting in the initrd node into the DTB,
+# 		  right now it is unfortunately hard-coded.
+
+# @ivanv: check that the path of SDK_PATH/BOARD exists
+# @ivanv: Have a list of supported boards to check with, if it's not one of those
+# have a helpful message that lists all the support boards.
+
+# @ivanv: incremental builds don't work with IMAGE_DIR changing
+
+BOARD_DIR := $(SEL4CP_SDK)/board/$(BOARD)/$(CONFIG)
+VMM_SRC_DIR := ../../src
+SYSTEM_DESCRIPTION := board/$(BOARD)/$(SYSTEM)
+
+IMAGE_DIR := board/$(BOARD)
+KERNEL_IMAGE := $(IMAGE_DIR)/linux
+DTS := $(IMAGE_DIR)/linux.dts
+DTB_IMAGE := $(BUILD_DIR)/linux.dtb
+INITRD_IMAGE := $(IMAGE_DIR)/rootfs.cpio.gz
+IMAGES := vmm.elf
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+
+# @ivanv: should only compile printf.o in debug
+VMM_OBJS := vmm.o printf.o virq.o linux.o guest.o psci.o smc.o fault.o util.o vgic.o package_guest_images.o
+
+# @ivanv: hack...
+# This step should be done based on the DTB
+ifeq ($(BOARD),imx8mm_evk)
+	VMM_OBJS += vgic_v3.o
+else
+	VMM_OBJS += vgic_v2.o
+endif
+
+# Toolchain flags
+# FIXME: For optimisation we should consider providing the flag -mcpu.
+# FIXME: We should also consider whether -mgeneral-regs-only should be
+# used to avoid the use of the FPU and therefore seL4 does not have to
+# context switch the FPU.
+CFLAGS := -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall -Wno-unused-function -Werror -I$(VMM_SRC_DIR)/arch/aarch64 -I$(VMM_SRC_DIR)/util -I$(BOARD_DIR)/include -DBOARD_$(BOARD) -DCONFIG_$(CONFIG)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lsel4cp -Tsel4cp.ld
+
+all: directories $(IMAGE_FILE)
+
+run: all
+	# @ivanv: check that the amount of RAM given to QEMU is at least the number of RAM that QEMU is setup with for seL4.
+	if ! command -v $(QEMU) &> /dev/null; then echo "Could not find dependenyc: qemu-system-aarch64"; exit 1; fi
+	$(QEMU) -machine virt,virtualization=on,highmem=off,secure=off \
+			-cpu cortex-a53 \
+			-serial mon:stdio \
+			-device loader,file=$(IMAGE_FILE),addr=0x70000000,cpu-num=0 \
+			-m size=2G \
+			-nographic
+
+directories:
+	$(shell mkdir -p $(BUILD_DIR))
+
+$(DTB_IMAGE): $(DTS)
+	if ! command -v $(DTC) &> /dev/null; then echo "Could not find dependency: Device Tree Compiler (dtc)"; exit 1; fi
+	# @ivanv: Shouldn't supress warnings
+	$(DTC) -q -I dts -O dtb $< > $@
+
+$(BUILD_DIR)/package_guest_images.o: package_guest_images.S $(IMAGE_DIR) $(KERNEL_IMAGE) $(INITRD_IMAGE) $(DTB_IMAGE)
+	$(CC) -c -g3 -x assembler-with-cpp \
+					-DGUEST_KERNEL_IMAGE_PATH=\"$(KERNEL_IMAGE)\" \
+					-DGUEST_DTB_IMAGE_PATH=\"$(DTB_IMAGE)\" \
+					-DGUEST_INITRD_IMAGE_PATH=\"$(INITRD_IMAGE)\" \
+					$< -o $@
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/util/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/arch/aarch64/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: $(VMM_SRC_DIR)/arch/aarch64/vgic/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/vmm.elf: $(addprefix $(BUILD_DIR)/, $(VMM_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) $(SYSTEM_DESCRIPTION) $(IMAGE_DIR)
+	$(SEL4CP_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

board/qemu_arm_virt_hyp/systems/simple.system → examples/simple/board/qemu_arm_virt_hyp/simple.system

@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!--
- Copyright 2022, UNSW (ABN 57 195 873 179)
+ Copyright 2023, UNSW
 
  SPDX-License-Identifier: BSD-2-Clause
 -->
@@ -35,7 +35,7 @@
             starting address of RAM is 0x40000000, so we map in the guest RAM
             at the same address in the VMMs virutal address space.
         -->
-        <map mr="guest_ram" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
+        <map mr="guest_ram" vaddr="0x40000000" perms="rw" />
         <virtual_machine name="linux" id="0">
             <!--
              The device tree given to Linux specifies that RAM will start

examples/simple/build.zig

@@ -0,0 +1,144 @@
+const std = @import("std");
+
+pub fn build(b: *std.Build) void {
+    const target = b.standardTargetOptions(.{});
+    // @ivanv: need to somehow relate sel4cp config with this optimisation level?
+    const optimize = b.standardOptimizeOption(.{});
+
+    // @ivanv sort out
+    const sdk_path = "/Users/ivanv/ts/sel4cp_dev/release/sel4cp-sdk-1.2.6";
+    const board = "qemu_arm_virt_hyp";
+    const config = "debug";
+    // Since we are relying on Zig to produce the final ELF, it needs to do the
+    // linking step as well.
+    const sdk_board_dir = sdk_path ++ "/board/" ++ board ++ "/" ++ config;
+
+    const vmmlib = b.addStaticLibrary(.{
+        .name = "vmm",
+        .target = target,
+        .optimize = optimize,
+    });
+
+    // The paths are required to have quotes around them
+    const linux_image_path = "\"board/" ++ board ++ "/linux\"";
+    // @ivanv: come back to
+    const dtb_image_path = "\"build/linux.dtb\"";
+    const initrd_image_path = "\"board/" ++ board ++ "/rootfs.cpio.gz\"";
+
+    const vmm_src_dir = "../../src/";
+    // @ivanv: obviously for other archs we want a different dir
+    const vmm_src_arch_dir = vmm_src_dir ++ "arch/aarch64/";
+    vmmlib.addCSourceFiles(&.{
+        vmm_src_dir ++ "guest.c",
+        vmm_src_dir ++ "util/util.c",
+        vmm_src_dir ++ "util/printf.c",
+        vmm_src_arch_dir ++ "vgic/vgic.c",
+        vmm_src_arch_dir ++ "vgic/vgic_v2.c",
+        vmm_src_arch_dir ++ "fault.c",
+        vmm_src_arch_dir ++ "psci.c",
+        vmm_src_arch_dir ++ "smc.c",
+        vmm_src_arch_dir ++ "virq.c",
+        vmm_src_arch_dir ++ "linux.c",
+    }, &.{
+        "-Wall",
+        "-Werror",
+        "-Wno-unused-function",
+        "-mstrict-align",
+        "-DBOARD_qemu_arm_virt_hyp",
+    });
+
+    vmmlib.addIncludePath(vmm_src_dir);
+    vmmlib.addIncludePath(vmm_src_dir ++ "util/");
+    vmmlib.addIncludePath(vmm_src_arch_dir);
+    vmmlib.addIncludePath(vmm_src_arch_dir ++ "vgic/");
+    vmmlib.addIncludePath(sdk_board_dir ++ "/include");
+
+    b.installArtifact(vmmlib);
+
+    const exe = b.addExecutable(.{
+        .name = "vmm.elf",
+        .target = target,
+        .optimize = optimize,
+    });
+
+    // Add sel4cp.h to be used by the API wrapper.
+    exe.addIncludePath(sdk_board_dir ++ "/include");
+    exe.addIncludePath(vmm_src_dir);
+    exe.addIncludePath(vmm_src_arch_dir);
+    // Add the static library that provides each protection domain's entry
+    // point (`main()`), which runs the main handler loop.
+    exe.addObjectFile(sdk_board_dir ++ "/lib/libsel4cp.a");
+    exe.linkLibrary(vmmlib);
+    // Specify the linker script, this is necessary to set the ELF entry point address.
+    exe.setLinkerScriptPath(.{ .path = sdk_board_dir ++ "/lib/sel4cp.ld"});
+
+    exe.addCSourceFiles(&.{"vmm.c"}, &.{
+        "-Wall",
+        "-Werror",
+        "-Wno-unused-function",
+        "-mstrict-align",
+        "-DBOARD_qemu_arm_virt_hyp",
+    });
+
+    const guest_images = b.addObject(.{
+        .name = "guest_images",
+        .target = target,
+        .optimize = optimize,
+    });
+
+    guest_images.addCSourceFiles(&.{"package_guest_images.S"}, &.{
+        "-DGUEST_KERNEL_IMAGE_PATH=" ++ linux_image_path,
+        "-DGUEST_DTB_IMAGE_PATH=" ++ dtb_image_path,
+        "-DGUEST_INITRD_IMAGE_PATH=" ++ initrd_image_path,
+        "-x",
+        "assembler-with-cpp",
+    });
+
+    exe.addObject(guest_images);
+    b.installArtifact(exe);
+
+    const system_description_path = "board/" ++ board ++ "/simple.system";
+    const sel4cp_tool_cmd = b.addSystemCommand(&[_][]const u8{
+       sdk_path ++ "/bin/sel4cp",
+       system_description_path,
+       "--search-path",
+       "zig-out/bin",
+       "--board",
+       board,
+       "--config",
+       config,
+       "-o",
+       "zig-out/bin/loader.img",
+       "-r",
+       "zig-out/report.txt",
+    });
+    // Running the seL4CP tool depends on 
+    sel4cp_tool_cmd.step.dependOn(b.getInstallStep());
+    // Add the "sel4cp" step, and make it the default step when we execute `zig build`>
+    const sel4cp_step = b.step("sel4cp", "Compile and build the final bootable image");
+    sel4cp_step.dependOn(&sel4cp_tool_cmd.step);
+    b.default_step = sel4cp_step;
+
+    // This is setting up a `simulate` command for running the system via QEMU,
+    // which we only want to do when we have a board that we can actually simulate.
+    // @ivanv we should try get renode working as well
+    if (std.mem.eql(u8, board, "qemu_arm_virt_hyp")) {
+        const simulate_cmd = b.addSystemCommand(&[_][]const u8{
+            "qemu-system-aarch64",
+            "-machine",
+            "virt,virtualization=on,highmem=off,secure=off",
+            "-cpu",
+            "cortex-a53",
+            "-serial",
+            "mon:stdio",
+            "-device",
+            "loader,file=zig-out/bin/loader.img,addr=0x70000000,cpu-num=0",
+            "-m",
+            "2G",
+            "-nographic",
+        });
+        simulate_cmd.step.dependOn(b.default_step);
+        const simulate_step = b.step("simulate", "Simulate the image via QEMU");
+        simulate_step.dependOn(&simulate_cmd.step);
+    }
+}

examples/simple/package_guest_images.S

@@ -0,0 +1,32 @@
+/*
+ * Copyright 2023, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+/* @probits is used to say that this section contains data. */
+/* The attributes "aw" is to say that the section is allocatable and that it is writeable. */
+
+#if defined(GUEST_KERNEL_IMAGE_PATH)
+.section .guest_kernel_image, "aw", @progbits
+.global _guest_kernel_image, _guest_kernel_image_end
+_guest_kernel_image:
+.incbin GUEST_KERNEL_IMAGE_PATH
+_guest_kernel_image_end:
+#endif
+
+#if defined(GUEST_DTB_IMAGE_PATH)
+.section .guest_dtb_image, "aw", @progbits
+.global _guest_dtb_image, _guest_dtb_image_end
+_guest_dtb_image:
+.incbin GUEST_DTB_IMAGE_PATH
+_guest_dtb_image_end:
+#endif
+
+#if defined(GUEST_INITRD_IMAGE_PATH)
+.section .guest_initrd_image, "aw", @progbits
+.global _guest_initrd_image, _guest_initrd_image_end
+_guest_initrd_image:
+.incbin GUEST_INITRD_IMAGE_PATH
+_guest_initrd_image_end:
+#endif