Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / README.md @ 507da95d

History | View | Annotate | Download (8.85 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
### Ada backend 
129

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

    
132
For the ADA backend:
133
- GNAT 2018 community edition on https://www.adacore.com/download
134
- gprbuild shall be in your path
135

    
136
## Uninstall 
137

    
138
Just run `opam unpin lustrec`
139

    
140
# Developer guide
141

    
142
## Description
143

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

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

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

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

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

    
154
# Additional dependencies for developers
155

    
156
``` 
157
# apt-get install -y cmake
158
```
159

    
160
## How to build ?
161

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

    
164
```
165
$ autoconf
166
$ ./configure
167
seal plugin : disabled because the following libraries are missing : seal.
168
zustre plugin : enabled
169
tiny plugin : enabled
170
salsa plugin : disabled because the following libraries are missing : salsa.
171
checking for gcc... gcc
172
checking whether the C compiler works... yes
173
checking for C compiler default output file name... a.out
174
checking for suffix of executables... 
175
checking whether we are cross compiling... no
176
checking for suffix of object files... o
177
checking whether we are using the GNU C compiler... yes
178
checking whether gcc accepts -g... yes
179
checking for gcc option to accept ISO C89... none needed
180
checking for __gmpz_init in -lgmp... yes
181
checking for mpfr_add in -lmpfr... yes
182
configure: creating ./config.status
183
config.status: creating Makefile
184
config.status: creating src/dune
185
config.status: creating plugins/zustre/dune
186
config.status: creating src/pluginList.ml
187
config.status: creating src/verifierList.ml
188
config.status: creating lib/version.ml
189
config.status: creating share/FindLustre.cmake
190

    
191
$ dune build
192

    
193
```
194

    
195
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. 
196
You can force-enable a plugin with the `--enable-{seal/zustre/tiny/salsa}`flag
197
You can also disable a plugin with the `--disable-{seal/zustre/salsa}` flag
198

    
199
The build result is in `_build/`.
200

    
201
You will find the executables in `_build/default/src` under the names :
202
 * `main_lustre_compiler` for lustrec
203
 * `main_lustre_verifier`  for lustrev
204
 * `main_lustre_testgen` for lustret
205

    
206

    
207
To build the executable like they will be released you can use `dune build @install`.
208
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.
209

    
210
## How to install ? 
211

    
212
As a developper you have two ways of installed lustrec binaries so that there are available systemwide.
213

    
214
### With opam 
215

    
216
``` 
217
$ opam pin --kind=local . # add lustrec packages to opam
218
$ opam depext lustrec # install the required system dependencies
219
$ opam install lustrec # install Lustrec
220
```
221

    
222
### Without opam (with dune)
223

    
224
Simply run :
225
```
226
dune build @install
227
dune install
228
```
229

    
230
Beware that dune is just the build system, so dependencies will not be resolved and installed.
231

    
232
## Dockerfile.ubuntu 
233

    
234
This Dockerfile install the lustrec, lustrev and lustret tools in an Ubuntu 20.04 container.
235
It is a good example of how to build and install lustrec.
236

    
237
## Dependency management
238

    
239
You can see the dependency graph between the plugins and the core library with `dune-deps`
240
```
241
$ opam install dune-deps 
242
$ dune-deps | tred | dot -Tpng > deps.png
243
```
244

    
245
## Release process
246
Example for "v0.1" : 
247

    
248
opam install dune-release
249

    
250
```
251
git tag -a 0.1
252
git push origin 0.1
253
``` 
254

    
255

    
256

    
257

    
258
# People
259
  * Pierre-Loic Garoche (ONERA)
260
  * Xavier Thirioux (IRIT)
261
  * Temesghen Kahsai (NASA Ames / CMU)