Repository files navigation

These source files contain the implementation, models, and proof ofcorrectness of a formally verified Lustre compiler

This file contains instructions for (i) using the compiler from (ii) a localopam installation.

Theexamples/ subdirectory contains another readme file presenting severalexample programs that can be used to test the compiler.

Thepre operator used in many Lustre programs is not yet treated.An uninitialized delaypre e must be replaced by an initialized one0 fby e.

Compiler error messages are still very brutal. In particular the parser onlyreports syntax errors with a line number and character offset. We willimplement more helpful messages when we have finalized one or two remainingdetails of the final language.

In this artifact, we provide the totality of the source code of Vélus.Vélus depends on a tweaked version of CompCert, which is also provided.We have anonymized this distribution by removing the names of the authors of thesubmission from the source code.The artifact can be compiled and executed using the instructions below.

Thestepper-motor example presented in the submission is available in theexamples/stepper-motor/ subdirectory.We have already provided the code produced by the compiler after each pass inthe same directory.

Thedoc/ folder contains the documentation generated from the Coq source files.Theindex.html file cross-references the Coq definitions relevant to the different sections of the submission.It also points to the different parts of the compiler outlined in figure 14 of the submission.

To run the compiler:

./velus -h

In particular, typing

./velus examples/count.lus

will compile the Lustre program in examples/count.lus into an assemblerprogram examples/count.s.

The compiler also accepts the options

• -dnolastOutput the Lustre code after compilation of last declarations into .nolast.lus

• -dnoautoOutput the Lustre code after compilation of state machines into .noauto.lus

• -dnoswitchOutput the Lustre code after compilation of switch blocks into .noswitch.lus

• -dnolocalOutput the Lustre code after inlining of local scopes into .nolocal.lus

• -dnlustreOutput the normalized NLustre code into .n.lus

• -dstcOutput the Stc intermediate code into .stc

• -dschOutput the scheduled code into .sch.stc

• -dobcOutput the Obc intermediate code into .obc

• -dclightOutput the generated Clight code into .light.c

• -nofusionDisable the if/then/else fusion optimization.

• -syncGenerate an optionalmain_sync entry point and a .sync.ccontaining a simulation that prints the outputs at each cycle and requestsinputs. In contrast tomain_proved, this entry point is not formally verifiedbut it is useful for testing the dynamic behaviour of compiled programs.Seeexamples/Makefile for examples.

Vélus has been implemented in Coq.8.16.1. It includes amodified version of CompCert and depends on menhir >= 20230608.

To build a self-contained installation for compiling and runningVélus, we recommend installing an ad-hocopam directory:

$ cd $VELUS_DIR$ mkdir opam$ opam init --root=opam --compiler=4.13.1$ eval `opam config env --root=$VELUS_DIR/opam`$ opam install -j4 ocamlbuild coq.8.16.1 menhir.20230608 ocamlgraph

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 oneadditional-compcertdir option to specify the CompCert directory.