CristalCaveGem » LustreC

Current Status:    [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)

# What is LustreC ?

LustreC is a modular compiler of Lustre code into C and Horn Clauses.

# User guide 

## Installation

You need to have OPAM the OCaml Package Manager installed. 

You will find instruction on how to install opam on your system at https://opam.ocaml.org/doc/Install.html

You also need to install `rsync`.

Other packages will be required. The list of the required system package is system-dependent. But don't worry OPAM is able to determine which packages to install.

Clone this project with git and open a terminal in the root directory of the project then run :

``` 

$ opam pin -n mlmpfr 4.0.2+dune  # Needed on ubuntu <= 20.04 or debian based system because mlmpfr package needs a specific system version of libmpfr-dev to work, an issue has been open to fix this bug see https://github.com/thvnx/mlmpfr/issues/10

$ opam pin -n -y . # add lustrec to opam

$ opam depext lustrec # install the required system dependencies

$ opam install lustrec # install Lustrec

```

Now run ̀`lustrec -version` to check that the install was successful. You should see something similar to this output 

```

Lustrec compiler, version 1.7

Standard lib: /home/corentin/.opam/default/share/lustrec

User provided include directory: .

```

If you encounter this error message ̀`lustrec : command not found`, you should make sure that opam path is in your PATH environment variable.

`opam init` normally adds automatically the needed code to your `.bashrc`. An easy (but temporary) fix is to run `eval $(opam env)` in your terminal.

## Plugins 

You can enable the plugin simply by installing the corresponding opam package. See the table below

| Plugin name | Description                                                | Required package      |

|-------------|------------------------------------------------------------|-----------------------|

| Zustre      | A verifier plugin based on z3                              | lustrec-enable-zustre |

| Tiny        | A verifier plugin based on the tiny abstract analysis tool | tiny                  |

| Salsa       | ?                                                          | salsa                 |

| Seal        | A verifier plugin based on seal                            | seal                  |

For instance to enable the zustre plugin, you should run 

```

$ opam depext lustrec-enable-zustre

$ opam install lustrec-enable-zustre

```

## Usage 

You can then use the following executables :

  * `lustrec` : a Lustre Compiler that can output C, C++, Horn clauses, EMF, Ada

  * `lustrev` : a Lustre Verifier with static analysis 

  * `lustret` : a Lustre test generator

## Alternative installation with Docker

We also provide two Dockerfiles 

  * Dockerfile.ubuntu : based on Ubuntu 20.04

  * Dockerfile.alpine : based on Alpine (more lightweight)

The images have lustrec installed and `lustrec`, `lustret` and `lustrev` are available in the PATH.

### Options

You can choose to build the docker container with or without the Zustre plugin and / or the Tiny plugin.

You just have to comment / uncomment the indicated lines in the corresponding Dockerfile.

### Usage

In a shell with the root of this project as current directory run `sudo docker build --file={Dockerfile.ubuntu/Dockerfile.alpine} --tag=lustrec .`  in order to build the docker image 

Then you can use lustrec, lustrev, or lustret with the following commands :

```

sudo docker run --rm -v $(pwd):/workdir -w /workdir --entrypoint "lustrec" lustrec' # for lustrec

sudo docker run --rm -v $(pwd):/workdir -w /workdir --entrypoint "lustret" lustrec' # for lustret

sudo docker run --rm -v $(pwd):/workdir -w /workdir --entrypoint "lustrev" lustrec' # for lustrev

``` 

These commands create a temporary container that share your working directory and run the desired utility

You might want to define aliases to make using lustrec easier and add them to your `.bashrc`

### Lustrec

In a modular setting:

```

# lustrec <filename.lus>

```

will generate filename.c and filename.h

With a main node:

```

# lustrec -node <main_node> <filename.lus>

```

will generate the same two files,

but also filename_main.c that contains a main function

and filename_alloc.h that contains the node allocation macros 

With a main node, with a static memory allocation scheme:

```

# lustrec -node <main_node> -dynamic <filename.lus>

```

same as above, but main function will dynamically allocate node memory

To compile it:

```

# gcc -Iinclude filename.c

# gcc -Iinclude filename_main.c

```

where include links to the include folder

To run it with the generated main function:

- compile the io_frontend.o

```

# gcc -c include/io_frontend.c

# gcc -Iinclude -o target_name io_frontend.o filename.o filename_main.o

# ./target_name

```

To analyze it with frama-c

```

# frama-c -cpp-extra-args='-Iinclude'  filename.c

```

### Ada backend 

Download ada from https://www.adacore.com/download

For the ADA backend:

- GNAT 2018 community edition on https://www.adacore.com/download

- gprbuild shall be in your path

## Uninstall 

Just run `opam unpin lustrec`

# Developer guide

## Description

This project uses [dune](https://dune.readthedocs.io/en/stable/quick-start.html) build system, and `autoconf` for configuration.

The `lib/` folder contains an essential library that is used by the various plugins.

The `plugins/` folder contains optional plugins that add feature to the compiler or verifier when enabled.

The `backends` folder contains the different backends for the supported languages (Ada, C, Horn, etc.).

The `src/` folder contains the remaining code, that is to say the code to generate the executables and put together all the plugins.

# Additional dependencies for developers

``` 

# apt-get install -y cmake

```

## How to build ?

Note: a Makefile is also provided, merely as a shortcut to dune commands.

```

$ autoconf

$ ./configure

configure: Git branch: {CURRENT_GIT_BRANCH}

configure: ******** Configuration ********

configure: bin path:     NONE/bin

configure: include path: NONE/include

seal plugin : enabled

zustre plugin : enabled

tiny plugin : enabled

salsa plugin : disabled because the following libraries are missing : salsa.

checking for gcc... gcc

checking whether the C compiler works... yes

checking for C compiler default output file name... a.out

checking for suffix of executables... 

checking whether we are cross compiling... no

checking for suffix of object files... o

checking whether we are using the GNU C compiler... yes

checking whether gcc accepts -g... yes

checking for gcc option to accept ISO C89... none needed

checking for __gmpz_init in -lgmp... yes

checking for mpfr_add in -lmpfr... yes

configure: ../lustrec-tests/regression_tests

checking for ../lustrec-tests/regression_tests/CMakeLists.txt... yes

configure: creating ./config.status

config.status: creating Makefile

config.status: creating src/dune

config.status: creating src/pluginList.ml

config.status: creating src/verifierList.ml

config.status: creating lib/version.ml

config.status: creating share/FindLustre.cmake

configure: ****** Regression Tests  ******

configure: tests path: ../lustrec-tests/regression_tests

configure: ******** Configuration ********

configure: Execute "make; make install" now

$ dune build

```

When running `./configure` the plugins (seal plugin, zustre plugin, tiny plugin, salsa plugin) will be enable by default if all the required dependencies are met. 

You can force-enable a plugin with the `--enable-{seal/zustre/tiny/salsa}`flag

You can also disable a plugin with the `--disable-{seal/zustre/salsa}` flag

The build result is in `_build/`.

You will find the executables in `_build/default/src` under the names :

 * `main_lustre_compiler` for lustrec

 * `main_lustre_verifier`  for lustrev

 * `main_lustre_testgen` for lustret

## Dockerfile.ubuntu 

This Dockerfile install the lustrec, lustrev and lustret tools in an Ubuntu 20.04 container.

It is a good example of how to build and install lustrec.

## Dependency management

You can see the dependency graph between the plugins and the core library with `dune-deps`

```

$ opam install dune-deps 

$ dune-deps | tred | dot -Tpng > deps.png

```

# People

  * Pierre-Loic Garoche (ONERA)

  * Xavier Thirioux (IRIT)

  * Temesghen Kahsai (NASA Ames / CMU)