Selfie: Towards Minimal Symbolic Execution
Selfie is a self-contained 64-bit implementation of (1) a self-compiling compiler written in a tiny subset of C called C* targeting a tiny subset of 64-bit RISC-V called RISC-U, (2) a self-executing RISC-U emulator, and (3) a self-hosting hypervisor that virtualizes the emulated RISC-U machine. Selfie is implemented in a single 8k-line file and can compile, execute, and virtualize itself any number of times in a single invocation of the system given adequate resources. There is also a simple linker, disassembler, debugger, and profiler. Selfie has originally been developed just for educational purposes but has recently become a research platform as well. C* supports only two data types, uint64_t and uint64_t*, and RISC-U features just 14 instructions, in particular for unsigned arithmetic only, which significantly simplifies reasoning about correctness. In this paper, we report on an ongoing effort in designing and implementing a symbolic execution engine for RISC-U within selfie that is supposed to explore non-trivial parts of the system including itself. The idea is to identify the set of ingredients that are necessary to do this such as the data structures for representing traces, path conditions, and symbolic states as well as algorithms for SAT and SMT solving. The key difference to other more advanced projects is that we are interested in reasoning just about selfie, for now, and are able to change selfie if necessary, as reasoning target but also as integrated platform for compilation, (symbolic) execution, and virtualization. Since selfie generates unoptimized code we are also exploring ways to leverage our symbolic execution engine in code optimization.
Extended Abstract (paper.pdf) | 360KiB |
Mon 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | |||
11:00 30mTalk | Understanding Task Granularity on the JVM: Profiling, Analysis, and Optimization MoreVMs Andrea Rosà University of Lugano, Switzerland, Eduardo Rosales University of Lugano, Switzerland, Filippo Schiavio Università della Svizzera italiana, Walter Binder University of Lugano, Switzerland File Attached | ||
11:30 30mTalk | Selfie: Towards Minimal Symbolic Execution MoreVMs Alireza S. Abyaneh University of Salzburg, Simon Bauer University of Salzburg, Christoph Kirsch University of Salzburg, Philipp Mayer University of Salzburg, Christian Mösl University of Salzburg, Clément Poncelet University of Salzburg, Sara Seidl University of Salzburg, Ana Sokolova University of Salzburg, Manuel Widmoser University of Salzburg File Attached | ||
12:00 30mTalk | Self-hosted scripting in Guile MoreVMs Andy Wingo Igalia, S.L. Pre-print File Attached |