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.14.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.

First, install Frama-C through opam (we are currently using version 26.1 Iron of Frama-C):

opam install frama-c

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

The Alt-Ergo is installed with Frama-C. We also recommend to use two others SMT 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

LustreC use custom strategies for the Frama-C WP plugin that must be compiled (TODO: add detail here). Go to the lustrec_wp_strategies directory and execute the following commands:

dune build @install
dune install

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

dune uninstall

in the lustrec_wp_strategies directory.

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>

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 build @tests/regression_tests/runtest --no-buffer

ACSL verification tests

dune build @offline_tests/runtest --no-buffer

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]