diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions.tar.gz b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions.tar.gz new file mode 100644 index 0000000..109a236 Binary files /dev/null and b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions.tar.gz differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/Makefile b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/Makefile new file mode 100644 index 0000000..be1dd3f --- /dev/null +++ b/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) diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/client.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/client.c new file mode 100644 index 0000000..7df54d8 --- /dev/null +++ b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/client.c @@ -0,0 +1,153 @@ +#include +#include +#include +#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; + } + } +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/printf.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/printf.c new file mode 100644 index 0000000..9302974 --- /dev/null +++ b/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 +#include + +#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 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 +#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 +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; +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/printf.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/printf.h new file mode 100644 index 0000000..211def2 --- /dev/null +++ b/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 +#include + + +#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_ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/wordle.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/include/wordle.h new file mode 100644 index 0000000..2221f27 --- /dev/null +++ b/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. +}; diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/serial_server.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/serial_server.c new file mode 100644 index 0000000..e70b233 --- /dev/null +++ b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/serial_server.c @@ -0,0 +1,80 @@ +#include +#include +#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; + } +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/linux b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/linux new file mode 100644 index 0000000..f029d0e Binary files /dev/null and b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/linux differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/linux.dtb b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/linux.dtb new file mode 100644 index 0000000..80ee7b5 Binary files /dev/null and b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/linux.dtb differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/rootfs.cpio.gz b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/rootfs.cpio.gz new file mode 100644 index 0000000..289d278 Binary files /dev/null and b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/images/rootfs.cpio.gz differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/arch/aarch64/linux.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/arch/aarch64/linux.h new file mode 100644 index 0000000..8a0b52f --- /dev/null +++ b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/arch/aarch64/linux.h @@ -0,0 +1,20 @@ +#include + +// 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) +}; diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/fault.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/fault.c new file mode 100644 index 0000000..165216f --- /dev/null +++ b/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 ®s->x0; + case 1: return ®s->x1; + case 2: return ®s->x2; + case 3: return ®s->x3; + case 4: return ®s->x4; + case 5: return ®s->x5; + case 6: return ®s->x6; + case 7: return ®s->x7; + case 8: return ®s->x8; + case 9: return ®s->x9; + case 10: return ®s->x10; + case 11: return ®s->x11; + case 12: return ®s->x12; + case 13: return ®s->x13; + case 14: return ®s->x14; + case 15: return ®s->x15; + case 16: return ®s->x16; + case 17: return ®s->x17; + case 18: return ®s->x18; + case 19: return ®s->x19; + case 20: return ®s->x20; + case 21: return ®s->x21; + case 22: return ®s->x22; + case 23: return ®s->x23; + case 24: return ®s->x24; + case 25: return ®s->x25; + case 26: return ®s->x26; + case 27: return ®s->x27; + case 28: return ®s->x28; + case 29: return ®s->x29; + case 30: return ®s->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); +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/fault.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/fault.h new file mode 100644 index 0000000..7c163fe --- /dev/null +++ b/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 +#include +#include + +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); diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/global_data.S b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/global_data.S new file mode 100644 index 0000000..ac72fce --- /dev/null +++ b/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 diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/hsr.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/hsr.h new file mode 100644 index 0000000..2219962 --- /dev/null +++ b/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) diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/psci.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/psci.c new file mode 100644 index 0000000..6a5fc2c --- /dev/null +++ b/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 +#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; +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/psci.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/psci.h new file mode 100644 index 0000000..c7f6731 --- /dev/null +++ b/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 +#include + +/* 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); diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/smc.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/smc.c new file mode 100644 index 0000000..3ccda8f --- /dev/null +++ b/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, ®s); + assert(err == seL4_NoError); + + uint64_t fn_number = smc_get_function_number(®s); + 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, ®s, 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; +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/smc.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/smc.h new file mode 100644 index 0000000..084dd90 --- /dev/null +++ b/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 +#include +#include + +// 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); diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/printf.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/printf.c new file mode 100644 index 0000000..9302974 --- /dev/null +++ b/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 +#include + +#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 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 +#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 +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; +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/printf.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/printf.h new file mode 100644 index 0000000..211def2 --- /dev/null +++ b/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 +#include + + +#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_ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/util.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/util.c new file mode 100644 index 0000000..2a85941 --- /dev/null +++ b/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) {} +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/util.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/util/util.h new file mode 100644 index 0000000..e6761a6 --- /dev/null +++ b/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 +#include +#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) + diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vdist.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vdist.h new file mode 100644 index 0000000..5274e38 --- /dev/null +++ b/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; +} + diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic.c new file mode 100644 index 0000000..7753950 --- /dev/null +++ b/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 +#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; +} \ No newline at end of file diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic.h new file mode 100644 index 0000000..f6f4b7c --- /dev/null +++ b/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 +#include +#include + +// @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); diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v2.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v2.c new file mode 100644 index 0000000..54eb3da --- /dev/null +++ b/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 +#include + +#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)); +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v2.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v2.h new file mode 100644 index 0000000..166f2ef --- /dev/null +++ b/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 +#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; +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v3.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v3.c new file mode 100644 index 0000000..2b55eb6 --- /dev/null +++ b/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 + +#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); +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v3.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/vgic_v3.h new file mode 100644 index 0000000..aeba921 --- /dev/null +++ b/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; +} + diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/virq.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vgic/virq.h new file mode 100644 index 0000000..2751b79 --- /dev/null +++ b/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 +#include +#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; +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vmm.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vmm.c new file mode 100644 index 0000000..1176c17 --- /dev/null +++ b/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 +#include +#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, ®s); + assert(!err); + + return fault_advance_vcpu(®s); +} + +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, ®s); + if (ret != seL4_NoError) { + printf("Failure reading regs, error %d", ret); + return false; + } else { + print_tcb_regs(®s); + } + + 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, ®s); + assert(err == seL4_NoError); + + switch (addr) { + case WORDLE_BUFFER_ADDR...WORDLE_BUFFER_ADDR + WORDLE_BUFFER_SIZE: { + char character = fault_get_data(®s, 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(®s); + } + } + case GIC_DIST_PADDR...GIC_DIST_PADDR + GIC_DIST_SIZE: + return handle_vgic_dist_fault(GUEST_VCPU_ID, addr, fsr, ®s); +#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, ®s); +#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(®s); + 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) + ®s + ); + 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; +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vmm.h b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vmm.h new file mode 100644 index 0000000..2f69e6d --- /dev/null +++ b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/vmm/src/vmm.h @@ -0,0 +1,50 @@ +#include + +// @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); diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle.system b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle.system new file mode 100644 index 0000000..e33fee3 --- /dev/null +++ b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle.system @@ -0,0 +1,83 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle_server.c b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle_server.c new file mode 100644 index 0000000..0147529 --- /dev/null +++ b/ME_2150/microkit_tutorial/microkit_tutorial/solution/solutions/wordle_server.c @@ -0,0 +1,64 @@ +#include +#include +#include +#include +#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); +} diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.elf b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.elf index 9fa1017..41fef0c 100755 Binary files a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.elf and b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.elf differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.o b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.o index 1f053e9..a69508d 100644 Binary files a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.o and b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/client.o differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/loader.img b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/loader.img index 6673e94..87a40ae 100644 Binary files a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/loader.img and b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/loader.img differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/report.txt b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/report.txt index d4fa767..2d49610 100644 --- a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/report.txt +++ b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/report.txt @@ -3,23 +3,25 @@ # of fixed caps : 16 # of page table caps: 2 # of page caps : 8 - # of untyped objects: 69 + # of untyped objects: 70 # Loader Regions - + + + # Monitor (Initial Task) Info virtual memory : MemoryRegion(base=0x8a000000, end=0x8a008000) - physical memory: MemoryRegion(base=0x60256000, end=0x6025e000) + physical memory: MemoryRegion(base=0x6025c000, end=0x60264000) # Allocated Kernel Objects Summary - # of allocated objects: 46 + # of allocated objects: 65 # Bootstrap Kernel Invocations Summary @@ -28,57 +30,76 @@ # System Kernel Invocations Summary - # of invocations : 84 - size of invocations: 5,944 + # of invocations : 110 + size of invocations: 7,880 # Allocated Kernel Objects Detail Page(4 KiB): IPC Buffer PD=serial_server 9 cap_addr=8000000000000003 phys_addr=60003000 Page(4 KiB): IPC Buffer PD=client 9 cap_addr=8000000000000004 phys_addr=60004000 - Page(4 KiB): MR=serial_to_client #0 9 cap_addr=8000000000000005 phys_addr=60005000 - Page(4 KiB): MR=client_to_serial #0 9 cap_addr=8000000000000006 phys_addr=60006000 - Page(4 KiB): MR=STACK:serial_server #0 9 cap_addr=8000000000000007 phys_addr=60007000 - Page(4 KiB): MR=STACK:client #0 9 cap_addr=8000000000000008 phys_addr=60008000 - Page(4 KiB): MR=uart @ 9000000 9 cap_addr=8000000000000009 phys_addr=9000000 - Page(4 KiB): MR=ELF:serial_server-0 @ 60248000 9 cap_addr=800000000000000a phys_addr=60248000 - Page(4 KiB): MR=ELF:serial_server-0 @ 60249000 9 cap_addr=800000000000000b phys_addr=60249000 - Page(4 KiB): MR=ELF:serial_server-0 @ 6024a000 9 cap_addr=800000000000000c phys_addr=6024a000 - Page(4 KiB): MR=ELF:serial_server-0 @ 6024b000 9 cap_addr=800000000000000d phys_addr=6024b000 - Page(4 KiB): MR=ELF:serial_server-0 @ 6024c000 9 cap_addr=800000000000000e phys_addr=6024c000 - Page(4 KiB): MR=ELF:serial_server-0 @ 6024d000 9 cap_addr=800000000000000f phys_addr=6024d000 - Page(4 KiB): MR=ELF:serial_server-1 @ 6024e000 9 cap_addr=8000000000000010 phys_addr=6024e000 - Page(4 KiB): MR=ELF:client-0 @ 6024f000 9 cap_addr=8000000000000011 phys_addr=6024f000 - Page(4 KiB): MR=ELF:client-0 @ 60250000 9 cap_addr=8000000000000012 phys_addr=60250000 - Page(4 KiB): MR=ELF:client-0 @ 60251000 9 cap_addr=8000000000000013 phys_addr=60251000 - Page(4 KiB): MR=ELF:client-0 @ 60252000 9 cap_addr=8000000000000014 phys_addr=60252000 - Page(4 KiB): MR=ELF:client-0 @ 60253000 9 cap_addr=8000000000000015 phys_addr=60253000 - Page(4 KiB): MR=ELF:client-0 @ 60254000 9 cap_addr=8000000000000016 phys_addr=60254000 - Page(4 KiB): MR=ELF:client-1 @ 60255000 9 cap_addr=8000000000000017 phys_addr=60255000 - TCB: PD=serial_server 1 cap_addr=8000000000000018 phys_addr=60009000 - TCB: PD=client 1 cap_addr=8000000000000019 phys_addr=60009800 - SchedContext: PD=serial_server 5 cap_addr=800000000000001a phys_addr=6000a000 - SchedContext: PD=client 5 cap_addr=800000000000001b phys_addr=6000c000 - Reply: Monitor 6 cap_addr=800000000000001c phys_addr=6000e000 - Reply: PD=serial_server 6 cap_addr=800000000000001d phys_addr=6000e020 - Reply: PD=client 6 cap_addr=800000000000001e phys_addr=6000e040 - EP: Monitor Fault 2 cap_addr=800000000000001f phys_addr=6000e060 - Notification: PD=serial_server 3 cap_addr=8000000000000020 phys_addr=6000e080 - Notification: PD=client 3 cap_addr=8000000000000021 phys_addr=6000e0c0 - VSpace: PD=serial_server 8 cap_addr=8000000000000022 phys_addr=60260000 - VSpace: PD=client 8 cap_addr=8000000000000023 phys_addr=60262000 - PageTable: PD=serial_server VADDR=0x0 11 cap_addr=8000000000000024 phys_addr=60264000 - PageTable: PD=serial_server VADDR=0xffc0000000 11 cap_addr=8000000000000025 phys_addr=60265000 - PageTable: PD=client VADDR=0x0 11 cap_addr=8000000000000026 phys_addr=60266000 - PageTable: PD=client VADDR=0xffc0000000 11 cap_addr=8000000000000027 phys_addr=60267000 - PageTable: PD=serial_server VADDR=0x200000 11 cap_addr=8000000000000028 phys_addr=60268000 - PageTable: PD=serial_server VADDR=0x2000000 11 cap_addr=8000000000000029 phys_addr=60269000 - PageTable: PD=serial_server VADDR=0x4000000 11 cap_addr=800000000000002a phys_addr=6026a000 - PageTable: PD=serial_server VADDR=0xffffe00000 11 cap_addr=800000000000002b phys_addr=6026b000 - PageTable: PD=client VADDR=0x200000 11 cap_addr=800000000000002c phys_addr=6026c000 - PageTable: PD=client VADDR=0x4000000 11 cap_addr=800000000000002d phys_addr=6026d000 - PageTable: PD=client VADDR=0xffffe00000 11 cap_addr=800000000000002e phys_addr=6026e000 - CNode: PD=serial_server 4 cap_addr=800000000000002f phys_addr=60270000 - CNode: PD=client 4 cap_addr=8000000000000030 phys_addr=60274000 + Page(4 KiB): IPC Buffer PD=wordle_server 9 cap_addr=8000000000000005 phys_addr=60005000 + Page(4 KiB): MR=serial_to_client #0 9 cap_addr=8000000000000006 phys_addr=60006000 + Page(4 KiB): MR=client_to_serial #0 9 cap_addr=8000000000000007 phys_addr=60007000 + Page(4 KiB): MR=STACK:serial_server #0 9 cap_addr=8000000000000008 phys_addr=60008000 + Page(4 KiB): MR=STACK:client #0 9 cap_addr=8000000000000009 phys_addr=60009000 + Page(4 KiB): MR=STACK:wordle_server #0 9 cap_addr=800000000000000a phys_addr=6000a000 + Page(4 KiB): MR=uart @ 9000000 9 cap_addr=800000000000000b phys_addr=9000000 + Page(4 KiB): MR=ELF:serial_server-0 @ 60248000 9 cap_addr=800000000000000c phys_addr=60248000 + Page(4 KiB): MR=ELF:serial_server-0 @ 60249000 9 cap_addr=800000000000000d phys_addr=60249000 + Page(4 KiB): MR=ELF:serial_server-0 @ 6024a000 9 cap_addr=800000000000000e phys_addr=6024a000 + Page(4 KiB): MR=ELF:serial_server-0 @ 6024b000 9 cap_addr=800000000000000f phys_addr=6024b000 + Page(4 KiB): MR=ELF:serial_server-0 @ 6024c000 9 cap_addr=8000000000000010 phys_addr=6024c000 + Page(4 KiB): MR=ELF:serial_server-0 @ 6024d000 9 cap_addr=8000000000000011 phys_addr=6024d000 + Page(4 KiB): MR=ELF:serial_server-1 @ 6024e000 9 cap_addr=8000000000000012 phys_addr=6024e000 + Page(4 KiB): MR=ELF:client-0 @ 6024f000 9 cap_addr=8000000000000013 phys_addr=6024f000 + Page(4 KiB): MR=ELF:client-0 @ 60250000 9 cap_addr=8000000000000014 phys_addr=60250000 + Page(4 KiB): MR=ELF:client-0 @ 60251000 9 cap_addr=8000000000000015 phys_addr=60251000 + Page(4 KiB): MR=ELF:client-0 @ 60252000 9 cap_addr=8000000000000016 phys_addr=60252000 + Page(4 KiB): MR=ELF:client-0 @ 60253000 9 cap_addr=8000000000000017 phys_addr=60253000 + Page(4 KiB): MR=ELF:client-0 @ 60254000 9 cap_addr=8000000000000018 phys_addr=60254000 + Page(4 KiB): MR=ELF:client-1 @ 60255000 9 cap_addr=8000000000000019 phys_addr=60255000 + Page(4 KiB): MR=ELF:wordle_server-0 @ 60256000 9 cap_addr=800000000000001a phys_addr=60256000 + Page(4 KiB): MR=ELF:wordle_server-0 @ 60257000 9 cap_addr=800000000000001b phys_addr=60257000 + Page(4 KiB): MR=ELF:wordle_server-0 @ 60258000 9 cap_addr=800000000000001c phys_addr=60258000 + Page(4 KiB): MR=ELF:wordle_server-0 @ 60259000 9 cap_addr=800000000000001d phys_addr=60259000 + Page(4 KiB): MR=ELF:wordle_server-0 @ 6025a000 9 cap_addr=800000000000001e phys_addr=6025a000 + Page(4 KiB): MR=ELF:wordle_server-1 @ 6025b000 9 cap_addr=800000000000001f phys_addr=6025b000 + TCB: PD=serial_server 1 cap_addr=8000000000000020 phys_addr=6000b000 + TCB: PD=client 1 cap_addr=8000000000000021 phys_addr=6000b800 + TCB: PD=wordle_server 1 cap_addr=8000000000000022 phys_addr=6000c000 + SchedContext: PD=serial_server 5 cap_addr=8000000000000023 phys_addr=60268000 + SchedContext: PD=client 5 cap_addr=8000000000000024 phys_addr=6026a000 + SchedContext: PD=wordle_server 5 cap_addr=8000000000000025 phys_addr=6026c000 + Reply: Monitor 6 cap_addr=8000000000000026 phys_addr=6000c800 + Reply: PD=serial_server 6 cap_addr=8000000000000027 phys_addr=6000c820 + Reply: PD=client 6 cap_addr=8000000000000028 phys_addr=6000c840 + Reply: PD=wordle_server 6 cap_addr=8000000000000029 phys_addr=6000c860 + EP: Monitor Fault 2 cap_addr=800000000000002a phys_addr=6000c880 + EP: PD=wordle_server 2 cap_addr=800000000000002b phys_addr=6000c890 + Notification: PD=serial_server 3 cap_addr=800000000000002c phys_addr=6000c8c0 + Notification: PD=client 3 cap_addr=800000000000002d phys_addr=6000c900 + Notification: PD=wordle_server 3 cap_addr=800000000000002e phys_addr=6000c940 + VSpace: PD=serial_server 8 cap_addr=800000000000002f phys_addr=60270000 + VSpace: PD=client 8 cap_addr=8000000000000030 phys_addr=60272000 + VSpace: PD=wordle_server 8 cap_addr=8000000000000031 phys_addr=60274000 + PageTable: PD=serial_server VADDR=0x0 11 cap_addr=8000000000000032 phys_addr=60276000 + PageTable: PD=serial_server VADDR=0xffc0000000 11 cap_addr=8000000000000033 phys_addr=60277000 + PageTable: PD=client VADDR=0x0 11 cap_addr=8000000000000034 phys_addr=60278000 + PageTable: PD=client VADDR=0xffc0000000 11 cap_addr=8000000000000035 phys_addr=60279000 + PageTable: PD=wordle_server VADDR=0x0 11 cap_addr=8000000000000036 phys_addr=6027a000 + PageTable: PD=wordle_server VADDR=0xffc0000000 11 cap_addr=8000000000000037 phys_addr=6027b000 + PageTable: PD=serial_server VADDR=0x200000 11 cap_addr=8000000000000038 phys_addr=60280000 + PageTable: PD=serial_server VADDR=0x2000000 11 cap_addr=8000000000000039 phys_addr=60281000 + PageTable: PD=serial_server VADDR=0x4000000 11 cap_addr=800000000000003a phys_addr=60282000 + PageTable: PD=serial_server VADDR=0xffffe00000 11 cap_addr=800000000000003b phys_addr=60283000 + PageTable: PD=client VADDR=0x200000 11 cap_addr=800000000000003c phys_addr=60284000 + PageTable: PD=client VADDR=0x4000000 11 cap_addr=800000000000003d phys_addr=60285000 + PageTable: PD=client VADDR=0xffffe00000 11 cap_addr=800000000000003e phys_addr=60286000 + PageTable: PD=wordle_server VADDR=0x200000 11 cap_addr=800000000000003f phys_addr=60287000 + PageTable: PD=wordle_server VADDR=0xffffe00000 11 cap_addr=8000000000000040 phys_addr=60288000 + CNode: PD=serial_server 4 cap_addr=8000000000000041 phys_addr=6028c000 + CNode: PD=client 4 cap_addr=8000000000000042 phys_addr=60290000 + CNode: PD=wordle_server 4 cap_addr=8000000000000043 phys_addr=60294000 # Bootstrap Kernel Invocations Detail @@ -88,9 +109,9 @@ root (cap) 0x0000000000000002 (CNode: init) node_index 0 node_depth 0 - node_offset 96 + node_offset 97 num_objects 1 - 0x0001 CNode - Mint - 0x0000000000000060 (CNode: root) + 0x0001 CNode - Mint - 0x0000000000000061 (CNode: root) dest_index 0 dest_depth 1 src_root (cap) 0x0000000000000002 (CNode: init) @@ -100,7 +121,7 @@ badge 51 0x0002 TCB - SetSpace - 0x0000000000000001 (TCB: init) fault_ep (cap) 0x0000000000000000 (null) - cspace_root (cap) 0x0000000000000060 (CNode: root) + cspace_root (cap) 0x0000000000000061 (CNode: root) cspace_root_data 0 vspace_root (cap) 0x0000000000000003 (VSpace: init) vspace_root_data 0 @@ -110,20 +131,20 @@ root (cap) 0x0000000000000002 (CNode: init) node_index 0 node_depth 0 - node_offset 97 + node_offset 98 num_objects 1 - 0x0004 CNode - Mint - 0x0000000000000060 (CNode: root) + 0x0004 CNode - Mint - 0x0000000000000061 (CNode: root) dest_index 1 dest_depth 1 src_root (cap) 0x0000000000000002 (CNode: init) - src_obj (cap) 0x0000000000000061 (CNode: system) + src_obj (cap) 0x0000000000000062 (CNode: system) src_depth 64 rights 15 badge 56 0x0005 Untyped - Retype - 0x000000000000001b (Untyped @ 0x60246000:0x2000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 0 @@ -131,7 +152,7 @@ 0x0006 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) object_type 11 (SEL4_PAGE_TABLE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 2 @@ -152,537 +173,703 @@ 0x0000 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 3 - num_objects 6 + num_objects 8 0x0001 Untyped - Retype - 0x0000000000000033 (Untyped @ 0x9000000:0x1000000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) - node_index 1 - node_depth 1 - node_offset 9 - num_objects 1 - 0x0002 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) - object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) - size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) - node_index 1 - node_depth 1 - node_offset 10 - num_objects 1 - 0x0003 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) - object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) - size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 11 num_objects 1 - 0x0004 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) + 0x0002 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 12 num_objects 1 - 0x0005 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) + 0x0003 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 13 num_objects 1 - 0x0006 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) + 0x0004 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 14 num_objects 1 - 0x0007 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) + 0x0005 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 15 num_objects 1 - 0x0008 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) + 0x0006 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 16 num_objects 1 - 0x0009 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) + 0x0007 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 17 num_objects 1 - 0x000a Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x4000 (device)) + 0x0008 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 18 num_objects 1 - 0x000b Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x4000 (device)) + 0x0009 Untyped - Retype - 0x000000000000001c (Untyped @ 0x60248000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 19 num_objects 1 - 0x000c Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x4000 (device)) + 0x000a Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 20 num_objects 1 - 0x000d Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x4000 (device)) + 0x000b Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 21 num_objects 1 - 0x000e Untyped - Retype - 0x000000000000001e (Untyped @ 0x60254000:0x2000 (device)) + 0x000c Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 22 num_objects 1 - 0x000f Untyped - Retype - 0x000000000000001e (Untyped @ 0x60254000:0x2000 (device)) + 0x000d Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 23 num_objects 1 - 0x0010 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) - object_type 1 (SEL4_TCB_OBJECT - 0x800) + 0x000e Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 24 - num_objects 2 - 0x0011 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) - object_type 5 (SEL4_SCHEDCONTEXT_OBJECT - variable size) - size_bits 8 (0x100) - root (cap) 0x0000000000000060 (CNode: root) + num_objects 1 + 0x000f Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 25 + num_objects 1 + 0x0010 Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 26 - num_objects 2 - 0x0012 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) - object_type 6 (SEL4_REPLY_OBJECT - 0x20) + num_objects 1 + 0x0011 Untyped - Retype - 0x000000000000001d (Untyped @ 0x60250000:0x8000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 27 + num_objects 1 + 0x0012 Untyped - Retype - 0x000000000000001e (Untyped @ 0x60258000:0x4000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 28 - num_objects 3 - 0x0013 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) - object_type 2 (SEL4_ENDPOINT_OBJECT - 0x10) + num_objects 1 + 0x0013 Untyped - Retype - 0x000000000000001e (Untyped @ 0x60258000:0x4000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 29 + num_objects 1 + 0x0014 Untyped - Retype - 0x000000000000001e (Untyped @ 0x60258000:0x4000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 30 + num_objects 1 + 0x0015 Untyped - Retype - 0x000000000000001e (Untyped @ 0x60258000:0x4000 (device)) + object_type 9 (SEL4_SMALL_PAGE_OBJECT - 0x1000) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 31 num_objects 1 - 0x0014 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) - object_type 3 (SEL4_NOTIFICATION_OBJECT - 0x40) + 0x0016 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) + object_type 1 (SEL4_TCB_OBJECT - 0x800) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 32 + num_objects 3 + 0x0017 Untyped - Retype - 0x0000000000000044 (Untyped @ 0x60268000:0x8000) + object_type 5 (SEL4_SCHEDCONTEXT_OBJECT - variable size) + size_bits 8 (0x100) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 35 + num_objects 3 + 0x0018 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) + object_type 6 (SEL4_REPLY_OBJECT - 0x20) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 38 + num_objects 4 + 0x0019 Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) + object_type 2 (SEL4_ENDPOINT_OBJECT - 0x10) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 42 num_objects 2 - 0x0015 Untyped - Retype - 0x0000000000000044 (Untyped @ 0x60260000:0x20000) + 0x001a Untyped - Retype - 0x0000000000000042 (Untyped @ 0x60000000:0x10000) + object_type 3 (SEL4_NOTIFICATION_OBJECT - 0x40) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 44 + num_objects 3 + 0x001b Untyped - Retype - 0x0000000000000045 (Untyped @ 0x60270000:0x10000) object_type 8 (SEL4_VSPACE_OBJECT - 0x2000) size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) - node_index 1 - node_depth 1 - node_offset 34 - num_objects 2 - 0x0016 Untyped - Retype - 0x0000000000000044 (Untyped @ 0x60260000:0x20000) - object_type 11 (SEL4_PAGE_TABLE_OBJECT - 0x1000) - size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) - node_index 1 - node_depth 1 - node_offset 36 - num_objects 4 - 0x0017 Untyped - Retype - 0x0000000000000044 (Untyped @ 0x60260000:0x20000) - object_type 11 (SEL4_PAGE_TABLE_OBJECT - 0x1000) - size_bits 0 (N/A) - root (cap) 0x0000000000000060 (CNode: root) - node_index 1 - node_depth 1 - node_offset 40 - num_objects 7 - 0x0018 Untyped - Retype - 0x0000000000000044 (Untyped @ 0x60260000:0x20000) - object_type 4 (SEL4_CNODE_OBJECT - variable size) - size_bits 9 (0x200) - root (cap) 0x0000000000000060 (CNode: root) + root (cap) 0x0000000000000061 (CNode: root) node_index 1 node_depth 1 node_offset 47 - num_objects 2 - 0x0019 IRQ Control - Get - 0x0000000000000004 (IRQ Control) + num_objects 3 + 0x001c Untyped - Retype - 0x0000000000000045 (Untyped @ 0x60270000:0x10000) + object_type 11 (SEL4_PAGE_TABLE_OBJECT - 0x1000) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 50 + num_objects 6 + 0x001d Untyped - Retype - 0x0000000000000046 (Untyped @ 0x60280000:0x80000) + object_type 11 (SEL4_PAGE_TABLE_OBJECT - 0x1000) + size_bits 0 (N/A) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 56 + num_objects 9 + 0x001e Untyped - Retype - 0x0000000000000046 (Untyped @ 0x60280000:0x80000) + object_type 4 (SEL4_CNODE_OBJECT - variable size) + size_bits 9 (0x200) + root (cap) 0x0000000000000061 (CNode: root) + node_index 1 + node_depth 1 + node_offset 65 + num_objects 3 + 0x001f IRQ Control - Get - 0x0000000000000004 (IRQ Control) irq 33 trigger 0 - dest_root (cap) 0x0000000000000060 (CNode: root) - dest_index 9223372036854775857 + dest_root (cap) 0x0000000000000061 (CNode: root) + dest_index 9223372036854775876 dest_depth 64 - 0x001a ASID Pool - Assign - 0x0000000000000006 (ASID Pool: init) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) - REPEAT: count=2 - 0x001b CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 50 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000009 (Page(4 KiB): MR=uart @ 9000000) - src_depth 64 - rights 3 - badge 0 - 0x001c CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 51 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000005 (Page(4 KiB): MR=serial_to_client #0) - src_depth 64 - rights 3 - badge 0 - 0x001d CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 52 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000006 (Page(4 KiB): MR=client_to_serial #0) - src_depth 64 - rights 2 - badge 0 - 0x001e CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 53 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x800000000000000a (Page(4 KiB): MR=ELF:serial_server-0 @ 60248000) - src_depth 64 - rights 2 - badge 0 - REPEAT: count=6 - 0x001f CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 59 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000010 (Page(4 KiB): MR=ELF:serial_server-1 @ 6024e000) - src_depth 64 - rights 3 - badge 0 - 0x0020 CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 60 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000007 (Page(4 KiB): MR=STACK:serial_server #0) - src_depth 64 - rights 3 - badge 0 - 0x0021 CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 61 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000005 (Page(4 KiB): MR=serial_to_client #0) - src_depth 64 - rights 2 - badge 0 - 0x0022 CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 62 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000006 (Page(4 KiB): MR=client_to_serial #0) - src_depth 64 - rights 3 - badge 0 - 0x0023 CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 63 - dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000011 (Page(4 KiB): MR=ELF:client-0 @ 6024f000) - src_depth 64 - rights 2 - badge 0 - REPEAT: count=6 - 0x0024 CNode - Mint - 0x0000000000000061 (CNode: system) + 0x0020 ASID Pool - Assign - 0x0000000000000006 (ASID Pool: init) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) + REPEAT: count=3 + 0x0021 CNode - Mint - 0x0000000000000062 (CNode: system) dest_index 69 dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000017 (Page(4 KiB): MR=ELF:client-1 @ 60255000) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000000b (Page(4 KiB): MR=uart @ 9000000) src_depth 64 rights 3 badge 0 - 0x0025 CNode - Mint - 0x0000000000000061 (CNode: system) + 0x0022 CNode - Mint - 0x0000000000000062 (CNode: system) dest_index 70 dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000008 (Page(4 KiB): MR=STACK:client #0) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000006 (Page(4 KiB): MR=serial_to_client #0) src_depth 64 rights 3 badge 0 - 0x0026 CNode - Mint - 0x0000000000000061 (CNode: system) + 0x0023 CNode - Mint - 0x0000000000000062 (CNode: system) dest_index 71 dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000020 (Notification: PD=serial_server) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000007 (Page(4 KiB): MR=client_to_serial #0) src_depth 64 - rights 15 - badge 2 - 0x0027 CNode - Mint - 0x0000000000000061 (CNode: system) + rights 2 + badge 0 + 0x0024 CNode - Mint - 0x0000000000000062 (CNode: system) dest_index 72 dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x800000000000001f (EP: Monitor Fault) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000000c (Page(4 KiB): MR=ELF:serial_server-0 @ 60248000) src_depth 64 - rights 15 - badge 1 - 0x0028 CNode - Mint - 0x0000000000000061 (CNode: system) - dest_index 73 + rights 2 + badge 0 + REPEAT: count=6 + 0x0025 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 78 dest_depth 7 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x800000000000001f (EP: Monitor Fault) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000012 (Page(4 KiB): MR=ELF:serial_server-1 @ 6024e000) + src_depth 64 + rights 3 + badge 0 + 0x0026 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 79 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000008 (Page(4 KiB): MR=STACK:serial_server #0) + src_depth 64 + rights 3 + badge 0 + 0x0027 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 80 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000006 (Page(4 KiB): MR=serial_to_client #0) + src_depth 64 + rights 2 + badge 0 + 0x0028 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 81 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000007 (Page(4 KiB): MR=client_to_serial #0) + src_depth 64 + rights 3 + badge 0 + 0x0029 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 82 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000013 (Page(4 KiB): MR=ELF:client-0 @ 6024f000) + src_depth 64 + rights 2 + badge 0 + REPEAT: count=6 + 0x002a CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 88 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000019 (Page(4 KiB): MR=ELF:client-1 @ 60255000) + src_depth 64 + rights 3 + badge 0 + 0x002b CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 89 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000009 (Page(4 KiB): MR=STACK:client #0) + src_depth 64 + rights 3 + badge 0 + 0x002c CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 90 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000001a (Page(4 KiB): MR=ELF:wordle_server-0 @ 60256000) + src_depth 64 + rights 2 + badge 0 + REPEAT: count=5 + 0x002d CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 95 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000001f (Page(4 KiB): MR=ELF:wordle_server-1 @ 6025b000) + src_depth 64 + rights 3 + badge 0 + 0x002e CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 96 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000000a (Page(4 KiB): MR=STACK:wordle_server #0) + src_depth 64 + rights 3 + badge 0 + 0x002f CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 97 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002c (Notification: PD=serial_server) src_depth 64 rights 15 badge 2 - 0x0029 CNode - Mint - 0x800000000000002f (CNode: PD=serial_server) + 0x0030 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 98 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002a (EP: Monitor Fault) + src_depth 64 + rights 15 + badge 1 + 0x0031 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 99 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002a (EP: Monitor Fault) + src_depth 64 + rights 15 + badge 2 + 0x0032 CNode - Mint - 0x0000000000000062 (CNode: system) + dest_index 100 + dest_depth 7 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002a (EP: Monitor Fault) + src_depth 64 + rights 15 + badge 3 + 0x0033 CNode - Mint - 0x8000000000000041 (CNode: PD=serial_server) dest_index 1 dest_depth 9 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000020 (Notification: PD=serial_server) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002c (Notification: PD=serial_server) src_depth 64 rights 15 badge 0 - 0x002a CNode - Mint - 0x8000000000000030 (CNode: PD=client) + 0x0034 CNode - Mint - 0x8000000000000042 (CNode: PD=client) dest_index 1 dest_depth 9 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000021 (Notification: PD=client) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002d (Notification: PD=client) src_depth 64 rights 15 badge 0 - 0x002b CNode - Mint - 0x800000000000002f (CNode: PD=serial_server) + 0x0035 CNode - Mint - 0x8000000000000043 (CNode: PD=wordle_server) + dest_index 1 + dest_depth 9 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002b (EP: PD=wordle_server) + src_depth 64 + rights 15 + badge 0 + 0x0036 CNode - Mint - 0x8000000000000041 (CNode: PD=serial_server) dest_index 4 dest_depth 9 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x800000000000001d (Reply: PD=serial_server) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000027 (Reply: PD=serial_server) src_depth 64 rights 15 badge 1 - REPEAT: count=2 - 0x002c CNode - Mint - 0x800000000000002f (CNode: PD=serial_server) + REPEAT: count=3 + 0x0037 CNode - Mint - 0x8000000000000041 (CNode: PD=serial_server) dest_index 3 dest_depth 9 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000022 (VSpace: PD=serial_server) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002f (VSpace: PD=serial_server) src_depth 64 rights 15 badge 0 - REPEAT: count=2 - 0x002d CNode - Mint - 0x800000000000002f (CNode: PD=serial_server) + REPEAT: count=3 + 0x0038 CNode - Mint - 0x8000000000000041 (CNode: PD=serial_server) dest_index 139 dest_depth 9 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000031 (IRQ Handler: irq=33) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x8000000000000044 (IRQ Handler: irq=33) src_depth 64 rights 15 badge 0 - 0x002e CNode - Mint - 0x800000000000002f (CNode: PD=serial_server) + 0x0039 CNode - Mint - 0x8000000000000041 (CNode: PD=serial_server) dest_index 12 dest_depth 9 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000021 (Notification: PD=client) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002d (Notification: PD=client) src_depth 64 rights 15 badge 2 - 0x002f CNode - Mint - 0x8000000000000030 (CNode: PD=client) + 0x003a CNode - Mint - 0x8000000000000042 (CNode: PD=client) dest_index 11 dest_depth 9 - src_root (cap) 0x0000000000000060 (CNode: root) - src_obj (cap) 0x8000000000000020 (Notification: PD=serial_server) + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002c (Notification: PD=serial_server) src_depth 64 rights 15 badge 4 - 0x0030 IRQ Handler - SetNotification - 0x8000000000000031 (IRQ Handler: irq=33) - notification (cap) 0x8000000000000047 (Notification: PD=serial_server (badge=0x2)) - 0x0031 Page Table - Map - 0x8000000000000024 (PageTable: PD=serial_server VADDR=0x0) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x003b CNode - Mint - 0x8000000000000042 (CNode: PD=client) + dest_index 12 + dest_depth 9 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002e (Notification: PD=wordle_server) + src_depth 64 + rights 15 + badge 2 + 0x003c CNode - Mint - 0x8000000000000043 (CNode: PD=wordle_server) + dest_index 11 + dest_depth 9 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002d (Notification: PD=client) + src_depth 64 + rights 15 + badge 4 + 0x003d CNode - Mint - 0x8000000000000042 (CNode: PD=client) + dest_index 76 + dest_depth 9 + src_root (cap) 0x0000000000000061 (CNode: root) + src_obj (cap) 0x800000000000002b (EP: PD=wordle_server) + src_depth 64 + rights 15 + badge 9223372036854775809 + 0x003e IRQ Handler - SetNotification - 0x8000000000000044 (IRQ Handler: irq=33) + notification (cap) 0x8000000000000061 (Notification: PD=serial_server (badge=0x2)) + 0x003f Page Table - Map - 0x8000000000000032 (PageTable: PD=serial_server VADDR=0x0) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x0 attr 3 - 0x0032 Page Table - Map - 0x8000000000000025 (PageTable: PD=serial_server VADDR=0xffc0000000) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0040 Page Table - Map - 0x8000000000000033 (PageTable: PD=serial_server VADDR=0xffc0000000) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0xffc0000000 attr 3 - 0x0033 Page Table - Map - 0x8000000000000026 (PageTable: PD=client VADDR=0x0) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0041 Page Table - Map - 0x8000000000000034 (PageTable: PD=client VADDR=0x0) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x0 attr 3 - 0x0034 Page Table - Map - 0x8000000000000027 (PageTable: PD=client VADDR=0xffc0000000) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0042 Page Table - Map - 0x8000000000000035 (PageTable: PD=client VADDR=0xffc0000000) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0xffc0000000 attr 3 - 0x0035 Page Table - Map - 0x8000000000000028 (PageTable: PD=serial_server VADDR=0x200000) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0043 Page Table - Map - 0x8000000000000036 (PageTable: PD=wordle_server VADDR=0x0) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0x0 + attr 3 + 0x0044 Page Table - Map - 0x8000000000000037 (PageTable: PD=wordle_server VADDR=0xffc0000000) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0xffc0000000 + attr 3 + 0x0045 Page Table - Map - 0x8000000000000038 (PageTable: PD=serial_server VADDR=0x200000) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x200000 attr 3 - 0x0036 Page Table - Map - 0x8000000000000029 (PageTable: PD=serial_server VADDR=0x2000000) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0046 Page Table - Map - 0x8000000000000039 (PageTable: PD=serial_server VADDR=0x2000000) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x2000000 attr 3 - 0x0037 Page Table - Map - 0x800000000000002a (PageTable: PD=serial_server VADDR=0x4000000) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0047 Page Table - Map - 0x800000000000003a (PageTable: PD=serial_server VADDR=0x4000000) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x4000000 attr 3 - 0x0038 Page Table - Map - 0x800000000000002b (PageTable: PD=serial_server VADDR=0xffffe00000) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0048 Page Table - Map - 0x800000000000003b (PageTable: PD=serial_server VADDR=0xffffe00000) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0xffffe00000 attr 3 - 0x0039 Page Table - Map - 0x800000000000002c (PageTable: PD=client VADDR=0x200000) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0049 Page Table - Map - 0x800000000000003c (PageTable: PD=client VADDR=0x200000) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x200000 attr 3 - 0x003a Page Table - Map - 0x800000000000002d (PageTable: PD=client VADDR=0x4000000) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x004a Page Table - Map - 0x800000000000003d (PageTable: PD=client VADDR=0x4000000) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x4000000 attr 3 - 0x003b Page Table - Map - 0x800000000000002e (PageTable: PD=client VADDR=0xffffe00000) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x004b Page Table - Map - 0x800000000000003e (PageTable: PD=client VADDR=0xffffe00000) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0xffffe00000 attr 3 - 0x003c Page - Map - 0x8000000000000032 (Page(4 KiB): MR=uart @ 9000000 (derived)) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x004c Page Table - Map - 0x800000000000003f (PageTable: PD=wordle_server VADDR=0x200000) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0x200000 + attr 3 + 0x004d Page Table - Map - 0x8000000000000040 (PageTable: PD=wordle_server VADDR=0xffffe00000) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0xffffe00000 + attr 3 + 0x004e Page - Map - 0x8000000000000045 (Page(4 KiB): MR=uart @ 9000000 (derived)) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x2000000 rights 3 attr 6 - 0x003d Page - Map - 0x8000000000000033 (Page(4 KiB): MR=serial_to_client #0 (derived)) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x004f Page - Map - 0x8000000000000046 (Page(4 KiB): MR=serial_to_client #0 (derived)) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x4000000 rights 3 attr 7 - 0x003e Page - Map - 0x8000000000000034 (Page(4 KiB): MR=client_to_serial #0 (derived)) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0050 Page - Map - 0x8000000000000047 (Page(4 KiB): MR=client_to_serial #0 (derived)) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x4001000 rights 2 attr 7 - 0x003f Page - Map - 0x8000000000000035 (Page(4 KiB): MR=ELF:serial_server-0 @ 60248000 (derived)) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0051 Page - Map - 0x8000000000000048 (Page(4 KiB): MR=ELF:serial_server-0 @ 60248000 (derived)) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x200000 rights 2 attr 3 REPEAT: count=6 - 0x0040 Page - Map - 0x800000000000003b (Page(4 KiB): MR=ELF:serial_server-1 @ 6024e000 (derived)) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0052 Page - Map - 0x800000000000004e (Page(4 KiB): MR=ELF:serial_server-1 @ 6024e000 (derived)) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x206000 rights 3 attr 7 - 0x0041 Page - Map - 0x800000000000003c (Page(4 KiB): MR=STACK:serial_server #0 (derived)) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0053 Page - Map - 0x800000000000004f (Page(4 KiB): MR=STACK:serial_server #0 (derived)) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0xfffffff000 rights 3 attr 7 - 0x0042 Page - Map - 0x800000000000003d (Page(4 KiB): MR=serial_to_client #0 (derived)) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0054 Page - Map - 0x8000000000000050 (Page(4 KiB): MR=serial_to_client #0 (derived)) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x4000000 rights 2 attr 7 - 0x0043 Page - Map - 0x800000000000003e (Page(4 KiB): MR=client_to_serial #0 (derived)) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0055 Page - Map - 0x8000000000000051 (Page(4 KiB): MR=client_to_serial #0 (derived)) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x4001000 rights 3 attr 7 - 0x0044 Page - Map - 0x800000000000003f (Page(4 KiB): MR=ELF:client-0 @ 6024f000 (derived)) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0056 Page - Map - 0x8000000000000052 (Page(4 KiB): MR=ELF:client-0 @ 6024f000 (derived)) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x200000 rights 2 attr 3 REPEAT: count=6 - 0x0045 Page - Map - 0x8000000000000045 (Page(4 KiB): MR=ELF:client-1 @ 60255000 (derived)) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0057 Page - Map - 0x8000000000000058 (Page(4 KiB): MR=ELF:client-1 @ 60255000 (derived)) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x206000 rights 3 attr 7 - 0x0046 Page - Map - 0x8000000000000046 (Page(4 KiB): MR=STACK:client #0 (derived)) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x0058 Page - Map - 0x8000000000000059 (Page(4 KiB): MR=STACK:client #0 (derived)) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0xfffffff000 rights 3 attr 7 - 0x0047 Page - Map - 0x8000000000000003 (Page(4 KiB): IPC Buffer PD=serial_server) - vspace (cap) 0x8000000000000022 (VSpace: PD=serial_server) + 0x0059 Page - Map - 0x800000000000005a (Page(4 KiB): MR=ELF:wordle_server-0 @ 60256000 (derived)) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0x200000 + rights 2 + attr 3 + REPEAT: count=5 + 0x005a Page - Map - 0x800000000000005f (Page(4 KiB): MR=ELF:wordle_server-1 @ 6025b000 (derived)) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0x205000 + rights 3 + attr 7 + 0x005b Page - Map - 0x8000000000000060 (Page(4 KiB): MR=STACK:wordle_server #0 (derived)) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0xfffffff000 + rights 3 + attr 7 + 0x005c Page - Map - 0x8000000000000003 (Page(4 KiB): IPC Buffer PD=serial_server) + vspace (cap) 0x800000000000002f (VSpace: PD=serial_server) vaddr 0x207000 rights 3 attr 7 - 0x0048 Page - Map - 0x8000000000000004 (Page(4 KiB): IPC Buffer PD=client) - vspace (cap) 0x8000000000000023 (VSpace: PD=client) + 0x005d Page - Map - 0x8000000000000004 (Page(4 KiB): IPC Buffer PD=client) + vspace (cap) 0x8000000000000030 (VSpace: PD=client) vaddr 0x207000 rights 3 attr 7 - 0x0049 SchedControl - ConfigureFlags - 0x0000000000000012 (None) - schedcontext (cap) 0x800000000000001a (SchedContext: PD=serial_server) + 0x005e Page - Map - 0x8000000000000005 (Page(4 KiB): IPC Buffer PD=wordle_server) + vspace (cap) 0x8000000000000031 (VSpace: PD=wordle_server) + vaddr 0x206000 + rights 3 + attr 7 + 0x005f SchedControl - ConfigureFlags - 0x0000000000000012 (None) + schedcontext (cap) 0x8000000000000023 (SchedContext: PD=serial_server) budget 1000 period 1000 extra_refills 0 badge 256 flags 0 - 0x004a SchedControl - ConfigureFlags - 0x0000000000000012 (None) - schedcontext (cap) 0x800000000000001b (SchedContext: PD=client) + 0x0060 SchedControl - ConfigureFlags - 0x0000000000000012 (None) + schedcontext (cap) 0x8000000000000024 (SchedContext: PD=client) budget 1000 period 1000 extra_refills 0 badge 257 flags 0 - 0x004b TCB - SetSchedParams - 0x8000000000000018 (TCB: PD=serial_server) + 0x0061 SchedControl - ConfigureFlags - 0x0000000000000012 (None) + schedcontext (cap) 0x8000000000000025 (SchedContext: PD=wordle_server) + budget 1000 + period 1000 + extra_refills 0 + badge 258 + flags 0 + 0x0062 TCB - SetSchedParams - 0x8000000000000020 (TCB: PD=serial_server) authority (cap) 0x0000000000000001 (TCB: init) mcp 254 priority 254 - sched_context (cap) 0x800000000000001a (SchedContext: PD=serial_server) - fault_ep (cap) 0x800000000000001f (EP: Monitor Fault) - 0x004c TCB - SetSchedParams - 0x8000000000000019 (TCB: PD=client) + sched_context (cap) 0x8000000000000023 (SchedContext: PD=serial_server) + fault_ep (cap) 0x800000000000002a (EP: Monitor Fault) + 0x0063 TCB - SetSchedParams - 0x8000000000000021 (TCB: PD=client) authority (cap) 0x0000000000000001 (TCB: init) mcp 253 priority 253 - sched_context (cap) 0x800000000000001b (SchedContext: PD=client) - fault_ep (cap) 0x800000000000001f (EP: Monitor Fault) - 0x004d TCB - SetSpace - 0x8000000000000018 (TCB: PD=serial_server) - fault_ep (cap) 0x8000000000000048 (None) - cspace_root (cap) 0x800000000000002f (CNode: PD=serial_server) + sched_context (cap) 0x8000000000000024 (SchedContext: PD=client) + fault_ep (cap) 0x800000000000002a (EP: Monitor Fault) + 0x0064 TCB - SetSchedParams - 0x8000000000000022 (TCB: PD=wordle_server) + authority (cap) 0x0000000000000001 (TCB: init) + mcp 254 + priority 254 + sched_context (cap) 0x8000000000000025 (SchedContext: PD=wordle_server) + fault_ep (cap) 0x800000000000002a (EP: Monitor Fault) + 0x0065 TCB - SetSpace - 0x8000000000000020 (TCB: PD=serial_server) + fault_ep (cap) 0x8000000000000062 (None) + cspace_root (cap) 0x8000000000000041 (CNode: PD=serial_server) cspace_root_data 55 - vspace_root (cap) 0x8000000000000022 (VSpace: PD=serial_server) + vspace_root (cap) 0x800000000000002f (VSpace: PD=serial_server) vspace_root_data 0 - REPEAT: count=2 - 0x004e TCB - SetIPCBuffer - 0x8000000000000018 (TCB: PD=serial_server) + REPEAT: count=3 + 0x0066 TCB - SetIPCBuffer - 0x8000000000000020 (TCB: PD=serial_server) buffer 0x207000 buffer_frame (cap) 0x8000000000000003 (Page(4 KiB): IPC Buffer PD=serial_server) - 0x004f TCB - SetIPCBuffer - 0x8000000000000019 (TCB: PD=client) + 0x0067 TCB - SetIPCBuffer - 0x8000000000000021 (TCB: PD=client) buffer 0x207000 buffer_frame (cap) 0x8000000000000004 (Page(4 KiB): IPC Buffer PD=client) - 0x0050 TCB - WriteRegisters - 0x8000000000000018 (TCB: PD=serial_server) + 0x0068 TCB - SetIPCBuffer - 0x8000000000000022 (TCB: PD=wordle_server) + buffer 0x206000 + buffer_frame (cap) 0x8000000000000005 (Page(4 KiB): IPC Buffer PD=wordle_server) + 0x0069 TCB - WriteRegisters - 0x8000000000000020 (TCB: PD=serial_server) resume false arch_flags 0 regs pc: 0x0000000000200000 @@ -721,7 +908,7 @@ x28: 0x0000000000000000 tpidr_el0: 0x0000000000000000 tpidrro_el0: 0x0000000000000000 - 0x0051 TCB - WriteRegisters - 0x8000000000000019 (TCB: PD=client) + 0x006a TCB - WriteRegisters - 0x8000000000000021 (TCB: PD=client) resume false arch_flags 0 regs pc: 0x0000000000200000 @@ -760,9 +947,48 @@ x28: 0x0000000000000000 tpidr_el0: 0x0000000000000000 tpidrro_el0: 0x0000000000000000 - 0x0052 TCB - BindNotification - 0x8000000000000018 (TCB: PD=serial_server) - notification (cap) 0x8000000000000020 (Notification: PD=serial_server) - REPEAT: count=2 - 0x0053 TCB - Resume - 0x8000000000000018 (TCB: PD=serial_server) + 0x006b TCB - WriteRegisters - 0x8000000000000022 (TCB: PD=wordle_server) + resume false + arch_flags 0 + regs pc: 0x0000000000200000 + sp: 0x0000010000000000 + spsr: 0x0000000000000000 + x0: 0x0000000000000000 + x1: 0x0000000000000000 + x2: 0x0000000000000000 + x3: 0x0000000000000000 + x4: 0x0000000000000000 + x5: 0x0000000000000000 + x6: 0x0000000000000000 + x7: 0x0000000000000000 + x8: 0x0000000000000000 + x16: 0x0000000000000000 + x17: 0x0000000000000000 + x18: 0x0000000000000000 + x29: 0x0000000000000000 + x30: 0x0000000000000000 + x9: 0x0000000000000000 + x10: 0x0000000000000000 + x11: 0x0000000000000000 + x12: 0x0000000000000000 + x13: 0x0000000000000000 + x14: 0x0000000000000000 + x15: 0x0000000000000000 + x19: 0x0000000000000000 + x20: 0x0000000000000000 + x21: 0x0000000000000000 + x22: 0x0000000000000000 + x23: 0x0000000000000000 + x24: 0x0000000000000000 + x25: 0x0000000000000000 + x26: 0x0000000000000000 + x27: 0x0000000000000000 + x28: 0x0000000000000000 + tpidr_el0: 0x0000000000000000 + tpidrro_el0: 0x0000000000000000 + 0x006c TCB - BindNotification - 0x8000000000000020 (TCB: PD=serial_server) + notification (cap) 0x800000000000002c (Notification: PD=serial_server) + REPEAT: count=3 + 0x006d TCB - Resume - 0x8000000000000020 (TCB: PD=serial_server) - REPEAT: count=2 + REPEAT: count=3 diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/wordle_server.elf b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/wordle_server.elf new file mode 100755 index 0000000..0185226 Binary files /dev/null and b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/wordle_server.elf differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/wordle_server.o b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/wordle_server.o new file mode 100644 index 0000000..b7f85a4 Binary files /dev/null and b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/build/wordle_server.o differ diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/client.c b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/client.c index b1851db..9c8cf93 100644 --- a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/client.c +++ b/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) { diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle.system b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle.system index caec863..450ef55 100644 --- a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle.system +++ b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle.system @@ -18,9 +18,19 @@ + + + + + + + + + + diff --git a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle_server.c b/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle_server.c index baceb15..6136b7b 100644 --- a/ME_2150/microkit_tutorial/microkit_tutorial/tutorial/wordle_server.c +++ b/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) {}