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:

.dockerignore
1
_build/
2
.git/
.gitignore
1 1
*~
2
/src/_build/
3
/setup.data
4
/setup.log
5
/src/version.ml
6
/src/pluginList.ml
7
/myocamlbuild.ml
8
*.cmt
9
*.log
2
/_build/
3
/test
10 4
Makefile
11 5
/configure
12
/src/_tags
13
/bin
14
*cache/
15
/config.status
6
/config.log
7
/config.status
8
/*cache/
9
*.merlin
10
/Makefile
11
/src/dune
12
/plugins/zustre/dune
13
/src/pluginList.ml
14
/src/verifierList.ml
15
/lib/version.ml
16
/include/z3librc
17
/share/FindLustre.cmake
18
/deps.png
.merlin
1
S src
2
S src/backends
3
S src/backends/C
4
S src/backends/EMF
5
S src/backends/Horn
6
S src/backends/Java
7
S src/checks
8
S src/features
9
S src/features/machine_types
10
S src/parsers
11
S src/plugins
12
S src/plugins/mpfr
13
S src/plugins/salsa
14
S src/plugins/scopes
15
S src/tools
16
S src/tools/stateflow
17
S src/tools/stateflow/common
18
S src/tools/stateflow/json-parser
19
S src/tools/stateflow/models
20
S src/tools/stateflow/semantics
21
S src/utils
22

  
23
B src/_build
24
B src/_build/backends
25
B src/_build/backends/C
26
B src/_build/backends/EMF
27
B src/_build/backends/Horn
28
B src/_build/checks
29
B src/_build/features
30
B src/_build/features/machine_types
31
B src/_build/parsers
32
B src/_build/plugins
33
B src/_build/plugins/mpfr
34
B src/_build/plugins/salsa
35
B src/_build/plugins/scopes
36
B src/_build/tools
37
B src/_build/tools/stateflow
38
B src/_build/tools/stateflow/common
39
B src/_build/tools/stateflow/models
40
B src/_build/tools/stateflow/semantics
41
B src/_build/utils
42

  
43
B test
.ocaml-config.sh
1
#!/bin/sh
2
case "$OCAML_VERSION,$OPAM_VERSION" in
3
    4.01.0,1.1.0) ppa=avsm/ocaml41+opam11 ;;
4
    4.01.0,1.2.0) ppa=avsm/ocaml41+opam12 ;;
5
    4.02.1,1.1.0) ppa=avsm/ocaml42+opam11 ;;
6
    4.02.1,1.2.0) ppa=avsm/ocaml42+opam12 ;;
7
    *) echo Unknown $OCAML_VERSION,$OPAM_VERSION; exit 1 ;;
8
esac
9

  
10
echo "\n" | add-apt-repository ppa:$ppa
Dockerfile.alpine
1
FROM alpine:3.12 
2

  
3
RUN apk add --no-cache \ 
4
    make \
5
    rsync \
6
    git \ 
7
    m4 \ 
8
    patch \
9
    pkgconfig \ 
10
    libc-dev \
11
    gcc \ 
12
    ocaml ocaml-compiler-libs ocaml-ocamldoc opam ocaml-findlib \ 
13
    mpfr-dev=4.0.2-r4
14

  
15
# Configuration de OPAM
16
RUN opam init --auto-setup -y --disable-sandboxing && opam clean
17

  
18
ENV PATH "$PATH:/root/.opam/default/bin"
19

  
20
COPY . /lustrec
21

  
22
WORKDIR /lustrec
23

  
24
RUN eval $(opam env) && \ 
25
    opam update && \
26
    opam pin -n mlmpfr 4.0.2+dune && \
27
    opam pin -y -n . && \
28
    opam install -y depext && \
29
    opam depext --yes lustrec && \
30
    opam install -y lustrec && \
31
    #
32
    # To enable Zustre plugin, uncomment the lines below : 
33
    # opam depext --yes lustrec-enable-zustre && \
34
    # # z3 install requires a C++ compiler (g++ or clang)
35
    # apk add --no-cache g++ && \ 
36
    # opam install -y lustrec-enable-zustre && \ 
37
    # ----
38
    # To enable Tiny plugin, uncomment the lines below :
39
    # opam pin -y -n https://cavale.enseeiht.fr/git/ikocos.tiny#master && \
40
    # opam depext --yes tiny && \
41
    # opam install -y tiny && \
42
    # ---- 
43
    opam clean
Dockerfile.ubuntu
1
FROM ubuntu:20.04
2

  
3

  
4
RUN apt-get update && apt-get install -y --no-install-recommends \
5
    opam \
6
    ca-certificates \
7
    m4 \
8
    rsync \
9
    git \
10
    && rm -rf /var/lib/apt/lists/*
11

  
12

  
13
RUN opam init --auto-setup -y --disable-sandboxing 
14
ENV PATH "$PATH:/root/.opam/default/bin"
15

  
16
COPY . /lustrec
17

  
18
WORKDIR /lustrec
19

  
20
RUN eval $(opam config env) && \ 
21
    apt-get update && \
22
    opam pin -n mlmpfr 4.0.2+dune && \
23
    opam pin -y -n . && \
24
    opam install -y depext && \
25
    opam depext --yes lustrec && \
26
    opam install -y lustrec && \
27
    #
28
    # To enable Zustre plugin, uncomment the lines below : 
29
    # opam depext --yes lustrec-enable-zustre && \
30
    # opam install -y lustrec-enable-zustre && \ 
31
    # ----
32
    # To enable Tiny plugin, uncomment the lines below :
33
    # opam pin -y -n https://cavale.enseeiht.fr/git/ikocos.tiny#master && \
34
    # opam depext --yes tiny && \
35
    # opam install -y tiny && \
36
    # ----
37
    opam clean && \
38
    rm -rf /var/lib/apt/lists/*
INSTALL
1
On Mac
2
brew install autoconf opam cmake
3
Download ada from https://www.adacore.com/download
4

  
5

  
6
Then
7
opam install ocamlfind ocamlgraph cmdliner fmt logs dune num yojson 
8

  
9

  
10

  
11
For the ADA backend:
12
- GNAT 2018 community edition on https://www.adacore.com/download
13
- gprbuild shall be in your path
Makefile.in
1
# @configure_input@
2

  
1 3
prefix=@prefix@
2 4
exec_prefix=@exec_prefix@
3 5
bindir=@bindir@
4 6
datarootdir = ${prefix}/share
5 7
includedir = ${prefix}/include
6 8

  
9
configure: configure.ac
10
	@echo configure.ac has changed relaunching autoconf
11
	@autoconf
12

  
13
Makefile: Makefile.in config.status configure
14
	@echo Makefile.in has changed relaunching autoconf
15
	@./config.status --recheck
16

  
17
default: build
18

  
19
build: Makefile
20
	dune build
21

  
22
test: test-config
23
	cd test; ctest -D Experimental -R ${DEFAULT_TEST_TARGET} -E ${DEFAULT_EXCLUDE_TEST}
24

  
25
test-config: ${bindir}/lustrec ${bindir}/lustrev ${bindir}/lustret
26
	mkdir -p test; \
27
	cd test; \
28
	cmake -DLUSTRE_PATH_HINT=${bindir} -DSUBPROJ=@CDASHSUBPROJ@ ../@PATH_TO_TESTS@; \
29
	
30
install: Makefile
31
	dune install
32

  
33
uninstall: Makefile
34
	dune uninstall
35

  
36
clean:
37
	dune clean
38
	# Optionally, remove all files/folders ignored by git as defined
39
	# in .gitignore (-X).
40
	# git clean -dfXq
41

  
42

  
43

  
7 44
LUSI_LIBS=include/lustrec_math.lusi include/simulink_math_fcn.lusi include/conv.lusi
8 45
LUSI_MPFR_LIB=include/mpfr_lustre.lusi
9 46
LOCAL_BINDIR=bin
......
13 50
DEFAULT_TEST_TARGET=COMPIL_LUS\|MAKE\|BIN\|DIFF
14 51
DEFAULT_EXCLUDE_TEST=LUSTRET
15 52

  
16
all: $(BIN_TARGETS)
17

  
18
lustrec:
19
	@echo Compiling binary lustrec
20
	@make -C src lustrec
21 53

  
22
lustret:
23
	@echo Compiling binary lustret
24
	@make -C src lustret
25

  
26
lustrev:
27
	@echo Compiling binary lustrev
28
	@make -C src lustrev
29

  
30
lustrei:
31
	@echo Compiling binary lustrei
32
	@make -C src lustrei
33

  
34
@lustresf@
35

  
36
configure: configure.ac
37
	@echo configure.ac has changed relaunching autoconf
38
	@autoconf
39

  
40
Makefile: Makefile.in config.status configure
41
	@echo Makefile.in has changed relaunching autoconf
42
	@./config.status --recheck
43 54

  
44 55
doc:
45 56
	@echo Generating doc
......
48 59
dot: doc
49 60
	@make -C src dot
50 61

  
51
clean: clean-lusic
52
	@make -C src clean
53 62

  
54 63
dist-src-clean: clean
55 64
	@rm -f config.log config.status include/*.lusic include/lustrec_math.h include/simulink_math_fcn.h include/conv.h include/mpfr_lustre.h
......
65 74
dist-clean: dist-src-clean
66 75
	@rm -f configure Makefile opam share/FindLustre.cmake
67 76

  
68
%.lusic: %.lusi
69
	@echo Compiling $<
70
	@$(LOCAL_BINDIR)/lustrec -verbose 0 -I include -d include $<
71

  
72
clean-lusic:
73
	@rm -f $(LUSI_LIBS:%.lusi=%.lusic)
74
	@rm -f $(LUSI_MPFR_LIB:%.lusi=%.lusic)
75

  
76
compile-lusi: $(LUSI_LIBS:%.lusi=%.lusic)
77

  
78
compile-mpfr-lusi: $(LUSI_MPFR_LIB)
79
	@echo Compiling $<
80
	@$(LOCAL_BINDIR)/lustrec -verbose 0 -mpfr 1 -d include $<
81

  
82
install-include: compile-lusi compile-mpfr-lusi
83
	install -m 0655 include/* ${includedir}/lustrec
84 77

  
85
install-base: clean-lusic
86
	mkdir -p ${bindir}
87
	for x in $(BIN_TARGETS); do install -m 0755 $(LOCAL_BINDIR)/$$x ${bindir}; done
88
	mkdir -p ${datarootdir}
89
	install -m 0655 share/*.cmake ${datarootdir}
90
	mkdir -p ${includedir}/lustrec
91
	install -m 0655 include/* ${includedir}/lustrec
92

  
93
install: install-base install-include
94

  
95
uninstall:
96
	rm -Rf ${includedir}/lustrec
97
	rm -Rf ${datarootdir}/share/FindLustre.cmake
98
	for x in $(BIN_TARGETS); do rm -f ${bindir}/$$x; done
99

  
100
test-config: ${bindir}/lustrec
101
	if @PATH_TO_TESTS_DEFINED@; then \
102
	  mkdir -p test; \
103
	  cd test; \
104
	  cmake -DLUSTRE_PATH_HINT=${bindir} -DSUBPROJ=@CDASHSUBPROJ@ ../@PATH_TO_TESTS@; \
105
	fi
106 78

  
107 79
test-no-submit: test-config
108 80
	cd test; ctest -M Experimental -T Start -T Update -T Configure -T Build -T Test -R ${DEFAULT_TEST_TARGET} -E ${DEFAULT_EXCLUDE_TEST}
......
111 83
	cd test; ctest -M Experimental -T Submit -R ${DEFAULT_TEST_TARGET} -E ${DEFAULT_EXCLUDE_TEST}
112 84

  
113 85

  
114
test: test-config
115
	cd test; ctest -D Experimental -R ${DEFAULT_TEST_TARGET} -E ${DEFAULT_EXCLUDE_TEST}
116 86

  
117 87

  
118 88
test-full-no-submit: test-config
README.lustrec
1
To compile Lustrec:
2
------------------
3

  
4
# autoconf
5
# ./configure
6
# make
7
# make install
8

  
9

  
10
To use lustrec:
11
--------------
12

  
13
In a modular setting:
14
# lustrec <filename.lus>
15
will generate filename.c and filename.h
16

  
17
With a main node:
18
# lustrec -node <main_node> <filename.lus>
19
will generate the same two files,
20
but also filename_main.c that contains a main function
21
and filename_alloc.h that contains the node allocation macros 
22

  
23
With a main node, with a static memory allocation scheme:
24
# lustrec -node <main_node> -dynamic <filename.lus>
25
same as above, but main function will dynamically allocate node memory
26

  
27
To compile it:
28
# gcc -Iinclude filename.c
29
# gcc -Iinclude filename_main.c
30
where include links to the include folder
31

  
32
To run it with the generated main function:
33
- compile the io_frontend.o
34
# gcc -c include/io_frontend.c
35
# gcc -Iinclude -o target_name io_frontend.o filename.o filename_main.o
36
# ./target_name
37

  
38
To analyze it with frama-c
39
# frama-c -cpp-extra-args='-Iinclude'  filename.c
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)
backends/Ada/README
1
This is the Ada Backend generating Ada code from the machine code computed
2
from a Lustre file.
3

  
4
The backend is split in several files described in this README.
5

  
6
=> misc_lustre_function.ml
7
Some fonction on pure Lustre machine code, no printers
8
or anything related to Ada. It just compute information from the Machine Code.
9
It contains mostly the unification code used for polymorphic type. It is
10
important since the Lustrec.Arrow node is polymorphic.
11

  
12
=> misc_printer.ml
13
Some general format printer function, not related at all
14
to Ada but used by this backend.
15

  
16
=> ada_printer.mli
17
=> ada_printer.ml
18
It contains Type representing some part of Ada syntaxe and printers function
19
to generates it. There is nothing specifics to Lustre in this file. It is
20
mostly printers for the declarative part of Ada. The printer functions takes in
21
general directly printer function build by other files(like ada_backend_common.ml)
22
to print instruction and expression contained in the declaration.
23
For example, the printer for the declaration of a variable will take
24
two printer functions as argument:
25
 - pp_type: printing the type
26
 - pp_name: printing the variable name
27
The printer will looks like :
28
--
29
let pp_var_decl pp_type pp_name =
30
  fprintf fmt "%t : %t" pp_type pp_name
31
--
32

  
33
=> ada_backend_common.mli
34
=> ada_backend_common.ml
35
It contains function printing Ada code(instruction and exression) from Machine
36
Code. This functions are used or could be used for ads and/or adb and/or
37
wrappers.
38

  
39
=> ada_backend_ads.ml
40
It contains function printing Ada code(instruction and exression) from Machine
41
Code for the Ads file.
42

  
43
=> ada_backend_adb.ml
44
It contains function printing Ada code(instruction and exression) from Machine
45
Code for the Adb file.
46

  
47
=> ada_backend_wrapper.ml
48
It contains function printing Ada code(instruction and exression) from Machine
49
Code for :
50
  - an adb file witha main function containg a loop calling step.
51
  - a project file
52
  - a configuration file
53

  
54
=> ada_backend.ml
55
It contains the main function of the backend which perform the unification
56
and write all the files using the previsous code.
57

  
58

  
backends/Ada/ada_backend.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Format
13
open Lustrec.Machine_code_types
14

  
15
open Misc_lustre_function
16
open Ada_printer
17
open Ada_backend_common
18

  
19
let indent_size = 2
20

  
21
(** Log at level 2 a string message with some indentation.
22
   @param indent the indentation level
23
   @param info the message
24
**)
25
let log_str_level_two indent info =
26
  let str_indent = String.make (indent*indent_size) ' ' in
27
  let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
28
  Lustrec.Log.report ~level:2 pp_message;
29
  Format.pp_print_flush Format.err_formatter ()
30

  
31
(** Write a new file with formatter
32
   @param destname folder where the file shoudl be created
33
   @param pp_filename function printing the filename
34
   @param pp_file function wich pretty print the file
35
   @param arg will be given to pp_filename and pp_file
36
**)
37
let write_file destname pp_filename pp_file arg =
38
  let path = asprintf "%s%a" destname pp_filename arg in
39
  let out = open_out path in
40
  let fmt = formatter_of_out_channel out in
41
  log_str_level_two 2 ("generating "^path);
42
  pp_file fmt arg;
43
  pp_print_flush fmt ();
44
  close_out out
45

  
46

  
47
(** Exception raised when a machine contains a feature not supported by the
48
  Ada backend*)
49
exception CheckFailed of string
50

  
51

  
52
(** Check that a machine match the requirement for an Ada compilation :
53
      - No constants.
54
   @param machine the machine to test
55
**)
56
let check machine =
57
  match machine.mconst with
58
    | [] -> ()
59
    | _ -> raise (CheckFailed "machine.mconst should be void")
60

  
61

  
62
let get_typed_submachines machines m =
63
  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
64
  let submachines = List.map (get_machine machines) instances in
65
  List.map2
66
    (fun instance submachine ->
67
      let ident = (fst instance) in
68
      ident, (get_substitution m ident submachine, submachine))
69
    instances submachines
70

  
71
let extract_contract machines m =
72
  let rec find_submachine_from_ident ident = function
73
    | [] -> raise Not_found
74
    | h::t when h.mname.node_id = ident -> h
75
    | _::t -> find_submachine_from_ident ident t
76
  in
77
  let extract_ident eexpr =
78
    match eexpr.Lustrec.Lustre_types.eexpr_qfexpr.expr_desc with
79
      | Expr_ident ident -> ident
80
      | _ -> assert false
81
      (*
82
      | Expr_const cst -> assert false
83
      | Expr_tuple exprs -> assert false
84
      | Expr_ite (expr1, expr2, expr3) -> assert false
85
      | Expr_arrow (expr1, expr2)  -> assert false
86
      | Expr_fby (expr1, expr2) -> assert false
87
      | Expr_array exprs -> assert false
88
      | Expr_access (expr1, dim) -> assert false
89
      | Expr_power (expr1, dim) -> assert false
90
      | Expr_pre expr -> assert false
91
      | Expr_when (expr,ident,label) -> assert false
92
      | Expr_merge (ident, l) -> assert false
93
      | Expr_appl call -> assert false
94
      *)
95
  in
96
  match m.mspec with
97
    | Some (NodeSpec ident) ->
98
      begin
99
        let machine_spec = find_submachine_from_ident ident machines in
100
        let guarantees =
101
          match machine_spec.mspec with
102
            | Some (Contract contract) ->
103
                assert (contract.consts=[]);
104
                assert (contract.locals=[]);
105
                assert (contract.stmts=[]);
106
                assert (contract.assume=[]);
107
                List.map extract_ident contract.guarantees
108
            | _ -> assert false
109
        in
110
        let opt_machine_spec =
111
          match machine_spec.mstep.step_instrs with
112
            | [] -> None
113
            | _ -> Some machine_spec
114
        in
115
        (opt_machine_spec, guarantees)
116
      end
117
    | _ -> None, []
118

  
119
(** Main function of the Ada backend. It calls all the subfunction creating all
120
the file and fill them with Ada code representing the machines list given.
121
   @param basename name of the lustre file
122
   @param prog useless
123
   @param prog list of machines to translate
124
   @param dependencies useless
125
**)
126
let translate_to_ada basename prog machines dependencies =
127
  let module Ads = Ada_backend_ads.Main in
128
  let module Adb = Ada_backend_adb.Main in
129
  let module Wrapper = Ada_backend_wrapper.Main in
130

  
131
  let is_real_machine m =
132
    match m.mspec with
133
      | Some (Contract x) -> false
134
      | _ -> true
135
  in
136

  
137
  let filtered_machines = List.filter is_real_machine machines in
138

  
139
  let typed_submachines =
140
    List.map (get_typed_submachines machines) filtered_machines in
141
  
142
  let contracts = List.map (extract_contract machines) filtered_machines in
143

  
144
  let _machines = List.combine contracts filtered_machines in
145

  
146
  let _machines = List.combine typed_submachines _machines in
147

  
148
  let _pp_filename ext fmt (_, (_, machine)) =
149
    pp_machine_filename ext fmt machine in
150

  
151
  (* Extract the main machine if there is one *)
152
  let main_machine = (match !Lustrec.Options.main_node with
153
  | "" -> None
154
  | main_node -> (
155
    match Lustrec.Machine_code_common.get_machine_opt filtered_machines main_node with
156
    | None -> begin
157
      Format.eprintf "Ada Code generation error: %a@." Lustrec.Error.pp_error_msg Lustrec.Error.Main_not_found;
158
      raise (Lustrec.Error.Error (Lustrec.Location.dummy_loc,Lustrec.Error.Main_not_found))
159
    end
160
    | Some m -> Some m
161
  )) in
162

  
163
  let destname = !Lustrec.Options.dest_dir ^ "/" in
164

  
165
  log_str_level_two 1 "Checking machines";
166
  List.iter check machines;
167

  
168
  log_str_level_two 1 "Generating ads";
169
  List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
170

  
171
  log_str_level_two 1 "Generating adb";
172
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
173

  
174
  (* If a main node is given we generate a main adb file and a project file *)
175
  log_str_level_two 1 "Generating wrapper files";
176
  (match main_machine with
177
    | None -> ()
178
    | Some machine ->
179
        write_file destname pp_main_filename (Wrapper.pp_main_adb (get_typed_submachines filtered_machines machine)) machine;
180
        write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file filtered_machines basename) main_machine);
181
  write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
182
  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file filtered_machines basename) None;
183

  
184

  
185
(* Local Variables: *)
186
(* compile-command:"make -C ../../.." *)
187
(* End: *)
backends/Ada/ada_backend_adb.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Format
13

  
14
open Lustrec.Machine_code_types
15
open Lustrec.Lustre_types
16
open Lustrec.Corelang
17
open Lustrec.Machine_code_common
18

  
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
22
open Ada_backend_common
23

  
24
(** Main module for generating packages bodies
25
 **)
26
module Main =
27
struct
28

  
29
  (** Printing function for basic assignement [var := value].
30

  
31
      @param fmt the formater to print on
32
      @param var_name the name of the variable
33
      @param value the value to be assigned
34
   **)
35
  let pp_assign env fmt var value =
36
    fprintf fmt "%a := %a"
37
      (pp_var env) var
38
      (pp_value env) value
39

  
40
  (** Printing function for instruction. See
41
      {!type:Lustrec.Machine_code_types.instr_t} for more details on
42
      machine types.
43

  
44
      @param typed_submachines list of all typed machine instances of this machine
45
      @param machine the current machine
46
      @param fmt the formater to print on
47
      @param instr the instruction to print
48
   **)
49
  let rec pp_machine_instr typed_submachines env instr fmt =
50
    let pp_instr = pp_machine_instr typed_submachines env in
51
    (* Print args for a step call *)
52
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
53
    (* Print a when branch of a case *)
54
    let pp_when (cond, instrs) fmt =
55
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
56
    in
57
    (* Print a case *)
58
    let pp_case fmt (g, hl) =
59
      fprintf fmt "case %a is@,%aend case"
60
        (pp_value env) g
61
        pp_block (List.map pp_when hl)
62
    in
63
    (* Print a if *)
64
    (* If neg is true the we must test for the negation of the condition. It
65
       first check that we don't have a negation and a else case, if so it
66
       inverses the two branch and remove the negation doing a recursive
67
       call. *)
68
    let pp_if fmt (neg, g, instrs1, instrs2) =
69
      let pp_cond =
70
        if neg then
71
          fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
72
        else
73
          pp_value env
74
      in
75
      let pp_else = match instrs2 with
76
        | None -> fun fmt -> fprintf fmt ""
77
        | Some i2 -> fun fmt ->
78
            fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
79
      in
80
      fprintf fmt "if %a then@,%a%tend if"
81
        pp_cond g
82
        pp_block (List.map pp_instr instrs1)
83
        pp_else
84
    in
85
    match get_instr_desc instr with
86
      (* no reset *)
87
      | MNoReset _ -> ()
88
      (* reset  *)
89
      | MReset i when List.mem_assoc i typed_submachines ->
90
          let (substitution, submachine) = get_instance i typed_submachines in
91
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
92
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
93
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
94
      | MLocalAssign (ident, value) ->
95
          pp_assign env fmt ident value
96
      | MStateAssign (ident, value) ->
97
          pp_assign env fmt ident value
98
      | MStep ([i0], i, vl) when is_builtin_fun i ->
99
          let value = mk_val (Fun (i, vl)) i0.var_type in
100
            pp_assign env fmt i0 value
101
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
102
          let (substitution, submachine) = get_instance i typed_submachines in
103
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
104
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
105
          let output = List.map pp_var_name il in
106
          let args =
107
            (if is_machine_statefull submachine then [[pp_state i]] else [])
108
              @(if input!=[] then [input] else [])
109
              @(if output!=[] then [output] else [])
110
          in
111
          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
112
      | MBranch (_, []) -> assert false
113
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
114
          pp_if fmt (build_if g c1 i1 tl)
115
      | MBranch (g, hl) -> pp_case fmt (g, hl)
116
      | MComment s  ->
117
          let lines = String.split_on_char '\n' s in
118
          fprintf fmt "%a" (Lustrec.Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
119
      | _ -> assert false
120

  
121
  (** Print the definition of the step procedure from a machine.
122

  
123
     @param typed_submachines list of all typed machine instances of this machine
124
     @param fmt the formater to print on
125
     @param machine the machine
126
  **)
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129
      | MLocalAssign (ident, value) -> 
130
          { instr_desc = MStateAssign (ident, value);
131
            lustre_eq= instr.lustre_eq }
132
      | x -> instr
133
    in
134
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
135
      | None -> [], []
136
      | Some m_spec ->
137
          List.map (build_pp_var_decl_local (Some (true, false, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
138
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
139
    in
140
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
141
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
142
    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
143
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
144

  
145
  (** Print the definition of the reset procedure from a machine.
146

  
147
     @param typed_submachines list of all typed machine instances of this machine
148
     @param fmt the formater to print on
149
     @param machine the machine
150
  **)
151
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
152
    let build_assign = function var ->
153
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
154
    in
155
    let env, memory = match m_spec_opt with
156
      | None -> env, m.mmemory
157
      | Some m_spec ->
158
          env,
159
          (m.mmemory)
160
    in
161
    let assigns = List.map build_assign memory in
162
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
163
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
164

  
165
  (** Print the package definition(ads) of a machine.
166
    It requires the list of all typed instance.
167
    A typed submachine instance is (ident, type_machine) with ident
168
    the instance name and typed_machine is (substitution, machine) with machine
169
    the machine associated to the instance and substitution the instanciation of
170
    all its polymorphic types.
171
     @param fmt the formater to print on
172
     @param typed_submachines list of all typed machine instances of this machine
173
     @param m the machine
174
  **)
175
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
176
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
177
    let pp_reset fmt =
178
      if is_machine_statefull machine then
179
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
180
      else
181
        fprintf fmt ""
182
    in
183
    let aux pkgs (id, _) =
184
      try
185
        let (pkg, _) = List.assoc id ada_supported_funs in
186
        if List.mem pkg pkgs then
187
          pkgs
188
        else
189
          pkg::pkgs
190
      with Not_found -> pkgs
191
    in
192
    let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
193
    let pp_content fmt =
194
      fprintf fmt "%t%a"
195
        (*Define the reset procedure*)
196
        pp_reset
197
        
198
        (*Define the step procedure*)
199
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
200
    in
201
    fprintf fmt "%a%t%a;@."
202
      
203
      (* Include all the required packages*)
204
      (Lustrec.Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
205
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," packages)
206
      
207
      (*Print package*)
208
      (pp_package (pp_package_name machine) [] true ) pp_content
209

  
210
end
211

  
212
(* Local Variables: *)
213
(* compile-command: "make -C ../../.." *)
214
(* End: *)
backends/Ada/ada_backend_ads.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Format
13

  
14
open Lustrec.Machine_code_types
15
open Lustrec.Lustre_types
16
open Lustrec.Corelang
17
open Lustrec.Machine_code_common
18

  
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
22
open Ada_backend_common
23

  
24

  
25

  
26
(** Functions printing the .ads file **)
27
module Main =
28
struct
29

  
30
  let rec init f = function i when i < 0 -> [] | i -> (f i)::(init f (i-1)) (*should be replaced by the init of list from ocaml std lib*)
31

  
32
  let suffixOld = "_old"
33
  let suffixNew = "_new"
34
  let pp_invariant_name fmt = fprintf fmt "inv"
35
  let pp_transition_name fmt = fprintf fmt "transition"
36
  let pp_init_name fmt = fprintf fmt "init"
37
  let pp_state_name_predicate suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
38
  let pp_axiomatize_package_name fmt = fprintf  fmt "axiomatize"
39

  
40
  (** Print the expression function representing the transition predicate.
41
     @param fmt the formater to print on
42
     @param machine the machine
43
  **)
44
  let pp_init_predicate typed_submachines fmt (opt_spec_machine, m) =
45
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
46
    pp_predicate pp_init_name [[new_state]] true fmt None
47

  
48
  (** Print the expression function representing the transition predicate.
49
     @param fmt the formater to print on
50
     @param machine the machine
51
  **)
52
  let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
53
    let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in
54
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
55
    let inputs = build_pp_var_decl_step_input AdaIn None m in
56
    let outputs = build_pp_var_decl_step_output AdaIn None m in
57
    pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) true fmt None
58

  
59
  let pp_invariant_predicate typed_submachines fmt (opt_spec_machine, m) =
60
    pp_predicate pp_invariant_name [[build_pp_state_decl AdaIn None]] true fmt None
61

  
62
  (** Print a new statement instantiating a generic package.
63
     @param fmt the formater to print on
64
     @param substitutions the instanciation substitution
65
     @param machine the machine to instanciate
66
  **)
67
  let pp_new_package fmt (substitutions, machine) =
68
    let pp_name = pp_package_name machine in
69
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
70
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
71
    pp_package_instanciation pp_new_name pp_name fmt instanciations
72

  
73
  (** Remove duplicates from a list according to a given predicate.
74
     @param eq the predicate defining equality
75
     @param l the list to parse
76
  **)
77
  let remove_duplicates eq l =
78
    let aux l x = if List.exists (eq x) l then l else x::l in
79
    List.fold_left aux [] l
80

  
81

  
82
  (** Compare two typed machines.
83
  **)
84
  let eq_typed_machine (subst1, machine1) (subst2, machine2) =
85
    (String.equal machine1.mname.node_id machine2.mname.node_id) &&
86
    (List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
87

  
88

  
89
  (** Print the package declaration(ads) of a machine.
90
    It requires the list of all typed instance.
91
    A typed submachine is a (ident, typed_machine) with
92
      - ident: the name 
93
      - typed_machine: a (substitution, machine) with
94
        - machine: the submachine struct
95
        - substitution the instanciation of all its polymorphic types.
96
     @param fmt the formater to print on
97
     @param typed_submachines list of all typed submachines of this machine
98
     @param m the machine
99
  **)
100
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
101
    let typed_machines = snd (List.split typed_submachines) in
102
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
103
    
104
    let machines_to_import = List.map pp_package_name (snd (List.split typed_machines_set)) in
105

  
106
    let polymorphic_types = find_all_polymorphic_type m in
107
    
108
    let typed_machines_to_instanciate =
109
      List.filter (fun (l, _) -> l != []) typed_machines_set in
110

  
111
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
112

  
113
    let memories = match m_spec_opt with
114
      | None -> []
115
      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x)) m.mmemory
116
    in
117
    let ghost_private = memories in
118
    (* Commented since not used. Could be reinjected in the code 
119
    let vars_spec = match m_spec_opt with
120
      | None -> []
121
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, false, [], []))) (m_spec.mmemory)
122
    in *)
123
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
124
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
125
    let var_lists =
126
      (if states = [] then [] else [states]) @
127
      (if vars = [] then [] else [vars]) in
128
    
129
    let pp_ifstatefull fmt pp =
130
      if is_machine_statefull m then
131
        fprintf fmt "%t" pp
132
      else
133
        fprintf fmt ""
134
    in
135

  
136
    let pp_state_decl_and_reset fmt =
137
      let init fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_init_name, [[pp_state_name]]) in
138
      let contract = Some (false, false, [], [init]) in
139
      fprintf fmt "%t;@,@,%a;@,@,"
140
        (*Declare the state type*)
141
        (pp_type_decl pp_state_type AdaPrivate)
142
        
143
        (*Declare the reset procedure*)
144
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract) AdaNoContent
145
    in
146

  
147
    let pp_private_section fmt =
148
      fprintf fmt "@,private@,@,%a%t%a%t%a"
149
      (*Instantiate the polymorphic type that need to be instantiated*)
150
      (Lustrec.Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
151
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
152
      
153
      (*Define the state type*)
154
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
155
        
156
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
157
      (Lustrec.Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private
158
    in
159

  
160
    let pp_content fmt =
161
      let pp_contract_opt =
162
        let pp_var x fmt =
163
            pp_clean_ada_identifier fmt x
164
        in
165
        let guarantee_post_conditions = List.map pp_var guarantees in
166
        let state_pre_conditions, state_post_conditions =
167
          if is_machine_statefull m then
168
          begin
169
            let input = List.map pp_var_name m.mstep.step_inputs in
170
            let output = List.map pp_var_name m.mstep.step_outputs in
171
            let args =
172
              [[pp_old pp_state_name;pp_state_name]]
173
                @(if input!=[] then [input] else [])
174
                @(if output!=[] then [output] else [])
175
            in
176
            let transition fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_transition_name, args) in
177
            let invariant fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_invariant_name, [[pp_state_name]]) in
178
            [invariant], [transition;invariant]
179
          end
180
          else
181
            [], []
182
        in
183
        let post_conditions = state_post_conditions@guarantee_post_conditions in
184
        let pre_conditions = state_pre_conditions in
185
        if post_conditions = [] && pre_conditions = [] then
186
          None
187
        else
188
          Some (false, false, pre_conditions, post_conditions)
189
      in
190
      let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, false, [], []))) in
191
      let ghost_public = List.map pp_guarantee guarantees in
192
      fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%t"
193
        
194
        (Lustrec.Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_public
195
        (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
196
        
197
        pp_ifstatefull pp_state_decl_and_reset
198
        
199
        (*Declare the step procedure*)
200
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
201
        
202
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
203
        
204
        (pp_package (pp_axiomatize_package_name) [] false)
205
          (fun fmt -> fprintf fmt "pragma Annotate (GNATProve, External_Axiomatization);@,@,%a;@,%a;@,%a"
206
            (*Declare the init predicate*)
207
            (pp_init_predicate typed_submachines) (m_spec_opt, m)
208
            (*Declare the transition predicate*)
209
            (pp_transition_predicate typed_submachines) (m_spec_opt, m)
210
            (*Declare the invariant predicate*)
211
            (pp_invariant_predicate typed_submachines) (m_spec_opt, m)
212
          )
213
        
214
        (*Print the private section*)
215
        pp_private_section
216
    in
217
    
218
    let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
219
    let pp_generics = List.map pp_poly_type polymorphic_types in
220
    
221
    fprintf fmt "@[<v>%a%t%a;@]@."
222
      
223
      (* Include all the subinstance package*)
224
      (Lustrec.Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
225
      (Lustrec.Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
226
      
227
      (*Begin the package*)
228
      (pp_package (pp_package_name m) pp_generics false) pp_content
229

  
230
end
backends/Ada/ada_backend_common.ml
1
open Format
2

  
3
open Lustrec.Machine_code_types
4
open Lustrec.Lustre_types
5
open Lustrec.Corelang
6
open Lustrec.Machine_code_common
7

  
8
open Ada_printer
9
open Misc_printer
10
open Misc_lustre_function
11

  
12
(** Exception for unsupported features in Ada backend **)
13
exception Ada_not_supported of string
14

  
15
(** Print the name of the state variable.
16
   @param fmt the formater to print on
17
**)
18
let pp_state_name fmt = fprintf fmt "state"
19
(** Print the type of the state variable.
20
   @param fmt the formater to print on
21
**)
22
let pp_state_type fmt = fprintf fmt "TState"
23
(** Print the name of the reset procedure
24
   @param fmt the formater to print on
25
**)
26
let pp_reset_procedure_name fmt = fprintf fmt "reset"
27
(** Print the name of the step procedure
28
   @param fmt the formater to print on
29
**)
30
let pp_step_procedure_name fmt = fprintf fmt "step"
31
(** Print the name of the main procedure.
32
   @param fmt the formater to print on
33
**)
34
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
35
(** Print the name of the arrow package.
36
   @param fmt the formater to print on
37
**)
38
let pp_arrow_package_name fmt = fprintf fmt "Lustrec.Arrow"
39
(** Print the type of a polymorphic type.
40
   @param fmt the formater to print on
41
   @param id the id of the polymorphic type
42
**)
43
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
44

  
45
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
46

  
47

  
48

  
49

  
50

  
51

  
52

  
53

  
54

  
55
(*TODO Check all this function with unit test, improve this system and
56
   add support for : "cbrt", "erf", "log10", "pow", "atan2".
57
*)
58
let ada_supported_funs =
59
  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));
60
   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));
61
   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));
62
   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));
63
   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));
64
   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));
65
   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));
66
   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));
67
   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));
68
   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));
69
   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));
70
   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));
71
   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));
72
   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
73
   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
74
   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
75
   
76
   ("ceil",  ("", "Float'Ceiling"));
77
   ("floor", ("", "Float'Floor"));
78
   ("fmod",  ("", "Float'Remainder"));
79
   ("round", ("", "Float'Rounding"));
80
   ("trunc", ("", "Float'Truncation"));
81

  
82
   ("fabs", ("", "abs"));]
83

  
84
let is_builtin_fun ident =
85
  List.mem ident Lustrec.Basic_library.internal_funs ||
86
    List.mem_assoc ident ada_supported_funs
87

  
88
(** Print the name of a package associated to a machine.
89
   @param fmt the formater to print on
90
   @param machine the machine
91
**)
92
let pp_package_name machine fmt =
93
  if is_arrow machine then
94
      fprintf fmt "%t" pp_arrow_package_name
95
  else
96
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
97

  
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff