Home

Awesome

LVC Compiler Project

LVC stands for Linear Verified Compiler. The compiler is based on the linear first-order language IL [1,2]. The goal of the project is to show that functional SSA, i.e. using a functional style lexical variable binding provides for a viable semantic foundation for static single assignment (SSA).

Dependencies

Building LVC

Get the source code via

git clone https://github.com/sigurdschneider/lvc
git submodule update --init --recursive

After installing the dependencies, you can (but if you did not change anthring, you do not have to) use

./configure.sh

to generate _CoqProject from the sources. This step is strictly optional, as we also provide a _CoqProject in this distribution. Then build LVC using

make
make extraction

This will generate a OCaml bytecode, and the following symbolic link will point to it

extraction/lvcc.byte

There are some example files in extraction/examples. Run one by issuing the following command:

cd extraction
./lvcc.byte examples/dve.il
./lvcc.byte examples/dve+dce.il

The output after different compilation phases will be in files example/dve.il.$PHASE where $PHASE is the compilation phase.

Disclaimer

The sources incorporate ideas and code from various sources.

References

[1] Sigurd Schneider: Semantics of an Intermediate Language for Program Transformation. Master's Thesis. Saarland University, 2013. [2] Sigurd Schneider, Gert Smolka, Sebastian Hack: A Linear First-Order Functional Intermediate Language for Verified Compilers. ITP 2015 [3] Julian Rosemann, Sigurd Schneider, Sebastian Hack: Verified Spilling and Translation Validation with Repair. ITP 2017