more sel4 work for ME2150

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/Makefile

@@ -0,0 +1,124 @@
+# If you would like to choose a different path to the SDK, you can pass it as an
+# argument.
+ifndef MICROKIT_SDK
+	MICROKIT_SDK := ../microkit-sdk-1.4.0
+endif
+
+# In case the default compiler triple doesn't work for you or your package manager
+# only has aarch64-none-elf or something, you can specifiy the toolchain.
+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
+
+BOARD := qemu_virt_aarch64
+MICROKIT_CONFIG := debug
+BUILD_DIR := build
+
+CPU := cortex-a53
+
+CC := $(TOOLCHAIN)-gcc
+LD := $(TOOLCHAIN)-ld
+AS := $(TOOLCHAIN)-as
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
+
+PRINTF_OBJS := printf.o util.o
+SERIAL_SERVER_OBJS := $(PRINTF_OBJS) serial_server.o
+CLIENT_OBJS := $(PRINTF_OBJS) client.o
+WORDLE_SERVER_OBJS := $(PRINTF_OBJS) wordle_server.o
+VMM_OBJS := $(PRINTF_OBJS) vmm.o psci.o smc.o fault.o vgic.o global_data.o vgic_v2.o
+
+BOARD_DIR := $(MICROKIT_SDK)/board/$(BOARD)/$(MICROKIT_CONFIG)
+
+IMAGES_PART_1 := serial_server.elf
+IMAGES_PART_2 := serial_server.elf client.elf
+IMAGES_PART_3 := serial_server.elf client.elf wordle_server.elf
+IMAGES_PART_4 := serial_server.elf client.elf wordle_server.elf vmm.elf
+# Note that these warnings being disabled is to avoid compilation errors while in the middle of completing each exercise part
+CFLAGS := -mcpu=$(CPU) -mstrict-align -nostdlib -ffreestanding -g -Wall -Wno-array-bounds -Wno-unused-variable -Wno-unused-function -Werror -I$(BOARD_DIR)/include -Ivmm/src/util -Iinclude -DBOARD_$(BOARD)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lmicrokit -Tmicrokit.ld
+
+IMAGE_FILE_PART_1 = $(BUILD_DIR)/wordle_part_one.img
+IMAGE_FILE_PART_2 = $(BUILD_DIR)/wordle_part_two.img
+IMAGE_FILE_PART_3 = $(BUILD_DIR)/wordle_part_three.img
+IMAGE_FILE_PART_4 = $(BUILD_DIR)/wordle_part_four.img
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+
+# VMM defines
+KERNEL_IMAGE = vmm/images/linux
+DTB_IMAGE = vmm/images/linux.dtb
+INITRD_IMAGE = vmm/images/rootfs.cpio.gz
+
+all: directories $(IMAGE_FILE)
+
+directories:
+	$(info $(shell mkdir -p $(BUILD_DIR)))
+
+run: $(IMAGE_FILE)
+	qemu-system-aarch64 -machine virt,virtualization=on \
+		-cpu $(CPU) \
+		-serial mon:stdio \
+		-device loader,file=$(IMAGE_FILE),addr=0x70000000,cpu-num=0 \
+		-m size=2G \
+		-nographic \
+		-netdev user,id=mynet0 \
+		-device virtio-net-device,netdev=mynet0,mac=52:55:00:d1:55:01
+
+part1: directories $(BUILD_DIR)/serial_server.elf $(IMAGE_FILE_PART_1)
+part2: directories $(BUILD_DIR)/client.elf $(IMAGE_FILE_PART_2)
+part3: directories $(BUILD_DIR)/wordle_server.elf $(IMAGE_FILE_PART_3)
+part4: directories $(BUILD_DIR)/vmm.elf $(IMAGE_FILE_PART_4)
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: vmm/src/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: vmm/src/util/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: vmm/src/vgic/%.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/global_data.o: vmm/src/global_data.S $(KERNEL_IMAGE) $(INITRD_IMAGE) $(DTB_IMAGE)
+	$(CC) -c -g -x assembler-with-cpp \
+					-DVM_KERNEL_IMAGE_PATH=\"$(KERNEL_IMAGE)\" \
+					-DVM_DTB_IMAGE_PATH=\"$(DTB_IMAGE)\" \
+					-DVM_INITRD_IMAGE_PATH=\"$(INITRD_IMAGE)\" \
+					$< -o $@
+
+$(BUILD_DIR)/serial_server.elf: $(addprefix $(BUILD_DIR)/, $(SERIAL_SERVER_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(BUILD_DIR)/client.elf: $(addprefix $(BUILD_DIR)/, $(CLIENT_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(BUILD_DIR)/wordle_server.elf: $(addprefix $(BUILD_DIR)/, $(WORDLE_SERVER_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(BUILD_DIR)/vmm.elf: $(addprefix $(BUILD_DIR)/, $(VMM_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE_PART_1): $(addprefix $(BUILD_DIR)/, $(IMAGES_PART_1)) wordle.system
+	$(MICROKIT_TOOL) wordle.system --search-path $(BUILD_DIR) --board $(BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+
+$(IMAGE_FILE_PART_2): $(addprefix $(BUILD_DIR)/, $(IMAGES_PART_2)) wordle.system
+	$(MICROKIT_TOOL) wordle.system --search-path $(BUILD_DIR) --board $(BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+
+$(IMAGE_FILE_PART_3): $(addprefix $(BUILD_DIR)/, $(IMAGES_PART_3)) wordle.system
+	$(MICROKIT_TOOL) wordle.system --search-path $(BUILD_DIR) --board $(BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+
+$(IMAGE_FILE_PART_4): $(addprefix $(BUILD_DIR)/, $(IMAGES_PART_4)) wordle.system
+	$(MICROKIT_TOOL) wordle.system --search-path $(BUILD_DIR) --board $(BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/client.c

@@ -0,0 +1,153 @@
+#include <stdint.h>
+#include <stdbool.h>
+#include <microkit.h>
+#include "printf.h"
+#include "wordle.h"
+
+#define SERIAL_CHANNEL 1
+#define WORDLE_CHANNEL 2
+
+uintptr_t serial_to_client_vaddr;
+uintptr_t client_to_serial_vaddr;
+
+#define MOVE_CURSOR_UP "\033[5A"
+#define CLEAR_TERMINAL_BELOW_CURSOR "\033[0J"
+
+#define INVALID_CHAR (-1)
+
+struct wordle_char {
+    int ch;
+    enum character_state state;
+};
+
+// Store game state
+static struct wordle_char table[NUM_TRIES][WORD_LENGTH];
+// Use these global variables to keep track of the character index that the
+// player is currently trying to input.
+static int curr_row = 0;
+static int curr_letter = 0;
+
+void wordle_server_send() {
+    // Implement this function to send the word over PPC
+    for (int i = 0; i < WORD_LENGTH; i++) {
+        microkit_mr_set(i, table[curr_row][i].ch);
+    }
+    microkit_ppcall(WORDLE_CHANNEL, microkit_msginfo_new(0, WORD_LENGTH));
+    // After doing the PPC, the Wordle server should have updated
+    // the message-registers containing the state of each character.
+    // Look at the message registers and update the `table` accordingly.
+    for (int i = 0; i < WORD_LENGTH; i++) {
+        table[curr_row][i].state = microkit_mr_get(i);
+    }
+}
+
+void serial_send(char *str) {
+    // Implement this function to get the serial server to print the string.
+    int i = 0;
+    while (str[i] != '\0') {
+        ((char *)client_to_serial_vaddr)[i] = str[i];
+        i++;
+    }
+    ((char *)client_to_serial_vaddr)[i] = '\0';
+    microkit_notify(SERIAL_CHANNEL);
+}
+
+// This function prints a CLI Wordle using pretty colours for what characters
+// are correct, or correct but in the wrong place etc.
+void print_table(bool clear_terminal) {
+    if (clear_terminal) {
+        // Assuming we have already printed a Wordle table, this will clear the
+        // table we have already printed and then print the updated one. This
+        // is done by moving the cursor up 5 lines and then clearing everything
+        // below it.
+        serial_send(MOVE_CURSOR_UP);
+        serial_send(CLEAR_TERMINAL_BELOW_CURSOR);
+    }
+
+    for (int row = 0; row < NUM_TRIES; row++) {
+        for (int letter = 0; letter < WORD_LENGTH; letter++) {
+            serial_send("[");
+            enum character_state state = table[row][letter].state;
+            int ch = table[row][letter].ch;
+            if (ch != INVALID_CHAR) {
+                switch (state) {
+                    case INCORRECT: break;
+                    case CORRECT_PLACEMENT: serial_send("\x1B[32m"); break;
+                    case INCORRECT_PLACEMENT: serial_send("\x1B[33m"); break;
+                    default:
+                        // Print out error messages/debug info via debug output
+                        microkit_dbg_puts("CLIENT|ERROR: unexpected character state\n");
+                }
+                char ch_str[] = { ch, '\0' };
+                serial_send(ch_str);
+                // Reset colour
+                serial_send("\x1B[0m");
+            } else {
+                serial_send(" ");
+            }
+            serial_send("] ");
+        }
+        serial_send("\n");
+    }
+}
+
+void init_table() {
+    for (int row = 0; row < NUM_TRIES; row++) {
+        for (int letter = 0; letter < WORD_LENGTH; letter++) {
+            table[row][letter].ch = INVALID_CHAR;
+            table[row][letter].state = INCORRECT;
+        }
+    }
+}
+
+bool char_is_backspace(int ch) {
+    return (ch == 0x7f);
+}
+
+bool char_is_valid(int ch) {
+    // Only allow alphabetical letters and do not accept a character if the
+    // current word has already been filled.
+    return ((ch >= 'a' && ch <= 'z') || (ch >= 'A' && ch <= 'Z')) && curr_letter != WORD_LENGTH;
+}
+
+void add_char_to_table(char c) {
+    if (char_is_backspace(c)) {
+        if (curr_letter > 0) {
+            curr_letter--;
+            table[curr_row][curr_letter].ch = INVALID_CHAR;
+        }
+    } else if (c != '\r' && c != ' ' && curr_letter != WORD_LENGTH) {
+        table[curr_row][curr_letter].ch = c;
+        curr_letter++;
+    }
+
+    // If the user has finished inputting a word, we want to send the
+    // word to the server and move the cursor to the next row.
+    if (c == '\r' && curr_letter == WORD_LENGTH) {
+        wordle_server_send();
+        curr_row += 1;
+        curr_letter = 0;
+    }
+}
+
+void init(void) {
+    microkit_dbg_puts("CLIENT: starting\n");
+    serial_send("Welcome to the Wordle client!\n");
+
+    init_table();
+    // Don't want to clear the terminal yet since this is the first time
+    // we are printing it (we want to clear just the Wordle table, not
+    // everything on the terminal).
+    print_table(false);
+}
+
+void notified(microkit_channel channel) {
+    switch (channel) {
+        case SERIAL_CHANNEL: {
+            char ch = ((char *)serial_to_client_vaddr)[0];
+            add_char_to_table(ch);
+            print_table(true);
+            break;
+        }
+    }
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/printf.c

@@ -0,0 +1,914 @@
+///////////////////////////////////////////////////////////////////////////////
+// \author (c) Marco Paland (info@paland.com)
+//             2014-2019, PALANDesign Hannover, Germany
+//
+// \license The MIT License (MIT)
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in
+// all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// THE SOFTWARE.
+//
+// \brief Tiny printf, sprintf and (v)snprintf implementation, optimized for speed on
+//        embedded systems with a very limited resources. These routines are thread
+//        safe and reentrant!
+//        Use this instead of the bloated standard/newlib printf cause these use
+//        malloc for printf (and may not be thread safe).
+//
+///////////////////////////////////////////////////////////////////////////////
+
+#include <stdbool.h>
+#include <stdint.h>
+
+#include "printf.h"
+
+
+// define this globally (e.g. gcc -DPRINTF_INCLUDE_CONFIG_H ...) to include the
+// printf_config.h header file
+// default: undefined
+#ifdef PRINTF_INCLUDE_CONFIG_H
+#include "printf_config.h"
+#endif
+
+
+// 'ntoa' conversion buffer size, this must be big enough to hold one converted
+// numeric number including padded zeros (dynamically created on stack)
+// default: 32 byte
+#ifndef PRINTF_NTOA_BUFFER_SIZE
+#define PRINTF_NTOA_BUFFER_SIZE    32U
+#endif
+
+// 'ftoa' conversion buffer size, this must be big enough to hold one converted
+// float number including padded zeros (dynamically created on stack)
+// default: 32 byte
+#ifndef PRINTF_FTOA_BUFFER_SIZE
+#define PRINTF_FTOA_BUFFER_SIZE    32U
+#endif
+
+// support for the floating point type (%f)
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_FLOAT
+#define PRINTF_SUPPORT_FLOAT
+#endif
+
+// support for exponential floating point notation (%e/%g)
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_EXPONENTIAL
+#define PRINTF_SUPPORT_EXPONENTIAL
+#endif
+
+// define the default floating point precision
+// default: 6 digits
+#ifndef PRINTF_DEFAULT_FLOAT_PRECISION
+#define PRINTF_DEFAULT_FLOAT_PRECISION  6U
+#endif
+
+// define the largest float suitable to print with %f
+// default: 1e9
+#ifndef PRINTF_MAX_FLOAT
+#define PRINTF_MAX_FLOAT  1e9
+#endif
+
+// support for the long long types (%llu or %p)
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_LONG_LONG
+#define PRINTF_SUPPORT_LONG_LONG
+#endif
+
+// support for the ptrdiff_t type (%t)
+// ptrdiff_t is normally defined in <stddef.h> as long or long long type
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_PTRDIFF_T
+#define PRINTF_SUPPORT_PTRDIFF_T
+#endif
+
+///////////////////////////////////////////////////////////////////////////////
+
+// internal flag definitions
+#define FLAGS_ZEROPAD   (1U <<  0U)
+#define FLAGS_LEFT      (1U <<  1U)
+#define FLAGS_PLUS      (1U <<  2U)
+#define FLAGS_SPACE     (1U <<  3U)
+#define FLAGS_HASH      (1U <<  4U)
+#define FLAGS_UPPERCASE (1U <<  5U)
+#define FLAGS_CHAR      (1U <<  6U)
+#define FLAGS_SHORT     (1U <<  7U)
+#define FLAGS_LONG      (1U <<  8U)
+#define FLAGS_LONG_LONG (1U <<  9U)
+#define FLAGS_PRECISION (1U << 10U)
+#define FLAGS_ADAPT_EXP (1U << 11U)
+
+
+// import float.h for DBL_MAX
+#if defined(PRINTF_SUPPORT_FLOAT)
+#include <float.h>
+#endif
+
+
+// output function type
+typedef void (*out_fct_type)(char character, void* buffer, size_t idx, size_t maxlen);
+
+
+// wrapper (used as buffer) for output function type
+typedef struct {
+  void  (*fct)(char character, void* arg);
+  void* arg;
+} out_fct_wrap_type;
+
+
+// internal buffer output
+static inline void _out_buffer(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  if (idx < maxlen) {
+    ((char*)buffer)[idx] = character;
+  }
+}
+
+
+// internal null output
+static inline void _out_null(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  (void)character; (void)buffer; (void)idx; (void)maxlen;
+}
+
+
+// internal _putchar wrapper
+static inline void _out_char(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  (void)buffer; (void)idx; (void)maxlen;
+  if (character) {
+    _putchar(character);
+  }
+}
+
+
+// internal output function wrapper
+static inline void _out_fct(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  (void)idx; (void)maxlen;
+  if (character) {
+    // buffer is the output fct pointer
+    ((out_fct_wrap_type*)buffer)->fct(character, ((out_fct_wrap_type*)buffer)->arg);
+  }
+}
+
+
+// internal secure strlen
+// \return The length of the string (excluding the terminating 0) limited by 'maxsize'
+static inline unsigned int _strnlen_s(const char* str, size_t maxsize)
+{
+  const char* s;
+  for (s = str; *s && maxsize--; ++s);
+  return (unsigned int)(s - str);
+}
+
+
+// internal test if char is a digit (0-9)
+// \return true if char is a digit
+static inline bool _is_digit(char ch)
+{
+  return (ch >= '0') && (ch <= '9');
+}
+
+
+// internal ASCII string to unsigned int conversion
+static unsigned int _atoi(const char** str)
+{
+  unsigned int i = 0U;
+  while (_is_digit(**str)) {
+    i = i * 10U + (unsigned int)(*((*str)++) - '0');
+  }
+  return i;
+}
+
+
+// output the specified string in reverse, taking care of any zero-padding
+static size_t _out_rev(out_fct_type out, char* buffer, size_t idx, size_t maxlen, const char* buf, size_t len, unsigned int width, unsigned int flags)
+{
+  const size_t start_idx = idx;
+
+  // pad spaces up to given width
+  if (!(flags & FLAGS_LEFT) && !(flags & FLAGS_ZEROPAD)) {
+    for (size_t i = len; i < width; i++) {
+      out(' ', buffer, idx++, maxlen);
+    }
+  }
+
+  // reverse string
+  while (len) {
+    out(buf[--len], buffer, idx++, maxlen);
+  }
+
+  // append pad spaces up to given width
+  if (flags & FLAGS_LEFT) {
+    while (idx - start_idx < width) {
+      out(' ', buffer, idx++, maxlen);
+    }
+  }
+
+  return idx;
+}
+
+
+// internal itoa format
+static size_t _ntoa_format(out_fct_type out, char* buffer, size_t idx, size_t maxlen, char* buf, size_t len, bool negative, unsigned int base, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  // pad leading zeros
+  if (!(flags & FLAGS_LEFT)) {
+    if (width && (flags & FLAGS_ZEROPAD) && (negative || (flags & (FLAGS_PLUS | FLAGS_SPACE)))) {
+      width--;
+    }
+    while ((len < prec) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = '0';
+    }
+    while ((flags & FLAGS_ZEROPAD) && (len < width) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = '0';
+    }
+  }
+
+  // handle hash
+  if (flags & FLAGS_HASH) {
+    if (!(flags & FLAGS_PRECISION) && len && ((len == prec) || (len == width))) {
+      len--;
+      if (len && (base == 16U)) {
+        len--;
+      }
+    }
+    if ((base == 16U) && !(flags & FLAGS_UPPERCASE) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = 'x';
+    }
+    else if ((base == 16U) && (flags & FLAGS_UPPERCASE) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = 'X';
+    }
+    else if ((base == 2U) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = 'b';
+    }
+    if (len < PRINTF_NTOA_BUFFER_SIZE) {
+      buf[len++] = '0';
+    }
+  }
+
+  if (len < PRINTF_NTOA_BUFFER_SIZE) {
+    if (negative) {
+      buf[len++] = '-';
+    }
+    else if (flags & FLAGS_PLUS) {
+      buf[len++] = '+';  // ignore the space if the '+' exists
+    }
+    else if (flags & FLAGS_SPACE) {
+      buf[len++] = ' ';
+    }
+  }
+
+  return _out_rev(out, buffer, idx, maxlen, buf, len, width, flags);
+}
+
+
+// internal itoa for 'long' type
+static size_t _ntoa_long(out_fct_type out, char* buffer, size_t idx, size_t maxlen, unsigned long value, bool negative, unsigned long base, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  char buf[PRINTF_NTOA_BUFFER_SIZE];
+  size_t len = 0U;
+
+  // no hash for 0 values
+  if (!value) {
+    flags &= ~FLAGS_HASH;
+  }
+
+  // write if precision != 0 and value is != 0
+  if (!(flags & FLAGS_PRECISION) || value) {
+    do {
+      const char digit = (char)(value % base);
+      buf[len++] = digit < 10 ? '0' + digit : (flags & FLAGS_UPPERCASE ? 'A' : 'a') + digit - 10;
+      value /= base;
+    } while (value && (len < PRINTF_NTOA_BUFFER_SIZE));
+  }
+
+  return _ntoa_format(out, buffer, idx, maxlen, buf, len, negative, (unsigned int)base, prec, width, flags);
+}
+
+
+// internal itoa for 'long long' type
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+static size_t _ntoa_long_long(out_fct_type out, char* buffer, size_t idx, size_t maxlen, unsigned long long value, bool negative, unsigned long long base, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  char buf[PRINTF_NTOA_BUFFER_SIZE];
+  size_t len = 0U;
+
+  // no hash for 0 values
+  if (!value) {
+    flags &= ~FLAGS_HASH;
+  }
+
+  // write if precision != 0 and value is != 0
+  if (!(flags & FLAGS_PRECISION) || value) {
+    do {
+      const char digit = (char)(value % base);
+      buf[len++] = digit < 10 ? '0' + digit : (flags & FLAGS_UPPERCASE ? 'A' : 'a') + digit - 10;
+      value /= base;
+    } while (value && (len < PRINTF_NTOA_BUFFER_SIZE));
+  }
+
+  return _ntoa_format(out, buffer, idx, maxlen, buf, len, negative, (unsigned int)base, prec, width, flags);
+}
+#endif  // PRINTF_SUPPORT_LONG_LONG
+
+
+#if defined(PRINTF_SUPPORT_FLOAT)
+
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+// forward declaration so that _ftoa can switch to exp notation for values > PRINTF_MAX_FLOAT
+static size_t _etoa(out_fct_type out, char* buffer, size_t idx, size_t maxlen, double value, unsigned int prec, unsigned int width, unsigned int flags);
+#endif
+
+
+// internal ftoa for fixed decimal floating point
+static size_t _ftoa(out_fct_type out, char* buffer, size_t idx, size_t maxlen, double value, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  char buf[PRINTF_FTOA_BUFFER_SIZE];
+  size_t len  = 0U;
+  double diff = 0.0;
+
+  // powers of 10
+  static const double pow10[] = { 1, 10, 100, 1000, 10000, 100000, 1000000, 10000000, 100000000, 1000000000 };
+
+  // test for special values
+  if (value != value)
+    return _out_rev(out, buffer, idx, maxlen, "nan", 3, width, flags);
+  if (value < -DBL_MAX)
+    return _out_rev(out, buffer, idx, maxlen, "fni-", 4, width, flags);
+  if (value > DBL_MAX)
+    return _out_rev(out, buffer, idx, maxlen, (flags & FLAGS_PLUS) ? "fni+" : "fni", (flags & FLAGS_PLUS) ? 4U : 3U, width, flags);
+
+  // test for very large values
+  // standard printf behavior is to print EVERY whole number digit -- which could be 100s of characters overflowing your buffers == bad
+  if ((value > PRINTF_MAX_FLOAT) || (value < -PRINTF_MAX_FLOAT)) {
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+    return _etoa(out, buffer, idx, maxlen, value, prec, width, flags);
+#else
+    return 0U;
+#endif
+  }
+
+  // test for negative
+  bool negative = false;
+  if (value < 0) {
+    negative = true;
+    value = 0 - value;
+  }
+
+  // set default precision, if not set explicitly
+  if (!(flags & FLAGS_PRECISION)) {
+    prec = PRINTF_DEFAULT_FLOAT_PRECISION;
+  }
+  // limit precision to 9, cause a prec >= 10 can lead to overflow errors
+  while ((len < PRINTF_FTOA_BUFFER_SIZE) && (prec > 9U)) {
+    buf[len++] = '0';
+    prec--;
+  }
+
+  int whole = (int)value;
+  double tmp = (value - whole) * pow10[prec];
+  unsigned long frac = (unsigned long)tmp;
+  diff = tmp - frac;
+
+  if (diff > 0.5) {
+    ++frac;
+    // handle rollover, e.g. case 0.99 with prec 1 is 1.0
+    if (frac >= pow10[prec]) {
+      frac = 0;
+      ++whole;
+    }
+  }
+  else if (diff < 0.5) {
+  }
+  else if ((frac == 0U) || (frac & 1U)) {
+    // if halfway, round up if odd OR if last digit is 0
+    ++frac;
+  }
+
+  if (prec == 0U) {
+    diff = value - (double)whole;
+    if ((!(diff < 0.5) || (diff > 0.5)) && (whole & 1)) {
+      // exactly 0.5 and ODD, then round up
+      // 1.5 -> 2, but 2.5 -> 2
+      ++whole;
+    }
+  }
+  else {
+    unsigned int count = prec;
+    // now do fractional part, as an unsigned number
+    while (len < PRINTF_FTOA_BUFFER_SIZE) {
+      --count;
+      buf[len++] = (char)(48U + (frac % 10U));
+      if (!(frac /= 10U)) {
+        break;
+      }
+    }
+    // add extra 0s
+    while ((len < PRINTF_FTOA_BUFFER_SIZE) && (count-- > 0U)) {
+      buf[len++] = '0';
+    }
+    if (len < PRINTF_FTOA_BUFFER_SIZE) {
+      // add decimal
+      buf[len++] = '.';
+    }
+  }
+
+  // do whole part, number is reversed
+  while (len < PRINTF_FTOA_BUFFER_SIZE) {
+    buf[len++] = (char)(48 + (whole % 10));
+    if (!(whole /= 10)) {
+      break;
+    }
+  }
+
+  // pad leading zeros
+  if (!(flags & FLAGS_LEFT) && (flags & FLAGS_ZEROPAD)) {
+    if (width && (negative || (flags & (FLAGS_PLUS | FLAGS_SPACE)))) {
+      width--;
+    }
+    while ((len < width) && (len < PRINTF_FTOA_BUFFER_SIZE)) {
+      buf[len++] = '0';
+    }
+  }
+
+  if (len < PRINTF_FTOA_BUFFER_SIZE) {
+    if (negative) {
+      buf[len++] = '-';
+    }
+    else if (flags & FLAGS_PLUS) {
+      buf[len++] = '+';  // ignore the space if the '+' exists
+    }
+    else if (flags & FLAGS_SPACE) {
+      buf[len++] = ' ';
+    }
+  }
+
+  return _out_rev(out, buffer, idx, maxlen, buf, len, width, flags);
+}
+
+
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+// internal ftoa variant for exponential floating-point type, contributed by Martijn Jasperse <m.jasperse@gmail.com>
+static size_t _etoa(out_fct_type out, char* buffer, size_t idx, size_t maxlen, double value, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  // check for NaN and special values
+  if ((value != value) || (value > DBL_MAX) || (value < -DBL_MAX)) {
+    return _ftoa(out, buffer, idx, maxlen, value, prec, width, flags);
+  }
+
+  // determine the sign
+  const bool negative = value < 0;
+  if (negative) {
+    value = -value;
+  }
+
+  // default precision
+  if (!(flags & FLAGS_PRECISION)) {
+    prec = PRINTF_DEFAULT_FLOAT_PRECISION;
+  }
+
+  // determine the decimal exponent
+  // based on the algorithm by David Gay (https://www.ampl.com/netlib/fp/dtoa.c)
+  union {
+    uint64_t U;
+    double   F;
+  } conv;
+
+  conv.F = value;
+  int exp2 = (int)((conv.U >> 52U) & 0x07FFU) - 1023;           // effectively log2
+  conv.U = (conv.U & ((1ULL << 52U) - 1U)) | (1023ULL << 52U);  // drop the exponent so conv.F is now in [1,2)
+  // now approximate log10 from the log2 integer part and an expansion of ln around 1.5
+  int expval = (int)(0.1760912590558 + exp2 * 0.301029995663981 + (conv.F - 1.5) * 0.289529654602168);
+  // now we want to compute 10^expval but we want to be sure it won't overflow
+  exp2 = (int)(expval * 3.321928094887362 + 0.5);
+  const double z  = expval * 2.302585092994046 - exp2 * 0.6931471805599453;
+  const double z2 = z * z;
+  conv.U = (uint64_t)(exp2 + 1023) << 52U;
+  // compute exp(z) using continued fractions, see https://en.wikipedia.org/wiki/Exponential_function#Continued_fractions_for_ex
+  conv.F *= 1 + 2 * z / (2 - z + (z2 / (6 + (z2 / (10 + z2 / 14)))));
+  // correct for rounding errors
+  if (value < conv.F) {
+    expval--;
+    conv.F /= 10;
+  }
+
+  // the exponent format is "%+03d" and largest value is "307", so set aside 4-5 characters
+  unsigned int minwidth = ((expval < 100) && (expval > -100)) ? 4U : 5U;
+
+  // in "%g" mode, "prec" is the number of *significant figures* not decimals
+  if (flags & FLAGS_ADAPT_EXP) {
+    // do we want to fall-back to "%f" mode?
+    if ((value >= 1e-4) && (value < 1e6)) {
+      if ((int)prec > expval) {
+        prec = (unsigned)((int)prec - expval - 1);
+      }
+      else {
+        prec = 0;
+      }
+      flags |= FLAGS_PRECISION;   // make sure _ftoa respects precision
+      // no characters in exponent
+      minwidth = 0U;
+      expval   = 0;
+    }
+    else {
+      // we use one sigfig for the whole part
+      if ((prec > 0) && (flags & FLAGS_PRECISION)) {
+        --prec;
+      }
+    }
+  }
+
+  // will everything fit?
+  unsigned int fwidth = width;
+  if (width > minwidth) {
+    // we didn't fall-back so subtract the characters required for the exponent
+    fwidth -= minwidth;
+  } else {
+    // not enough characters, so go back to default sizing
+    fwidth = 0U;
+  }
+  if ((flags & FLAGS_LEFT) && minwidth) {
+    // if we're padding on the right, DON'T pad the floating part
+    fwidth = 0U;
+  }
+
+  // rescale the float value
+  if (expval) {
+    value /= conv.F;
+  }
+
+  // output the floating part
+  const size_t start_idx = idx;
+  idx = _ftoa(out, buffer, idx, maxlen, negative ? -value : value, prec, fwidth, flags & ~FLAGS_ADAPT_EXP);
+
+  // output the exponent part
+  if (minwidth) {
+    // output the exponential symbol
+    out((flags & FLAGS_UPPERCASE) ? 'E' : 'e', buffer, idx++, maxlen);
+    // output the exponent value
+    idx = _ntoa_long(out, buffer, idx, maxlen, (expval < 0) ? -expval : expval, expval < 0, 10, 0, minwidth-1, FLAGS_ZEROPAD | FLAGS_PLUS);
+    // might need to right-pad spaces
+    if (flags & FLAGS_LEFT) {
+      while (idx - start_idx < width) out(' ', buffer, idx++, maxlen);
+    }
+  }
+  return idx;
+}
+#endif  // PRINTF_SUPPORT_EXPONENTIAL
+#endif  // PRINTF_SUPPORT_FLOAT
+
+
+// internal vsnprintf
+static int _vsnprintf(out_fct_type out, char* buffer, const size_t maxlen, const char* format, va_list va)
+{
+  unsigned int flags, width, precision, n;
+  size_t idx = 0U;
+
+  if (!buffer) {
+    // use null output function
+    out = _out_null;
+  }
+
+  while (*format)
+  {
+    // format specifier?  %[flags][width][.precision][length]
+    if (*format != '%') {
+      // no
+      out(*format, buffer, idx++, maxlen);
+      format++;
+      continue;
+    }
+    else {
+      // yes, evaluate it
+      format++;
+    }
+
+    // evaluate flags
+    flags = 0U;
+    do {
+      switch (*format) {
+        case '0': flags |= FLAGS_ZEROPAD; format++; n = 1U; break;
+        case '-': flags |= FLAGS_LEFT;    format++; n = 1U; break;
+        case '+': flags |= FLAGS_PLUS;    format++; n = 1U; break;
+        case ' ': flags |= FLAGS_SPACE;   format++; n = 1U; break;
+        case '#': flags |= FLAGS_HASH;    format++; n = 1U; break;
+        default :                                   n = 0U; break;
+      }
+    } while (n);
+
+    // evaluate width field
+    width = 0U;
+    if (_is_digit(*format)) {
+      width = _atoi(&format);
+    }
+    else if (*format == '*') {
+      const int w = va_arg(va, int);
+      if (w < 0) {
+        flags |= FLAGS_LEFT;    // reverse padding
+        width = (unsigned int)-w;
+      }
+      else {
+        width = (unsigned int)w;
+      }
+      format++;
+    }
+
+    // evaluate precision field
+    precision = 0U;
+    if (*format == '.') {
+      flags |= FLAGS_PRECISION;
+      format++;
+      if (_is_digit(*format)) {
+        precision = _atoi(&format);
+      }
+      else if (*format == '*') {
+        const int prec = (int)va_arg(va, int);
+        precision = prec > 0 ? (unsigned int)prec : 0U;
+        format++;
+      }
+    }
+
+    // evaluate length field
+    switch (*format) {
+      case 'l' :
+        flags |= FLAGS_LONG;
+        format++;
+        if (*format == 'l') {
+          flags |= FLAGS_LONG_LONG;
+          format++;
+        }
+        break;
+      case 'h' :
+        flags |= FLAGS_SHORT;
+        format++;
+        if (*format == 'h') {
+          flags |= FLAGS_CHAR;
+          format++;
+        }
+        break;
+#if defined(PRINTF_SUPPORT_PTRDIFF_T)
+      case 't' :
+        flags |= (sizeof(ptrdiff_t) == sizeof(long) ? FLAGS_LONG : FLAGS_LONG_LONG);
+        format++;
+        break;
+#endif
+      case 'j' :
+        flags |= (sizeof(intmax_t) == sizeof(long) ? FLAGS_LONG : FLAGS_LONG_LONG);
+        format++;
+        break;
+      case 'z' :
+        flags |= (sizeof(size_t) == sizeof(long) ? FLAGS_LONG : FLAGS_LONG_LONG);
+        format++;
+        break;
+      default :
+        break;
+    }
+
+    // evaluate specifier
+    switch (*format) {
+      case 'd' :
+      case 'i' :
+      case 'u' :
+      case 'x' :
+      case 'X' :
+      case 'o' :
+      case 'b' : {
+        // set the base
+        unsigned int base;
+        if (*format == 'x' || *format == 'X') {
+          base = 16U;
+        }
+        else if (*format == 'o') {
+          base =  8U;
+        }
+        else if (*format == 'b') {
+          base =  2U;
+        }
+        else {
+          base = 10U;
+          flags &= ~FLAGS_HASH;   // no hash for dec format
+        }
+        // uppercase
+        if (*format == 'X') {
+          flags |= FLAGS_UPPERCASE;
+        }
+
+        // no plus or space flag for u, x, X, o, b
+        if ((*format != 'i') && (*format != 'd')) {
+          flags &= ~(FLAGS_PLUS | FLAGS_SPACE);
+        }
+
+        // ignore '0' flag when precision is given
+        if (flags & FLAGS_PRECISION) {
+          flags &= ~FLAGS_ZEROPAD;
+        }
+
+        // convert the integer
+        if ((*format == 'i') || (*format == 'd')) {
+          // signed
+          if (flags & FLAGS_LONG_LONG) {
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+            const long long value = va_arg(va, long long);
+            idx = _ntoa_long_long(out, buffer, idx, maxlen, (unsigned long long)(value > 0 ? value : 0 - value), value < 0, base, precision, width, flags);
+#endif
+          }
+          else if (flags & FLAGS_LONG) {
+            const long value = va_arg(va, long);
+            idx = _ntoa_long(out, buffer, idx, maxlen, (unsigned long)(value > 0 ? value : 0 - value), value < 0, base, precision, width, flags);
+          }
+          else {
+            const int value = (flags & FLAGS_CHAR) ? (char)va_arg(va, int) : (flags & FLAGS_SHORT) ? (short int)va_arg(va, int) : va_arg(va, int);
+            idx = _ntoa_long(out, buffer, idx, maxlen, (unsigned int)(value > 0 ? value : 0 - value), value < 0, base, precision, width, flags);
+          }
+        }
+        else {
+          // unsigned
+          if (flags & FLAGS_LONG_LONG) {
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+            idx = _ntoa_long_long(out, buffer, idx, maxlen, va_arg(va, unsigned long long), false, base, precision, width, flags);
+#endif
+          }
+          else if (flags & FLAGS_LONG) {
+            idx = _ntoa_long(out, buffer, idx, maxlen, va_arg(va, unsigned long), false, base, precision, width, flags);
+          }
+          else {
+            const unsigned int value = (flags & FLAGS_CHAR) ? (unsigned char)va_arg(va, unsigned int) : (flags & FLAGS_SHORT) ? (unsigned short int)va_arg(va, unsigned int) : va_arg(va, unsigned int);
+            idx = _ntoa_long(out, buffer, idx, maxlen, value, false, base, precision, width, flags);
+          }
+        }
+        format++;
+        break;
+      }
+#if defined(PRINTF_SUPPORT_FLOAT)
+      case 'f' :
+      case 'F' :
+        if (*format == 'F') flags |= FLAGS_UPPERCASE;
+        idx = _ftoa(out, buffer, idx, maxlen, va_arg(va, double), precision, width, flags);
+        format++;
+        break;
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+      case 'e':
+      case 'E':
+      case 'g':
+      case 'G':
+        if ((*format == 'g')||(*format == 'G')) flags |= FLAGS_ADAPT_EXP;
+        if ((*format == 'E')||(*format == 'G')) flags |= FLAGS_UPPERCASE;
+        idx = _etoa(out, buffer, idx, maxlen, va_arg(va, double), precision, width, flags);
+        format++;
+        break;
+#endif  // PRINTF_SUPPORT_EXPONENTIAL
+#endif  // PRINTF_SUPPORT_FLOAT
+      case 'c' : {
+        unsigned int l = 1U;
+        // pre padding
+        if (!(flags & FLAGS_LEFT)) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        // char output
+        out((char)va_arg(va, int), buffer, idx++, maxlen);
+        // post padding
+        if (flags & FLAGS_LEFT) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        format++;
+        break;
+      }
+
+      case 's' : {
+        const char* p = va_arg(va, char*);
+        unsigned int l = _strnlen_s(p, precision ? precision : (size_t)-1);
+        // pre padding
+        if (flags & FLAGS_PRECISION) {
+          l = (l < precision ? l : precision);
+        }
+        if (!(flags & FLAGS_LEFT)) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        // string output
+        while ((*p != 0) && (!(flags & FLAGS_PRECISION) || precision--)) {
+          out(*(p++), buffer, idx++, maxlen);
+        }
+        // post padding
+        if (flags & FLAGS_LEFT) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        format++;
+        break;
+      }
+
+      case 'p' : {
+        width = sizeof(void*) * 2U;
+        flags |= FLAGS_ZEROPAD | FLAGS_UPPERCASE;
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+        const bool is_ll = sizeof(uintptr_t) == sizeof(long long);
+        if (is_ll) {
+          idx = _ntoa_long_long(out, buffer, idx, maxlen, (uintptr_t)va_arg(va, void*), false, 16U, precision, width, flags);
+        }
+        else {
+#endif
+          idx = _ntoa_long(out, buffer, idx, maxlen, (unsigned long)((uintptr_t)va_arg(va, void*)), false, 16U, precision, width, flags);
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+        }
+#endif
+        format++;
+        break;
+      }
+
+      case '%' :
+        out('%', buffer, idx++, maxlen);
+        format++;
+        break;
+
+      default :
+        out(*format, buffer, idx++, maxlen);
+        format++;
+        break;
+    }
+  }
+
+  // termination
+  out((char)0, buffer, idx < maxlen ? idx : maxlen - 1U, maxlen);
+
+  // return written chars without terminating \0
+  return (int)idx;
+}
+
+
+///////////////////////////////////////////////////////////////////////////////
+
+int printf_(const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  char buffer[1];
+  const int ret = _vsnprintf(_out_char, buffer, (size_t)-1, format, va);
+  va_end(va);
+  return ret;
+}
+
+
+int sprintf_(char* buffer, const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  const int ret = _vsnprintf(_out_buffer, buffer, (size_t)-1, format, va);
+  va_end(va);
+  return ret;
+}
+
+
+int snprintf_(char* buffer, size_t count, const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  const int ret = _vsnprintf(_out_buffer, buffer, count, format, va);
+  va_end(va);
+  return ret;
+}
+
+
+int vprintf_(const char* format, va_list va)
+{
+  char buffer[1];
+  return _vsnprintf(_out_char, buffer, (size_t)-1, format, va);
+}
+
+
+int vsnprintf_(char* buffer, size_t count, const char* format, va_list va)
+{
+  return _vsnprintf(_out_buffer, buffer, count, format, va);
+}
+
+
+int fctprintf(void (*out)(char character, void* arg), void* arg, const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  const out_fct_wrap_type out_fct_wrap = { out, arg };
+  const int ret = _vsnprintf(_out_fct, (char*)(uintptr_t)&out_fct_wrap, (size_t)-1, format, va);
+  va_end(va);
+  return ret;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/printf.h

@@ -0,0 +1,117 @@
+///////////////////////////////////////////////////////////////////////////////
+// \author (c) Marco Paland (info@paland.com)
+//             2014-2019, PALANDesign Hannover, Germany
+//
+// \license The MIT License (MIT)
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in
+// all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// THE SOFTWARE.
+//
+// \brief Tiny printf, sprintf and snprintf implementation, optimized for speed on
+//        embedded systems with a very limited resources.
+//        Use this instead of bloated standard/newlib printf.
+//        These routines are thread safe and reentrant.
+//
+///////////////////////////////////////////////////////////////////////////////
+
+#ifndef _PRINTF_H_
+#define _PRINTF_H_
+
+#include <stdarg.h>
+#include <stddef.h>
+
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+
+/**
+ * Output a character to a custom device like UART, used by the printf() function
+ * This function is declared here only. You have to write your custom implementation somewhere
+ * \param character Character to output
+ */
+void _putchar(char character);
+
+
+/**
+ * Tiny printf implementation
+ * You have to implement _putchar if you use printf()
+ * To avoid conflicts with the regular printf() API it is overridden by macro defines
+ * and internal underscore-appended functions like printf_() are used
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are written into the array, not counting the terminating null character
+ */
+#define printf printf_
+int printf_(const char* format, ...);
+
+
+/**
+ * Tiny sprintf implementation
+ * Due to security reasons (buffer overflow) YOU SHOULD CONSIDER USING (V)SNPRINTF INSTEAD!
+ * \param buffer A pointer to the buffer where to store the formatted string. MUST be big enough to store the output!
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are WRITTEN into the buffer, not counting the terminating null character
+ */
+#define sprintf sprintf_
+int sprintf_(char* buffer, const char* format, ...);
+
+
+/**
+ * Tiny snprintf/vsnprintf implementation
+ * \param buffer A pointer to the buffer where to store the formatted string
+ * \param count The maximum number of characters to store in the buffer, including a terminating null character
+ * \param format A string that specifies the format of the output
+ * \param va A value identifying a variable arguments list
+ * \return The number of characters that COULD have been written into the buffer, not counting the terminating
+ *         null character. A value equal or larger than count indicates truncation. Only when the returned value
+ *         is non-negative and less than count, the string has been completely written.
+ */
+#define snprintf  snprintf_
+#define vsnprintf vsnprintf_
+int  snprintf_(char* buffer, size_t count, const char* format, ...);
+int vsnprintf_(char* buffer, size_t count, const char* format, va_list va);
+
+
+/**
+ * Tiny vprintf implementation
+ * \param format A string that specifies the format of the output
+ * \param va A value identifying a variable arguments list
+ * \return The number of characters that are WRITTEN into the buffer, not counting the terminating null character
+ */
+#define vprintf vprintf_
+int vprintf_(const char* format, va_list va);
+
+
+/**
+ * printf with output function
+ * You may use this as dynamic alternative to printf() with its fixed _putchar() output
+ * \param out An output function which takes one character and an argument pointer
+ * \param arg An argument pointer for user data passed to output function
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are sent to the output function, not counting the terminating null character
+ */
+int fctprintf(void (*out)(char character, void* arg), void* arg, const char* format, ...);
+
+
+#ifdef __cplusplus
+}
+#endif
+
+
+#endif  // _PRINTF_H_

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/wordle.h

@@ -0,0 +1,8 @@
+#define NUM_TRIES 5
+#define WORD_LENGTH 5
+
+enum character_state {
+    CORRECT_PLACEMENT = 0, // Correct character, in the correct index of the word.
+    INCORRECT_PLACEMENT = 1, // Correct character, in the incorrect index of the word.
+    INCORRECT = 2, // Character does not appear in the word.
+};

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/serial_server.c

@@ -0,0 +1,80 @@
+#include <stdint.h>
+#include <microkit.h>
+#include "printf.h"
+
+// This variable will have the address of the UART device
+uintptr_t uart_base_vaddr;
+
+#define RHR_MASK 0b111111111
+#define UARTDR 0x000
+#define UARTFR 0x018
+#define UARTIMSC 0x038
+#define UARTICR 0x044
+#define PL011_UARTFR_TXFF (1 << 5)
+#define PL011_UARTFR_RXFE (1 << 4)
+
+#define REG_PTR(base, offset) ((volatile uint32_t *)((base) + (offset)))
+
+void uart_init() {
+    *REG_PTR(uart_base_vaddr, UARTIMSC) = 0x50;
+}
+
+int uart_get_char() {
+    int ch = 0;
+
+    if ((*REG_PTR(uart_base_vaddr, UARTFR) & PL011_UARTFR_RXFE) == 0) {
+        ch = *REG_PTR(uart_base_vaddr, UARTDR) & RHR_MASK;
+    }
+
+    return ch;
+}
+
+void uart_put_char(int ch) {
+    while ((*REG_PTR(uart_base_vaddr, UARTFR) & PL011_UARTFR_TXFF) != 0);
+
+    *REG_PTR(uart_base_vaddr, UARTDR) = ch;
+    if (ch == '\r') {
+        uart_put_char('\n');
+    }
+}
+
+void uart_handle_irq() {
+    *REG_PTR(uart_base_vaddr, UARTICR) = 0x7f0;
+}
+
+void uart_put_str(char *str) {
+    while (*str) {
+        uart_put_char(*str);
+        str++;
+    }
+}
+
+void init(void) {
+    // First we initialise the UART device, which will write to the
+    // device's hardware registers. Which means we need access to
+    // the UART device.
+    uart_init();
+    // After initialising the UART, print a message to the terminal
+    // saying that the serial server has started.
+    uart_put_str("SERIAL SERVER: starting\n");
+}
+
+#define UART_IRQ_CH 1
+#define CLIENT_CH 2
+
+uintptr_t serial_to_client_vaddr;
+uintptr_t client_to_serial_vaddr;
+
+void notified(microkit_channel channel) {
+    switch (channel) {
+        case UART_IRQ_CH:
+            ((char *)serial_to_client_vaddr)[0] = uart_get_char();
+            uart_handle_irq();
+            microkit_irq_ack(channel);
+            microkit_notify(CLIENT_CH);
+            break;
+        case CLIENT_CH:
+            uart_put_str((char *)client_to_serial_vaddr);
+            break;
+    }
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/arch/aarch64/linux.h

@@ -0,0 +1,20 @@
+#include <stdint.h>
+
+// The structure of the kernel image header and the magic value comes from the
+// Linux kernel documentation that can be found here:
+// https://www.kernel.org/doc/Documentation/arm64/booting.txt
+
+#define LINUX_IMAGE_MAGIC 0x644d5241
+
+struct linux_image_header {
+    uint32_t code0;       // Executable code
+    uint32_t code1;       // Executable code
+    uint64_t text_offset; // Image load offset, little endian
+    uint64_t image_size;  // Effective Image size, little endian
+    uint64_t flags;       // kernel flags, little endian
+    uint64_t res2;        // reserved
+    uint64_t res3;        // reserved
+    uint64_t res4;        // reserved
+    uint32_t magic;       // Magic number, little endian, "ARM\x64"
+    uint32_t res5;        // reserved (used for PE COFF offset)
+};

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/fault.c

@@ -0,0 +1,207 @@
+/*
+ * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include "hsr.h"
+#include "util/util.h"
+#include "fault.h"
+
+// #define CPSR_THUMB                 (1 << 5)
+// #define CPSR_IS_THUMB(x)           ((x) & CPSR_THUMB)
+
+// int fault_is_32bit_instruction(seL4_UserContext *regs)
+// {
+//     // @ivanv: assuming VCPU fault
+//     return !CPSR_IS_THUMB(regs->spsr);
+// }
+
+bool fault_advance_vcpu(seL4_UserContext *regs) {
+    // For now we just ignore it and continue
+    // Assume 64-bit instruction
+    regs->pc += 4;
+    int err = seL4_TCB_WriteRegisters(BASE_VM_TCB_CAP + GUEST_ID, true, 0, SEL4_USER_CONTEXT_SIZE, regs);
+    assert(err == seL4_NoError);
+
+    return (err == seL4_NoError);
+}
+
+char *fault_to_string(seL4_Word fault_label) {
+    switch (fault_label) {
+        case seL4_Fault_VMFault: return "virtual memory";
+        case seL4_Fault_UnknownSyscall: return "unknown syscall";
+        case seL4_Fault_UserException: return "user exception";
+        case seL4_Fault_VGICMaintenance: return "VGIC maintenance";
+        case seL4_Fault_VCPUFault: return "VCPU fault";
+        case seL4_Fault_VPPIEvent: return "VPPI event";
+        default: return "unknown fault";
+    }
+}
+
+enum fault_width {
+    WIDTH_DOUBLEWORD = 0,
+    WIDTH_WORD = 1,
+    WIDTH_HALFWORD = 2,
+    WIDTH_BYTE = 3,
+};
+
+static enum fault_width fault_get_width(uint64_t fsr)
+{
+    if (HSR_IS_SYNDROME_VALID(fsr)) {
+        switch (HSR_SYNDROME_WIDTH(fsr)) {
+            case 0: return WIDTH_BYTE;
+            case 1: return WIDTH_HALFWORD;
+            case 2: return WIDTH_WORD;
+            case 3: return WIDTH_DOUBLEWORD;
+            default:
+                // @ivanv: reviist
+                // print_fault(f);
+                assert(0);
+                return 0;
+        }
+    } else {
+        LOG_VMM_ERR("Received invalid FSR: 0x%lx\n", fsr);
+        // @ivanv: reviist
+        // int rt;
+        // rt = decode_instruction(f);
+        // assert(rt >= 0);
+        return -1;
+    }
+}
+
+uint64_t fault_get_data_mask(uint64_t addr, uint64_t fsr)
+{
+    uint64_t mask = 0;
+    switch (fault_get_width(fsr)) {
+        case WIDTH_BYTE:
+            mask = 0x000000ff;
+            assert(!(addr & 0x0));
+            break;
+        case WIDTH_HALFWORD:
+            mask = 0x0000ffff;
+            assert(!(addr & 0x1));
+            break;
+        case WIDTH_WORD:
+            mask = 0xffffffff;
+            assert(!(addr & 0x3));
+            break;
+        case WIDTH_DOUBLEWORD:
+            mask = ~mask;
+            break;
+        default:
+            LOG_VMM_ERR("unknown width: 0x%lx, from FSR: 0x%lx, addr: 0x%lx\n",
+                fault_get_width(fsr), fsr, addr);
+            assert(0);
+            return 0;
+    }
+    mask <<= (addr & 0x3) * 8;
+    return mask;
+}
+
+static uint64_t wzr = 0;
+uint64_t *decode_rt(uint64_t reg, seL4_UserContext *regs)
+{
+    switch (reg) {
+        case 0: return &regs->x0;
+        case 1: return &regs->x1;
+        case 2: return &regs->x2;
+        case 3: return &regs->x3;
+        case 4: return &regs->x4;
+        case 5: return &regs->x5;
+        case 6: return &regs->x6;
+        case 7: return &regs->x7;
+        case 8: return &regs->x8;
+        case 9: return &regs->x9;
+        case 10: return &regs->x10;
+        case 11: return &regs->x11;
+        case 12: return &regs->x12;
+        case 13: return &regs->x13;
+        case 14: return &regs->x14;
+        case 15: return &regs->x15;
+        case 16: return &regs->x16;
+        case 17: return &regs->x17;
+        case 18: return &regs->x18;
+        case 19: return &regs->x19;
+        case 20: return &regs->x20;
+        case 21: return &regs->x21;
+        case 22: return &regs->x22;
+        case 23: return &regs->x23;
+        case 24: return &regs->x24;
+        case 25: return &regs->x25;
+        case 26: return &regs->x26;
+        case 27: return &regs->x27;
+        case 28: return &regs->x28;
+        case 29: return &regs->x29;
+        case 30: return &regs->x30;
+        case 31: return &wzr;
+        default:
+            printf("invalid reg %d\n", reg);
+            assert(!"Invalid register");
+            return NULL;
+    }
+}
+
+bool fault_is_write(uint64_t fsr)
+{
+    return (fsr & (1U << 6)) != 0;
+}
+
+bool fault_is_read(uint64_t fsr)
+{
+    return !fault_is_write(fsr);
+}
+
+static int get_rt(uint64_t fsr)
+{
+
+    int rt = -1;
+    if (HSR_IS_SYNDROME_VALID(fsr)) {
+        rt = HSR_SYNDROME_RT(fsr);
+    } else {
+        printf("decode_insturction for arm64 not implemented\n");
+        assert(0);
+        // @ivanv: implement decode instruction for aarch64
+        // rt = decode_instruction(f);
+    }
+    assert(rt >= 0);
+    return rt;
+}
+
+uint64_t fault_get_data(seL4_UserContext *regs, uint64_t fsr)
+{
+    /* Get register opearand */
+    int rt  = get_rt(fsr);
+
+    uint64_t data = *decode_rt(rt, regs);
+
+    return data;
+}
+
+uint64_t fault_emulate(seL4_UserContext *regs, uint64_t reg, uint64_t addr, uint64_t fsr, uint64_t reg_val)
+{
+    uint64_t m, s;
+    s = (addr & 0x3) * 8;
+    m = fault_get_data_mask(addr, fsr);
+    if (fault_is_read(fsr)) {
+        /* Read data must be shifted to lsb */
+        return (reg & ~(m >> s)) | ((reg_val & m) >> s);
+    } else {
+        /* Data to write must be shifted left to compensate for alignment */
+        return (reg & ~m) | ((reg_val << s) & m);
+    }
+}
+
+bool fault_advance(seL4_UserContext *regs, uint64_t addr, uint64_t fsr, uint64_t reg_val)
+{
+    /* Get register opearand */
+    int rt = get_rt(fsr);
+
+    uint64_t *reg_ctx = decode_rt(rt, regs);
+    *reg_ctx = fault_emulate(regs, *reg_ctx, addr, fsr, reg_val);
+    // DFAULT("%s: Emulate fault @ 0x%x from PC 0x%x\n",
+    //        fault->vcpu->vm->vm_name, fault->addr, fault->ip);
+
+    return fault_advance_vcpu(regs);
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/fault.h

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <stdbool.h>
+#include <stdint.h>
+#include <microkit.h>
+
+bool fault_advance_vcpu(seL4_UserContext *regs);
+bool fault_advance(seL4_UserContext *regs, uint64_t addr, uint64_t fsr, uint64_t reg_val);
+uint64_t fault_get_data_mask(uint64_t addr, uint64_t fsr);
+uint64_t fault_get_data(seL4_UserContext *regs, uint64_t fsr);
+uint64_t fault_emulate(seL4_UserContext *regs, uint64_t reg, uint64_t addr, uint64_t fsr, uint64_t reg_val);
+
+/* Take the fault label given by the kernel and convert it to a string. */
+char *fault_to_string(seL4_Word fault_label);
+
+bool fault_is_write(uint64_t fsr);
+bool fault_is_read(uint64_t fsr);

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/global_data.S

@@ -0,0 +1,27 @@
+/* @ivanv: need to consider the case where not all of these are used! */
+/* @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(VM_KERNEL_IMAGE_PATH)
+.section .guest_kernel_image, "aw", @progbits
+.global _guest_kernel_image, _guest_kernel_image_end
+_guest_kernel_image:
+.incbin VM_KERNEL_IMAGE_PATH
+_guest_kernel_image_end:
+#endif
+
+#if defined(VM_DTB_IMAGE_PATH)
+.section .guest_dtb_image, "aw", @progbits
+.global _guest_dtb_image, _guest_dtb_image_end
+_guest_dtb_image:
+.incbin VM_DTB_IMAGE_PATH
+_guest_dtb_image_end:
+#endif
+
+#if defined(VM_INITRD_IMAGE_PATH)
+.section .guest_initrd_image, "aw", @progbits
+.global _guest_initrd_image, _guest_initrd_image_end
+_guest_initrd_image:
+.incbin VM_INITRD_IMAGE_PATH
+_guest_initrd_image_end:
+#endif

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/hsr.h

@@ -0,0 +1,50 @@
+// @ivanv, where do these come from?
+// @ivanv: license
+#define HSR_EXCEPTION_CLASS_SHIFT   (26)
+#define HSR_EXCEPTION_CLASS_MASK    (HSR_MAX_EXCEPTION << HSR_EXCEPTION_CLASS_SHIFT)
+#define HSR_EXCEPTION_CLASS(hsr)    (((hsr) & HSR_EXCEPTION_CLASS_MASK) >> HSR_EXCEPTION_CLASS_SHIFT)
+
+#define HSR_SYNDROME_VALID         (1 << 24)
+#define HSR_IS_SYNDROME_VALID(hsr) ((hsr) & HSR_SYNDROME_VALID)
+#define HSR_SYNDROME_WIDTH(x)      (((x) >> 22) & 0x3)
+#define HSR_SYNDROME_RT(x)         (((x) >> 16) & 0x1f)
+
+/* HSR Exception Value */
+#define HSR_UNKNOWN_EXCEPTION       (0x0)
+#define HSR_WFx_EXCEPTION           (0x1)
+#define HSR_CP15_32_EXCEPTION       (0x3)
+#define HSR_CP15_64_EXCEPTION       (0x4)
+#define HSR_CP14_32_EXCEPTION       (0x5)
+#define HSR_CP14_LC_32_EXCEPTION    (0x6)
+#define HSR_SIMD_EXCEPTION          (0x7)
+#define HSR_CP10_EXCEPTION          (0x8)
+#define HSR_CP14_EXCEPTION          (0xC)
+#define HSR_ILLEGAL_EXCEPTION       (0xE)
+#define HSR_SVC_32_EXCEPTION        (0x11)
+#define HSR_HVC_32_EXCEPTION        (0x12)
+#define HSR_SMC_32_EXCEPTION        (0x13)
+#define HSR_SVC_64_EXCEPTION        (0x15)
+#define HSR_HVC_64_EXCEPTION        (0x16)
+#define HSR_SMC_64_EXCEPTION        (0x17)
+#define HSR_SYSREG_64_EXCEPTION     (0x18)
+#define HSR_IMPL_DEF_EXCEPTION      (0x1f)
+#define HSR_IABT_LOW_EXCEPTION      (0x20)
+#define HSR_IABT_CURR_EXCEPTION     (0x21)
+#define HSR_PC_ALIGN_EXCEPTION      (0x22)
+#define HSR_DABT_LOW_EXCEPTION      (0x24)
+#define HSR_DABT_CUR_EXCEPTION      (0x25)
+#define HSR_SP_ALIGN_EXCEPTION      (0x26)
+#define HSR_FP32_EXCEPTION          (0x28)
+#define HSR_FP64_EXCEPTION          (0x2C)
+#define HSR_SERROR_EXCEPTION        (0x2F)
+#define HSR_BRK_LOW_EXCEPTION       (0x30)
+#define HSR_BRK_CUR_EXCEPTION       (0x31)
+#define HSR_SWSTEP_LOW_EXCEPTION    (0x32)
+#define HSR_SWSTEP_CUR_EXCEPTION    (0x33)
+#define HSR_WATCHPT_LOW_EXCEPTION   (0x34)
+#define HSR_WATCHPT_CUR_EXCEPTION   (0x35)
+#define HSR_SWBRK_32_EXCEPTION      (0x38)
+#define HSW_VECTOR_32_EXCEPTION     (0x3a)
+#define HSR_SWBRK_64_EXCEPTION      (0x3c)
+/* Remaining values (0x3d - 0x3f) are reserved */
+#define HSR_MAX_EXCEPTION           (0x3f)

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/psci.c

@@ -0,0 +1,84 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <stdbool.h>
+#include "psci.h"
+#include "smc.h"
+#include "fault.h"
+#include "util/util.h"
+#include "vmm.h"
+
+bool handle_psci(uint64_t vcpu_id, seL4_UserContext *regs, uint64_t fn_number, uint32_t hsr)
+{
+    // @ivanv: write a note about what convention we assume, should we be checking
+    // the convention?
+    switch (fn_number) {
+        case PSCI_VERSION: {
+            /* We support PSCI version 1.2 */
+            uint32_t version = PSCI_MAJOR_VERSION(1) | PSCI_MINOR_VERSION(2);
+            smc_set_return_value(regs, version);
+            break;
+        }
+        case PSCI_CPU_ON: {
+            uintptr_t target_cpu = smc_get_arg(regs, 1);
+            // Right now we only have one vCPU and so any fault for a target vCPU
+            // that isn't the one that's already on we consider an error on the
+            // guest's side.
+            // @ivanv: adapt for starting other vCPUs
+            if (target_cpu == vcpu_id) {
+                smc_set_return_value(regs, PSCI_ALREADY_ON);
+            } else {
+                // The guest has requested to turn on a virtual CPU that does
+                // not exist.
+                smc_set_return_value(regs, PSCI_INVALID_PARAMETERS);
+            }
+            break;
+        }
+        case PSCI_MIGRATE_INFO_TYPE:
+            /*
+             * There are multiple possible return values for MIGRATE_INFO_TYPE.
+             * In this case returning 2 will tell the guest that this is a
+             * system that does not use a "Trusted OS" as the PSCI
+             * specification says.
+             */
+            smc_set_return_value(regs, 2);
+            break;
+        case PSCI_FEATURES:
+            // @ivanv: seems weird that we just return nothing here.
+            smc_set_return_value(regs, PSCI_NOT_SUPPORTED);
+            break;
+        case PSCI_SYSTEM_RESET: {
+            bool success = guest_restart();
+            if (!success) {
+                LOG_VMM_ERR("Failed to restart guest\n");
+                smc_set_return_value(regs, PSCI_INTERNAL_FAILURE);
+            } else {
+                /*
+                 * If we've successfully restarted the guest, all we want to do
+                 * is reply to the fault that caused us to handle the PSCI call
+                 * so that the guest can continue executing. We do not need to
+                 * advance the vCPU program counter as we typically do when
+                 * handling a fault since the correct PC has been set when we
+                 * call guest_restart().
+                 */
+                return true;
+            }
+            break;
+        }
+        case PSCI_SYSTEM_OFF:
+            guest_stop();
+            return true;
+        default:
+            LOG_VMM_ERR("Unhandled PSCI function ID 0x%lx\n", fn_number);
+            return false;
+    }
+
+    bool success = fault_advance_vcpu(regs);
+    assert(success);
+
+    return success;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/psci.h

@@ -0,0 +1,63 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ */
+
+#include <microkit.h>
+#include <stdint.h>
+
+/* Values in this file are taken from the:
+ * ARM Power State Coordination Interface
+ * Platform Design Document
+ * Issue E (PSCI version 1.2)
+ */
+
+/*
+ * The PSCI version is represented by a 32-bit unsigned integer.
+ * The upper 15 bits represent the major version.
+ * The lower 16 bits represent the minor version.
+*/
+#define PSCI_MAJOR_VERSION(v) ((v) << 16)
+#define PSCI_MINOR_VERSION(v) ((v) & ((1 << 16) - 1))
+
+/* PSCI return codes */
+#define PSCI_SUCCESS 0
+#define PSCI_NOT_SUPPORTED -1
+#define PSCI_INVALID_PARAMETERS -2
+#define PSCI_DENIED -3
+#define PSCI_ALREADY_ON -4
+#define PSCI_ON_PENDING -5
+#define PSCI_INTERNAL_FAILURE -6
+#define PSCI_NOT_PRESENT -7
+#define PSCI_DISABLED -8
+#define PSCI_INVALID_ADDRESS -9
+
+/* PSCI function IDs */
+typedef enum psci {
+    PSCI_VERSION = 0x0,
+    PSCI_CPU_SUSPEND = 0x1,
+    PSCI_CPU_OFF = 0x2,
+    PSCI_CPU_ON = 0x3,
+    PSCI_AFFINTY_INFO = 0x4,
+    PSCI_MIGRATE = 0x5,
+    PSCI_MIGRATE_INFO_TYPE = 0x6,
+    PSCI_MIGRATE_INFO_UP_CPU = 0x7,
+    PSCI_SYSTEM_OFF = 0x8,
+    PSCI_SYSTEM_RESET = 0x9,
+    PSCI_FEATURES = 0xa,
+    PSCI_CPU_FREEZE = 0xb,
+    PSCI_CPU_DEFAULT_SUSPEND = 0xc,
+    PSCI_NODE_HW_STATE = 0xd,
+    PSCI_SYSTEM_SUSPEND = 0xe,
+    PSCI_SET_SUSPEND_MODE = 0xf,
+    PSCI_STAT_RESIDENCY = 0x10,
+    PSCI_STAT_COUNT = 0x11,
+    PSCI_SYSTEM_RESET2 = 0x12,
+    PSCI_MEM_PROTECT = 0x13,
+    PSCI_MEM_PROTECT_CHECK_RANGE = 0x14,
+    PSCI_MAX = 0x1f
+} psci_id_t;
+
+bool handle_psci(uint64_t vcpu_id, seL4_UserContext *regs,  uint64_t fn_number, uint32_t hsr);

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/smc.c

@@ -0,0 +1,118 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include "smc.h"
+#include "psci.h"
+#include "util/util.h"
+
+// Values in this file are taken from:
+// SMC CALLING CONVENTION
+// System Software on ARM (R) Platforms
+// Issue B
+#define SMC_SERVICE_CALL_MASK 0x3F
+#define SMC_SERVICE_CALL_SHIFT 24
+
+#define SMC_FUNC_ID_MASK 0xFFFF
+
+/* SMC and HVC function identifiers */
+typedef enum {
+    SMC_CALL_ARM_ARCH = 0,
+    SMC_CALL_CPU_SERVICE = 1,
+    SMC_CALL_SIP_SERVICE = 2,
+    SMC_CALL_OEM_SERVICE = 3,
+    SMC_CALL_STD_SERVICE = 4,
+    SMC_CALL_STD_HYP_SERVICE = 5,
+    SMC_CALL_VENDOR_HYP_SERVICE = 6,
+    SMC_CALL_TRUSTED_APP = 48,
+    SMC_CALL_TRUSTED_OS = 50,
+    SMC_CALL_RESERVED = 64,
+} smc_call_id_t;
+
+static smc_call_id_t smc_get_call(uintptr_t func_id)
+{
+    uint64_t service = ((func_id >> SMC_SERVICE_CALL_SHIFT) & SMC_SERVICE_CALL_MASK);
+    assert(service >= 0 && service <= 0xFFFF);
+
+    if (service <= SMC_CALL_VENDOR_HYP_SERVICE) {
+        return service;
+    } else if (service < SMC_CALL_TRUSTED_APP) {
+        return SMC_CALL_RESERVED;
+    } else if (service < SMC_CALL_TRUSTED_OS) {
+        return SMC_CALL_TRUSTED_APP;
+    } else if (service < SMC_CALL_RESERVED) {
+        return SMC_CALL_TRUSTED_OS;
+    } else {
+        return SMC_CALL_RESERVED;
+    }
+}
+
+static inline uint64_t smc_get_function_number(seL4_UserContext *regs)
+{
+    return regs->x0 & SMC_FUNC_ID_MASK;
+}
+
+inline void smc_set_return_value(seL4_UserContext *u, uint64_t val)
+{
+    u->x0 = val;
+}
+
+uint64_t smc_get_arg(seL4_UserContext *u, uint64_t arg)
+{
+    switch (arg) {
+        case 1: return u->x1;
+        case 2: return u->x2;
+        case 3: return u->x3;
+        case 4: return u->x4;
+        case 5: return u->x5;
+        case 6: return u->x6;
+        default:
+            LOG_VMM_ERR("trying to get SMC arg: 0x%lx, SMC only has 6 argument registers\n", arg);
+            // @ivanv: come back to this
+            return 0;
+    }
+}
+
+static void smc_set_arg(seL4_UserContext *u, uint64_t arg, uint64_t val)
+{
+    switch (arg) {
+        case 1: u->x1 = val; break;
+        case 2: u->x2 = val; break;
+        case 3: u->x3 = val; break;
+        case 4: u->x4 = val; break;
+        case 5: u->x5 = val; break;
+        case 6: u->x6 = val; break;
+        default:
+            LOG_VMM_ERR("trying to set SMC arg: 0x%lx, with val: 0x%lx, SMC only has 6 argument registers\n", arg, val);
+    }
+}
+
+// @ivanv: print out which SMC call as a string we can't handle.
+bool handle_smc(uint64_t vcpu_id, uint32_t hsr)
+{
+    // @ivanv: An optimisation to be made is to store the TCB registers so we don't
+    // end up reading them multiple times
+    seL4_UserContext regs;
+    int err = seL4_TCB_ReadRegisters(BASE_VM_TCB_CAP + GUEST_ID, false, 0, SEL4_USER_CONTEXT_SIZE, &regs);
+    assert(err == seL4_NoError);
+
+    uint64_t fn_number = smc_get_function_number(&regs);
+    smc_call_id_t service = smc_get_call(regs.x0);
+
+    switch (service) {
+        case SMC_CALL_STD_SERVICE:
+            if (fn_number < PSCI_MAX) {
+                return handle_psci(vcpu_id, &regs, fn_number, hsr);
+            }
+            LOG_VMM_ERR("Unhandled SMC: standard service call %lu\n", fn_number);
+            break;
+        default:
+            LOG_VMM_ERR("Unhandled SMC: unknown value service: 0x%lx, function number: 0x%lx\n", service, fn_number);
+            break;
+    }
+
+    return false;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/smc.h

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+
+#include <stdint.h>
+#include <stdbool.h>
+#include <microkit.h>
+
+// SMC vCPU fault handler
+bool handle_smc(uint64_t vcpu_id, uint32_t hsr);
+
+// Helper functions
+void smc_set_return_value(seL4_UserContext *u, uint64_t val);
+
+/* Gets the value of x1-x6 */
+uint64_t smc_get_arg(seL4_UserContext *u, uint64_t arg);

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/printf.c

@@ -0,0 +1,914 @@
+///////////////////////////////////////////////////////////////////////////////
+// \author (c) Marco Paland (info@paland.com)
+//             2014-2019, PALANDesign Hannover, Germany
+//
+// \license The MIT License (MIT)
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in
+// all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// THE SOFTWARE.
+//
+// \brief Tiny printf, sprintf and (v)snprintf implementation, optimized for speed on
+//        embedded systems with a very limited resources. These routines are thread
+//        safe and reentrant!
+//        Use this instead of the bloated standard/newlib printf cause these use
+//        malloc for printf (and may not be thread safe).
+//
+///////////////////////////////////////////////////////////////////////////////
+
+#include <stdbool.h>
+#include <stdint.h>
+
+#include "printf.h"
+
+
+// define this globally (e.g. gcc -DPRINTF_INCLUDE_CONFIG_H ...) to include the
+// printf_config.h header file
+// default: undefined
+#ifdef PRINTF_INCLUDE_CONFIG_H
+#include "printf_config.h"
+#endif
+
+
+// 'ntoa' conversion buffer size, this must be big enough to hold one converted
+// numeric number including padded zeros (dynamically created on stack)
+// default: 32 byte
+#ifndef PRINTF_NTOA_BUFFER_SIZE
+#define PRINTF_NTOA_BUFFER_SIZE    32U
+#endif
+
+// 'ftoa' conversion buffer size, this must be big enough to hold one converted
+// float number including padded zeros (dynamically created on stack)
+// default: 32 byte
+#ifndef PRINTF_FTOA_BUFFER_SIZE
+#define PRINTF_FTOA_BUFFER_SIZE    32U
+#endif
+
+// support for the floating point type (%f)
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_FLOAT
+#define PRINTF_SUPPORT_FLOAT
+#endif
+
+// support for exponential floating point notation (%e/%g)
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_EXPONENTIAL
+#define PRINTF_SUPPORT_EXPONENTIAL
+#endif
+
+// define the default floating point precision
+// default: 6 digits
+#ifndef PRINTF_DEFAULT_FLOAT_PRECISION
+#define PRINTF_DEFAULT_FLOAT_PRECISION  6U
+#endif
+
+// define the largest float suitable to print with %f
+// default: 1e9
+#ifndef PRINTF_MAX_FLOAT
+#define PRINTF_MAX_FLOAT  1e9
+#endif
+
+// support for the long long types (%llu or %p)
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_LONG_LONG
+#define PRINTF_SUPPORT_LONG_LONG
+#endif
+
+// support for the ptrdiff_t type (%t)
+// ptrdiff_t is normally defined in <stddef.h> as long or long long type
+// default: activated
+#ifndef PRINTF_DISABLE_SUPPORT_PTRDIFF_T
+#define PRINTF_SUPPORT_PTRDIFF_T
+#endif
+
+///////////////////////////////////////////////////////////////////////////////
+
+// internal flag definitions
+#define FLAGS_ZEROPAD   (1U <<  0U)
+#define FLAGS_LEFT      (1U <<  1U)
+#define FLAGS_PLUS      (1U <<  2U)
+#define FLAGS_SPACE     (1U <<  3U)
+#define FLAGS_HASH      (1U <<  4U)
+#define FLAGS_UPPERCASE (1U <<  5U)
+#define FLAGS_CHAR      (1U <<  6U)
+#define FLAGS_SHORT     (1U <<  7U)
+#define FLAGS_LONG      (1U <<  8U)
+#define FLAGS_LONG_LONG (1U <<  9U)
+#define FLAGS_PRECISION (1U << 10U)
+#define FLAGS_ADAPT_EXP (1U << 11U)
+
+
+// import float.h for DBL_MAX
+#if defined(PRINTF_SUPPORT_FLOAT)
+#include <float.h>
+#endif
+
+
+// output function type
+typedef void (*out_fct_type)(char character, void* buffer, size_t idx, size_t maxlen);
+
+
+// wrapper (used as buffer) for output function type
+typedef struct {
+  void  (*fct)(char character, void* arg);
+  void* arg;
+} out_fct_wrap_type;
+
+
+// internal buffer output
+static inline void _out_buffer(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  if (idx < maxlen) {
+    ((char*)buffer)[idx] = character;
+  }
+}
+
+
+// internal null output
+static inline void _out_null(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  (void)character; (void)buffer; (void)idx; (void)maxlen;
+}
+
+
+// internal _putchar wrapper
+static inline void _out_char(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  (void)buffer; (void)idx; (void)maxlen;
+  if (character) {
+    _putchar(character);
+  }
+}
+
+
+// internal output function wrapper
+static inline void _out_fct(char character, void* buffer, size_t idx, size_t maxlen)
+{
+  (void)idx; (void)maxlen;
+  if (character) {
+    // buffer is the output fct pointer
+    ((out_fct_wrap_type*)buffer)->fct(character, ((out_fct_wrap_type*)buffer)->arg);
+  }
+}
+
+
+// internal secure strlen
+// \return The length of the string (excluding the terminating 0) limited by 'maxsize'
+static inline unsigned int _strnlen_s(const char* str, size_t maxsize)
+{
+  const char* s;
+  for (s = str; *s && maxsize--; ++s);
+  return (unsigned int)(s - str);
+}
+
+
+// internal test if char is a digit (0-9)
+// \return true if char is a digit
+static inline bool _is_digit(char ch)
+{
+  return (ch >= '0') && (ch <= '9');
+}
+
+
+// internal ASCII string to unsigned int conversion
+static unsigned int _atoi(const char** str)
+{
+  unsigned int i = 0U;
+  while (_is_digit(**str)) {
+    i = i * 10U + (unsigned int)(*((*str)++) - '0');
+  }
+  return i;
+}
+
+
+// output the specified string in reverse, taking care of any zero-padding
+static size_t _out_rev(out_fct_type out, char* buffer, size_t idx, size_t maxlen, const char* buf, size_t len, unsigned int width, unsigned int flags)
+{
+  const size_t start_idx = idx;
+
+  // pad spaces up to given width
+  if (!(flags & FLAGS_LEFT) && !(flags & FLAGS_ZEROPAD)) {
+    for (size_t i = len; i < width; i++) {
+      out(' ', buffer, idx++, maxlen);
+    }
+  }
+
+  // reverse string
+  while (len) {
+    out(buf[--len], buffer, idx++, maxlen);
+  }
+
+  // append pad spaces up to given width
+  if (flags & FLAGS_LEFT) {
+    while (idx - start_idx < width) {
+      out(' ', buffer, idx++, maxlen);
+    }
+  }
+
+  return idx;
+}
+
+
+// internal itoa format
+static size_t _ntoa_format(out_fct_type out, char* buffer, size_t idx, size_t maxlen, char* buf, size_t len, bool negative, unsigned int base, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  // pad leading zeros
+  if (!(flags & FLAGS_LEFT)) {
+    if (width && (flags & FLAGS_ZEROPAD) && (negative || (flags & (FLAGS_PLUS | FLAGS_SPACE)))) {
+      width--;
+    }
+    while ((len < prec) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = '0';
+    }
+    while ((flags & FLAGS_ZEROPAD) && (len < width) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = '0';
+    }
+  }
+
+  // handle hash
+  if (flags & FLAGS_HASH) {
+    if (!(flags & FLAGS_PRECISION) && len && ((len == prec) || (len == width))) {
+      len--;
+      if (len && (base == 16U)) {
+        len--;
+      }
+    }
+    if ((base == 16U) && !(flags & FLAGS_UPPERCASE) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = 'x';
+    }
+    else if ((base == 16U) && (flags & FLAGS_UPPERCASE) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = 'X';
+    }
+    else if ((base == 2U) && (len < PRINTF_NTOA_BUFFER_SIZE)) {
+      buf[len++] = 'b';
+    }
+    if (len < PRINTF_NTOA_BUFFER_SIZE) {
+      buf[len++] = '0';
+    }
+  }
+
+  if (len < PRINTF_NTOA_BUFFER_SIZE) {
+    if (negative) {
+      buf[len++] = '-';
+    }
+    else if (flags & FLAGS_PLUS) {
+      buf[len++] = '+';  // ignore the space if the '+' exists
+    }
+    else if (flags & FLAGS_SPACE) {
+      buf[len++] = ' ';
+    }
+  }
+
+  return _out_rev(out, buffer, idx, maxlen, buf, len, width, flags);
+}
+
+
+// internal itoa for 'long' type
+static size_t _ntoa_long(out_fct_type out, char* buffer, size_t idx, size_t maxlen, unsigned long value, bool negative, unsigned long base, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  char buf[PRINTF_NTOA_BUFFER_SIZE];
+  size_t len = 0U;
+
+  // no hash for 0 values
+  if (!value) {
+    flags &= ~FLAGS_HASH;
+  }
+
+  // write if precision != 0 and value is != 0
+  if (!(flags & FLAGS_PRECISION) || value) {
+    do {
+      const char digit = (char)(value % base);
+      buf[len++] = digit < 10 ? '0' + digit : (flags & FLAGS_UPPERCASE ? 'A' : 'a') + digit - 10;
+      value /= base;
+    } while (value && (len < PRINTF_NTOA_BUFFER_SIZE));
+  }
+
+  return _ntoa_format(out, buffer, idx, maxlen, buf, len, negative, (unsigned int)base, prec, width, flags);
+}
+
+
+// internal itoa for 'long long' type
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+static size_t _ntoa_long_long(out_fct_type out, char* buffer, size_t idx, size_t maxlen, unsigned long long value, bool negative, unsigned long long base, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  char buf[PRINTF_NTOA_BUFFER_SIZE];
+  size_t len = 0U;
+
+  // no hash for 0 values
+  if (!value) {
+    flags &= ~FLAGS_HASH;
+  }
+
+  // write if precision != 0 and value is != 0
+  if (!(flags & FLAGS_PRECISION) || value) {
+    do {
+      const char digit = (char)(value % base);
+      buf[len++] = digit < 10 ? '0' + digit : (flags & FLAGS_UPPERCASE ? 'A' : 'a') + digit - 10;
+      value /= base;
+    } while (value && (len < PRINTF_NTOA_BUFFER_SIZE));
+  }
+
+  return _ntoa_format(out, buffer, idx, maxlen, buf, len, negative, (unsigned int)base, prec, width, flags);
+}
+#endif  // PRINTF_SUPPORT_LONG_LONG
+
+
+#if defined(PRINTF_SUPPORT_FLOAT)
+
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+// forward declaration so that _ftoa can switch to exp notation for values > PRINTF_MAX_FLOAT
+static size_t _etoa(out_fct_type out, char* buffer, size_t idx, size_t maxlen, double value, unsigned int prec, unsigned int width, unsigned int flags);
+#endif
+
+
+// internal ftoa for fixed decimal floating point
+static size_t _ftoa(out_fct_type out, char* buffer, size_t idx, size_t maxlen, double value, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  char buf[PRINTF_FTOA_BUFFER_SIZE];
+  size_t len  = 0U;
+  double diff = 0.0;
+
+  // powers of 10
+  static const double pow10[] = { 1, 10, 100, 1000, 10000, 100000, 1000000, 10000000, 100000000, 1000000000 };
+
+  // test for special values
+  if (value != value)
+    return _out_rev(out, buffer, idx, maxlen, "nan", 3, width, flags);
+  if (value < -DBL_MAX)
+    return _out_rev(out, buffer, idx, maxlen, "fni-", 4, width, flags);
+  if (value > DBL_MAX)
+    return _out_rev(out, buffer, idx, maxlen, (flags & FLAGS_PLUS) ? "fni+" : "fni", (flags & FLAGS_PLUS) ? 4U : 3U, width, flags);
+
+  // test for very large values
+  // standard printf behavior is to print EVERY whole number digit -- which could be 100s of characters overflowing your buffers == bad
+  if ((value > PRINTF_MAX_FLOAT) || (value < -PRINTF_MAX_FLOAT)) {
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+    return _etoa(out, buffer, idx, maxlen, value, prec, width, flags);
+#else
+    return 0U;
+#endif
+  }
+
+  // test for negative
+  bool negative = false;
+  if (value < 0) {
+    negative = true;
+    value = 0 - value;
+  }
+
+  // set default precision, if not set explicitly
+  if (!(flags & FLAGS_PRECISION)) {
+    prec = PRINTF_DEFAULT_FLOAT_PRECISION;
+  }
+  // limit precision to 9, cause a prec >= 10 can lead to overflow errors
+  while ((len < PRINTF_FTOA_BUFFER_SIZE) && (prec > 9U)) {
+    buf[len++] = '0';
+    prec--;
+  }
+
+  int whole = (int)value;
+  double tmp = (value - whole) * pow10[prec];
+  unsigned long frac = (unsigned long)tmp;
+  diff = tmp - frac;
+
+  if (diff > 0.5) {
+    ++frac;
+    // handle rollover, e.g. case 0.99 with prec 1 is 1.0
+    if (frac >= pow10[prec]) {
+      frac = 0;
+      ++whole;
+    }
+  }
+  else if (diff < 0.5) {
+  }
+  else if ((frac == 0U) || (frac & 1U)) {
+    // if halfway, round up if odd OR if last digit is 0
+    ++frac;
+  }
+
+  if (prec == 0U) {
+    diff = value - (double)whole;
+    if ((!(diff < 0.5) || (diff > 0.5)) && (whole & 1)) {
+      // exactly 0.5 and ODD, then round up
+      // 1.5 -> 2, but 2.5 -> 2
+      ++whole;
+    }
+  }
+  else {
+    unsigned int count = prec;
+    // now do fractional part, as an unsigned number
+    while (len < PRINTF_FTOA_BUFFER_SIZE) {
+      --count;
+      buf[len++] = (char)(48U + (frac % 10U));
+      if (!(frac /= 10U)) {
+        break;
+      }
+    }
+    // add extra 0s
+    while ((len < PRINTF_FTOA_BUFFER_SIZE) && (count-- > 0U)) {
+      buf[len++] = '0';
+    }
+    if (len < PRINTF_FTOA_BUFFER_SIZE) {
+      // add decimal
+      buf[len++] = '.';
+    }
+  }
+
+  // do whole part, number is reversed
+  while (len < PRINTF_FTOA_BUFFER_SIZE) {
+    buf[len++] = (char)(48 + (whole % 10));
+    if (!(whole /= 10)) {
+      break;
+    }
+  }
+
+  // pad leading zeros
+  if (!(flags & FLAGS_LEFT) && (flags & FLAGS_ZEROPAD)) {
+    if (width && (negative || (flags & (FLAGS_PLUS | FLAGS_SPACE)))) {
+      width--;
+    }
+    while ((len < width) && (len < PRINTF_FTOA_BUFFER_SIZE)) {
+      buf[len++] = '0';
+    }
+  }
+
+  if (len < PRINTF_FTOA_BUFFER_SIZE) {
+    if (negative) {
+      buf[len++] = '-';
+    }
+    else if (flags & FLAGS_PLUS) {
+      buf[len++] = '+';  // ignore the space if the '+' exists
+    }
+    else if (flags & FLAGS_SPACE) {
+      buf[len++] = ' ';
+    }
+  }
+
+  return _out_rev(out, buffer, idx, maxlen, buf, len, width, flags);
+}
+
+
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+// internal ftoa variant for exponential floating-point type, contributed by Martijn Jasperse <m.jasperse@gmail.com>
+static size_t _etoa(out_fct_type out, char* buffer, size_t idx, size_t maxlen, double value, unsigned int prec, unsigned int width, unsigned int flags)
+{
+  // check for NaN and special values
+  if ((value != value) || (value > DBL_MAX) || (value < -DBL_MAX)) {
+    return _ftoa(out, buffer, idx, maxlen, value, prec, width, flags);
+  }
+
+  // determine the sign
+  const bool negative = value < 0;
+  if (negative) {
+    value = -value;
+  }
+
+  // default precision
+  if (!(flags & FLAGS_PRECISION)) {
+    prec = PRINTF_DEFAULT_FLOAT_PRECISION;
+  }
+
+  // determine the decimal exponent
+  // based on the algorithm by David Gay (https://www.ampl.com/netlib/fp/dtoa.c)
+  union {
+    uint64_t U;
+    double   F;
+  } conv;
+
+  conv.F = value;
+  int exp2 = (int)((conv.U >> 52U) & 0x07FFU) - 1023;           // effectively log2
+  conv.U = (conv.U & ((1ULL << 52U) - 1U)) | (1023ULL << 52U);  // drop the exponent so conv.F is now in [1,2)
+  // now approximate log10 from the log2 integer part and an expansion of ln around 1.5
+  int expval = (int)(0.1760912590558 + exp2 * 0.301029995663981 + (conv.F - 1.5) * 0.289529654602168);
+  // now we want to compute 10^expval but we want to be sure it won't overflow
+  exp2 = (int)(expval * 3.321928094887362 + 0.5);
+  const double z  = expval * 2.302585092994046 - exp2 * 0.6931471805599453;
+  const double z2 = z * z;
+  conv.U = (uint64_t)(exp2 + 1023) << 52U;
+  // compute exp(z) using continued fractions, see https://en.wikipedia.org/wiki/Exponential_function#Continued_fractions_for_ex
+  conv.F *= 1 + 2 * z / (2 - z + (z2 / (6 + (z2 / (10 + z2 / 14)))));
+  // correct for rounding errors
+  if (value < conv.F) {
+    expval--;
+    conv.F /= 10;
+  }
+
+  // the exponent format is "%+03d" and largest value is "307", so set aside 4-5 characters
+  unsigned int minwidth = ((expval < 100) && (expval > -100)) ? 4U : 5U;
+
+  // in "%g" mode, "prec" is the number of *significant figures* not decimals
+  if (flags & FLAGS_ADAPT_EXP) {
+    // do we want to fall-back to "%f" mode?
+    if ((value >= 1e-4) && (value < 1e6)) {
+      if ((int)prec > expval) {
+        prec = (unsigned)((int)prec - expval - 1);
+      }
+      else {
+        prec = 0;
+      }
+      flags |= FLAGS_PRECISION;   // make sure _ftoa respects precision
+      // no characters in exponent
+      minwidth = 0U;
+      expval   = 0;
+    }
+    else {
+      // we use one sigfig for the whole part
+      if ((prec > 0) && (flags & FLAGS_PRECISION)) {
+        --prec;
+      }
+    }
+  }
+
+  // will everything fit?
+  unsigned int fwidth = width;
+  if (width > minwidth) {
+    // we didn't fall-back so subtract the characters required for the exponent
+    fwidth -= minwidth;
+  } else {
+    // not enough characters, so go back to default sizing
+    fwidth = 0U;
+  }
+  if ((flags & FLAGS_LEFT) && minwidth) {
+    // if we're padding on the right, DON'T pad the floating part
+    fwidth = 0U;
+  }
+
+  // rescale the float value
+  if (expval) {
+    value /= conv.F;
+  }
+
+  // output the floating part
+  const size_t start_idx = idx;
+  idx = _ftoa(out, buffer, idx, maxlen, negative ? -value : value, prec, fwidth, flags & ~FLAGS_ADAPT_EXP);
+
+  // output the exponent part
+  if (minwidth) {
+    // output the exponential symbol
+    out((flags & FLAGS_UPPERCASE) ? 'E' : 'e', buffer, idx++, maxlen);
+    // output the exponent value
+    idx = _ntoa_long(out, buffer, idx, maxlen, (expval < 0) ? -expval : expval, expval < 0, 10, 0, minwidth-1, FLAGS_ZEROPAD | FLAGS_PLUS);
+    // might need to right-pad spaces
+    if (flags & FLAGS_LEFT) {
+      while (idx - start_idx < width) out(' ', buffer, idx++, maxlen);
+    }
+  }
+  return idx;
+}
+#endif  // PRINTF_SUPPORT_EXPONENTIAL
+#endif  // PRINTF_SUPPORT_FLOAT
+
+
+// internal vsnprintf
+static int _vsnprintf(out_fct_type out, char* buffer, const size_t maxlen, const char* format, va_list va)
+{
+  unsigned int flags, width, precision, n;
+  size_t idx = 0U;
+
+  if (!buffer) {
+    // use null output function
+    out = _out_null;
+  }
+
+  while (*format)
+  {
+    // format specifier?  %[flags][width][.precision][length]
+    if (*format != '%') {
+      // no
+      out(*format, buffer, idx++, maxlen);
+      format++;
+      continue;
+    }
+    else {
+      // yes, evaluate it
+      format++;
+    }
+
+    // evaluate flags
+    flags = 0U;
+    do {
+      switch (*format) {
+        case '0': flags |= FLAGS_ZEROPAD; format++; n = 1U; break;
+        case '-': flags |= FLAGS_LEFT;    format++; n = 1U; break;
+        case '+': flags |= FLAGS_PLUS;    format++; n = 1U; break;
+        case ' ': flags |= FLAGS_SPACE;   format++; n = 1U; break;
+        case '#': flags |= FLAGS_HASH;    format++; n = 1U; break;
+        default :                                   n = 0U; break;
+      }
+    } while (n);
+
+    // evaluate width field
+    width = 0U;
+    if (_is_digit(*format)) {
+      width = _atoi(&format);
+    }
+    else if (*format == '*') {
+      const int w = va_arg(va, int);
+      if (w < 0) {
+        flags |= FLAGS_LEFT;    // reverse padding
+        width = (unsigned int)-w;
+      }
+      else {
+        width = (unsigned int)w;
+      }
+      format++;
+    }
+
+    // evaluate precision field
+    precision = 0U;
+    if (*format == '.') {
+      flags |= FLAGS_PRECISION;
+      format++;
+      if (_is_digit(*format)) {
+        precision = _atoi(&format);
+      }
+      else if (*format == '*') {
+        const int prec = (int)va_arg(va, int);
+        precision = prec > 0 ? (unsigned int)prec : 0U;
+        format++;
+      }
+    }
+
+    // evaluate length field
+    switch (*format) {
+      case 'l' :
+        flags |= FLAGS_LONG;
+        format++;
+        if (*format == 'l') {
+          flags |= FLAGS_LONG_LONG;
+          format++;
+        }
+        break;
+      case 'h' :
+        flags |= FLAGS_SHORT;
+        format++;
+        if (*format == 'h') {
+          flags |= FLAGS_CHAR;
+          format++;
+        }
+        break;
+#if defined(PRINTF_SUPPORT_PTRDIFF_T)
+      case 't' :
+        flags |= (sizeof(ptrdiff_t) == sizeof(long) ? FLAGS_LONG : FLAGS_LONG_LONG);
+        format++;
+        break;
+#endif
+      case 'j' :
+        flags |= (sizeof(intmax_t) == sizeof(long) ? FLAGS_LONG : FLAGS_LONG_LONG);
+        format++;
+        break;
+      case 'z' :
+        flags |= (sizeof(size_t) == sizeof(long) ? FLAGS_LONG : FLAGS_LONG_LONG);
+        format++;
+        break;
+      default :
+        break;
+    }
+
+    // evaluate specifier
+    switch (*format) {
+      case 'd' :
+      case 'i' :
+      case 'u' :
+      case 'x' :
+      case 'X' :
+      case 'o' :
+      case 'b' : {
+        // set the base
+        unsigned int base;
+        if (*format == 'x' || *format == 'X') {
+          base = 16U;
+        }
+        else if (*format == 'o') {
+          base =  8U;
+        }
+        else if (*format == 'b') {
+          base =  2U;
+        }
+        else {
+          base = 10U;
+          flags &= ~FLAGS_HASH;   // no hash for dec format
+        }
+        // uppercase
+        if (*format == 'X') {
+          flags |= FLAGS_UPPERCASE;
+        }
+
+        // no plus or space flag for u, x, X, o, b
+        if ((*format != 'i') && (*format != 'd')) {
+          flags &= ~(FLAGS_PLUS | FLAGS_SPACE);
+        }
+
+        // ignore '0' flag when precision is given
+        if (flags & FLAGS_PRECISION) {
+          flags &= ~FLAGS_ZEROPAD;
+        }
+
+        // convert the integer
+        if ((*format == 'i') || (*format == 'd')) {
+          // signed
+          if (flags & FLAGS_LONG_LONG) {
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+            const long long value = va_arg(va, long long);
+            idx = _ntoa_long_long(out, buffer, idx, maxlen, (unsigned long long)(value > 0 ? value : 0 - value), value < 0, base, precision, width, flags);
+#endif
+          }
+          else if (flags & FLAGS_LONG) {
+            const long value = va_arg(va, long);
+            idx = _ntoa_long(out, buffer, idx, maxlen, (unsigned long)(value > 0 ? value : 0 - value), value < 0, base, precision, width, flags);
+          }
+          else {
+            const int value = (flags & FLAGS_CHAR) ? (char)va_arg(va, int) : (flags & FLAGS_SHORT) ? (short int)va_arg(va, int) : va_arg(va, int);
+            idx = _ntoa_long(out, buffer, idx, maxlen, (unsigned int)(value > 0 ? value : 0 - value), value < 0, base, precision, width, flags);
+          }
+        }
+        else {
+          // unsigned
+          if (flags & FLAGS_LONG_LONG) {
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+            idx = _ntoa_long_long(out, buffer, idx, maxlen, va_arg(va, unsigned long long), false, base, precision, width, flags);
+#endif
+          }
+          else if (flags & FLAGS_LONG) {
+            idx = _ntoa_long(out, buffer, idx, maxlen, va_arg(va, unsigned long), false, base, precision, width, flags);
+          }
+          else {
+            const unsigned int value = (flags & FLAGS_CHAR) ? (unsigned char)va_arg(va, unsigned int) : (flags & FLAGS_SHORT) ? (unsigned short int)va_arg(va, unsigned int) : va_arg(va, unsigned int);
+            idx = _ntoa_long(out, buffer, idx, maxlen, value, false, base, precision, width, flags);
+          }
+        }
+        format++;
+        break;
+      }
+#if defined(PRINTF_SUPPORT_FLOAT)
+      case 'f' :
+      case 'F' :
+        if (*format == 'F') flags |= FLAGS_UPPERCASE;
+        idx = _ftoa(out, buffer, idx, maxlen, va_arg(va, double), precision, width, flags);
+        format++;
+        break;
+#if defined(PRINTF_SUPPORT_EXPONENTIAL)
+      case 'e':
+      case 'E':
+      case 'g':
+      case 'G':
+        if ((*format == 'g')||(*format == 'G')) flags |= FLAGS_ADAPT_EXP;
+        if ((*format == 'E')||(*format == 'G')) flags |= FLAGS_UPPERCASE;
+        idx = _etoa(out, buffer, idx, maxlen, va_arg(va, double), precision, width, flags);
+        format++;
+        break;
+#endif  // PRINTF_SUPPORT_EXPONENTIAL
+#endif  // PRINTF_SUPPORT_FLOAT
+      case 'c' : {
+        unsigned int l = 1U;
+        // pre padding
+        if (!(flags & FLAGS_LEFT)) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        // char output
+        out((char)va_arg(va, int), buffer, idx++, maxlen);
+        // post padding
+        if (flags & FLAGS_LEFT) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        format++;
+        break;
+      }
+
+      case 's' : {
+        const char* p = va_arg(va, char*);
+        unsigned int l = _strnlen_s(p, precision ? precision : (size_t)-1);
+        // pre padding
+        if (flags & FLAGS_PRECISION) {
+          l = (l < precision ? l : precision);
+        }
+        if (!(flags & FLAGS_LEFT)) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        // string output
+        while ((*p != 0) && (!(flags & FLAGS_PRECISION) || precision--)) {
+          out(*(p++), buffer, idx++, maxlen);
+        }
+        // post padding
+        if (flags & FLAGS_LEFT) {
+          while (l++ < width) {
+            out(' ', buffer, idx++, maxlen);
+          }
+        }
+        format++;
+        break;
+      }
+
+      case 'p' : {
+        width = sizeof(void*) * 2U;
+        flags |= FLAGS_ZEROPAD | FLAGS_UPPERCASE;
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+        const bool is_ll = sizeof(uintptr_t) == sizeof(long long);
+        if (is_ll) {
+          idx = _ntoa_long_long(out, buffer, idx, maxlen, (uintptr_t)va_arg(va, void*), false, 16U, precision, width, flags);
+        }
+        else {
+#endif
+          idx = _ntoa_long(out, buffer, idx, maxlen, (unsigned long)((uintptr_t)va_arg(va, void*)), false, 16U, precision, width, flags);
+#if defined(PRINTF_SUPPORT_LONG_LONG)
+        }
+#endif
+        format++;
+        break;
+      }
+
+      case '%' :
+        out('%', buffer, idx++, maxlen);
+        format++;
+        break;
+
+      default :
+        out(*format, buffer, idx++, maxlen);
+        format++;
+        break;
+    }
+  }
+
+  // termination
+  out((char)0, buffer, idx < maxlen ? idx : maxlen - 1U, maxlen);
+
+  // return written chars without terminating \0
+  return (int)idx;
+}
+
+
+///////////////////////////////////////////////////////////////////////////////
+
+int printf_(const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  char buffer[1];
+  const int ret = _vsnprintf(_out_char, buffer, (size_t)-1, format, va);
+  va_end(va);
+  return ret;
+}
+
+
+int sprintf_(char* buffer, const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  const int ret = _vsnprintf(_out_buffer, buffer, (size_t)-1, format, va);
+  va_end(va);
+  return ret;
+}
+
+
+int snprintf_(char* buffer, size_t count, const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  const int ret = _vsnprintf(_out_buffer, buffer, count, format, va);
+  va_end(va);
+  return ret;
+}
+
+
+int vprintf_(const char* format, va_list va)
+{
+  char buffer[1];
+  return _vsnprintf(_out_char, buffer, (size_t)-1, format, va);
+}
+
+
+int vsnprintf_(char* buffer, size_t count, const char* format, va_list va)
+{
+  return _vsnprintf(_out_buffer, buffer, count, format, va);
+}
+
+
+int fctprintf(void (*out)(char character, void* arg), void* arg, const char* format, ...)
+{
+  va_list va;
+  va_start(va, format);
+  const out_fct_wrap_type out_fct_wrap = { out, arg };
+  const int ret = _vsnprintf(_out_fct, (char*)(uintptr_t)&out_fct_wrap, (size_t)-1, format, va);
+  va_end(va);
+  return ret;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/printf.h

@@ -0,0 +1,117 @@
+///////////////////////////////////////////////////////////////////////////////
+// \author (c) Marco Paland (info@paland.com)
+//             2014-2019, PALANDesign Hannover, Germany
+//
+// \license The MIT License (MIT)
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy
+// of this software and associated documentation files (the "Software"), to deal
+// in the Software without restriction, including without limitation the rights
+// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+// copies of the Software, and to permit persons to whom the Software is
+// furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in
+// all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+// THE SOFTWARE.
+//
+// \brief Tiny printf, sprintf and snprintf implementation, optimized for speed on
+//        embedded systems with a very limited resources.
+//        Use this instead of bloated standard/newlib printf.
+//        These routines are thread safe and reentrant.
+//
+///////////////////////////////////////////////////////////////////////////////
+
+#ifndef _PRINTF_H_
+#define _PRINTF_H_
+
+#include <stdarg.h>
+#include <stddef.h>
+
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+
+/**
+ * Output a character to a custom device like UART, used by the printf() function
+ * This function is declared here only. You have to write your custom implementation somewhere
+ * \param character Character to output
+ */
+void _putchar(char character);
+
+
+/**
+ * Tiny printf implementation
+ * You have to implement _putchar if you use printf()
+ * To avoid conflicts with the regular printf() API it is overridden by macro defines
+ * and internal underscore-appended functions like printf_() are used
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are written into the array, not counting the terminating null character
+ */
+#define printf printf_
+int printf_(const char* format, ...);
+
+
+/**
+ * Tiny sprintf implementation
+ * Due to security reasons (buffer overflow) YOU SHOULD CONSIDER USING (V)SNPRINTF INSTEAD!
+ * \param buffer A pointer to the buffer where to store the formatted string. MUST be big enough to store the output!
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are WRITTEN into the buffer, not counting the terminating null character
+ */
+#define sprintf sprintf_
+int sprintf_(char* buffer, const char* format, ...);
+
+
+/**
+ * Tiny snprintf/vsnprintf implementation
+ * \param buffer A pointer to the buffer where to store the formatted string
+ * \param count The maximum number of characters to store in the buffer, including a terminating null character
+ * \param format A string that specifies the format of the output
+ * \param va A value identifying a variable arguments list
+ * \return The number of characters that COULD have been written into the buffer, not counting the terminating
+ *         null character. A value equal or larger than count indicates truncation. Only when the returned value
+ *         is non-negative and less than count, the string has been completely written.
+ */
+#define snprintf  snprintf_
+#define vsnprintf vsnprintf_
+int  snprintf_(char* buffer, size_t count, const char* format, ...);
+int vsnprintf_(char* buffer, size_t count, const char* format, va_list va);
+
+
+/**
+ * Tiny vprintf implementation
+ * \param format A string that specifies the format of the output
+ * \param va A value identifying a variable arguments list
+ * \return The number of characters that are WRITTEN into the buffer, not counting the terminating null character
+ */
+#define vprintf vprintf_
+int vprintf_(const char* format, va_list va);
+
+
+/**
+ * printf with output function
+ * You may use this as dynamic alternative to printf() with its fixed _putchar() output
+ * \param out An output function which takes one character and an argument pointer
+ * \param arg An argument pointer for user data passed to output function
+ * \param format A string that specifies the format of the output
+ * \return The number of characters that are sent to the output function, not counting the terminating null character
+ */
+int fctprintf(void (*out)(char character, void* arg), void* arg, const char* format, ...);
+
+
+#ifdef __cplusplus
+}
+#endif
+
+
+#endif  // _PRINTF_H_

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/util.c

@@ -0,0 +1,28 @@
+/*
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include "util.h"
+
+/* This is required to use the printf library we brought in, it is
+   simply for convenience since there's a lot of logging/debug printing
+   in the VMM. */
+void _putchar(char character)
+{
+    microkit_dbg_putc(character);
+}
+
+ __attribute__ ((__noreturn__))
+void __assert_func(const char *file, int line, const char *function, const char *str)
+{
+    microkit_dbg_puts("assert failed: ");
+    microkit_dbg_puts(str);
+    microkit_dbg_puts(" ");
+    microkit_dbg_puts(file);
+    microkit_dbg_puts(" ");
+    microkit_dbg_puts(function);
+    microkit_dbg_puts("\n");
+    while (1) {}
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/util.h

@@ -0,0 +1,190 @@
+/*
+ * Copyright 2021, Breakaway Consulting Pty. Ltd.
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+
+#include <stdint.h>
+#include <microkit.h>
+#include "printf.h"
+
+// @ivanv: these are here for convience, should not be here though
+#define GUEST_ID 0
+#define GUEST_VCPU_ID 0
+#define GUEST_NUM_VCPUS 1
+// Note that this is AArch64 specific
+#if defined(CONFIG_ARCH_AARCH64)
+    #define SEL4_USER_CONTEXT_SIZE 0x24
+#endif
+
+#define PAGE_SIZE_4K 4096
+
+#define ARRAY_SIZE(x) (sizeof(x)/sizeof((x)[0]))
+
+#define CTZ(x) __builtin_ctz(x)
+
+#if __STDC_VERSION__ >= 201112L && !defined(__cplusplus)
+#define static_assert _Static_assert
+#endif
+
+//  __attribute__ ((__noreturn__))
+// void __assert_func(const char *file, int line, const char *function, const char *str);
+
+void _putchar(char character);
+
+#define LOG_VMM(...) do{ printf("%s|INFO: ", microkit_name); printf(__VA_ARGS__); }while(0)
+#define LOG_VMM_ERR(...) do{ printf("%s|ERROR: ", microkit_name); printf(__VA_ARGS__); }while(0)
+
+static char
+decchar(unsigned int v) {
+    return '0' + v;
+}
+
+static void
+put8(uint8_t x)
+{
+    char tmp[4];
+    unsigned i = 3;
+    tmp[3] = 0;
+    do {
+        uint8_t c = x % 10;
+        tmp[--i] = decchar(c);
+        x /= 10;
+    } while (x);
+    microkit_dbg_puts(&tmp[i]);
+}
+
+// @ivanv: sort this out...
+static void
+reply_to_fault()
+{
+    microkit_msginfo msg = microkit_msginfo_new(0, 0);
+    seL4_Send(4, msg);
+}
+
+static uint64_t get_vmm_id(char *microkit_name)
+{
+    // @ivanv: Absolute hack
+    return microkit_name[4] - '0';
+}
+
+static void
+print_tcb_regs(seL4_UserContext *ctx) {
+#if defined(ARCH_aarch64)
+    // I don't know if it's the best idea, but here we'll just dump the
+    // registers in the same order they are defined in seL4_UserContext
+    printf("VMM|INFO: TCB registers:\n");
+    // Frame registers
+    printf("    pc:   0x%016lx\n", ctx->pc);
+    printf("    sp:   0x%016lx\n", ctx->sp);
+    printf("    spsr: 0x%016lx\n", ctx->spsr);
+    printf("    x0:   0x%016lx\n", ctx->x0);
+    printf("    x1:   0x%016lx\n", ctx->x1);
+    printf("    x2:   0x%016lx\n", ctx->x2);
+    printf("    x3:   0x%016lx\n", ctx->x3);
+    printf("    x4:   0x%016lx\n", ctx->x4);
+    printf("    x5:   0x%016lx\n", ctx->x5);
+    printf("    x6:   0x%016lx\n", ctx->x6);
+    printf("    x7:   0x%016lx\n", ctx->x7);
+    printf("    x8:   0x%016lx\n", ctx->x8);
+    printf("    x16:  0x%016lx\n", ctx->x16);
+    printf("    x17:  0x%016lx\n", ctx->x17);
+    printf("    x18:  0x%016lx\n", ctx->x18);
+    printf("    x29:  0x%016lx\n", ctx->x29);
+    printf("    x30:  0x%016lx\n", ctx->x30);
+    // Other integer registers
+    printf("    x9:   0x%016lx\n", ctx->x9);
+    printf("    x10:  0x%016lx\n", ctx->x10);
+    printf("    x11:  0x%016lx\n", ctx->x11);
+    printf("    x12:  0x%016lx\n", ctx->x12);
+    printf("    x13:  0x%016lx\n", ctx->x13);
+    printf("    x14:  0x%016lx\n", ctx->x14);
+    printf("    x15:  0x%016lx\n", ctx->x15);
+    printf("    x19:  0x%016lx\n", ctx->x19);
+    printf("    x20:  0x%016lx\n", ctx->x20);
+    printf("    x21:  0x%016lx\n", ctx->x21);
+    printf("    x22:  0x%016lx\n", ctx->x22);
+    printf("    x23:  0x%016lx\n", ctx->x23);
+    printf("    x24:  0x%016lx\n", ctx->x24);
+    printf("    x25:  0x%016lx\n", ctx->x25);
+    printf("    x26:  0x%016lx\n", ctx->x26);
+    printf("    x27:  0x%016lx\n", ctx->x27);
+    printf("    x28:  0x%016lx\n", ctx->x28);
+    // TODO(ivanv): print out thread ID registers?
+#endif
+}
+
+// @ivanv: this should have the same foramtting as the TCB registers
+static void
+print_vcpu_regs(uint64_t vcpu_id) {
+    printf("VMM|INFO: VCPU registers: \n");
+    /* VM control registers EL1 */
+    printf("    SCTLR: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_SCTLR));
+    printf("    TTBR0: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_TTBR0));
+    printf("    TTBR1: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_TTBR1));
+    printf("    TCR:   0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_TCR));
+    printf("    MAIR:  0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_MAIR));
+    printf("    AMAIR: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_AMAIR));
+    printf("    CIDR:  0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_CIDR));
+    /* other system registers EL1 */
+    printf("    ACTLR: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_ACTLR));
+    printf("    CPACR: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_CPACR));
+    /* exception handling registers EL1 */
+    printf("    AFSR0: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_AFSR0));
+    printf("    AFSR1: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_AFSR1));
+    printf("    ESR:   0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_ESR));
+    printf("    FAR:   0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_FAR));
+    printf("    ISR:   0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_ISR));
+    printf("    VBAR:  0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_VBAR));
+    /* thread pointer/ID registers EL0/EL1 */
+    printf("    TPIDR_EL1: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_TPIDR_EL1));
+#if CONFIG_MAX_NUM_NODES > 1
+    /* Virtualisation Multiprocessor ID Register */
+    printf("    VMPIDR_EL2: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_VMPIDR_EL2));
+#endif
+    /* general registers x0 to x30 have been saved by traps.S */
+    printf("    SP_EL1: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_SP_EL1));
+    printf("    ELR_EL1: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_ELR_EL1));
+    printf("    SPSR_EL1: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_SPSR_EL1)); // 32-bit // @ivanv what
+    /* generic timer registers, to be completed */
+    printf("    CNTV_CTL: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_CNTV_CTL));
+    printf("    CNTV_CVAL: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_CNTV_CVAL));
+    printf("    CNTVOFF: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_CNTVOFF));
+    printf("    CNTKCTL_EL1: 0x%lx\n", microkit_vcpu_arm_read_reg(vcpu_id, seL4_VCPUReg_CNTKCTL_EL1));
+}
+
+static void *memcpy(void *restrict dest, const void *restrict src, size_t n)
+{
+    unsigned char *d = dest;
+    const unsigned char *s = src;
+    for (; n; n--) *d++ = *s++;
+    return dest;
+}
+
+static void *memset(void *dest, int c, size_t n)
+{
+    unsigned char *s = dest;
+    for (; n; n--, s++) *s = c;
+    return dest;
+}
+
+static void assert_fail(
+    const char  *assertion,
+    const char  *file,
+    unsigned int line,
+    const char  *function)
+{
+    printf("Failed assertion '%s' at %s:%u in function %s\n", assertion, file, line, function);
+    while (1) {}
+}
+
+#define assert(expr) \
+    do { \
+        if (!(expr)) { \
+            assert_fail(#expr, __FILE__, __LINE__, __FUNCTION__); \
+        } \
+    } while(0)
+

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vdist.h

@@ -0,0 +1,624 @@
+/*
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include "../util/util.h"
+#include "../fault.h"
+
+/* GIC Distributor register access utilities */
+#define GIC_DIST_REGN(offset, reg) ((offset-reg)/sizeof(uint32_t))
+#define RANGE32(a, b) a ... b + (sizeof(uint32_t)-1)
+
+#define IRQ_IDX(irq) ((irq) / 32)
+#define IRQ_BIT(irq) (1U << ((irq) % 32))
+
+static inline void set_sgi_ppi_pending(struct gic_dist_map *gic_dist, int irq, bool set_pending, int vcpu_id)
+{
+    if (set_pending) {
+        gic_dist->pending_set0[vcpu_id] |= IRQ_BIT(irq);
+        gic_dist->pending_clr0[vcpu_id] |= IRQ_BIT(irq);
+    } else {
+        gic_dist->pending_set0[vcpu_id] &= ~IRQ_BIT(irq);
+        gic_dist->pending_clr0[vcpu_id] &= ~IRQ_BIT(irq);
+    }
+}
+
+static inline void set_spi_pending(struct gic_dist_map *gic_dist, int irq, bool set_pending)
+{
+    if (set_pending) {
+        gic_dist->pending_set[IRQ_IDX(irq)] |= IRQ_BIT(irq);
+        gic_dist->pending_clr[IRQ_IDX(irq)] |= IRQ_BIT(irq);
+    } else {
+        gic_dist->pending_set[IRQ_IDX(irq)] &= ~IRQ_BIT(irq);
+        gic_dist->pending_clr[IRQ_IDX(irq)] &= ~IRQ_BIT(irq);
+    }
+}
+
+static inline void set_pending(struct gic_dist_map *gic_dist, int irq, bool set_pending, int vcpu_id)
+{
+    if (irq < NUM_VCPU_LOCAL_VIRQS) {
+        set_sgi_ppi_pending(gic_dist, irq, set_pending, vcpu_id);
+    } else {
+        set_spi_pending(gic_dist, irq, set_pending);
+    }
+}
+
+static inline bool is_sgi_ppi_pending(struct gic_dist_map *gic_dist, int irq, int vcpu_id)
+{
+    return !!(gic_dist->pending_set0[vcpu_id] & IRQ_BIT(irq));
+}
+
+static inline bool is_spi_pending(struct gic_dist_map *gic_dist, int irq)
+{
+    return !!(gic_dist->pending_set[IRQ_IDX(irq)] & IRQ_BIT(irq));
+}
+
+static inline bool is_pending(struct gic_dist_map *gic_dist, int irq, int vcpu_id)
+{
+    if (irq < NUM_VCPU_LOCAL_VIRQS) {
+        return is_sgi_ppi_pending(gic_dist, irq, vcpu_id);
+    } else {
+        return is_spi_pending(gic_dist, irq);
+    }
+}
+
+static inline void set_sgi_ppi_enable(struct gic_dist_map *gic_dist, int irq, bool set_enable, int vcpu_id)
+{
+    if (set_enable) {
+        gic_dist->enable_set0[vcpu_id] |= IRQ_BIT(irq);
+        gic_dist->enable_clr0[vcpu_id] |= IRQ_BIT(irq);
+    } else {
+        gic_dist->enable_set0[vcpu_id] &= ~IRQ_BIT(irq);
+        gic_dist->enable_clr0[vcpu_id] &= ~IRQ_BIT(irq);
+    }
+}
+
+static inline void set_spi_enable(struct gic_dist_map *gic_dist, int irq, bool set_enable)
+{
+    if (set_enable) {
+        gic_dist->enable_set[IRQ_IDX(irq)] |= IRQ_BIT(irq);
+        gic_dist->enable_clr[IRQ_IDX(irq)] |= IRQ_BIT(irq);
+    } else {
+        gic_dist->enable_set[IRQ_IDX(irq)] &= ~IRQ_BIT(irq);
+        gic_dist->enable_clr[IRQ_IDX(irq)] &= ~IRQ_BIT(irq);
+    }
+}
+
+static inline void set_enable(struct gic_dist_map *gic_dist, int irq, bool set_enable, int vcpu_id)
+{
+    if (irq < NUM_VCPU_LOCAL_VIRQS) {
+        set_sgi_ppi_enable(gic_dist, irq, set_enable, vcpu_id);
+    } else {
+        set_spi_enable(gic_dist, irq, set_enable);
+    }
+}
+
+static inline bool is_sgi_ppi_enabled(struct gic_dist_map *gic_dist, int irq, int vcpu_id)
+{
+    return !!(gic_dist->enable_set0[vcpu_id] & IRQ_BIT(irq));
+}
+
+static inline bool is_spi_enabled(struct gic_dist_map *gic_dist, int irq)
+{
+    return !!(gic_dist->enable_set[IRQ_IDX(irq)] & IRQ_BIT(irq));
+}
+
+static inline bool is_enabled(struct gic_dist_map *gic_dist, int irq, int vcpu_id)
+{
+    if (irq < NUM_VCPU_LOCAL_VIRQS) {
+        return is_sgi_ppi_enabled(gic_dist, irq, vcpu_id);
+    } else {
+        return is_spi_enabled(gic_dist, irq);
+    }
+}
+
+static inline bool is_sgi_ppi_active(struct gic_dist_map *gic_dist, int irq, int vcpu_id)
+{
+    return !!(gic_dist->active0[vcpu_id] & IRQ_BIT(irq));
+}
+
+static inline bool is_spi_active(struct gic_dist_map *gic_dist, int irq)
+{
+    return !!(gic_dist->active[IRQ_IDX(irq)] & IRQ_BIT(irq));
+}
+
+static inline bool is_active(struct gic_dist_map *gic_dist, int irq, int vcpu_id)
+{
+    if (irq < NUM_VCPU_LOCAL_VIRQS) {
+        return is_sgi_ppi_active(gic_dist, irq, vcpu_id);
+    } else {
+        return is_spi_active(gic_dist, irq);
+    }
+}
+
+static void vgic_dist_enable_irq(vgic_t *vgic, uint64_t vcpu_id, int irq)
+{
+    LOG_DIST("Enabling IRQ %d\n", irq);
+    set_enable(vgic_get_dist(vgic->registers), irq, true, vcpu_id);
+    struct virq_handle *virq_data = virq_find_irq_data(vgic, vcpu_id, irq);
+    // assert(virq_data != NULL);
+    // @ivanv: explain
+    if (!virq_data) {
+        return;
+    }
+    if (virq_data->virq != VIRQ_INVALID) {
+        /* STATE b) */
+        if (!is_pending(vgic_get_dist(vgic->registers), virq_data->virq, vcpu_id)) {
+            virq_ack(vcpu_id, virq_data);
+        }
+    } else {
+        LOG_DIST("Enabled IRQ %d has no handle\n", irq);
+    }
+}
+
+static void vgic_dist_disable_irq(vgic_t *vgic, uint64_t vcpu_id, int irq)
+{
+    /* STATE g)
+     *
+     * It is IMPLEMENTATION DEFINED if a GIC allows disabling SGIs. Our vGIC
+     * implementation does not allows it, such requests are simply ignored.
+     * Since it is not uncommon that a guest OS tries disabling SGIs, e.g. as
+     * part of the platform initialization, no dedicated messages are logged
+     * here to avoid bloating the logs.
+     */
+    if (irq >= NUM_SGI_VIRQS) {
+        LOG_DIST("Disabling IRQ %d\n", irq);
+        set_enable(vgic_get_dist(vgic->registers), irq, false, vcpu_id);
+    }
+}
+
+static bool vgic_dist_set_pending_irq(vgic_t *vgic, uint64_t vcpu_id, int irq)
+{
+    // @ivanv: I believe this function causes a fault in the VMM if the IRQ has not
+    // been registered. This is not good.
+    /* STATE c) */
+
+    struct virq_handle *virq_data = virq_find_irq_data(vgic, vcpu_id, irq);
+    struct gic_dist_map *dist = vgic_get_dist(vgic->registers);
+
+    if (virq_data->virq == VIRQ_INVALID || !vgic_dist_is_enabled(dist) || !is_enabled(dist, irq, vcpu_id)) {
+        if (virq_data->virq == VIRQ_INVALID) {
+            LOG_DIST("vIRQ data could not be found\n");
+        }
+        if (!vgic_dist_is_enabled(dist)) {
+            LOG_DIST("vGIC distributor is not enabled\n");
+        }
+        if (!is_enabled(dist, irq, vcpu_id)) {
+            LOG_DIST("vIRQ is not enabled\n");
+        }
+        return false;
+    }
+
+    if (is_pending(dist, virq_data->virq, vcpu_id)) {
+        // Do nothing if it's already pending
+        return true;
+    }
+
+    LOG_DIST("Pending set: Inject IRQ from pending set (%d)\n", irq);
+    set_pending(dist, virq_data->virq, true, vcpu_id);
+
+    /* Enqueueing an IRQ and dequeueing it right after makes little sense
+     * now, but in the future this is needed to support IRQ priorities.
+     */
+    bool success = vgic_irq_enqueue(vgic, vcpu_id, virq_data);
+    if (!success) {
+        LOG_VMM_ERR("Failure enqueueing IRQ, increase MAX_IRQ_QUEUE_LEN");
+        assert(0);
+        return false;
+    }
+
+    int idx = vgic_find_empty_list_reg(vgic, vcpu_id);
+    if (idx < 0) {
+        /* There were no empty list registers available, but that's not a big
+         * deal -- we have already enqueued this IRQ and eventually the vGIC
+         * maintenance code will load it to a list register from the queue.
+         */
+        return true;
+    }
+
+    struct virq_handle *virq = vgic_irq_dequeue(vgic, vcpu_id);
+    assert(virq->virq != VIRQ_INVALID);
+
+#if defined(GIC_V2)
+    int group = 0;
+#elif defined(GIC_V3)
+    int group = 1;
+#else
+#error "Unknown GIC version"
+#endif
+
+    // @ivanv: I don't understand why GIC v2 is group 0 and GIC v3 is group 1.
+    return vgic_vcpu_load_list_reg(vgic, vcpu_id, idx, group, virq);
+}
+
+static void vgic_dist_clr_pending_irq(struct gic_dist_map *dist, uint32_t vcpu_id, int irq)
+{
+    LOG_DIST("Clear pending IRQ %d\n", irq);
+    set_pending(dist, irq, false, vcpu_id);
+    /* TODO: remove from IRQ queue and list registers as well */
+    // @ivanv
+}
+
+static bool vgic_dist_reg_read(uint64_t vcpu_id, vgic_t *vgic, uint64_t offset, uint64_t fsr, seL4_UserContext *regs)
+{
+    bool success = false;
+    struct gic_dist_map *gic_dist = vgic_get_dist(vgic->registers);
+    uint32_t reg = 0;
+    int reg_offset = 0;
+    uintptr_t base_reg;
+    uint32_t *reg_ptr;
+    switch (offset) {
+    case RANGE32(GIC_DIST_CTLR, GIC_DIST_CTLR):
+        reg = gic_dist->ctlr;
+        break;
+    case RANGE32(GIC_DIST_TYPER, GIC_DIST_TYPER):
+        reg = gic_dist->typer;
+        break;
+    case RANGE32(GIC_DIST_IIDR, GIC_DIST_IIDR):
+        reg = gic_dist->iidr;
+        break;
+    case RANGE32(0x00C, 0x01C):
+        /* Reserved */
+        break;
+    case RANGE32(0x020, 0x03C):
+        /* IMPLEMENTATION DEFINED registers. */
+        break;
+    case RANGE32(0x040, 0x07C):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_IGROUPR0, GIC_DIST_IGROUPR0):
+        reg = gic_dist->irq_group0[vcpu_id];
+        break;
+    case RANGE32(GIC_DIST_IGROUPR1, GIC_DIST_IGROUPRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_IGROUPR1);
+        reg = gic_dist->irq_group[reg_offset];
+        break;
+    case RANGE32(GIC_DIST_ISENABLER0, GIC_DIST_ISENABLER0):
+        reg = gic_dist->enable_set0[vcpu_id];
+        break;
+    case RANGE32(GIC_DIST_ISENABLER1, GIC_DIST_ISENABLERN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ISENABLER1);
+        reg = gic_dist->enable_set[reg_offset];
+        break;
+    case RANGE32(GIC_DIST_ICENABLER0, GIC_DIST_ICENABLER0):
+        reg = gic_dist->enable_clr0[vcpu_id];
+        break;
+    case RANGE32(GIC_DIST_ICENABLER1, GIC_DIST_ICENABLERN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ICENABLER1);
+        reg = gic_dist->enable_clr[reg_offset];
+        break;
+    case RANGE32(GIC_DIST_ISPENDR0, GIC_DIST_ISPENDR0):
+        reg = gic_dist->pending_set0[vcpu_id];
+        break;
+    case RANGE32(GIC_DIST_ISPENDR1, GIC_DIST_ISPENDRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ISPENDR1);
+        reg = gic_dist->pending_set[reg_offset];
+        break;
+    case RANGE32(GIC_DIST_ICPENDR0, GIC_DIST_ICPENDR0):
+        reg = gic_dist->pending_clr0[vcpu_id];
+        break;
+    case RANGE32(GIC_DIST_ICPENDR1, GIC_DIST_ICPENDRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ICPENDR1);
+        reg = gic_dist->pending_clr[reg_offset];
+        break;
+    case RANGE32(GIC_DIST_ISACTIVER0, GIC_DIST_ISACTIVER0):
+        reg = gic_dist->active0[vcpu_id];
+        break;
+    case RANGE32(GIC_DIST_ISACTIVER1, GIC_DIST_ISACTIVERN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ISACTIVER1);
+        reg = gic_dist->active[reg_offset];
+        break;
+    case RANGE32(GIC_DIST_ICACTIVER0, GIC_DIST_ICACTIVER0):
+        reg = gic_dist->active_clr0[vcpu_id];
+        break;
+    case RANGE32(GIC_DIST_ICACTIVER1, GIC_DIST_ICACTIVERN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ICACTIVER1);
+        reg = gic_dist->active_clr[reg_offset];
+        break;
+    case RANGE32(GIC_DIST_IPRIORITYR0, GIC_DIST_IPRIORITYR7):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_IPRIORITYR0);
+        reg = gic_dist->priority0[vcpu_id][reg_offset];
+        break;
+    case RANGE32(GIC_DIST_IPRIORITYR8, GIC_DIST_IPRIORITYRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_IPRIORITYR8);
+        reg = gic_dist->priority[reg_offset];
+        break;
+    case RANGE32(0x7FC, 0x7FC):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_ITARGETSR0, GIC_DIST_ITARGETSR7):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ITARGETSR0);
+        reg = gic_dist->targets0[vcpu_id][reg_offset];
+        break;
+    case RANGE32(GIC_DIST_ITARGETSR8, GIC_DIST_ITARGETSRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ITARGETSR8);
+        reg = gic_dist->targets[reg_offset];
+        break;
+    case RANGE32(0xBFC, 0xBFC):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_ICFGR0, GIC_DIST_ICFGRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ICFGR0);
+        reg = gic_dist->config[reg_offset];
+        break;
+#if defined(GIC_V2)
+    case RANGE32(0xD00, 0xDE4):
+        /* IMPLEMENTATION DEFINED registers. */
+        base_reg = (uintptr_t) & (gic_dist->spi[0]);
+        reg_ptr = (uint32_t *)(base_reg + (offset - 0xD00));
+        reg = *reg_ptr;
+        break;
+#endif
+    case RANGE32(0xDE8, 0xEFC):
+        /* Reserved [0xDE8 - 0xE00) */
+        /* GIC_DIST_NSACR [0xE00 - 0xF00) - Not supported */
+        break; case RANGE32(GIC_DIST_SGIR, GIC_DIST_SGIR):
+        reg = gic_dist->sgir;
+        break;
+    case RANGE32(0xF04, 0xF0C):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_CPENDSGIR0, GIC_DIST_CPENDSGIRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_CPENDSGIR0);
+        reg = gic_dist->sgi_pending_clr[vcpu_id][reg_offset];
+        break;
+    case RANGE32(GIC_DIST_SPENDSGIR0, GIC_DIST_SPENDSGIRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_SPENDSGIR0);
+        reg = gic_dist->sgi_pending_set[vcpu_id][reg_offset];
+        break;
+    case RANGE32(0xF30, 0xFBC):
+        /* Reserved */
+        break;
+#if defined(GIC_V2)
+    // @ivanv: understand why this is GIC v2 specific and make a command so others can understand as well.
+    case RANGE32(0xFC0, 0xFFB):
+        base_reg = (uintptr_t) & (gic_dist->periph_id[0]);
+        reg_ptr = (uint32_t *)(base_reg + (offset - 0xFC0));
+        reg = *reg_ptr;
+        break;
+#endif
+#if defined(GIC_V3)
+    // @ivanv: Understand and comment GICv3 specific stuff
+    case RANGE32(0x6100, 0x7F00):
+        base_reg = (uintptr_t) & (gic_dist->irouter[0]);
+        reg_ptr = (uint32_t *)(base_reg + (offset - 0x6100));
+        reg = *reg_ptr;
+        break;
+
+    case RANGE32(0xFFD0, 0xFFFC):
+        base_reg = (uintptr_t) & (gic_dist->pidrn[0]);
+        reg_ptr = (uint32_t *)(base_reg + (offset - 0xFFD0));
+        reg = *reg_ptr;
+        break;
+#endif
+    default:
+        LOG_VMM_ERR("Unknown register offset 0x%x", offset);
+        // err = ignore_fault(fault);
+        success = fault_advance_vcpu(regs);
+        assert(success);
+        goto fault_return;
+    }
+    uint32_t mask = fault_get_data_mask(GIC_DIST_PADDR + offset, fsr);
+    // fault_set_data(fault, reg & mask);
+    // @ivanv: interesting, when we don't call fault_Set_data in the CAmkES VMM, everything works fine?...
+    success = fault_advance(regs, GIC_DIST_PADDR + offset, fsr, reg & mask);
+    assert(success);
+
+fault_return:
+    if (!success) {
+        printf("reg read success is false\n");
+    }
+    // @ivanv: revisit, also make fault_return consistint. it's called something else in vgic_dist_reg_write
+    return success;
+}
+
+static inline void emulate_reg_write_access(seL4_UserContext *regs, uint64_t addr, uint64_t fsr, uint32_t *reg)
+{
+    *reg = fault_emulate(regs, *reg, addr, fsr, fault_get_data(regs, fsr));
+}
+
+static bool vgic_dist_reg_write(uint64_t vcpu_id, vgic_t *vgic, uint64_t offset, uint64_t fsr, seL4_UserContext *regs)
+{
+    bool success = true;
+    struct gic_dist_map *gic_dist = vgic_get_dist(vgic->registers);
+    uint64_t addr = GIC_DIST_PADDR + offset;
+    uint32_t mask = fault_get_data_mask(addr, fsr);
+    uint32_t reg_offset = 0;
+    uint32_t data;
+    switch (offset) {
+    case RANGE32(GIC_DIST_CTLR, GIC_DIST_CTLR):
+        data = fault_get_data(regs, fsr);
+        if (data == GIC_ENABLED) {
+            vgic_dist_enable(gic_dist);
+        } else if (data == 0) {
+            vgic_dist_disable(gic_dist);
+        } else {
+            LOG_VMM_ERR("Unknown enable register encoding");
+            // @ivanv: goto ignore fault?
+        }
+        break;
+    case RANGE32(GIC_DIST_TYPER, GIC_DIST_TYPER):
+        /* TYPER provides information about the GIC configuration, we do not do
+         * anything here as there should be no reason for the guest to write to
+         * this register.
+         */
+        break;
+    case RANGE32(GIC_DIST_IIDR, GIC_DIST_IIDR):
+        /* IIDR provides information about the distributor's implementation, we
+         * do not do anything here as there should be no reason for the guest
+         * to write to this register.
+         */
+        break;
+    case RANGE32(0x00C, 0x01C):
+        /* Reserved */
+        break;
+    case RANGE32(0x020, 0x03C):
+        /* IMPLEMENTATION DEFINED registers. */
+        break;
+    case RANGE32(0x040, 0x07C):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_IGROUPR0, GIC_DIST_IGROUPR0):
+        emulate_reg_write_access(regs, addr, fsr, &gic_dist->irq_group0[vcpu_id]);
+        break;
+    case RANGE32(GIC_DIST_IGROUPR1, GIC_DIST_IGROUPRN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_IGROUPR1);
+        emulate_reg_write_access(regs, addr, fsr, &gic_dist->irq_group[reg_offset]);
+        break;
+    case RANGE32(GIC_DIST_ISENABLER0, GIC_DIST_ISENABLERN):
+        data = fault_get_data(regs, fsr);
+        /* Mask the data to write */
+        data &= mask;
+        while (data) {
+            int irq;
+            irq = CTZ(data);
+            data &= ~(1U << irq);
+            irq += (offset - GIC_DIST_ISENABLER0) * 8;
+            vgic_dist_enable_irq(vgic, vcpu_id, irq);
+        }
+        break;
+    case RANGE32(GIC_DIST_ICENABLER0, GIC_DIST_ICENABLERN):
+        data = fault_get_data(regs, fsr);
+        /* Mask the data to write */
+        data &= mask;
+        while (data) {
+            int irq;
+            irq = CTZ(data);
+            data &= ~(1U << irq);
+            irq += (offset - GIC_DIST_ICENABLER0) * 8;
+            vgic_dist_disable_irq(vgic, vcpu_id, irq);
+        }
+        break;
+    case RANGE32(GIC_DIST_ISPENDR0, GIC_DIST_ISPENDRN):
+        data = fault_get_data(regs, fsr);
+        /* Mask the data to write */
+        data &= mask;
+        while (data) {
+            int irq;
+            irq = CTZ(data);
+            data &= ~(1U << irq);
+            irq += (offset - GIC_DIST_ISPENDR0) * 8;
+            // @ivanv: should be checking this and other calls like it succeed
+            vgic_dist_set_pending_irq(vgic, vcpu_id, irq);
+        }
+        break;
+    case RANGE32(GIC_DIST_ICPENDR0, GIC_DIST_ICPENDRN):
+        data = fault_get_data(regs, fsr);
+        /* Mask the data to write */
+        data &= mask;
+        while (data) {
+            int irq;
+            irq = CTZ(data);
+            data &= ~(1U << irq);
+            irq += (offset - GIC_DIST_ICPENDR0) * 8;
+            vgic_dist_clr_pending_irq(gic_dist, vcpu_id, irq);
+        }
+        break;
+    case RANGE32(GIC_DIST_ISACTIVER0, GIC_DIST_ISACTIVER0):
+        emulate_reg_write_access(regs, addr, fsr, &gic_dist->active0[vcpu_id]);
+        break;
+    case RANGE32(GIC_DIST_ISACTIVER1, GIC_DIST_ISACTIVERN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ISACTIVER1);
+        emulate_reg_write_access(regs, addr, fsr, &gic_dist->active[reg_offset]);
+        break;
+    case RANGE32(GIC_DIST_ICACTIVER0, GIC_DIST_ICACTIVER0):
+        emulate_reg_write_access(regs, addr, fsr, &gic_dist->active_clr0[vcpu_id]);
+        break;
+    case RANGE32(GIC_DIST_ICACTIVER1, GIC_DIST_ICACTIVERN):
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ICACTIVER1);
+        emulate_reg_write_access(regs, addr, fsr, &gic_dist->active_clr[reg_offset]);
+        break;
+    case RANGE32(GIC_DIST_IPRIORITYR0, GIC_DIST_IPRIORITYRN):
+        break;
+    case RANGE32(0x7FC, 0x7FC):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_ITARGETSR0, GIC_DIST_ITARGETSRN):
+        break;
+    case RANGE32(0xBFC, 0xBFC):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_ICFGR0, GIC_DIST_ICFGRN):
+        /*
+         * Emulate accesses to interrupt configuration registers to set the IRQ
+         * to be edge-triggered or level-sensitive.
+         */
+        reg_offset = GIC_DIST_REGN(offset, GIC_DIST_ICFGR0);
+        emulate_reg_write_access(regs, addr, fsr, &gic_dist->config[reg_offset]);
+        break;
+    case RANGE32(0xD00, 0xDFC):
+        /* IMPLEMENTATION DEFINED registers. */
+        break;
+    case RANGE32(0xE00, 0xEFC):
+        /* GIC_DIST_NSACR [0xE00 - 0xF00) - Not supported */
+        break;
+    case RANGE32(GIC_DIST_SGIR, GIC_DIST_SGIR):
+        data = fault_get_data(regs, fsr);
+        int mode = (data & GIC_DIST_SGI_TARGET_LIST_FILTER_MASK) >> GIC_DIST_SGI_TARGET_LIST_FILTER_SHIFT;
+        int virq = (data & GIC_DIST_SGI_INTID_MASK);
+        uint16_t target_list = 0;
+        switch (mode) {
+        case GIC_DIST_SGI_TARGET_LIST_SPEC:
+            /* Forward VIRQ to VCPUs specified in CPUTargetList */
+            target_list = (data & GIC_DIST_SGI_CPU_TARGET_LIST_MASK) >> GIC_DIST_SGI_CPU_TARGET_LIST_SHIFT;
+            break;
+        case GIC_DIST_SGI_TARGET_LIST_OTHERS:
+            /* Forward virq to all VCPUs except the requesting VCPU */
+            target_list = (1 << GUEST_NUM_VCPUS) - 1;
+            target_list = target_list & ~(1 << vcpu_id);
+            break;
+        case GIC_DIST_SGI_TARGET_SELF:
+            /* Forward to virq to only the requesting vcpu */
+            target_list = (1 << vcpu_id);
+            break;
+        default:
+            LOG_VMM_ERR("Unknown SGIR Target List Filter mode");
+            goto ignore_fault;
+        }
+        // @ivanv: Here we're making the assumption that there's only one vCPU, and
+        // we're also blindly injectnig the given IRQ to that vCPU.
+        // @ivanv: come back to this, do we have two writes to the TCB registers?
+        success = vgic_inject_irq(vcpu_id, virq);
+        assert(success);
+        break;
+    case RANGE32(0xF04, 0xF0C):
+        /* Reserved */
+        break;
+    case RANGE32(GIC_DIST_CPENDSGIR0, GIC_DIST_SPENDSGIRN):
+        // @ivanv: come back to
+        assert(!"vgic SGI reg not implemented!\n");
+        break;
+    case RANGE32(0xF30, 0xFBC):
+        /* Reserved */
+        break;
+    case RANGE32(0xFC0, 0xFFC):
+        // @ivanv: GICv2 specific, GICv3 has different range for impl defined registers.
+        /* IMPLEMENTATION DEFINED registers. */
+        break;
+#if defined(GIC_V3)
+    // @ivanv: explain GICv3 specific stuff, and also don't use the hardcoded valuees
+    case RANGE32(0x6100, 0x7F00):
+    // @ivanv revisit
+        // data = fault_get_data(fault);
+        // ZF_LOGF_IF(data, "bad dist: 0x%x 0x%x", offset, data);
+        break;
+#endif
+    default:
+        LOG_VMM_ERR("Unknown register offset 0x%x", offset);
+        assert(0);
+    }
+ignore_fault:
+    assert(success);
+    if (!success) {
+        return false;
+    }
+
+    success = fault_advance_vcpu(regs);
+    assert(success);
+
+    return success;
+}
+

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic.c

@@ -0,0 +1,119 @@
+/* @ivanv double check
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <microkit.h>
+#include "vgic.h"
+#include "virq.h"
+#include "../util/util.h"
+#include "../fault.h"
+
+#if defined(GIC_V2)
+#include "vgic_v2.h"
+#elif defined(GIC_V3)
+#include "vgic_v3.h"
+#else
+#error "Unknown GIC version"
+#endif
+
+#include "vdist.h"
+
+/* The driver expects the VGIC state to be initialised before calling any of the driver functionality. */
+extern vgic_t vgic;
+
+bool handle_vgic_maintenance(uint64_t vcpu_id)
+{
+    // @ivanv: reivist, also inconsistency between int and bool
+    bool success = true;
+    int idx = microkit_mr_get(seL4_VGICMaintenance_IDX);
+    /* Currently not handling spurious IRQs */
+    // @ivanv: wtf, this comment seems irrelevant to the code.
+    assert(idx >= 0);
+
+    // @ivanv: Revisit and make sure it's still correct.
+    vgic_vcpu_t *vgic_vcpu = get_vgic_vcpu(&vgic, vcpu_id);
+    assert(vgic_vcpu);
+    assert((idx >= 0) && (idx < ARRAY_SIZE(vgic_vcpu->lr_shadow)));
+    struct virq_handle *slot = &vgic_vcpu->lr_shadow[idx];
+    assert(slot->virq != VIRQ_INVALID);
+    struct virq_handle lr_virq = *slot;
+    slot->virq = VIRQ_INVALID;
+    slot->ack_fn = NULL;
+    slot->ack_data = NULL;
+    /* Clear pending */
+    LOG_IRQ("Maintenance IRQ %d\n", lr_virq.virq);
+    set_pending(vgic_get_dist(vgic.registers), lr_virq.virq, false, vcpu_id);
+    virq_ack(vcpu_id, &lr_virq);
+    /* Check the overflow list for pending IRQs */
+    struct virq_handle *virq = vgic_irq_dequeue(&vgic, vcpu_id);
+
+#if defined(GIC_V2)
+    int group = 0;
+#elif defined(GIC_V3)
+    int group = 1;
+#else
+#error "Unknown GIC version"
+#endif
+
+    if (virq) {
+        success = vgic_vcpu_load_list_reg(&vgic, vcpu_id, idx, group, virq);
+    }
+
+    if (!success) {
+        printf("VGIC|ERROR: maintenance handler failed\n");
+        assert(0);
+    }
+
+    return success;
+}
+
+// @ivanv: maybe this shouldn't be here?
+bool vgic_register_irq(uint64_t vcpu_id, int virq_num, irq_ack_fn_t ack_fn, void *ack_data) {
+    assert(virq_num >= 0 && virq_num != VIRQ_INVALID);
+    struct virq_handle virq = {
+        .virq = virq_num,
+        .ack_fn = ack_fn,
+        .ack_data = ack_data,
+    };
+
+    return virq_add(vcpu_id, &vgic, &virq);
+}
+
+bool vgic_inject_irq(uint64_t vcpu_id, int irq)
+{
+    LOG_IRQ("Injecting IRQ %d\n", irq);
+
+    return vgic_dist_set_pending_irq(&vgic, vcpu_id, irq);
+
+    // @ivanv: explain why we don't check error before checking this fault stuff
+    // @ivanv: seperately, it seems weird to have this fault handling code here?
+    // @ivanv: revist
+    // if (!fault_handled(vcpu->vcpu_arch.fault) && fault_is_wfi(vcpu->vcpu_arch.fault)) {
+    //     // ignore_fault(vcpu->vcpu_arch.fault);
+    //     err = advance_vcpu_fault(regs);
+    // }
+}
+
+// @ivanv: revisit this whole function
+bool handle_vgic_dist_fault(uint64_t vcpu_id, uint64_t fault_addr, uint64_t fsr, seL4_UserContext *regs)
+{
+    /* Make sure that the fault address actually lies within the GIC distributor region. */
+    assert(fault_addr >= GIC_DIST_PADDR);
+    assert(fault_addr - GIC_DIST_PADDR < GIC_DIST_SIZE);
+
+    uint64_t offset = fault_addr - GIC_DIST_PADDR;
+    bool success = false;
+    if (fault_is_read(fsr)) {
+        // printf("VGIC|INFO: Read dist\n");
+        success = vgic_dist_reg_read(vcpu_id, &vgic, offset, fsr, regs);
+        assert(success);
+    } else {
+        // printf("VGIC|INFO: Write dist\n");
+        success = vgic_dist_reg_write(vcpu_id, &vgic, offset, fsr, regs);
+        assert(success);
+    }
+
+    return success;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic.h

@@ -0,0 +1,65 @@
+/*
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <microkit.h>
+#include <stdbool.h>
+#include <stdint.h>
+
+// @ivanv: this should all come from the DTS!
+#if defined(BOARD_qemu_virt_aarch64)
+#define GIC_V2
+#define GIC_DIST_PADDR      0x8000000
+#elif defined(BOARD_odroidc2_hyp)
+#define GIC_V2
+#define GIC_DIST_PADDR      0xc4301000
+#elif defined(BOARD_odroidc4_hyp)
+#define GIC_V2
+#define GIC_DIST_PADDR      0xffc01000
+#elif defined(BOARD_rpi4b_hyp)
+#define GIC_V2
+#define GIC_DIST_PADDR      0xff841000
+#elif defined(BOARD_imx8mm_evk_hyp)
+#define GIC_V3
+#define GIC_DIST_PADDR      0x38800000
+#define GIC_REDIST_PADDR    0x38880000
+#else
+#error Need to define GIC addresses
+#endif
+
+#if defined(GIC_V2)
+#define GIC_DIST_SIZE 0x1000
+#elif defined(GIC_V3)
+#define GIC_DIST_SIZE       0x10000
+#define GIC_REDIST_SIZE     0xc0000
+#else
+#error Unknown GIC version
+#endif
+
+/* Uncomment these defines for more verbose logging in the GIC driver. */
+// #define DEBUG_IRQ
+// #define DEBUG_DIST
+
+#if defined(DEBUG_IRQ)
+#define LOG_IRQ(...) do{ printf("VGIC|IRQ: "); printf(__VA_ARGS__); }while(0)
+#else
+#define LOG_IRQ(...) do{}while(0)
+#endif
+
+#if defined(DEBUG_DIST)
+#define LOG_DIST(...) do{ printf("VGIC|DIST: "); printf(__VA_ARGS__); }while(0)
+#else
+#define LOG_DIST(...) do{}while(0)
+#endif
+
+typedef void (*irq_ack_fn_t)(uint64_t vcpu_id, int irq, void *cookie);
+
+void vgic_init();
+bool handle_vgic_maintenance(uint64_t vcpu_id);
+bool handle_vgic_dist_fault(uint64_t vcpu_id, uint64_t fault_addr, uint64_t fsr, seL4_UserContext *regs);
+bool handle_vgic_redist_fault(uint64_t vcpu_id, uint64_t fault_addr, uint64_t fsr, seL4_UserContext *regs);
+bool vgic_register_irq(uint64_t vcpu_id, int virq_num, irq_ack_fn_t ack_fn, void *ack_data);
+bool vgic_inject_irq(uint64_t vcpu_id, int irq);

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v2.c

@@ -0,0 +1,131 @@
+/*
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+/*
+ * This file controls and maintains the virtualised GICv2 device for the VM. The spec used is: @ivanv
+ * IRQs must be registered at initialisation using the function: vm_register_irq
+ *
+ * @ivanv: talk about what features this driver actually implements
+ * This driver supports multiple vCPUs.
+ *
+ * This function creates and registers an IRQ data structure which will be used for IRQ maintenance
+ * b) ENABLING: When the VM enables the IRQ, it checks the pending flag for the VM.
+ *   - If the IRQ is not pending, we either
+ *        1) have not received an IRQ so it is still enabled in seL4
+ *        2) have received an IRQ, but ignored it because the VM had disabled it.
+ *     In either case, we simply ACK the IRQ with seL4. In case 1), the IRQ will come straight through,
+       in case 2), we have ACKed an IRQ that was not yet pending anyway.
+ *   - If the IRQ is already pending, we can assume that the VM has yet to ACK the IRQ and take no further
+ *     action.
+ *   Transitions: b->c
+ * c) PIRQ: When an IRQ is received from seL4, seL4 disables the IRQ and sends an async message. When the VMM
+ *    receives the message.
+ *   - If the IRQ is enabled, we set the pending flag in the VM and inject the appropriate IRQ
+ *     leading to state d)
+ *   - If the IRQ is disabled, the VMM takes no further action, leading to state b)
+ *   Transitions: (enabled)? c->d :  c->b
+ * d) When the VM acknowledges the IRQ, an exception is raised and delivered to the VMM. When the VMM
+ *    receives the exception, it clears the pending flag and acks the IRQ with seL4, leading back to state c)
+ *    Transition: d->c
+ * g) When/if the VM disables the IRQ, we may still have an IRQ resident in the GIC. We allow
+ *    this IRQ to be delivered to the VM, but subsequent IRQs will not be delivered as seen by state c)
+ *    Transitions g->c
+ *
+ *   NOTE: There is a big assumption that the VM will not manually manipulate our pending flags and
+ *         destroy our state. The affects of this will be an IRQ that is never acknowledged and hence,
+ *         will never occur again.
+ */
+
+#include <stdint.h>
+#include <microkit.h>
+
+#include "vgic.h"
+#include "vgic_v2.h"
+#include "virq.h"
+#include "vdist.h"
+#include "../util/util.h"
+#include "../fault.h"
+
+vgic_t vgic;
+struct gic_dist_map dist;
+
+static void vgic_dist_reset(struct gic_dist_map *gic_dist)
+{
+    gic_dist->typer = 0x0000fce7; /* RO */
+    gic_dist->iidr = 0x0200043b; /* RO */
+
+    for (int i = 0; i < CONFIG_MAX_NUM_NODES; i++) {
+        gic_dist->enable_set0[i] = 0x0000ffff; /* 16bit RO */
+        gic_dist->enable_clr0[i] = 0x0000ffff; /* 16bit RO */
+    }
+
+    /* Reset value depends on GIC configuration */
+    gic_dist->config[0]       = 0xaaaaaaaa; /* RO */
+    gic_dist->config[1]       = 0x55540000;
+    gic_dist->config[2]       = 0x55555555;
+    gic_dist->config[3]       = 0x55555555;
+    gic_dist->config[4]       = 0x55555555;
+    gic_dist->config[5]       = 0x55555555;
+    gic_dist->config[6]       = 0x55555555;
+    gic_dist->config[7]       = 0x55555555;
+    gic_dist->config[8]       = 0x55555555;
+    gic_dist->config[9]       = 0x55555555;
+    gic_dist->config[10]      = 0x55555555;
+    gic_dist->config[11]      = 0x55555555;
+    gic_dist->config[12]      = 0x55555555;
+    gic_dist->config[13]      = 0x55555555;
+    gic_dist->config[14]      = 0x55555555;
+    gic_dist->config[15]      = 0x55555555;
+
+    /* Configure per-processor SGI/PPI target registers */
+    for (int i = 0; i < CONFIG_MAX_NUM_NODES; i++) {
+        for (int j = 0; j < ARRAY_SIZE(gic_dist->targets0[i]); j++) {
+            for (int irq = 0; irq < sizeof(uint32_t); irq++) {
+                gic_dist->targets0[i][j] |= ((1 << i) << (irq * 8));
+            }
+        }
+    }
+    /* Deliver the SPI interrupts to the first CPU interface */
+    for (int i = 0; i < ARRAY_SIZE(gic_dist->targets); i++) {
+        gic_dist->targets[i] = 0x1010101;
+    }
+
+    /* identification */
+    gic_dist->periph_id[4]    = 0x00000004; /* RO */
+    gic_dist->periph_id[8]    = 0x00000090; /* RO */
+    gic_dist->periph_id[9]    = 0x000000b4; /* RO */
+    gic_dist->periph_id[10]   = 0x0000002b; /* RO */
+    gic_dist->component_id[0] = 0x0000000d; /* RO */
+    gic_dist->component_id[1] = 0x000000f0; /* RO */
+    gic_dist->component_id[2] = 0x00000005; /* RO */
+    gic_dist->component_id[3] = 0x000000b1; /* RO */
+}
+
+void vgic_init()
+{
+    memset(&vgic, 0, sizeof(vgic_t));
+    for (int i = 0; i < NUM_SLOTS_SPI_VIRQ; i++) {
+        vgic.vspis[i].virq = VIRQ_INVALID;
+    }
+    for (int i = 0; i < NUM_VCPU_LOCAL_VIRQS; i++) {
+        vgic.vgic_vcpu[GUEST_VCPU_ID].local_virqs[i].virq = VIRQ_INVALID;
+    }
+    for (int i = 0; i < NUM_LIST_REGS; i++) {
+        vgic.vgic_vcpu[GUEST_VCPU_ID].lr_shadow[i].virq = VIRQ_INVALID;
+    }
+    for (int i = 0; i < MAX_IRQ_QUEUE_LEN; i++) {
+        vgic.vgic_vcpu[GUEST_VCPU_ID].irq_queue.irqs[i] = NULL;
+    }
+    for (int i = 0; i < NUM_SLOTS_SPI_VIRQ; i++) {
+        vgic.vspis[i].virq = VIRQ_INVALID;
+        vgic.vspis[i].ack_fn = NULL;
+        vgic.vspis[i].ack_data = NULL;
+    }
+    vgic.registers = &dist;
+    memset(vgic.registers, 0, sizeof(struct gic_dist_map));
+    vgic_dist_reset(vgic_get_dist(vgic.registers));
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v2.h

@@ -0,0 +1,166 @@
+/*
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+
+#include <stdint.h>
+#include "../util/util.h"
+
+#define GIC_ENABLED 1
+
+/*
+ * This the memory map for the GIC distributor.
+ *
+ * You will note that some of these registers in the memory map are actually
+ * arrays with the length of the number of virtual CPUs that the guest has.
+ * The reason for this has to do with the fact that we are virtualising the GIC
+ * distributor. In actual hardware, these registers would be banked, meaning
+ * that the value of each register depends on the CPU that is accessing it.
+ * However, since we are dealing with virutal CPUs, we have to make the
+ * registers appear as if they are banked. You should note that the commented
+ * address offsets listed on the right of each register are the offset from the
+ * *guest's* perspective.
+ *
+ */
+struct gic_dist_map {
+    uint32_t ctlr;                                  /* 0x000 */
+    uint32_t typer;                                 /* 0x004 */
+    uint32_t iidr;                                  /* 0x008 */
+
+    uint32_t res1[29];                              /* [0x00C, 0x080) */
+
+    uint32_t irq_group0[GUEST_NUM_VCPUS];           /* [0x080, 0x84) */
+    uint32_t irq_group[31];                         /* [0x084, 0x100) */
+    uint32_t enable_set0[GUEST_NUM_VCPUS];          /* [0x100, 0x104) */
+    uint32_t enable_set[31];                        /* [0x104, 0x180) */
+    uint32_t enable_clr0[GUEST_NUM_VCPUS];          /* [0x180, 0x184) */
+    uint32_t enable_clr[31];                        /* [0x184, 0x200) */
+    uint32_t pending_set0[GUEST_NUM_VCPUS];         /* [0x200, 0x204) */
+    uint32_t pending_set[31];                       /* [0x204, 0x280) */
+    uint32_t pending_clr0[GUEST_NUM_VCPUS];         /* [0x280, 0x284) */
+    uint32_t pending_clr[31];                       /* [0x284, 0x300) */
+    uint32_t active0[GUEST_NUM_VCPUS];              /* [0x300, 0x304) */
+    uint32_t active[31];                            /* [0x300, 0x380) */
+    uint32_t active_clr0[GUEST_NUM_VCPUS];          /* [0x380, 0x384) */
+    uint32_t active_clr[31];                        /* [0x384, 0x400) */
+    uint32_t priority0[GUEST_NUM_VCPUS][8];         /* [0x400, 0x420) */
+    uint32_t priority[247];                         /* [0x420, 0x7FC) */
+    uint32_t res3;                                  /* 0x7FC */
+
+    uint32_t targets0[GUEST_NUM_VCPUS][8];          /* [0x800, 0x820) */
+    uint32_t targets[247];                          /* [0x820, 0xBFC) */
+    uint32_t res4;                                  /* 0xBFC */
+
+    uint32_t config[64];                            /* [0xC00, 0xD00) */
+
+    uint32_t spi[32];                               /* [0xD00, 0xD80) */
+    uint32_t res5[20];                              /* [0xD80, 0xDD0) */
+    uint32_t res6;                                  /* 0xDD0 */
+    uint32_t legacy_int;                            /* 0xDD4 */
+    uint32_t res7[2];                               /* [0xDD8, 0xDE0) */
+    uint32_t match_d;                               /* 0xDE0 */
+    uint32_t enable_d;                              /* 0xDE4 */
+    uint32_t res8[70];                              /* [0xDE8, 0xF00) */
+
+    uint32_t sgir;                                  /* 0xF00 */
+    uint32_t res9[3];                               /* [0xF04, 0xF10) */
+
+    uint32_t sgi_pending_clr[GUEST_NUM_VCPUS][4];   /* [0xF10, 0xF20) */
+    uint32_t sgi_pending_set[GUEST_NUM_VCPUS][4];   /* [0xF20, 0xF30) */
+    uint32_t res10[40];                             /* [0xF30, 0xFC0) */
+
+    uint32_t periph_id[12];                         /* [0xFC0, 0xFF0) */
+    uint32_t component_id[4];                       /* [0xFF0, 0xFFF] */
+};
+
+/*
+ * GIC Distributor Register Map
+ * ARM Generic Interrupt Controller (Architecture version 2.0)
+ * Architecture Specification (Issue B.b)
+ * Chapter 4 Programmers' Model - Table 4.1
+ */
+#define GIC_DIST_CTLR           0x000
+#define GIC_DIST_TYPER          0x004
+#define GIC_DIST_IIDR           0x008
+#define GIC_DIST_IGROUPR0       0x080
+#define GIC_DIST_IGROUPR1       0x084
+#define GIC_DIST_IGROUPRN       0x0FC
+#define GIC_DIST_ISENABLER0     0x100
+#define GIC_DIST_ISENABLER1     0x104
+#define GIC_DIST_ISENABLERN     0x17C
+#define GIC_DIST_ICENABLER0     0x180
+#define GIC_DIST_ICENABLER1     0x184
+#define GIC_DIST_ICENABLERN     0x1fC
+#define GIC_DIST_ISPENDR0       0x200
+#define GIC_DIST_ISPENDR1       0x204
+#define GIC_DIST_ISPENDRN       0x27C
+#define GIC_DIST_ICPENDR0       0x280
+#define GIC_DIST_ICPENDR1       0x284
+#define GIC_DIST_ICPENDRN       0x2FC
+#define GIC_DIST_ISACTIVER0     0x300
+#define GIC_DIST_ISACTIVER1     0x304
+#define GIC_DIST_ISACTIVERN     0x37C
+#define GIC_DIST_ICACTIVER0     0x380
+#define GIC_DIST_ICACTIVER1     0x384
+#define GIC_DIST_ICACTIVERN     0x3FC
+#define GIC_DIST_IPRIORITYR0    0x400
+#define GIC_DIST_IPRIORITYR7    0x41C
+#define GIC_DIST_IPRIORITYR8    0x420
+#define GIC_DIST_IPRIORITYRN    0x7F8
+#define GIC_DIST_ITARGETSR0     0x800
+#define GIC_DIST_ITARGETSR7     0x81C
+#define GIC_DIST_ITARGETSR8     0x820
+#define GIC_DIST_ITARGETSRN     0xBF8
+#define GIC_DIST_ICFGR0         0xC00
+#define GIC_DIST_ICFGRN         0xCFC
+#define GIC_DIST_NSACR0         0xE00
+#define GIC_DIST_NSACRN         0xEFC
+#define GIC_DIST_SGIR           0xF00
+#define GIC_DIST_CPENDSGIR0     0xF10
+#define GIC_DIST_CPENDSGIRN     0xF1C
+#define GIC_DIST_SPENDSGIR0     0xF20
+#define GIC_DIST_SPENDSGIRN     0xF2C
+
+/*
+ * ARM Generic Interrupt Controller (Architecture version 2.0)
+ * Architecture Specification (Issue B.b)
+ * 4.3.15: Software Generated Interrupt Register, GICD_SGI
+ * Values defined as per Table 4-21 (GICD_SGIR bit assignments)
+ */
+#define GIC_DIST_SGI_TARGET_LIST_FILTER_SHIFT   24
+#define GIC_DIST_SGI_TARGET_LIST_FILTER_MASK    0x3 << GIC_DIST_SGI_TARGET_LIST_FILTER_SHIFT
+#define GIC_DIST_SGI_TARGET_LIST_SPEC           0
+#define GIC_DIST_SGI_TARGET_LIST_OTHERS         1
+#define GIC_DIST_SGI_TARGET_SELF                2
+
+#define GIC_DIST_SGI_CPU_TARGET_LIST_SHIFT      16
+#define GIC_DIST_SGI_CPU_TARGET_LIST_MASK       0xFF << GIC_DIST_SGI_CPU_TARGET_LIST_SHIFT
+
+#define GIC_DIST_SGI_INTID_MASK                 0xF
+
+bool vgic_inject_irq(uint64_t vcpu_id, int irq);
+
+typedef struct gic_dist_map vgic_reg_t;
+
+static inline struct gic_dist_map *vgic_get_dist(void *registers)
+{
+    return (struct gic_dist_map *) registers;
+}
+
+static inline bool vgic_dist_is_enabled(struct gic_dist_map *gic_dist)
+{
+    return gic_dist->ctlr == GIC_ENABLED;
+}
+
+static inline void vgic_dist_enable(struct gic_dist_map *gic_dist) {
+    gic_dist->ctlr = GIC_ENABLED;
+}
+
+static inline void vgic_dist_disable(struct gic_dist_map *gic_dist)
+{
+    gic_dist->ctlr = 0;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v3.c

@@ -0,0 +1,232 @@
+/*
+ * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+/*
+ * This component controls and maintains the GIC for the VM.
+ * IRQs must be registered at init time with vm_virq_new(...)
+ * This function creates and registers an IRQ data structure which will be used for IRQ maintenance
+ * b) ENABLING: When the VM enables the IRQ, it checks the pending flag for the VM.
+ *   - If the IRQ is not pending, we either
+ *        1) have not received an IRQ so it is still enabled in seL4
+ *        2) have received an IRQ, but ignored it because the VM had disabled it.
+ *     In either case, we simply ACK the IRQ with seL4. In case 1), the IRQ will come straight through,
+       in case 2), we have ACKed an IRQ that was not yet pending anyway.
+ *   - If the IRQ is already pending, we can assume that the VM has yet to ACK the IRQ and take no further
+ *     action.
+ *   Transitions: b->c
+ * c) PIRQ: When an IRQ is received from seL4, seL4 disables the IRQ and sends an async message. When the VMM
+ *    receives the message.
+ *   - If the IRQ is enabled, we set the pending flag in the VM and inject the appropriate IRQ
+ *     leading to state d)
+ *   - If the IRQ is disabled, the VMM takes no further action, leading to state b)
+ *   Transitions: (enabled)? c->d :  c->b
+ * d) When the VM acknowledges the IRQ, an exception is raised and delivered to the VMM. When the VMM
+ *    receives the exception, it clears the pending flag and acks the IRQ with seL4, leading back to state c)
+ *    Transition: d->c
+ * g) When/if the VM disables the IRQ, we may still have an IRQ resident in the GIC. We allow
+ *    this IRQ to be delivered to the VM, but subsequent IRQs will not be delivered as seen by state c)
+ *    Transitions g->c
+ *
+ *   NOTE: There is a big assumption that the VM will not manually manipulate our pending flags and
+ *         destroy our state. The affects of this will be an IRQ that is never acknowledged and hence,
+ *         will never occur again.
+ */
+
+#include "vgic.h"
+
+#include <stdint.h>
+
+#include "../fault.h"
+#include "virq.h"
+#include "vgic_v3.h"
+#include "vdist.h"
+
+vgic_t vgic;
+
+static bool handle_vgic_redist_read_fault(uint64_t vcpu_id, vgic_t *vgic, uint64_t offset, uint64_t fsr, seL4_UserContext *regs)
+{
+    int err = 0;
+    struct gic_dist_map *gic_dist = vgic_get_dist(vgic->registers);
+    struct gic_redist_map *gic_redist = vgic_get_redist(vgic->registers);
+    uint32_t reg = 0;
+    uintptr_t base_reg;
+    uint32_t *reg_ptr;
+    switch (offset) {
+    case RANGE32(GICR_CTLR, GICR_CTLR):
+        reg = gic_redist->ctlr;
+        break;
+    case RANGE32(GICR_IIDR, GICR_IIDR):
+        reg = gic_redist->iidr;
+        break;
+    case RANGE32(GICR_TYPER, GICR_TYPER):
+        reg = gic_redist->typer;
+        break;
+    case RANGE32(GICR_WAKER, GICR_WAKER):
+        reg = gic_redist->waker;
+        break;
+    case RANGE32(0xFFD0, 0xFFFC):
+        base_reg = (uintptr_t) & (gic_redist->pidr4);
+        reg_ptr = (uint32_t *)(base_reg + (offset - 0xFFD0));
+        reg = *reg_ptr;
+        break;
+    case RANGE32(GICR_IGROUPR0, GICR_IGROUPR0):
+        base_reg = (uintptr_t) & (gic_dist->irq_group0[vcpu_id]);
+        reg_ptr = (uint32_t *)(base_reg + (offset - GICR_IGROUPR0));
+        reg = *reg_ptr;
+        break;
+    case RANGE32(GICR_ICFGR1, GICR_ICFGR1):
+        base_reg = (uintptr_t) & (gic_dist->config[1]);
+        reg_ptr = (uint32_t *)(base_reg + (offset - GICR_ICFGR1));
+        reg = *reg_ptr;
+        break;
+    default:
+        LOG_VMM_ERR("Unknown register offset 0x%x\n", offset);
+        // @ivanv: used to be ignore_fault, double check this is right
+        success = fault_advance_vcpu(regs);
+        goto fault_return;
+    }
+
+    uintptr_t fault_addr = GIC_REDIST_PADDR + offset;
+    uint32_t mask = fault_get_data_mask(fault_addr, fsr);
+    success = fault_advance(regs, fault_addr, fsr, reg & mask);
+
+fault_return:
+    return success;
+}
+
+
+static bool handle_vgic_redist_write_fault(uint64_t vcpu_id, vgic_t *vgic, uint64_t offset, uint64_t fsr, seL4_UserContext *regs)
+{
+    // @ivanv: why is this not reading from the redist?
+    uintptr_t fault_addr = GIC_REDIST_PADDR + offset;
+    struct gic_dist_map *gic_dist = vgic_get_dist(vgic->registers);
+    uint32_t mask = fault_get_data_mask(GIC_REDIST_PADDR + offset, fsr);
+    uint32_t data;
+    switch (offset) {
+    case RANGE32(GICR_WAKER, GICR_WAKER):
+        /* Writes are ignored */
+        break;
+    case RANGE32(GICR_IGROUPR0, GICR_IGROUPR0):
+        emulate_reg_write_access(regs, fault_addr, fsr, &gic_dist->irq_group0[vcpu_id]);
+        break;
+    case RANGE32(GICR_ISENABLER0, GICR_ISENABLER0):
+        data = fault_get_data(regs, fsr);
+        /* Mask the data to write */
+        data &= mask;
+        while (data) {
+            int irq;
+            irq = CTZ(data);
+            data &= ~(1U << irq);
+            vgic_dist_enable_irq(vgic, vcpu_id, irq);
+        }
+        break;
+    case RANGE32(GICR_ICENABLER0, GICR_ICENABLER0):
+        data = fault_get_data(regs, fsr);
+        /* Mask the data to write */
+        data &= mask;
+        while (data) {
+            int irq;
+            irq = CTZ(data);
+            data &= ~(1U << irq);
+            set_enable(gic_dist, irq, false, vcpu_id);
+        }
+        break;
+    case RANGE32(GICR_ICACTIVER0, GICR_ICACTIVER0):
+    // @ivanv: understand, this is a comment left over from kent
+    // TODO fix this
+        emulate_reg_write_access(regs, fault_addr, fsr, &gic_dist->active0[vcpu_id]);
+        break;
+    case RANGE32(GICR_IPRIORITYR0, GICR_IPRIORITYRN):
+        break;
+    default:
+        LOG_VMM_ERR("Unknown register offset 0x%x, value: 0x%x\n", offset, fault_get_data(regs, fsr));
+    }
+
+    int err = fault_advance_vcpu(regs);
+    assert(!err);
+    if (err) {
+        return false;
+    }
+
+    return true;
+}
+
+bool handle_vgic_redist_fault(uint64_t vcpu_id, uint64_t fault_addr, uint64_t fsr, seL4_UserContext *regs) {
+    assert(fault_addr >= GIC_REDIST_PADDR);
+    uint64_t offset = fault_addr - GIC_REDIST_PADDR;
+    assert(offset < GIC_REDIST_SIZE);
+
+    if (fault_is_read(fsr)) {
+        return handle_vgic_redist_read_fault(vcpu_id, &vgic, offset, fsr, regs);
+    } else {
+        return handle_vgic_redist_write_fault(vcpu_id, &vgic, offset, fsr, regs);
+    }
+}
+
+static void vgic_dist_reset(struct gic_dist_map *dist)
+{
+    // @ivanv: come back to, right now it's a global so we don't need to init the memory to zero
+    // memset(gic_dist, 0, sizeof(*gic_dist));
+
+    dist->typer            = 0x7B04B0; /* RO */
+    dist->iidr             = 0x1043B ; /* RO */
+
+    dist->enable_set[0]    = 0x0000ffff; /* 16bit RO */
+    dist->enable_clr[0]    = 0x0000ffff; /* 16bit RO */
+
+    dist->config[0]        = 0xaaaaaaaa; /* RO */
+
+    dist->pidrn[0]         = 0x44;     /* RO */
+    dist->pidrn[4]         = 0x92;     /* RO */
+    dist->pidrn[5]         = 0xB4;     /* RO */
+    dist->pidrn[6]         = 0x3B;     /* RO */
+
+    dist->cidrn[0]         = 0x0D;     /* RO */
+    dist->cidrn[1]         = 0xF0;     /* RO */
+    dist->cidrn[2]         = 0x05;     /* RO */
+    dist->cidrn[3]         = 0xB1;     /* RO */
+}
+
+static void vgic_redist_reset(struct gic_redist_map *redist) {
+    // @ivanv: come back to, right now it's a global so we don't need to init the memory to zero
+    // memset(redist, 0, sizeof(*redist));
+    redist->typer           = 0x11;      /* RO */
+    redist->iidr            = 0x1143B;  /* RO */
+
+    redist->pidr0           = 0x93;     /* RO */
+    redist->pidr1           = 0xB4;     /* RO */
+    redist->pidr2           = 0x3B;     /* RO */
+    redist->pidr4           = 0x44;     /* RO */
+
+    redist->cidr0           = 0x0D;     /* RO */
+    redist->cidr1           = 0xF0;     /* RO */
+    redist->cidr2           = 0x05;     /* RO */
+    redist->cidr3           = 0xB1;     /* RO */
+}
+
+// @ivanv: come back to
+struct gic_dist_map dist;
+struct gic_redist_map redist;
+vgic_reg_t vgic_regs;
+
+void vgic_init()
+{
+    for (int i = 0; i < NUM_SLOTS_SPI_VIRQ; i++) {
+        vgic.vspis[i].virq = VIRQ_INVALID;
+    }
+    for (int i = 0; i < NUM_VCPU_LOCAL_VIRQS; i++) {
+        vgic.vgic_vcpu[VCPU_ID].local_virqs[i].virq = VIRQ_INVALID;
+    }
+    for (int i = 0; i < NUM_LIST_REGS; i++) {
+        vgic.vgic_vcpu[VCPU_ID].lr_shadow[i].virq = VIRQ_INVALID;
+    }
+    vgic.registers = &vgic_regs;
+    vgic_regs.dist = &dist;
+    vgic_regs.redist = &redist;
+
+    vgic_dist_reset(&dist);
+    vgic_redist_reset(&redist);
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v3.h

@@ -0,0 +1,244 @@
+/*
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2019, DornerWorks
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#define GIC_500_GRP0     (1 << 0)
+#define GIC_500_GRP1_NS  (1 << 1)
+#define GIC_500_GRP1_S   (1 << 2)
+#define GIC_500_ARE_S    (1 << 4)
+
+#define GIC_500_ENABLED (GIC_500_ARE_S | GIC_500_GRP1_NS | GIC_500_GRP0)
+#define GIC_ENABLED GIC_500_ENABLED
+
+#define GIC_SGI_OFFSET  0x10000
+#define GIC_MAX_DISABLE 32
+#define GIC_GROUP       1
+
+struct gic_dist_map {
+    uint32_t ctlr;                /* 0x0000 */
+    uint32_t typer;               /* 0x0004 */
+    uint32_t iidr;                /* 0x0008 */
+    uint32_t res1[13];            /* [0x000C, 0x0040) */
+    uint32_t setspi_nsr;          /* 0x0040 */
+    uint32_t res2;                /* 0x0044 */
+    uint32_t clrspi_nsr;          /* 0x0048 */
+    uint32_t res3;                /* 0x004C */
+    uint32_t setspi_sr;           /* 0x0050 */
+    uint32_t res4;                /* 0x0054 */
+    uint32_t clrspi_sr;           /* 0x0058 */
+    uint32_t res5[9];             /* [0x005C, 0x0080) */
+    uint32_t irq_group0[GUEST_NUM_VCPUS];          /* [0x080, 0x84) */
+    uint32_t irq_group[31];                             /* [0x084, 0x100) */
+    uint32_t enable_set0[GUEST_NUM_VCPUS];         /* [0x100, 0x104) */
+    uint32_t enable_set[31];                            /* [0x104, 0x180) */
+    uint32_t enable_clr0[GUEST_NUM_VCPUS];         /* [0x180, 0x184) */
+    uint32_t enable_clr[31];                            /* [0x184, 0x200) */
+    uint32_t pending_set0[GUEST_NUM_VCPUS];        /* [0x200, 0x204) */
+    uint32_t pending_set[31];                           /* [0x204, 0x280) */
+    uint32_t pending_clr0[GUEST_NUM_VCPUS];        /* [0x280, 0x284) */
+    uint32_t pending_clr[31];                           /* [0x284, 0x300) */
+    uint32_t active0[GUEST_NUM_VCPUS];             /* [0x300, 0x304) */
+    uint32_t active[31];                                /* [0x300, 0x380) */
+    uint32_t active_clr0[GUEST_NUM_VCPUS];         /* [0x380, 0x384) */
+    uint32_t active_clr[31];                            /* [0x384, 0x400) */
+    uint32_t priority0[GUEST_NUM_VCPUS][8];        /* [0x400, 0x420) */
+    uint32_t priority[247];                             /* [0x420, 0x7FC) */
+    uint32_t res6;                  /* 0x7FC */
+
+    uint32_t targets0[GUEST_NUM_VCPUS][8];         /* [0x800, 0x820) */
+    uint32_t targets[247];                              /* [0x820, 0xBFC) */
+    uint32_t res7;                  /* 0xBFC */
+
+    uint32_t config[64];            /* [0xC00, 0xD00) */
+    uint32_t group_mod[64];         /* [0xD00, 0xE00) */
+    uint32_t nsacr[64];             /* [0xE00, 0xF00) */
+    uint32_t sgir;                  /* 0xF00 */
+    uint32_t res8[3];               /* [0xF00, 0xF10) */
+    uint32_t sgi_pending_clr[GUEST_NUM_VCPUS][4];  /* [0xF10, 0xF20) */
+    uint32_t sgi_pending_set[GUEST_NUM_VCPUS][4];  /* [0xF20, 0xF30) */
+    uint32_t res9[5235];            /* [0x0F30, 0x6100) */
+
+    uint64_t irouter[960];          /* [0x6100, 0x7F00) */
+    uint64_t res10[2080];           /* [0x7F00, 0xC000) */
+    uint32_t estatusr;              /* 0xC000 */
+    uint32_t errtestr;              /* 0xC004 */
+    uint32_t res11[31];             /* [0xC008, 0xC084) */
+    uint32_t spisr[30];             /* [0xC084, 0xC0FC) */
+    uint32_t res12[4021];           /* [0xC0FC, 0xFFD0) */
+
+    uint32_t pidrn[8];              /* [0xFFD0, 0xFFF0) */
+    uint32_t cidrn[4];              /* [0xFFD0, 0xFFFC] */
+};
+
+/* Memory map for GIC Redistributor Registers for control and physical LPI's */
+struct gic_redist_map {          /* Starting */
+    uint32_t    ctlr;           /* 0x0000 */
+    uint32_t    iidr;           /* 0x0004 */
+    uint64_t    typer;          /* 0x008 */
+    uint32_t    res0;           /* 0x0010 */
+    uint32_t    waker;          /* 0x0014 */
+    uint32_t    res1[21];       /* 0x0018 */
+    uint64_t    propbaser;      /* 0x0070 */
+    uint64_t    pendbaser;      /* 0x0078 */
+    uint32_t    res2[16340];    /* 0x0080 */
+    uint32_t    pidr4;          /* 0xFFD0 */
+    uint32_t    pidr5;          /* 0xFFD4 */
+    uint32_t    pidr6;          /* 0xFFD8 */
+    uint32_t    pidr7;          /* 0xFFDC */
+    uint32_t    pidr0;          /* 0xFFE0 */
+    uint32_t    pidr1;          /* 0xFFE4 */
+    uint32_t    pidr2;          /* 0xFFE8 */
+    uint32_t    pidr3;          /* 0xFFEC */
+    uint32_t    cidr0;          /* 0xFFF0 */
+    uint32_t    cidr1;          /* 0xFFF4 */
+    uint32_t    cidr2;          /* 0xFFF8 */
+    uint32_t    cidr3;          /* 0xFFFC */
+};
+
+/* Memory map for the GIC Redistributor Registers for the SGI and PPI's */
+// struct gic_redist_sgi_ppi_map {  /* Starting */
+//     uint32_t    res0[32];       /* 0x0000 */
+//     uint32_t    igroup[32];     /* 0x0080 */
+//     uint32_t    isenable[32];   /* 0x0100 */
+//     uint32_t    icenable[32];   /* 0x0180 */
+//     uint32_t    ispend[32];     /* 0x0200 */
+//     uint32_t    icpend[32];     /* 0x0280 */
+//     uint32_t    isactive[32];   /* 0x0300 */
+//     uint32_t    icactive[32];   /* 0x0380 */
+//     uint32_t    ipriorityrn[8]; /* 0x0400 */
+//     uint32_t    res1[504];      /* 0x0420 */
+//     uint32_t    icfgrn_ro;      /* 0x0C00 */
+//     uint32_t    icfgrn_rw;      /* 0x0C04 */
+//     uint32_t    res2[62];       /* 0x0C08 */
+//     uint32_t    igrpmod[64];    /* 0x0D00 */
+//     uint32_t    nsac;           /* 0x0E00 */
+//     uint32_t    res11[11391];   /* 0x0E04 */
+//     uint32_t    miscstatsr;     /* 0xC000 */
+//     uint32_t    res3[31];       /* 0xC004 */
+//     uint32_t    ppisr;          /* 0xC080 */
+//     uint32_t    res4[4062];     /* 0xC084 */
+// };
+
+/*
+ * GIC Distributor Register Map
+ * ARM Generic Interrupt Controller (Architecture version 3.0)
+ * Architecture Specification (Issue C)
+ * Chapter 8 Programmers' Model - Table 8-25
+ */
+#define GIC_DIST_CTLR           0x000
+#define GIC_DIST_TYPER          0x004
+#define GIC_DIST_IIDR           0x008
+#define GIC_DIST_STATUSR        0x010
+#define GIC_DIST_SETSPI_NSR     0x040
+#define GIC_DIST_CLRSPI_NSR     0x048
+#define GIC_DIST_SETSPI_SR      0x050
+#define GIC_DIST_CLRSPI_SR      0x058
+#define GIC_DIST_IGROUPR0       0x080
+#define GIC_DIST_IGROUPR1       0x084
+#define GIC_DIST_IGROUPRN       0x0FC
+#define GIC_DIST_ISENABLER0     0x100
+#define GIC_DIST_ISENABLER1     0x104
+#define GIC_DIST_ISENABLERN     0x17C
+#define GIC_DIST_ICENABLER0     0x180
+#define GIC_DIST_ICENABLER1     0x184
+#define GIC_DIST_ICENABLERN     0x1fC
+#define GIC_DIST_ISPENDR0       0x200
+#define GIC_DIST_ISPENDR1       0x204
+#define GIC_DIST_ISPENDRN       0x27C
+#define GIC_DIST_ICPENDR0       0x280
+#define GIC_DIST_ICPENDR1       0x284
+#define GIC_DIST_ICPENDRN       0x2FC
+#define GIC_DIST_ISACTIVER0     0x300
+#define GIC_DIST_ISACTIVER1     0x304
+#define GIC_DIST_ISACTIVERN     0x37C
+#define GIC_DIST_ICACTIVER0     0x380
+#define GIC_DIST_ICACTIVER1     0x384
+#define GIC_DIST_ICACTIVERN     0x3FC
+#define GIC_DIST_IPRIORITYR0    0x400
+#define GIC_DIST_IPRIORITYR7    0x41C
+#define GIC_DIST_IPRIORITYR8    0x420
+#define GIC_DIST_IPRIORITYRN    0x7F8
+#define GIC_DIST_ITARGETSR0     0x800
+#define GIC_DIST_ITARGETSR7     0x81C
+#define GIC_DIST_ITARGETSR8     0x820
+#define GIC_DIST_ITARGETSRN     0xBF8
+#define GIC_DIST_ICFGR0         0xC00
+#define GIC_DIST_ICFGRN         0xCFC
+#define GIC_DIST_IGRPMODR0      0xD00
+#define GIC_DIST_IGRPMODRN      0xD7C
+#define GIC_DIST_NSACR0         0xE00
+#define GIC_DIST_NSACRN         0xEFC
+#define GIC_DIST_SGIR           0xF00
+#define GIC_DIST_CPENDSGIR0     0xF10
+#define GIC_DIST_CPENDSGIRN     0xF1C
+#define GIC_DIST_SPENDSGIR0     0xF20
+#define GIC_DIST_SPENDSGIRN     0xF2C
+#define GIC_DIST_IROUTER0      0x6100
+#define GIC_DIST_IROUTERN      0x7FD8
+
+/*
+ * ARM Generic Interrupt Controller (Architecture version 3.0)
+ * Architecture Specification (Issue C)
+ * 8.9.21: Software Generated Interrupt Register, GICD_SGIR
+ */
+#define GIC_DIST_SGI_TARGET_LIST_FILTER_SHIFT   24
+#define GIC_DIST_SGI_TARGET_LIST_FILTER_MASK    0x3 << GIC_DIST_SGI_TARGET_LIST_FILTER_SHIFT
+#define GIC_DIST_SGI_TARGET_LIST_SPEC           0
+#define GIC_DIST_SGI_TARGET_LIST_OTHERS         1
+#define GIC_DIST_SGI_TARGET_SELF                2
+
+#define GIC_DIST_SGI_CPU_TARGET_LIST_SHIFT      16
+#define GIC_DIST_SGI_CPU_TARGET_LIST_MASK       0xFF << GIC_DIST_SGI_CPU_TARGET_LIST_SHIFT
+
+#define GIC_DIST_SGI_INTID_MASK                 0xF
+
+#define GICR_CTLR           0x000
+#define GICR_IIDR           0x004
+#define GICR_TYPER          0x008
+#define GICR_WAKER          0x014
+
+#define GICR_IGROUPR0       0x10080
+#define GICR_ISENABLER0     0x10100
+#define GICR_ICENABLER0     0x10180
+#define GICR_ICACTIVER0     0x10380
+#define GICR_IPRIORITYR0    0x10400
+#define GICR_IPRIORITYRN    0x1041C
+#define GICR_ICFGR1         0x10c04
+
+typedef struct {
+    /// Virtual distributor registers
+    struct gic_dist_map *dist;
+    /// Virtual redistributor registers for control and physical LPIs
+    struct gic_redist_map *redist;
+    /// Virtual redistributor for SGI and PPIs
+    // struct gic_redist_sgi_ppi_map *sgi;
+} vgic_reg_t;
+
+static inline bool vgic_dist_is_enabled(struct gic_dist_map *gic_dist) {
+    return gic_dist->ctlr & GIC_500_GRP1_NS;
+}
+
+static inline void vgic_dist_enable(struct gic_dist_map *gic_dist) {
+    gic_dist->ctlr |= GIC_500_GRP1_NS | GIC_500_ARE_S;
+}
+
+static inline void vgic_dist_disable(struct gic_dist_map *gic_dist)
+{
+    gic_dist->ctlr &= ~(GIC_500_GRP1_NS | GIC_500_ARE_S);
+}
+
+static inline struct gic_dist_map *vgic_get_dist(void *registers)
+{
+    assert(registers);
+    return ((vgic_reg_t *) registers)->dist;
+}
+
+static inline struct gic_redist_map *vgic_get_redist(void *registers)
+{
+    assert(registers);
+    return ((vgic_reg_t *) registers)->redist;
+}
+

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/virq.h

@@ -0,0 +1,215 @@
+/*
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+
+#include <stdint.h>
+#include <stdbool.h>
+#include "../util/util.h"
+
+/* The ARM GIC architecture defines 16 SGIs (0 - 7 is recommended for non-secure
+ * state, 8 - 15 for secure state), 16 PPIs (interrupt 16 - 31) and 988 SPIs
+ * (32 - 1019). The interrupt IDs 1020 - 1023 are used for special purposes.
+ * GICv3.1 is not implemented here, it supports 64 additional PPIs (interrupt
+ * 1056 - 1119) and 1024 SPIs (interrupt 4096 – 5119). LPIs starting at
+ * interrupt 8192 are also not implemented here.
+ */
+#define NUM_SGI_VIRQS           16   // vCPU local SGI interrupts
+#define NUM_PPI_VIRQS           16   // vCPU local PPI interrupts
+#define NUM_VCPU_LOCAL_VIRQS    (NUM_SGI_VIRQS + NUM_PPI_VIRQS)
+
+/* Usually, VMs do not use all SPIs. To reduce the memory footprint, our vGIC
+ * implementation manages the SPIs in a fixed size slot list. 200 entries have
+ * been good trade-off that is sufficient for most systems.
+ */
+#define NUM_SLOTS_SPI_VIRQ      200
+
+#define VIRQ_INVALID -1
+
+typedef void (*irq_ack_fn_t)(uint64_t vcpu_id, int irq, void *cookie);
+
+struct virq_handle {
+    int virq;
+    irq_ack_fn_t ack_fn;
+    void *ack_data;
+};
+
+// @ivanv: revisit
+static inline void virq_ack(uint64_t vcpu_id, struct virq_handle *irq)
+{
+    // printf("VGIC|INFO: Acking for vIRQ %d\n", irq->virq);
+    assert(irq->ack_fn);
+    irq->ack_fn(vcpu_id, irq->virq, irq->ack_data);
+}
+
+/* TODO: A typical number of list registers supported by GIC is four, but not
+ * always. One particular way to probe the number of registers is to inject a
+ * dummy IRQ with seL4_ARM_VCPU_InjectIRQ(), using LR index high enough to be
+ * not supported by any target; the kernel will reply with the supported range
+ * of LR indexes.
+ */
+#define NUM_LIST_REGS 4
+/* This is a rather arbitrary number, increase if needed. */
+#define MAX_IRQ_QUEUE_LEN 64
+#define IRQ_QUEUE_NEXT(_i) (((_i) + 1) & (MAX_IRQ_QUEUE_LEN - 1))
+
+static_assert((MAX_IRQ_QUEUE_LEN & (MAX_IRQ_QUEUE_LEN - 1)) == 0,
+              "IRQ ring buffer size must be power of two");
+
+// @ivanv: make a note of all datastructure invariants
+struct irq_queue {
+    struct virq_handle *irqs[MAX_IRQ_QUEUE_LEN]; /* circular buffer */
+    uint64_t head;
+    uint64_t tail;
+};
+
+/* vCPU specific interrupt context */
+typedef struct vgic_vcpu {
+    /* Mirrors the GIC's vCPU list registers */
+    struct virq_handle lr_shadow[NUM_LIST_REGS];
+    /* Queue for IRQs that don't fit in the GIC's vCPU list registers */
+    struct irq_queue irq_queue;
+    /*  vCPU local interrupts (SGI, PPI) */
+    struct virq_handle local_virqs[NUM_VCPU_LOCAL_VIRQS];
+} vgic_vcpu_t;
+
+/* GIC global interrupt context */
+typedef struct vgic {
+    /* virtual registers */
+    void *registers;
+    /* registered global interrupts (SPI) */
+    struct virq_handle vspis[NUM_SLOTS_SPI_VIRQ];
+    /* vCPU specific interrupt context */
+    vgic_vcpu_t vgic_vcpu[GUEST_NUM_VCPUS];
+} vgic_t;
+
+static inline vgic_vcpu_t *get_vgic_vcpu(vgic_t *vgic, int vcpu_id)
+{
+    assert(vgic);
+    assert((vcpu_id >= 0) && (vcpu_id < ARRAY_SIZE(vgic->vgic_vcpu)));
+    return &(vgic->vgic_vcpu[vcpu_id]);
+}
+
+static inline struct virq_handle *virq_get_sgi_ppi(vgic_t *vgic, uint64_t vcpu_id, int virq)
+{
+    vgic_vcpu_t *vgic_vcpu = get_vgic_vcpu(vgic, vcpu_id);
+    assert(vgic_vcpu);
+    assert((virq >= 0) && (virq < ARRAY_SIZE(vgic_vcpu->local_virqs)));
+    return &vgic_vcpu->local_virqs[virq];
+}
+
+static inline struct virq_handle *virq_find_spi_irq_data(struct vgic *vgic, int virq)
+{
+    for (int i = 0; i < ARRAY_SIZE(vgic->vspis); i++) {
+        if (vgic->vspis[i].virq != VIRQ_INVALID && vgic->vspis[i].virq == virq) {
+            return &vgic->vspis[i];
+        }
+    }
+    return NULL;
+}
+
+static inline struct virq_handle *virq_find_irq_data(struct vgic *vgic, uint64_t vcpu_id, int virq)
+{
+    if (virq < NUM_VCPU_LOCAL_VIRQS)  {
+        return virq_get_sgi_ppi(vgic, vcpu_id, virq);
+    }
+    return virq_find_spi_irq_data(vgic, virq);
+}
+
+static inline bool virq_spi_add(vgic_t *vgic, struct virq_handle *virq_data)
+{
+    for (int i = 0; i < ARRAY_SIZE(vgic->vspis); i++) {
+        if (vgic->vspis[i].virq == VIRQ_INVALID) {
+            vgic->vspis[i] = *virq_data;
+            return true;
+        }
+    }
+
+    LOG_VMM_ERR("Could not add SPI IRQ (0x%lx), ran out of slots.\n", virq_data->virq);
+    return false;
+}
+
+static inline bool virq_sgi_ppi_add(uint64_t vcpu_id, vgic_t *vgic, struct virq_handle *virq_data)
+{
+    // @ivanv: revisit
+    vgic_vcpu_t *vgic_vcpu = get_vgic_vcpu(vgic, vcpu_id);
+    assert(vgic_vcpu);
+    int irq = virq_data->virq;
+    assert((irq >= 0) && (irq < ARRAY_SIZE(vgic_vcpu->local_virqs)));
+    struct virq_handle *slot = &vgic_vcpu->local_virqs[irq];
+    if (slot->virq != VIRQ_INVALID) {
+        LOG_VMM_ERR("IRQ %d already registered on VCPU %u", virq_data->virq, vcpu_id);
+        return false;
+    }
+    *slot = *virq_data;
+    return true;
+}
+
+static inline bool virq_add(uint64_t vcpu_id, vgic_t *vgic, struct virq_handle *virq_handle)
+{
+    if (virq_handle->virq < NUM_VCPU_LOCAL_VIRQS) {
+        return virq_sgi_ppi_add(vcpu_id, vgic, virq_handle);
+    }
+    return virq_spi_add(vgic, virq_handle);
+}
+
+static inline bool vgic_irq_enqueue(vgic_t *vgic, uint64_t vcpu_id, struct virq_handle *irq)
+{
+    vgic_vcpu_t *vgic_vcpu = get_vgic_vcpu(vgic, vcpu_id);
+    assert(vgic_vcpu);
+    struct irq_queue *q = &vgic_vcpu->irq_queue;
+
+    // @ivanv: add "unlikely" call
+    if (IRQ_QUEUE_NEXT(q->tail) == q->head) {
+        return false;
+    }
+
+    q->irqs[q->tail] = irq;
+    q->tail = IRQ_QUEUE_NEXT(q->tail);
+
+    return true;
+}
+
+static inline struct virq_handle *vgic_irq_dequeue(vgic_t *vgic, uint64_t vcpu_id)
+{
+    vgic_vcpu_t *vgic_vcpu = get_vgic_vcpu(vgic, vcpu_id);
+    assert(vgic_vcpu);
+    struct irq_queue *q = &vgic_vcpu->irq_queue;
+    struct virq_handle *virq = NULL;
+
+    if (q->head != q->tail) {
+        virq = q->irqs[q->head];
+        q->head = IRQ_QUEUE_NEXT(q->head);
+    }
+
+    return virq;
+}
+
+static inline int vgic_find_empty_list_reg(vgic_t *vgic, uint64_t vcpu_id)
+{
+    vgic_vcpu_t *vgic_vcpu = get_vgic_vcpu(vgic, vcpu_id);
+    assert(vgic_vcpu);
+    for (int i = 0; i < ARRAY_SIZE(vgic_vcpu->lr_shadow); i++) {
+        if (vgic_vcpu->lr_shadow[i].virq == VIRQ_INVALID) {
+            return i;
+        }
+    }
+
+    return -1;
+}
+
+static inline bool vgic_vcpu_load_list_reg(vgic_t *vgic, uint64_t vcpu_id, int idx, int group, struct virq_handle *virq)
+{
+    vgic_vcpu_t *vgic_vcpu = get_vgic_vcpu(vgic, vcpu_id);
+    assert(vgic_vcpu);
+    assert((idx >= 0) && (idx < ARRAY_SIZE(vgic_vcpu->lr_shadow)));
+    // @ivanv: why is the priority 0?
+    microkit_vcpu_arm_inject_irq(GUEST_ID, virq->virq, 0, group, idx);
+    vgic_vcpu->lr_shadow[idx] = *virq;
+
+    return true;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vmm.c

@@ -0,0 +1,451 @@
+/*
+ * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
+ * Copyright 2022, UNSW (ABN 57 195 873 179)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stddef.h>
+#include <microkit.h>
+#include "util/util.h"
+#include "vgic/vgic.h"
+#include "smc.h"
+#include "fault.h"
+#include "hsr.h"
+#include "vmm.h"
+#include "arch/aarch64/linux.h"
+
+/* Data for the guest's kernel image. */
+extern char _guest_kernel_image[];
+extern char _guest_kernel_image_end[];
+/* Data for the device tree to be passed to the kernel. */
+extern char _guest_dtb_image[];
+extern char _guest_dtb_image_end[];
+/* Data for the initial RAM disk to be passed to the kernel. */
+extern char _guest_initrd_image[];
+extern char _guest_initrd_image_end[];
+/* seL4CP will set this variable to the start of the guest RAM memory region. */
+uintptr_t guest_ram_vaddr;
+
+/* @jade: find a better number */
+#define MAX_IRQ_CH 32
+int passthrough_irq_map[MAX_IRQ_CH];
+
+// @ivanv: document where these come from
+#define SYSCALL_PA_TO_IPA 65
+#define SYSCALL_NOP 67
+
+static bool handle_unknown_syscall(microkit_msginfo msginfo)
+{
+    // @ivanv: should print out the name of the VM the fault came from.
+    uint64_t syscall = microkit_mr_get(seL4_UnknownSyscall_Syscall);
+    uint64_t fault_ip = microkit_mr_get(seL4_UnknownSyscall_FaultIP);
+
+    LOG_VMM("Received syscall 0x%lx\n", syscall);
+    switch (syscall) {
+        case SYSCALL_PA_TO_IPA:
+            // @ivanv: why do we not do anything here?
+            // @ivanv, how to get the physical address to translate?
+            LOG_VMM("Received PA translation syscall\n");
+            break;
+        case SYSCALL_NOP:
+            LOG_VMM("Received NOP syscall\n");
+            break;
+        default:
+            LOG_VMM_ERR("Unknown syscall: syscall number: 0x%lx, PC: 0x%lx\n", syscall, fault_ip);
+            return false;
+    }
+
+    seL4_UserContext regs;
+    seL4_Error err = seL4_TCB_ReadRegisters(BASE_VM_TCB_CAP + GUEST_ID, false, 0, SEL4_USER_CONTEXT_SIZE, &regs);
+    assert(!err);
+
+    return fault_advance_vcpu(&regs);
+}
+
+static bool handle_vppi_event()
+{
+    uint64_t ppi_irq = microkit_mr_get(seL4_VPPIEvent_IRQ);
+    // We directly inject the interrupt assuming it has been previously registered.
+    // If not the interrupt will dropped by the VM.
+    bool success = vgic_inject_irq(GUEST_VCPU_ID, ppi_irq);
+    if (!success) {
+        // @ivanv, make a note that when having a lot of printing on it can cause this error
+        LOG_VMM_ERR("VPPI IRQ %lu dropped on vCPU %d\n", ppi_irq, GUEST_VCPU_ID);
+        // Acknowledge to unmask it as our guest will not use the interrupt
+        // @ivanv: We're going to assume that we only have one VCPU and that the
+        // cap is the base one.
+        microkit_vcpu_arm_ack_vppi(GUEST_ID, ppi_irq);
+    }
+
+    return true;
+}
+
+static bool handle_vcpu_fault(microkit_msginfo msginfo, uint64_t vcpu_id)
+{
+    uint32_t hsr = microkit_mr_get(seL4_VCPUFault_HSR);
+    uint64_t hsr_ec_class = HSR_EXCEPTION_CLASS(hsr);
+    switch (hsr_ec_class) {
+        case HSR_SMC_64_EXCEPTION:
+            return handle_smc(vcpu_id, hsr);
+        case HSR_WFx_EXCEPTION:
+            // If we get a WFI exception, we just do nothing in the VMM.
+            return true;
+        default:
+            LOG_VMM_ERR("unknown SMC exception, EC class: 0x%lx, HSR: 0x%lx\n", hsr_ec_class, hsr);
+            return false;
+    }
+}
+
+static int handle_user_exception(microkit_msginfo msginfo)
+{
+    // @ivanv: print out VM name/vCPU id when we have multiple VMs
+    uint64_t fault_ip = microkit_mr_get(seL4_UserException_FaultIP);
+    uint64_t number = microkit_mr_get(seL4_UserException_Number);
+    LOG_VMM_ERR("Invalid instruction fault at IP: 0x%lx, number: 0x%lx", fault_ip, number);
+
+    // Dump registers
+    seL4_UserContext regs = {0};
+    seL4_Error ret = seL4_TCB_ReadRegisters(BASE_VM_TCB_CAP + GUEST_ID, false, 0, SEL4_USER_CONTEXT_SIZE, &regs);
+    if (ret != seL4_NoError) {
+        printf("Failure reading regs, error %d", ret);
+        return false;
+    } else {
+        print_tcb_regs(&regs);
+    }
+
+    return true;
+}
+
+#define WORDLE_WORD_SIZE 5
+#define WORDLE_BUFFER_ADDR 0x50000000
+#define WORDLE_BUFFER_SIZE (WORDLE_WORD_SIZE * sizeof(char))
+#define WORDLE_SERVER_CHANNEL 1
+
+char word[WORDLE_WORD_SIZE] = {0};
+
+static bool handle_vm_fault()
+{
+    uint64_t addr = microkit_mr_get(seL4_VMFault_Addr);
+    uint64_t fsr = microkit_mr_get(seL4_VMFault_FSR);
+
+    seL4_UserContext regs;
+    int err = seL4_TCB_ReadRegisters(BASE_VM_TCB_CAP + GUEST_ID, false, 0, SEL4_USER_CONTEXT_SIZE, &regs);
+    assert(err == seL4_NoError);
+
+    switch (addr) {
+        case WORDLE_BUFFER_ADDR...WORDLE_BUFFER_ADDR + WORDLE_BUFFER_SIZE: {
+            char character = fault_get_data(&regs, fsr);
+            word[(addr - WORDLE_BUFFER_ADDR) / sizeof(char)] = character;
+            if (addr == WORDLE_BUFFER_ADDR + (WORDLE_BUFFER_SIZE - sizeof(char))) {
+                microkit_vcpu_stop(GUEST_ID);
+                microkit_msginfo msg = microkit_msginfo_new(0, WORDLE_WORD_SIZE);
+                for (int i = 0; i < WORDLE_WORD_SIZE; i++) {
+                    microkit_mr_set(i, word[i]);
+                }
+                microkit_ppcall(WORDLE_SERVER_CHANNEL, msg);
+                return true;
+            } else {
+                return fault_advance_vcpu(&regs);
+            }
+        }
+        case GIC_DIST_PADDR...GIC_DIST_PADDR + GIC_DIST_SIZE:
+            return handle_vgic_dist_fault(GUEST_VCPU_ID, addr, fsr, &regs);
+#if defined(GIC_V3)
+        /* Need to handle redistributor faults for GICv3 platforms. */
+        case GIC_REDIST_PADDR...GIC_REDIST_PADDR + GIC_REDIST_SIZE:
+            return handle_vgic_redist_fault(GUEST_VCPU_ID, addr, fsr, &regs);
+#endif
+        default: {
+            uint64_t ip = microkit_mr_get(seL4_VMFault_IP);
+            uint64_t is_prefetch = seL4_GetMR(seL4_VMFault_PrefetchFault);
+            uint64_t is_write = (fsr & (1 << 6)) != 0;
+            LOG_VMM_ERR("unexpected memory fault on address: 0x%lx, FSR: 0x%lx, IP: 0x%lx, is_prefetch: %s, is_write: %s\n", addr, fsr, ip, is_prefetch ? "true" : "false", is_write ? "true" : "false");
+            print_tcb_regs(&regs);
+            print_vcpu_regs(GUEST_ID);
+            return false;
+        }
+    }
+}
+
+#define SGI_RESCHEDULE_IRQ  0
+#define SGI_FUNC_CALL       1
+#define PPI_VTIMER_IRQ      27
+
+static void vppi_event_ack(uint64_t vcpu_id, int irq, void *cookie)
+{
+    microkit_vcpu_arm_ack_vppi(GUEST_ID, irq);
+}
+
+static void sgi_ack(uint64_t vcpu_id, int irq, void *cookie) {}
+
+static void serial_ack(uint64_t vcpu_id, int irq, void *cookie) {
+    /*
+     * For now we by default simply ack the serial IRQ, we have not
+     * come across a case yet where more than this needs to be done.
+     */
+    microkit_irq_ack(SERIAL_IRQ_CH);
+}
+
+static void passthrough_device_ack(uint64_t vcpu_id, int irq, void *cookie) {
+    microkit_channel irq_ch = (microkit_channel)(int64_t)cookie;
+    microkit_irq_ack(irq_ch);
+}
+
+static void register_passthrough_irq(int irq, microkit_channel irq_ch) {
+    LOG_VMM("Register passthrough IRQ %d (channel: 0x%lx)\n", irq, irq_ch);
+    assert(irq_ch < MAX_IRQ_CH);
+    passthrough_irq_map[irq_ch] = irq;
+
+    int err = vgic_register_irq(GUEST_VCPU_ID, irq, &passthrough_device_ack, (void *)(int64_t)irq_ch);
+    if (!err) {
+        LOG_VMM_ERR("Failed to register IRQ %d\n", irq);
+        return;
+    }
+}
+
+bool guest_init_images(void) {
+    // First we inspect the kernel image header to confirm it is a valid image
+    // and to determine where in memory to place the image. Currently this
+    // process assumes the guest is the Linux kernel.
+    struct linux_image_header *image_header = (struct linux_image_header *) &_guest_kernel_image;
+    assert(image_header->magic == LINUX_IMAGE_MAGIC);
+    if (image_header->magic != LINUX_IMAGE_MAGIC) {
+        LOG_VMM_ERR("Linux kernel image magic check failed\n");
+        return false;
+    }
+    // Copy the guest kernel image into the right location
+    uint64_t kernel_image_size = _guest_kernel_image_end - _guest_kernel_image;
+    uint64_t kernel_image_vaddr = guest_ram_vaddr + image_header->text_offset;
+    // This check is because the Linux kernel image requires to be placed at text_offset of
+    // a 2MiB aligned base address anywhere in usable system RAM and called there.
+    // In this case, we place the image at the text_offset of the start of the guest's RAM,
+    // so we need to make sure that the start of guest RAM is 2MiB aligned.
+    //
+    // @ivanv: Ideally this check would be done at build time, we have all the information
+    // we need at build time to enforce this.
+    assert((guest_ram_vaddr & ((1 << 20) - 1)) == 0);
+    LOG_VMM("Copying guest kernel image to 0x%x (0x%x bytes)\n", kernel_image_vaddr, kernel_image_size);
+    memcpy((char *)kernel_image_vaddr, _guest_kernel_image, kernel_image_size);
+    // Copy the guest device tree blob into the right location
+    uint64_t dtb_image_size = _guest_dtb_image_end - _guest_dtb_image;
+    LOG_VMM("Copying guest DTB to 0x%x (0x%x bytes)\n", GUEST_DTB_VADDR, dtb_image_size);
+    memcpy((char *)GUEST_DTB_VADDR, _guest_dtb_image, dtb_image_size);
+    // Copy the initial RAM disk into the right location
+    uint64_t initrd_image_size = _guest_initrd_image_end - _guest_initrd_image;
+    LOG_VMM("Copying guest initial RAM disk to 0x%x (0x%x bytes)\n", GUEST_INIT_RAM_DISK_VADDR, initrd_image_size);
+    memcpy((char *)GUEST_INIT_RAM_DISK_VADDR, _guest_initrd_image, initrd_image_size);
+
+    return true;
+}
+
+void guest_start(void) {
+    // Initialise the virtual GIC driver
+    vgic_init();
+#if defined(GIC_V2)
+    LOG_VMM("initialised virtual GICv2 driver\n");
+#elif defined(GIC_V3)
+    LOG_VMM("initialised virtual GICv3 driver\n");
+#else
+#error "Unsupported GIC version"
+#endif
+    bool err = vgic_register_irq(GUEST_VCPU_ID, PPI_VTIMER_IRQ, &vppi_event_ack, NULL);
+    if (!err) {
+        LOG_VMM_ERR("Failed to register vCPU virtual timer IRQ: 0x%lx\n", PPI_VTIMER_IRQ);
+        return;
+    }
+    err = vgic_register_irq(GUEST_VCPU_ID, SGI_RESCHEDULE_IRQ, &sgi_ack, NULL);
+    if (!err) {
+        LOG_VMM_ERR("Failed to register vCPU SGI 0 IRQ");
+        return;
+    }
+    err = vgic_register_irq(GUEST_VCPU_ID, SGI_FUNC_CALL, &sgi_ack, NULL);
+    if (!err) {
+        LOG_VMM_ERR("Failed to register vCPU SGI 1 IRQ");
+        return;
+    }
+
+    // Register the IRQ for the passthrough serial
+    register_passthrough_irq(79, 2);
+
+    seL4_UserContext regs = {0};
+    regs.x0 = GUEST_DTB_VADDR;
+    regs.spsr = 5; // PMODE_EL1h
+    // Read the entry point and set it to the program counter
+    struct linux_image_header *image_header = (struct linux_image_header *) &_guest_kernel_image;
+    uint64_t kernel_image_vaddr = guest_ram_vaddr + image_header->text_offset;
+    regs.pc = kernel_image_vaddr;
+    // Set all the TCB registers
+    err = seL4_TCB_WriteRegisters(
+        BASE_VM_TCB_CAP + GUEST_ID,
+        false, // We'll explcitly start the guest below rather than in this call
+        0, // No flags
+        SEL4_USER_CONTEXT_SIZE, // Writing to x0, pc, and spsr // @ivanv: for some reason having the number of registers here does not work... (in this case 2)
+        &regs
+    );
+    assert(!err);
+    // Set the PC to the kernel image's entry point and start the thread.
+    LOG_VMM("starting guest at 0x%lx, DTB at 0x%lx, initial RAM disk at 0x%lx\n",
+        regs.pc, regs.x0, GUEST_INIT_RAM_DISK_VADDR);
+    microkit_vcpu_restart(GUEST_ID, regs.pc);
+}
+
+#define SCTLR_EL1_UCI       (1 << 26)     /* Enable EL0 access to DC CVAU, DC CIVAC, DC CVAC,
+                                           and IC IVAU in AArch64 state   */
+#define SCTLR_EL1_C         (1 << 2)      /* Enable data and unified caches */
+#define SCTLR_EL1_I         (1 << 12)     /* Enable instruction cache       */
+#define SCTLR_EL1_CP15BEN   (1 << 5)      /* AArch32 CP15 barrier enable    */
+#define SCTLR_EL1_UTC       (1 << 15)     /* Enable EL0 access to CTR_EL0   */
+#define SCTLR_EL1_NTWI      (1 << 16)     /* WFI executed as normal         */
+#define SCTLR_EL1_NTWE      (1 << 18)     /* WFE executed as normal         */
+
+/* Disable MMU, SP alignment check, and alignment check */
+/* A57 default value */
+#define SCTLR_EL1_RES      0x30d00800   /* Reserved value */
+#define SCTLR_EL1          ( SCTLR_EL1_RES | SCTLR_EL1_CP15BEN | SCTLR_EL1_UTC \
+                           | SCTLR_EL1_NTWI | SCTLR_EL1_NTWE )
+#define SCTLR_EL1_NATIVE   (SCTLR_EL1 | SCTLR_EL1_C | SCTLR_EL1_I | SCTLR_EL1_UCI)
+#define SCTLR_DEFAULT      SCTLR_EL1_NATIVE
+
+void guest_stop(void) {
+    LOG_VMM("Stopping guest\n");
+    microkit_vcpu_stop(GUEST_ID);
+    LOG_VMM("Stopped guest\n");
+}
+
+bool guest_restart(void) {
+    LOG_VMM("Attempting to restart guest\n");
+    // First, stop the guest
+    microkit_vcpu_stop(GUEST_ID);
+    LOG_VMM("Stopped guest\n");
+    // Then, we need to clear all of RAM
+    LOG_VMM("Clearing guest RAM\n");
+    memset((char *)guest_ram_vaddr, 0, GUEST_RAM_SIZE);
+    // Copy back the images into RAM
+    bool success = guest_init_images();
+    if (!success) {
+        LOG_VMM_ERR("Failed to initialise guest images\n");
+        return false;
+    }
+    // Reset registers
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_SCTLR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_TTBR0, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_TTBR1, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_TCR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_MAIR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_AMAIR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_CIDR, 0);
+    /* other system registers EL1 */
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_ACTLR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_CPACR, 0);
+    /* exception handling registers EL1 */
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_AFSR0, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_AFSR1, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_ESR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_FAR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_ISR, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_VBAR, 0);
+    /* thread pointer/ID registers EL0/EL1 */
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_TPIDR_EL1, 0);
+#if CONFIG_MAX_NUM_NODES > 1
+    /* Virtualisation Multiprocessor ID Register */
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_VMPIDR_EL2, 0);
+#endif /* CONFIG_MAX_NUM_NODES > 1 */
+    /* general registers x0 to x30 have been saved by traps.S */
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_SP_EL1, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_ELR_EL1, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_SPSR_EL1, 0); // 32-bit
+    /* generic timer registers, to be completed */
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_CNTV_CTL, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_CNTV_CVAL, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_CNTVOFF, 0);
+    microkit_vcpu_arm_write_reg(GUEST_ID, seL4_VCPUReg_CNTKCTL_EL1, 0);
+    // Now we need to re-initialise all the VMM state
+    guest_start();
+    LOG_VMM("Restarted guest\n");
+    return true;
+}
+
+void
+init(void)
+{
+    // Initialise the VMM, the VCPU(s), and start the guest
+    LOG_VMM("starting \"%s\"\n", microkit_name);
+    // Place all the binaries in the right locations before starting the guest
+    bool success = guest_init_images();
+    if (!success) {
+        LOG_VMM_ERR("Failed to initialise guest images\n");
+        assert(0);
+    }
+    // Initialise and start guest (setup VGIC, setup interrupts, TCB registers)
+    guest_start();
+}
+
+void
+notified(microkit_channel ch)
+{
+    switch (ch) {
+        case SERIAL_IRQ_CH: {
+            bool success = vgic_inject_irq(GUEST_VCPU_ID, SERIAL_IRQ);
+            if (!success) {
+                LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", SERIAL_IRQ, GUEST_VCPU_ID);
+            }
+            break;
+        }
+        default:
+            if (passthrough_irq_map[ch]) {
+                bool success = vgic_inject_irq(GUEST_VCPU_ID, passthrough_irq_map[ch]);
+                if (!success) {
+                    LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", passthrough_irq_map[ch], GUEST_VCPU_ID);
+                }
+                break;
+            }
+            printf("Unexpected channel, ch: 0x%lx\n", ch);
+    }
+}
+
+seL4_Bool
+fault(microkit_child id, microkit_msginfo msginfo, microkit_msginfo *reply_msginfo)
+{
+    if (id != GUEST_ID) {
+        LOG_VMM_ERR("Unexpected faulting PD/VM with id %d\n", id);
+        return seL4_False;
+    }
+    // This is the primary fault handler for the guest, all faults that come
+    // from seL4 regarding the guest will need to be handled here.
+    uint64_t label = microkit_msginfo_get_label(msginfo);
+    bool success = false;
+    switch (label) {
+        case seL4_Fault_VMFault:
+            success = handle_vm_fault();
+            break;
+        case seL4_Fault_UnknownSyscall:
+            success = handle_unknown_syscall(msginfo);
+            break;
+        case seL4_Fault_UserException:
+            success = handle_user_exception(msginfo);
+            break;
+        case seL4_Fault_VGICMaintenance:
+            success = handle_vgic_maintenance(GUEST_VCPU_ID);
+            break;
+        case seL4_Fault_VCPUFault:
+            success = handle_vcpu_fault(msginfo, GUEST_VCPU_ID);
+            break;
+        case seL4_Fault_VPPIEvent:
+            success = handle_vppi_event();
+            break;
+        default:
+            LOG_VMM_ERR("unknown fault, stopping VM with ID %d\n", id);
+            microkit_vcpu_stop(id);
+            return seL4_False;
+            // @ivanv: print out the actual fault details
+    }
+
+    if (!success) {
+        LOG_VMM_ERR("Failed to handle %s fault\n", fault_to_string(label));
+        return seL4_False;
+    }
+
+    *reply_msginfo = microkit_msginfo_new(0, 0);
+
+    return seL4_True;
+}

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vmm.h

@@ -0,0 +1,50 @@
+#include <stdint.h>
+
+// @ivanv: ideally we would have none of these hardcoded values
+// initrd, ram size come from the DTB
+// We can probably add a node for the DTB addr and then use that.
+// Part of the problem is that we might need multiple DTBs for the same example
+// e.g one DTB for VMM one, one DTB for VMM two. we should be able to hide all
+// of this in the build system to avoid doing any run-time DTB stuff.
+#if defined(BOARD_qemu_virt_aarch64)
+#define GUEST_DTB_VADDR 0x4f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x4d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_rpi4b_hyp)
+#define GUEST_DTB_VADDR 0x2e000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x2d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_odroidc2_hyp)
+#define GUEST_DTB_VADDR 0x2f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x2d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_odroidc4_hyp)
+#define GUEST_DTB_VADDR 0x2f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x2d700000
+#define GUEST_RAM_SIZE 0x10000000
+#elif defined(BOARD_imx8mm_evk_hyp)
+#define GUEST_DTB_VADDR 0x4f000000
+#define GUEST_INIT_RAM_DISK_VADDR 0x4d700000
+#define GUEST_RAM_SIZE 0x10000000
+#else
+#error Need to define VM image address and DTB address
+#endif
+
+#if defined(BOARD_qemu_virt_aarch64)
+#define SERIAL_IRQ_CH 1
+#define SERIAL_IRQ 33
+#elif defined(BOARD_odroidc2_hyp) || defined(BOARD_odroidc4_hyp)
+#define SERIAL_IRQ_CH 1
+#define SERIAL_IRQ 225
+#elif defined(BOARD_rpi4b_hyp)
+#define SERIAL_IRQ_CH 1
+#define SERIAL_IRQ 57
+#elif defined(BOARD_imx8mm_evk_hyp)
+#define SERIAL_IRQ_CH 1
+#define SERIAL_IRQ 79
+#else
+#error Need to define serial interrupt
+#endif
+
+bool guest_restart(void);
+void guest_stop(void);

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle.system

@@ -0,0 +1,83 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<system>
+    <!-- Define your system here -->
+    <memory_region name="uart" size="0x1_000" phys_addr="0x9_000_000"/>
+    <memory_region name="client_to_serial" size="0x1000" />
+    <memory_region name="serial_to_client" size="0x1000" />
+
+    <protection_domain name="wordle_server" priority="254" pp="true">
+        <program_image path="wordle_server.elf" />
+    </protection_domain>
+
+    <protection_domain name="serial_server" priority="254">
+        <program_image path="serial_server.elf" />
+        <map mr="uart" vaddr="0x2000000" perms="rw" cached="false" setvar_vaddr="uart_base_vaddr"/>
+        <map mr="serial_to_client" vaddr="0x4000000" perms="wr" setvar_vaddr="serial_to_client_vaddr"/>
+        <map mr="client_to_serial" vaddr="0x4001000" perms="r" setvar_vaddr="client_to_serial_vaddr"/>
+        <irq irq="33" id="1" />
+    </protection_domain>
+
+    <protection_domain name="client" priority="253" pp="true">
+        <program_image path="client.elf" />
+        <map mr="serial_to_client" vaddr="0x4000000" perms="r" setvar_vaddr="serial_to_client_vaddr"/>
+        <map mr="client_to_serial" vaddr="0x4001000" perms="rw" setvar_vaddr="client_to_serial_vaddr"/>
+    </protection_domain>
+
+    <channel>
+        <end pd="client" id="1" />
+        <end pd="serial_server" id="2" />
+    </channel>
+
+    <channel>
+        <end pd="client" id="2" />
+        <end pd="wordle_server" id="1" />
+    </channel>
+
+    <!--
+        This is what the virtual machine will use as its "RAM".
+        Remember it does not know it is a VM and so  will expect a
+        block of contigious memory as RAM.
+    -->
+    <memory_region name="guest_ram" size="0x10000000" page_size="0x200_000"
+        phys_addr="0x40000000" />
+    <!-- Create a memory region for the ethernet device -->
+    <memory_region name="ethernet" size="0x1000" phys_addr="0xa003000" />
+    <!--
+        Create a memory region for the GIC vCPU, this is part of
+        ARM's hardware virtualisation, I will not go into detail here,
+        but it is necessary for the virtual machine to function.
+    -->
+    <memory_region name="gic_vcpu" size="0x1000" phys_addr="0x8040000" />
+
+    <!-- Create a VMM protection domain -->
+    <protection_domain name="vmm" priority="101">
+        <program_image path="vmm.elf" />
+        <!--
+            Map in the virtual machine's RAM region as the VMM needs
+            access to it as well for starting and setting up the VM.
+        -->
+        <map mr="guest_ram" vaddr="0x40000000" perms="rw"
+            setvar_vaddr="guest_ram_vaddr" />
+        <!--
+            Create the virtual machine, the `id` is used for the
+            VMM to refer to the VM. Similar to channels and IRQs
+        -->
+        <virtual_machine name="linux" priority="100">
+            <vcpu id="0" />
+            <map mr="guest_ram" vaddr="0x40000000" perms="rwx" />
+            <map mr="ethernet" vaddr="0xa003000" perms="rw" cached="false" />
+            <map mr="uart" vaddr="0x9000000" perms="rw" cached="false" />
+            <map mr="gic_vcpu" vaddr="0x8010000" perms="rw" cached="false" />
+        </virtual_machine>
+        <!--
+            We want the VMM to receive the ethernet interrupts, which it
+            will then deliver to the VM
+         -->
+        <irq irq="79" id="2" trigger="edge" />
+    </protection_domain>
+
+    <channel>
+        <end pd="vmm" id="1" />
+        <end pd="wordle_server" id="2" />
+    </channel>
+</system>

ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle_server.c

@@ -0,0 +1,64 @@
+#include <stdint.h>
+#include <stdbool.h>
+#include <microkit.h>
+#include <stddef.h>
+#include "printf.h"
+#include "wordle.h"
+
+/*
+ * Here we initialise the word to "hello", but later in the tutorial
+ * we will actually randomise the word the user is guessing.
+ */
+char word[WORD_LENGTH] = { 'h', 'e', 'l', 'l', 'o' };
+
+#define CLIENT_CHANNEL 1
+#define VMM_CHANNEL 2
+
+bool is_character_in_word(char *word, int ch) {
+    for (int i = 0; i < WORD_LENGTH; i++) {
+        if (word[i] == ch) {
+            return true;
+        }
+    }
+
+    return false;
+}
+
+enum character_state char_to_state(int ch, char *word, uint64_t index) {
+    if (ch == word[index]) {
+        return CORRECT_PLACEMENT;
+    } else if (is_character_in_word(word, ch)) {
+        return INCORRECT_PLACEMENT;
+    } else {
+        return INCORRECT;
+    }
+}
+
+void init(void) {
+    microkit_dbg_puts("WORDLE SERVER: starting\n");
+}
+
+void notified(microkit_channel channel) {}
+
+microkit_msginfo protected(microkit_channel channel, microkit_msginfo msginfo)
+{
+    switch (channel) {
+        case CLIENT_CHANNEL:
+            for (int i = 0; i < WORD_LENGTH; i++) {
+                char ch = microkit_mr_get(i);
+                microkit_mr_set(i, char_to_state(ch, word, i));
+            }
+            return microkit_msginfo_new(0, WORD_LENGTH);
+            break;
+        case VMM_CHANNEL:
+            for (int i = 0; i < WORD_LENGTH; i++) {
+                word[i] = microkit_mr_get(i);
+            }
+            break;
+        default:
+            microkit_dbg_puts("ERROR!\n");
+            break;
+    }
+
+    return microkit_msginfo_new(0, 0);
+}

ME_2150/microkit_tutorial/microkit_tutorial/tutorial/client.c

@@ -10,6 +10,7 @@ uintptr_t client_to_serial_vaddr;
 #define MOVE_CURSOR_UP "\033[5A"
 #define CLEAR_TERMINAL_BELOW_CURSOR "\033[0J"
 #define SERIAL_SERVER_CHANNEL_ID 1
+#define WORDLE_CHANNEL 2
 
 #define INVALID_CHAR (-1)
 
@@ -30,6 +31,15 @@ void wordle_server_send() {
     // After doing the PPC, the Wordle server should have updated
     // the message-registers containing the state of each character.
     // Look at the message registers and update the `table` accordingly.
+  for (int i = 0; i < WORD_LENGTH; i++) {
+    microkit_mr_set(i, table[curr_row][i].ch);
+  }
+
+  microkit_ppcall(WORDLE_CHANNEL, microkit_msginfo_new(0, WORD_LENGTH));
+
+  for (int i = 0; 1 < WORD_LENGTH; i++) {
+    table[curr_row][i].state = microkit_mr_get(i);
+  }
 }
 
 void serial_send(char *str) {

ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle.system

@@ -18,9 +18,19 @@
     <map mr="client_to_serial" vaddr="0x4_001_000" perms="rw" setvar_vaddr="client_to_serial_vaddr" />
   </protection_domain>
 
+  <protection_domain name="wordle_server" priority="254" pp="true">
+    <program_image path="wordle_server.elf" />
+  </protection_domain>
+
   <channel>
     <end pd="serial_server" id="2" />
     <end pd="client" id="1" />
   </channel>
+
+  <channel>
+    <end pd="client" id="2" />
+    <end pd="wordle_server" id="1" />
+  </channel>
+
 </system>
 

ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle_server.c

@@ -9,6 +9,9 @@
  * Here we initialise the word to "hello", but later in the tutorial
  * we will actually randomise the word the user is guessing.
  */
+#define CLIENT_CHANNEL 1
+#define VMM_CHANNEL 2
+
 char word[WORD_LENGTH] = { 'h', 'e', 'l', 'l', 'o' };
 
 bool is_character_in_word(char *word, int ch) {
@@ -35,4 +38,25 @@ void init(void) {
     microkit_dbg_puts("WORDLE SERVER: starting\n");
 }
 
-void notified(microkit_channel channel) {}
+microkit_msginfo protected(microkit_channel channel, microkit_msginfo msginfo)
+{
+    switch (channel) {
+        case CLIENT_CHANNEL:
+            for (int i = 0; i < WORD_LENGTH; i++) {
+                char ch = microkit_mr_get(i);
+                microkit_mr_set(i, char_to_state(ch, word, i));
+            }
+            return microkit_msginfo_new(0, WORD_LENGTH);
+            break;
+        case VMM_CHANNEL:
+            for (int i = 0; i < WORD_LENGTH; i++) {
+                word[i] = microkit_mr_get(i);
+            }
+            break;
+        default:
+            microkit_dbg_puts("ERROR!\n");
+            break;
+    }
+
+    return microkit_msginfo_new(0, 0);
+}void notified(microkit_channel channel) {}