Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / README.md @ 9b0432bc

History | View | Annotate | Download (9.96 KB)

1 5573fee2 Teme
2 7ec8e203 Temesghen Kahsai
Current Status:    [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)
3 5573fee2 Teme
4 9c4cc944 Corentin Lauverjat
# What is LustreC ?
5 e2068500 Temesghen Kahsai
6
LustreC is a modular compiler of Lustre code into C and Horn Clauses.
7
8 9c4cc944 Corentin Lauverjat
# User guide 
9
10
11
## Installation
12
13
You need to have OPAM the OCaml Package Manager installed. 
14
You will find instruction on how to install opam on your system at https://opam.ocaml.org/doc/Install.html
15
16
You also need to install `rsync`.
17
18
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.
19
20
Clone this project with git and open a terminal in the root directory of the project then run :
21
22
``` 
23
$ 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
24
$ opam pin -n -y . # add lustrec to opam
25
$ opam depext lustrec # install the required system dependencies
26
$ opam install lustrec # install Lustrec
27
```
28
29
Now run ̀`lustrec -version` to check that the install was successful. You should see something similar to this output 
30
```
31
Lustrec compiler, version 1.7
32
Standard lib: /home/corentin/.opam/default/share/lustrec
33
User provided include directory: .
34
```
35
36
If you encounter this error message ̀`lustrec : command not found`, you should make sure that opam path is in your PATH environment variable.
37
`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.
38
39
## Plugins 
40
41
You can enable the plugin simply by installing the corresponding opam package. See the table below
42
43
| Plugin name | Description                                                | Required package      |
44
|-------------|------------------------------------------------------------|-----------------------|
45
| Zustre      | A verifier plugin based on z3                              | lustrec-enable-zustre |
46
| Tiny        | A verifier plugin based on the tiny abstract analysis tool | tiny                  |
47
| Salsa       | ?                                                          | salsa                 |
48
| Seal        | A verifier plugin based on seal                            | seal                  |
49
50
For instance to enable the zustre plugin, you should run 
51
```
52
$ opam depext lustrec-enable-zustre
53
$ opam install lustrec-enable-zustre
54
```
55
## Usage 
56
57
You can then use the following executables :
58
  * `lustrec` : a Lustre Compiler that can output C, C++, Horn clauses, EMF, Ada
59
  * `lustrev` : a Lustre Verifier with static analysis 
60
  * `lustret` : a Lustre test generator
61
62
## Alternative installation with Docker
63
64
We also provide two Dockerfiles 
65
  * Dockerfile.ubuntu : based on Ubuntu 20.04
66
  * Dockerfile.alpine : based on Alpine (more lightweight)
67
68
The images have lustrec installed and `lustrec`, `lustret` and `lustrev` are available in the PATH.
69
70
### Options
71
72
You can choose to build the docker container with or without the Zustre plugin and / or the Tiny plugin.
73
You just have to comment / uncomment the indicated lines in the corresponding Dockerfile.
74
75
### Usage
76
77
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 
78
Then you can use lustrec, lustrev, or lustret with the following commands :
79
```
80
sudo docker run --rm -v $(pwd):/workdir -w /workdir --entrypoint "lustrec" lustrec' # for lustrec
81
sudo docker run --rm -v $(pwd):/workdir -w /workdir --entrypoint "lustret" lustrec' # for lustret
82
sudo docker run --rm -v $(pwd):/workdir -w /workdir --entrypoint "lustrev" lustrec' # for lustrev
83
``` 
84
These commands create a temporary container that share your working directory and run the desired utility
85
You might want to define aliases to make using lustrec easier and add them to your `.bashrc`
86
87
### Lustrec
88
89
In a modular setting:
90
```
91
# lustrec <filename.lus>
92
```
93
will generate filename.c and filename.h
94
95
With a main node:
96
```
97
# lustrec -node <main_node> <filename.lus>
98
```
99
will generate the same two files,
100
but also filename_main.c that contains a main function
101
and filename_alloc.h that contains the node allocation macros 
102
103
With a main node, with a static memory allocation scheme:
104 e2068500 Temesghen Kahsai
```
105 9c4cc944 Corentin Lauverjat
# lustrec -node <main_node> -dynamic <filename.lus>
106 e2068500 Temesghen Kahsai
```
107 9c4cc944 Corentin Lauverjat
same as above, but main function will dynamically allocate node memory
108
109
To compile it:
110
```
111
# gcc -Iinclude filename.c
112
# gcc -Iinclude filename_main.c
113
```
114
where include links to the include folder
115
116
To run it with the generated main function:
117
- compile the io_frontend.o
118
```
119
# gcc -c include/io_frontend.c
120
# gcc -Iinclude -o target_name io_frontend.o filename.o filename_main.o
121
# ./target_name
122
```
123
124
To analyze it with frama-c
125
```
126
# frama-c -cpp-extra-args='-Iinclude'  filename.c
127
```
128 9b0432bc Corentin Lauverjat
#### Tiny backend
129
130
The Tiny backend generates tiny (imperative) code from lustre. 
131
The example below generates tiny code for the node top of the two_counters.lus file
132
133
```
134
lustrec -d examples/two_counters -tiny -node top examples/two_counters/two_counters.lus
135
```
136
137
### Lustrev 
138
139
Lustrev is a Lustre verifier based on static analysis. 
140
141
#### Tiny verifier
142
143
With the option `-tiny` the verifier uses Tiny to analyse Lustre file. Tiny is based on theory of abstract interpretation. Set of values are represented as abstract values that overapproximate the values that can be taken by a variable.
144
145
This verifier runs an abstract simulation of the Lustre code. At each time step, the verifier outputs abstract values of the variable environnement.
146
147
It takes an Lustre file, a top node, a JSON file with the bounds on the parameters of the top node, and outputs a JSON file consisting of the abstract values of the variables at each time step.
148
149
The example below generates a two_counters_tiny.json file.
150
```
151
cd examples/two_counters
152
lustrev -node top -tiny -tiny-duration 5 -tiny-bounds-file tiny_input.json -tiny-output two_counters.lus 
153
```
154
155 9c4cc944 Corentin Lauverjat
### Ada backend 
156
157
Download ada from https://www.adacore.com/download
158
159
For the ADA backend:
160
- GNAT 2018 community edition on https://www.adacore.com/download
161
- gprbuild shall be in your path
162
163
## Uninstall 
164
165
Just run `opam unpin lustrec`
166
167
# Developer guide
168
169
## Description
170
171
This project uses [dune](https://dune.readthedocs.io/en/stable/quick-start.html) build system, and `autoconf` for configuration.
172
173
The `lib/` folder contains an essential library that is used by the various plugins.
174
175
The `plugins/` folder contains optional plugins that add feature to the compiler or verifier when enabled.
176
177
The `backends` folder contains the different backends for the supported languages (Ada, C, Horn, etc.).
178
179
The `src/` folder contains the remaining code, that is to say the code to generate the executables and put together all the plugins.
180
181
# Additional dependencies for developers
182
183
``` 
184
# apt-get install -y cmake
185
```
186
187
## How to build ?
188
189 b6a913e1 Corentin Lauverjat
Note: a Makefile is also provided, merely as a shortcut to dune commands.
190
191 9c4cc944 Corentin Lauverjat
```
192
$ autoconf
193
$ ./configure
194 507da95d Corentin Lauverjat
seal plugin : disabled because the following libraries are missing : seal.
195 9c4cc944 Corentin Lauverjat
zustre plugin : enabled
196
tiny plugin : enabled
197
salsa plugin : disabled because the following libraries are missing : salsa.
198
checking for gcc... gcc
199
checking whether the C compiler works... yes
200
checking for C compiler default output file name... a.out
201
checking for suffix of executables... 
202
checking whether we are cross compiling... no
203
checking for suffix of object files... o
204
checking whether we are using the GNU C compiler... yes
205
checking whether gcc accepts -g... yes
206
checking for gcc option to accept ISO C89... none needed
207
checking for __gmpz_init in -lgmp... yes
208
checking for mpfr_add in -lmpfr... yes
209
configure: creating ./config.status
210
config.status: creating Makefile
211
config.status: creating src/dune
212 507da95d Corentin Lauverjat
config.status: creating plugins/zustre/dune
213 9c4cc944 Corentin Lauverjat
config.status: creating src/pluginList.ml
214
config.status: creating src/verifierList.ml
215
config.status: creating lib/version.ml
216
config.status: creating share/FindLustre.cmake
217
218
$ dune build
219
220
```
221
222
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. 
223
You can force-enable a plugin with the `--enable-{seal/zustre/tiny/salsa}`flag
224
You can also disable a plugin with the `--disable-{seal/zustre/salsa}` flag
225
226
The build result is in `_build/`.
227
228
You will find the executables in `_build/default/src` under the names :
229
 * `main_lustre_compiler` for lustrec
230
 * `main_lustre_verifier`  for lustrev
231
 * `main_lustre_testgen` for lustret
232
233 507da95d Corentin Lauverjat
234
To build the executable like they will be released you can use `dune build @install`.
235
The executables will be located at `_build/install/default/bin`. The main difference with a simple build is that there will be no source code in the @install build, and the binaries will be put in the bin folder with there public names (lustrec, lustrev, lustret for instance), not the name of their Ocaml modules.
236
237
## How to install ? 
238
239
As a developper you have two ways of installed lustrec binaries so that there are available systemwide.
240
241
### With opam 
242
243
``` 
244
$ opam pin --kind=local . # add lustrec packages to opam
245
$ opam depext lustrec # install the required system dependencies
246
$ opam install lustrec # install Lustrec
247
```
248
249
### Without opam (with dune)
250
251
Simply run :
252
```
253
dune build @install
254
dune install
255
```
256
257
Beware that dune is just the build system, so dependencies will not be resolved and installed.
258
259 9c4cc944 Corentin Lauverjat
## Dockerfile.ubuntu 
260
261
This Dockerfile install the lustrec, lustrev and lustret tools in an Ubuntu 20.04 container.
262
It is a good example of how to build and install lustrec.
263
264
## Dependency management
265 e2068500 Temesghen Kahsai
266 9c4cc944 Corentin Lauverjat
You can see the dependency graph between the plugins and the core library with `dune-deps`
267 e2068500 Temesghen Kahsai
```
268 9c4cc944 Corentin Lauverjat
$ opam install dune-deps 
269
$ dune-deps | tred | dot -Tpng > deps.png
270 e2068500 Temesghen Kahsai
```
271
272 507da95d Corentin Lauverjat
## Release process
273
Example for "v0.1" : 
274
275
opam install dune-release
276
277
```
278
git tag -a 0.1
279
git push origin 0.1
280
``` 
281
282
283
284
285 e2068500 Temesghen Kahsai
# People
286 9c4cc944 Corentin Lauverjat
  * Pierre-Loic Garoche (ONERA)
287
  * Xavier Thirioux (IRIT)
288
  * Temesghen Kahsai (NASA Ames / CMU)