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.

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.20.1. It includes amodified version of CompCert and depends on menhir.

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

$ git clone https://github.com/INRIA/velus$cd velus$ git submodule --init --recursive$ opam switch create velus --packages=ocaml.4.14.2,coq.8.20.1$eval$(opam env --switch=velus --set-switch)$ opam install -j ocamlbuild menhir ocamlgraph

To check the proofs and build Vélus:

$ ./configure [options]<target>$ make -j# Uses all the available cores

The<target> must be one of thesupported target platformsof CompCert.

The configuration script has the same options as CompCert's withthe following specfic to Vélus:

• -velus-onlyOnly compile Vélus (and not CompCert). This option may be useful with-compcertdir.

• -compcertdirOverrides the default path to the directory containing your local version ofCompCert.

• -flocqdirSet the path to the directory containingFlocq if you're not using the onepackaged in CompCert.

• -menhirlibdirSet the path to the directory containingMenhirLib if you're not using theone packaged in CompCert.

If you are using thenix package manager, you candirectly compile Vélus using the flake with the commandnix build. This doesnot require a local version of CompCert to build.