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).

• CoqDoc documentation is available here.

Dependencies

• Coq

  Sources compile with Coq version 8.7.2 (March 2018). Other versions might work.

• OCaml (including ocamlbuild)

  Sources compile with ocaml version 4.04.2, other versions might work. OCaml should include ocamlbuild.

• menhir

  A parser generator mostly compatible with ocamlyacc (but better at explaining conflicts): http://gallium.inria.fr/~fpottier/menhir/ Sources compile with version 20171013. Other versions might work.

• ruby [optional]

  If you want build times to be output, you need ruby.

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.

• The subdir Containers contains a copy of the Containers library which is available on github was slightly adapted for the needs of the project.
• The subdir paco contains a copy of the Paco Library.
• The subdir TransVal/ contains work based on Heiko Becker's Bachelor's Thesis: Verified SMT-based Translation Validation.
• The file Lattice.v was inspired by the Lattice development from Daniel W.H. James and Ralf Hinze.
• The file Infra/SizeInduction.v contains the type-class based size-induction from AutoSubst.
• Parts of the spilling infrastructure in directory Spilling were done by Julian Rosemann and published at ITP 2017[3].

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