LVC verified compiler
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).
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.
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.
The sources incorporate ideas and code from various sources.
Containers
contains a copy of the Containers library which is available on github was slightly adapted for the needs of the project.paco
contains a copy of the Paco Library.Lattice.v
was inspired by the Lattice development from Daniel W.H. James and Ralf Hinze.Infra/SizeInduction.v
contains the type-class based size-induction from AutoSubst.Spilling
were done by Julian Rosemann and published at ITP 2017[3].[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