# LustreC: a Lustre compiler toolset

LustreC is structured around the modular compilation scheme proposed by
[Biernacki, Colaço, Hamon, and Pouzet at
LCTES'08](https://www.di.ens.fr/~pouzet/bib/lctes08a.pdf). It is an open source
lustre compiler that provides verification capabilities. It is currently mainly
used through the [CocoSim platform](https://github.com/NASA-SW-VnV/CoCoSim), 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](https://opam.ocaml.org/ "Link to opam
homepage"), 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

```sh
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:

```sh
eval $(opam env)
```

### 2. Install in opam switch

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

This should install LustreC on your current switch with its OCaml and
system dependencies. See the [Usage](#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](https://www.frama-c.com
"Link to Frama-C homepage") and SMT solvers.

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

```sh
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:

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

You may uninstall the plugin by executing

```sh
opam uninstall lustrec_wp_strategies
```


The [Alt-Ergo](https://alt-ergo.ocamlpro.com/ "Link to Alt-Ergo homepage") SMT
solver is installed with Frama-C. We also recommend to use two others solvers:

* [Z3](https://github.com/Z3Prover/z3 "Link to Z3 Github page"), that
  can be installed through opam with `opam install z3` (or through
  your distribution package manager)

* [CVC4](https://cvc4.github.io/ "Link to CVC4 homepage") that can be
  installed through your distribution package manager

After installing the solvers, you must configure the
[Why3](https://why3.lri.fr/ "Link to Why3 homepage"), the platform
used by Frama-C for deductive verification:

```sh
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](#acsl-generation-and-proof)):

```sh
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.:

```sh
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](https://dune.readthedocs.io/en/latest/ "Link to dune documentation") to
build and execute it.

To build LustreC with dune:

```sh
dune build @install
```

To execute LustreC, you should use `dune exec`:


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