Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / README.md @ 9b0432bc

History | View | Annotate | Download (9.96 KB)

1

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

    
4
# What is LustreC ?
5

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

    
8
# 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
```
105
# lustrec -node <main_node> -dynamic <filename.lus>
106
```
107
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
#### 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
### 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
Note: a Makefile is also provided, merely as a shortcut to dune commands.
190

    
191
```
192
$ autoconf
193
$ ./configure
194
seal plugin : disabled because the following libraries are missing : seal.
195
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
config.status: creating plugins/zustre/dune
213
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

    
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
## 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

    
266
You can see the dependency graph between the plugins and the core library with `dune-deps`
267
```
268
$ opam install dune-deps 
269
$ dune-deps | tred | dot -Tpng > deps.png
270
```
271

    
272
## 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
# People
286
  * Pierre-Loic Garoche (ONERA)
287
  * Xavier Thirioux (IRIT)
288
  * Temesghen Kahsai (NASA Ames / CMU)