theses/README.md
Rama main · réplica de lectura del repositorio original.
# Bachelor Theses on Selfie
## Autos: A Self-Contained, Self-Compiling Rust Compiler Targeting a Self-Emulating LLVM IR Emulator by Sam Crawford, University of Salzburg, Austria, 2026 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_crawford.pdf), [Repository](https://github.com/scrawfordlk/autos))
This thesis investigates how a self-contained, self-referential software system can be built
to compile and emulate itself. The Selfie system demonstrates this concept using C*,
a subset of C, as its implementation language and RISC-U, a subset of the RISC-V
instruction set architecture, as its target language. Since Selfie is written in C*,
it can compile its own source code into RISC-U, which its emulator can then execute,
producing a program that can compile itself again and, in principle, repeat the process
indefinitely.
Inspired by Selfie, this thesis presents Autos, a self-contained system that follows the
same principle using Rust and LLVM Intermediate Representation (LLVM IR) as opposed to C
and RISC-V. The central challenge lies in defining suitable subsets of both languages
that enable both self-compilation and self-emulation while preserving the essential
characteristics of Rust and LLVM IR. An additional challenge was resolving unexpected
performance issues, which, although not a primary focus of this work,
were largely addressed by revisiting the design of those subsets. To this end,
this thesis introduces *Rust, a subset of Rust, and LLLVM, a subset of LLVM IR.
Like Selfie, Autos is implemented entirely in its source language, *Rust,
allowing it to compile its own source code into LLLVM and execute the resulting
program through emulation. This demonstrates how carefully designed language subsets
can enable self-reference in a self-contained software system.
## Exploring Reasoning Performance of RISC-V Software Models in BTOR2 by Nadir Fejzić, University of Salzburg, Austria, 2024 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_fejzic.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_fejzic))
When working with software programs, we want to ensure that they do not
reach certain unsafe states. Various techniques exist for this purpose,
such as testing. However, testing requires running the program with every
possible input, which is often not practical because of the large input
space. Most often we want to check whether an input exists such that our
program reaches a specific state. This is known as the state reachability
problem, which can be reduced to the boolean satisfiability problem and
solved by SAT-solvers.
The reduction can be done by encoding the sequence of machine instructions
in the program as a satisfiability formula in the theory of bit-vectors,
known as a Satisfiability Modulo Theory (SMT) formula. The resulting
formula is the model of our program. SMT-formulae are then further reduced
to boolean logic formulae by technique called bit-blasting. We can then run
a SAT-solver on resulting boolean formulae, which will tell us whether the
program satisfies the given constraints. Effectively, we reduced the
problem of program correctness to the satisfiability problem. Important to
notice is that only a finite number of instructions can be transformed this
way, which makes the model checking bounded in number of executed
instructions.
As we reduced the program correctness problem to satisfiability problem,
solving it is NP-Complete and computationally expensive. However, model
generation is linear in the size of the input program. We took advantage of
this property and generated many equivalent models to analyze impact of
different configurations on solving performance of `btormc` model
checker.
In this thesis, we present a toolbox `peRISCope` for easy
benchmarking of different model configurations. We also present and analyze
results from benchmarking of solving time for models with different code
and non-code memory granularity configurations. We found that models with
smaller memory granularity were solved faster in models generated from
binaries compiled with `starc` compiler. On models generated from
binaries compiled with `gcc` compiler, models with larger memory
granularity were solved faster.
## Automated Testing of Atomic Instructions (`LR`/`SC`) Implementations in Selfie by Luis Thiele, University of Salzburg, Austria, 2022 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_thiele.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_thiele))
The selfie system is an educational self-compiling C\* to RISC-U compiler and self-executing RISC-U emulator (C\* is a subset of C and RISC-U is a subset of RISC-V). It contains an autograder that is written in python and considers source code submitted by students and runs tests against it. One of the assignments requires students to extend the selfie system such that the compiler supports the Treiber stack - a concurrent thread-safe and lock-free stack. This Treiber stack must be implemented using the atomic `LR` (load-reserved) and `SC` (store-conditional) instructions. They must also be implemented to be supported by both the compiler and the emulator.
This thesis is about extending the autograder to grade an assignment called `treiber-stack` where students must implement the Treiber stack using the atomic instructions `LR` and `SC`. The primary challenge of the new tests added to the autograder was about forcing specific interleavings of `LR` and `SC` run by the emulator the students extended. Some interleavings could be forced directly by the source code of the run test but some could only be forced by having the thread scheduler timeout and force a switch of the thread that is run. A timeout happens when the thread has run the set maximum amount of instructions sequentially without there ever being a switch to another thread in between.
Additionally, this thesis also describes the correct implementations of the `LR` and `SC` instructions in the emulator and a correct implementation of the Treiber stack in order to pass the entirety of the autograded `treiber-stack` assignment. All prerequesite requirements are also explained, namely a correct implementation of support for threads (`threads` assignment), as well as any concepts and details about the emulator one must understand such as paging or system calls.
## Visualizing BTOR2 Models by Markus Diller, University of Salzburg, Austria, 2022 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_diller.pdf), [Repository](https://github.com/cksystemsgroup/beator-visualizer))
The process of bounded model checking is very helpful in finding edge cases for invalid program inputs. To be able to do this, a format representing the model is necessary. Unfortunately, the model file itself does not provide any information about metrics or quality of a model. Its only purpose is to serve as an input to a model checker. In this thesis a tool called `beatle` for a subset of the BTOR2 modeling language is described. It helps to alleviate the aforementioned limitations of a standalone model file by visually displaying relevant information in the browser.
## RISC-U Binary Optimization for Selfie by David Pape, University of Salzburg, Austria, 2021 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_pape/bachelor_thesis_pape.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_pape))
Optimizers are part of any modern compiler, and their practical importance in writing performant code cannot be understated. Still, they introduce major complexity, and its complement: bugs. In this work, we present a binary optimizer for RISC-U, a small subset of RISC-V and the target architecture of selfies[@selfie] educational compiler. To address the complexity issue, our optimizer is structured as a standalone binary, keeping the compiler simple. Since this comes at the cost of compile-time information, a binary analyzer is a prerequisite. With it, our optimizer is able to remove redundant instructions and apply several peephole optimizations, leading to a roughly five percent speedup.
## Linear-Time Static Analysis of RISC-V Binary Code by Thomas Wulz, University of Salzburg, Austria, 2021 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_wulz/bachelor_thesis_wulz.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_wulz))
Selfie is, among other things, a compiler from a small subset of C (C*) to a small subset of RISC-V (RISC-U).
We present algorithms for static analysis of such RISC-V binaries along with a C* implementation. By traversing the binary forward and backward, we collect data about known register values and liveness of registers for each instruction. Our approach has some shortcomings when analyzing binaries with recursive function calls, as these calls result in a lot of information being lost, which can propagate through the program. However, it only requires linear time and space in the size of the binary. In future work, this data can be used to optimize the binaries generated by selfie, as they are almost entirely unoptimized.
## RISC-V Bare-Metal Library Operating System for Selfie by Marcell Haritopoulos, University of Salzburg, Austria, 2021 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_haritopoulos/bachelor_thesis_haritopoulos.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_haritopoulos))
Despite its young age, the field of Computer Science is multifaceted and complex, at the expense of the entry barrier. Selfie, an educational project, aims to close the gap on the fundamentals. It runs on a hosted environment, but was not able to run on bare metal RISC-V hardware. We introduce a simple library operating system for RISC-V that implements the system call interface of Selfie and supports (nearly) all applications, that are written in Selfie's tiny C subset C\* and are using its syscall interface, without any modifications, including Selfie itself. The OS is linked to the application as a static library and is responsible for maintaining a C environment. System calls are performed as mere function invocations instead of raising an exception using ecall. Files are stored in a static read-only file system. I/O system calls are implemented in a general way so that related projects may share the same semantics.
## RISC-V S-Mode-Hosted Bare-Metal Selfie by Martin Fischer, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_fischer/bachelor_thesis_fischer.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_fischer))
Modern operating systems like Linux run on a great variety of different machine architectures and have complicated mechanisms for process and resource management. Since this makes understanding their internals a tedious task, we present a simple preemptive multitasking kernel that targets a 64-bit RISC-V platform and which is tailored to run binaries compiled by selfie through the implementation of its Application Binary Interface. It runs in supervisor-mode, executes spatially isolated processes in user-mode, and communicates through the Supervisor Binary Interface with OpenSBI, a hardware abstraction layer, running in machine-mode; all while sharing core parts of its code base with a library operating system that is described in another bachelor thesis. The main difficulties that arise through the use of memory virtualization are discussed and solutions for them are presented. The kernel is able to execute on top of real RISC-V hardware in the form of a SiFive HiFive Unleashed.
## Conservative Garbage Collection in Kernel and Mutator Space by Gregor Bachinger, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_bachinger/bachelor_thesis_bachinger.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_bachinger))
Compiling C or any similar language into binaries only provides support for explicit, manual memory management. To combat these issues, garbage collectors have been employed which handle memory management automatically. Since garbage collectors are specialized and use a lot of assumptions about their target environments, different algorithms are usually used for collectors in and outside of the mutator's address space. We have designed and implemented a conservative garbage collector that can run either in kernel or mutator space, or even in both at the same time. Running our collector in kernel and mutator space at the same time shows, that the collector is able to collect its own garbage. Furthermore, our experiments show the runtime/space tradeoff between collector invoke frequency and running it on machine and application level.
## Generating Path Conditions for Bounded Model Checking of RISC-V Code in Selfie by Sebastian Landl, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_landl/bachelor_thesis_landl.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_landl))
Given a 64-bit RISC-V binary we compute a single logical formula that is satisfiable if and only if there exists input to the code such that there is a division by zero, invalid memory access, or a non-zero exit code when executing no more than a given maximum number of any type of instructions and a given maximum number of branch instructions. We do this by creating a logical formula, which is satisfiable if and only if a given instruction is reachable, called a path condition for each possible path of the program. This is commonly known as symbolic execution. We then merge different path conditions as soon as there is an instruction which can be reached from different paths in the control flow. Creating a single formula for all paths mimics bounded model checking. This is done by checking after every single executed instruction, whether there is another path condition which can be merged with the one we just extended by executing one instruction. Two path conditions are mergeable if they describe the reachability of the very same instruction and if the call stacks of their respective execution paths are the same. For that reason the call stacks of all paths are stored in a global tree structure. To determine which instruction shall be executed next, i.e. which path should be explored further, the path which has the biggest call stack and describes the reachability of the instruction with the lowest program counter is chosen, so that a merge always happens as soon as possible and no possible merge location is ever missed. The time it takes to schedule the next path is linear in the number of paths that are being explored. The size of the generated formula is in O(a ⋅ 2<sup>b</sup>) where a is the maximum number of instructions executed on each path and b ≤ a is the maximum number of branch instructions for which both branches are considered.
## Implementation and Application of a Parser for Boolector's Witness Format by Christoph Siller, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_siller/bachelor_thesis_siller.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_siller))
In this bachelor thesis, a parser for Boolector’s witness format is introduced, which enables automated input validation. The toolchain takes a C* file containing read calls as input and generates a Btor2 model of it, using Selfie’s model generator. The resulting model is then fed to the Boolector-based bounded model checker BtorMC. By using SMT-solving, BtorMC is able to find error states in the model within a maximum number of executed instructions. In case an error state is found, BtorMC generates a witness. This witness is parsed in order to extract the input string that causes the C* program to run into the error. To validate that the extracted string indeed triggers an error, it is fed to the C\* program while running it on Mipster. If the input string was generated correctly, Mipster runs into the predicted error. In addition to the parser, this thesis provides background information on all technologies used and the concepts they are based on.
## Selfie - RISC-V to x86-64 Binary Translation by Alexander Kollert, University of Salzburg, Austria, 2020 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_kollert/bachelor_thesis_kollert.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_kollert))
In this work I present an implementation of a binary translator that statically translates RISC-V machine code produced by starc into x86-64 machine code. The requirements are that the binary translator should be able to translate Selfie itself and the usage of a minimal subset of x86-64 instructions. As it is in the nature of Selfie the implementation should also be as minimal as possible. There are a few challenges to overcome to make this work. First the x86-64 ISA (Instruction Set Architecture) is an variable length instruction set which makes calculation of target addresses of jump instructions more difficult. Further the x86-64 instruction set mostly consists of two-operator instructions and even some single-operator instructions in contrast to three-operator instructions in RISC-V. And last but not least we will see that for some RISC-V instructions it is not possible to make an translation entirely without context. The result is a binary translator that is able to generate an x86-64 selfie binary with functioning self-compilation in x86-64. The difference with the translated binary is that there is no longer a need to link against a library, since it uses its own implemantations for the library routines.
## A Hybrid Symbolic Execution and Bounded Model Checking Engine in Selfie by Christian Edelmayer, University of Salzburg, Austria, 2019 ([PDF](https://github.com/cksystemsteaching/selfie/releases/download/bachelor_thesis_edelmayer/bachelor_thesis_edelmayer.pdf), [Release](https://github.com/cksystemsteaching/selfie/releases/tag/bachelor_thesis_edelmayer))
In a world dependent on software, it is of the utmost importance to ensure the correctness of that software. For this reason, software needs to be analyzed. In this thesis, the software analysis methods called symbolic execution and bounded model checking are explained in detail. Furthermore, a hybrid symbolic execution and bounded model checking engine was implemented in Selfie. It is outlined thoroughly how the symbolic execution engine was extended into the hybrid engine. The main challenge was to implement the merging of paths which corresponds to bounded model checking. Our experiments show that symbolic execution produces formulas which can be solved more easily at the cost of a slower translation time. Exactly the opposite is true for bounded model checking. In other words, both methods have their advantages and disadvantages.
## Symbolic Execution with Selfie --- Logics by Sara Seidl, University of Salzburg, Austria, 2019 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_seidl.pdf))
State-of-the-art symbolic execution engines are based on computationally expensive SMT solvers that may not perform well on large programs. There is, however, a trade-off between performance and completeness. Restricting completeness such that a solver works only on a subset of all possible programs may nevertheless allow us to make the solver faster and scale to larger programs. The solver we developed is based on interval modulo arithmetic rather than bit-vector logics used by many other symbolic execution engines. Further, constraint solving is not achieved by solving formulas but entirely through execution of code. It is interval modulo arithmetic in combination with this constraint solving technique that allows us to solve constraints fast. The solver is complete as long as the set of concrete values a symbolic value represents can be expressed as an interval. The challenge is to be able to detect if the solver is still complete during symbolic execution of a given program. Moreover, the subset of programs for which a solver may be complete during symbolic execution needs to be sufficiently interesting. For us, this is the case if non-trivial parts of our selfie system are part of that subset.
## Symbolic Execution with Selfie --- Systems by Simon Bauer, University of Salzburg, Austria, 2018 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_bauer.pdf))
This thesis presents a simple symbolic execution engine, which was integrated into the SELFIE project, an educational platform already containing a self-referential compiler, emulator and hypervisor. The idea behind symbolic execution is to provide a program with arbitrary symbolic - rather than concrete - input, which allows the symbolic engine to efficiently explore all control flow paths of the program. Our engine differs from state-of-the-art solutions as it does not utilise a constraint solver and is therefore faster than other tools. As a consequence, the engine is only able to handle a subset of all possible programs though. The thesis gives an overview over the engines building parts and their differences as well as similarities compared to other symbolic tools.
## Symbolic Execution with Selfie --- Arithmetics by Manuel Widmoser, University of Salzburg, Austria, 2018 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_widmoser.pdf))
Modern symbolic execution engines are lacking in scalability and performance due to computationally expensive Satisfiability Modulo Theory (SMT) solvers. Such engines attempt to execute for all possible inputs in order to find vulnerabilities in an elegant way. Within an entirely self-contained system, we developed a symbolic execution engine on machine code level without using a theory solver. This becomes achievable by interval arithmetic and the ability of backtracking code execution. However, there is a trade-off between performance and completeness. This thesis mainly describes the data structure behind the engine as well as symbolic code execution using interval arithmetic. Despite some reasonable limitations the subset of programs, which can be executed by the engine, keeps sufficiently interesting. In return, soundness and simplicity maintain.
## Porting Selfie to RISC-V: State-of-the-Art ISA Support by Simone Oblasser, University of Salzburg, Austria, 2017 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_oblasser.pdf))
The following thesis describes a newly developed alternative version of Selfie, a self-referential platform containing a compiler, an emulator and a hypervisor for teaching computer systems. Instead of MIPS32 code, this version supports a minimal subset of RISC-V (RV32I plus "M" standard extension), an open-source ISA developed at University of California, Berkeley. The port to this different architecture included the adaption of all major parts of Selfie, especially of the compiler and emulator. The key changes made involved register usage, encoding and decoding of the new instruction formats, and handling of immediate values. The resulting platform still fulfills all the self-referentiality requirements the original project did. Furthermore, the new support for RISC-V instructions paved the way for an additional project to make binaries generated by Selfie (and, in turn, Selfie itself) executable on official RISC-V emulators and hardware chips.
## Porting Selfie to RISC-V: Native Toolchain Support by Christian Barthel, University of Salzburg, Austria, 2017 ([PDF](https://github.com/cksystemsteaching/selfie/blob/main/theses/bachelor_thesis_barthel.pdf))
The goal of this project is to provide an educational system that consists of a simple self-compiling compiler, a self-executing instruction set emulator and a minimal self-hosting hypervisor, based on the RISC-V instruction set. Its main purpose is to introduce students to principal systems engineering techniques and teach students about computer architecture, compilers and operating systems. Everything is designed to be self-referential, to allow students to discover the intrinsics of system code which is known to be a big challenge. During this project, I worked on adding the ELF32 binary format to the compiler and emulator and making the overall system compatible with the RISC-V environment. Beside adding the ELF header, this involved also code adaption and synchronization with the operating system interface provided by the pk kernel. The work bridges the gap between the existing toolchain that is based on an artificial RAW binary format, and the RISCV32 GNU toolchain which is widely used on various operating systems and computer platforms. It is now possible to run binaries generated by starc on top of the RISC-V instruction set reference implementation spike. Furthermore, it should be simple to run binaries directly on RISC-V microprocessors.