A Formally Verified Compiler for Lustre
These source files contain the implementation, models, and proof of correctness of a formally verified Lustre compiler
This file contains instructions for (i) using the compiler from (ii) a local opam installation.
The doc/
subdirectory contains a file
index.html that links the definitions
in the EMSOFT 2021 article to the corresponding parts of the Coq source
files.
The examples/
subdirectory contains a file readme.md
presenting several example programs that can be used to test the compiler.
The pre
operator used in many Lustre programs is not yet treated.
An uninitialized delay pre e
must be replaced by an initialized one 0 fby e
.
Compiler error messages are still very brutal. In particular the parser only reports syntax errors with a line number and character offset. We will implement more helpful messages when we have finalized one or two remaining details of the final language.
Using the compiler
To run the compiler:
./velus -h
In particular, typing
./velus examples/count.lus
will compile the Lustre program in examples/count.lus into an assembler program examples/count.s.
The compiler also accepts the options
-
-dnlustre Output the normalized NLustre code into .n.lus
-
-dstc Output the Stc intermediate code into .stc
-
-dsch Output the scheduled code into .sch.stc
-
-dobc Output the Obc intermediate code into .obc
-
-dclight Output the generated Clight code into .light.c
-
-nofusion Disable the if/then/else fusion optimization.
-
-sync Generate an optional
main_sync
entry point and a .sync.c containing a simulation that prints the outputs at each cycle and requests inputs. In contrast tomain_proved
, this entry point is not formally verified but it is useful for testing the dynamic behaviour of compiled programs. Seeexamples/Makefile
for examples.
Local installation
Vélus has been implemented in Coq.8.9.1. It includes a modified version of CompCert and depends on menhir.20200624.
To build a self-contained installation for compiling and running Vélus, we recommend installing an ad-hoc opam directory:
$ cd $VELUS_DIR
$ mkdir opam
$ opam init --root=opam --compiler=4.07.1
$ eval `opam config env --root=$VELUS_DIR/opam`
$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam install -j4 coq.8.9.1 menhir.20200624 coq-menhirlib.20200624
To check the proofs and build Vélus:
$ cd $VELUS
$ ./configure [options] target
$ make
The configuration script uses the same options as CompCert's, except one
additional -compcertdir
option to specify the CompCert directory.