LustreC: a Lustre compiler toolset

LustreC is structured around the modular compilation scheme proposed by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08. It is an open source lustre compiler that provides verification capabilities. It is currently mainly used through the CocoSim platform, a Matlab toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre language is used as an intermediate representation and relies mainly on LustreC to produce code or verification artifacts.

Build

The easiest is to use opam, the OCaml package manager. We suppose here that opam version 2.1 is used.

1. Set a (local) opam switch using OCaml ≥ 4.11.1

opam switch create --no-install . 4.14.1

You may of course also use a global opam switch. Do not forget to update your opam environment after installing the switch:

eval $(opam env)

2. Install in opam switch

opam install . [--with-test] [--with-doc] --yes

This should install LustreC on your current switch with its OCaml and system dependencies. See the Usage section to use LustreC.

3. ACSL generation and proof

If you want to generate ACSL specifications and prove them on the generated C code, you will need Frama-C and SMT solvers.

LustreC use custom strategies for the Frama-C WP plugin that must be installed.

opam install lustrec_wp_strategies/

Frama-C should also be installed. Notice that if you have installed a local Opam switch, Frama-C should be installed in this local switch.

When starting Frama-C, you should now see the following message:

[lustrec-wp-strategies] LustreC WP strategies available.

You may uninstall the plugin by executing

opam uninstall lustrec_wp_strategies

The Alt-Ergo SMT solver is installed with Frama-C. We also recommend to use two others solvers:

• Z3, that can be installed through opam with opam install z3 (or through your distribution package manager)

• CVC4 that can be installed through your distribution package manager

After installing the solvers, you must configure the Why3, the platform used by Frama-C for deductive verification:

why3 config detect

Usage

To see a summary of options:

lustrec -help

To compile a Lustre file to C:

lustrec <file.lus>

To compile a Lustre file to C with ACSL annotations:

lustrec -acsl-spec [-compile_contracts] <file.lus>

The flag -compile_contracts enables the (experimental) translation of Kind2-like contracts into ACSL contracts.

To prove ACSL assertions (you should have installed the LustreC strategies to use the LustreC:Transitions and LustreC:MemoryPacks strategies, see the corresponding section):

frama-c[-gui]\
 -wp                                                `# use WP plugin` \
 -wp-model ref,real                                 `# use ref memory model and ideal floats as reals model` \
 -wp-prover alt-ergo,z3,cvc4                        `# use Alt-Ergo, Z3 and CVC4 solvers` \
 -wp-timeout 30                                     `# set per proof obligation timeout in seconds` \
 -wp-par 16                                         `# set the number of jobs` \
 -wp-no-warn-memory-model                           `# dismiss various memory model related warnings` \
 -wp-auto LustreC:Transitions,LustreC:MemoryPacks   `# use LustreC custom strategies` \
 -wp-auto-depth 100                                 `# set the recursive depth limit of custom strategies use` \
 -wp-auto-width 100                                 `# set the maxnumber of subgoals for custom strategies use` \
 <file.c>

A BASH shell script frama-c-lustrec.sh is available in the scripts directory. Execute it as frama-c-lustrec.sh -h to see all available options.

Run tests

Regression tests

If you plan on launching regression tests, you should install xsltproc as well, eg.:

apt install xsltproc

Then launch tests:

dune runtest tests/regression_tests --no-buffer

ACSL verification tests

To launch verification tests, create a directory <my_dir>/ in lustrec_tests/. The directory must contain symbolic links to lustrec_tests/{test.ml,dune} and to relevant Lustre files in lustrec_tests/lustre_files, and a JSON configuration file config.json. See lustrec_tests/{stopwatch_test,minimal_tests,offline_tests} for example setups. The fields of the configuration file are all optional (default values are provided).

To launch the tests:

dune runtest lustrec_tests/<my_dir> --no-buffer --display quiet

The results can be found in the results/ directory.

Some tests requires to install tokei https://github.com/XAMPPRocky/tokei/

Developing and hacking LustreC

If you want to hack LustreC, you should use dune to build and execute it.

To build LustreC with dune:

dune build @install

To execute LustreC, you should use dune exec:

dune exec src/main_lustre_compiler.exe -- [LustreC options]