Project

General

Profile

« Previous | Next » 

Revision 9c4cc944

Added by Corentin Lauverjat over 1 year ago

Transition to dune build system
Improvement of opam integration
Dockerfile based on Alpine
Dockerfile based on Ubuntu
Update the README.md

View differences:

README.md
1 1

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

  
4
[![Stories in Ready](https://badge.waffle.io/coco-team/lustrec.png?label=ready&title=Ready)](https://waffle.io/coco-team/lustrec)
5
[![Throughput Graph](https://graphs.waffle.io/coco-team/lustrec/throughput.svg)](https://waffle.io/coco-team/lustrec/metrics/throughput)
6

  
7
# LustreC
4
# What is LustreC ?
8 5

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

  
11
# Dependencies
12
On a fresh ubuntu/debian-like install
13
> apt-get install opam libmpfr-dev
14
Get a fresh version of ocaml
15
> opam switch 4.06.1
16
Install some dependencies
17
> opam install depext ocamlgraph mlmpfr num cmdliner fmt logs yojson menhir
18
In OSX, some issues with Z3, please pin the following version:
19
> opam pin add z3 4.8.1
20
> opam install z3
21
# Build
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:
22 104
```
23
> autoconf
24
> ./configure
25
> make
105
# lustrec -node <main_node> -dynamic <filename.lus>
26 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
```
163
$ autoconf
164
$ ./configure
165
configure: Git branch: {CURRENT_GIT_BRANCH}
166
configure: ******** Configuration ********
167
configure: bin path:     NONE/bin
168
configure: include path: NONE/include
169
seal plugin : enabled
170
zustre plugin : enabled
171
tiny plugin : enabled
172
salsa plugin : disabled because the following libraries are missing : salsa.
173
checking for gcc... gcc
174
checking whether the C compiler works... yes
175
checking for C compiler default output file name... a.out
176
checking for suffix of executables... 
177
checking whether we are cross compiling... no
178
checking for suffix of object files... o
179
checking whether we are using the GNU C compiler... yes
180
checking whether gcc accepts -g... yes
181
checking for gcc option to accept ISO C89... none needed
182
checking for __gmpz_init in -lgmp... yes
183
checking for mpfr_add in -lmpfr... yes
184
configure: ../lustrec-tests/regression_tests
185
checking for ../lustrec-tests/regression_tests/CMakeLists.txt... yes
186
configure: creating ./config.status
187
config.status: creating Makefile
188
config.status: creating src/dune
189
config.status: creating src/pluginList.ml
190
config.status: creating src/verifierList.ml
191
config.status: creating lib/version.ml
192
config.status: creating share/FindLustre.cmake
193
configure: ****** Regression Tests  ******
194
configure: tests path: ../lustrec-tests/regression_tests
195
configure: ******** Configuration ********
196
configure: Execute "make; make install" now
197

  
198
$ dune build
199

  
200
```
201

  
202
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. 
203
You can force-enable a plugin with the `--enable-{seal/zustre/tiny/salsa}`flag
204
You can also disable a plugin with the `--disable-{seal/zustre/salsa}` flag
205

  
206
The build result is in `_build/`.
207

  
208
You will find the executables in `_build/default/src` under the names :
209
 * `main_lustre_compiler` for lustrec
210
 * `main_lustre_verifier`  for lustrev
211
 * `main_lustre_testgen` for lustret
212

  
213
## Dockerfile.ubuntu 
214

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

  
218
## Dependency management
27 219

  
28
# Usage
220
You can see the dependency graph between the plugins and the core library with `dune-deps`
29 221
```
30
> ./bin/lustrec -help
222
$ opam install dune-deps 
223
$ dune-deps | tred | dot -Tpng > deps.png
31 224
```
32 225

  
33 226
# People
34
* Pierre-Loic Garoche (ONERA)
35
* Xavier Thirioux (IRIT)
36
* Temesghen Kahsai (NASA Ames / CMU)
227
  * Pierre-Loic Garoche (ONERA)
228
  * Xavier Thirioux (IRIT)
229
  * Temesghen Kahsai (NASA Ames / CMU)

Also available in: Unified diff