Project

General

Profile

Revision 3769b712

View differences:

.gitignore
1 1
*~
2
/src/_build/
2
_build/
3 3
/setup.data
4 4
/setup.log
5 5
/src/version.ml
6
/src/verifierList.ml
6 7
/src/pluginList.ml
7 8
/myocamlbuild.ml
8 9
*.cmt
Makefile.in
13 13
DEFAULT_TEST_TARGET=COMPIL_LUS\|MAKE\|BIN\|DIFF
14 14
DEFAULT_EXCLUDE_TEST=LUSTRET
15 15

  
16
all: $(BIN_TARGETS)
17

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

  
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 16
configure: configure.ac
37 17
	@echo configure.ac has changed relaunching autoconf
38 18
	@autoconf
......
48 28
dot: doc
49 29
	@make -C src dot
50 30

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

  
54 32
dist-src-clean: clean
55 33
	@rm -f config.log config.status include/*.lusic include/lustrec_math.h include/simulink_math_fcn.h include/conv.h include/mpfr_lustre.h
configure.ac
2 2

  
3 3
AC_INIT([lustrec], 1.7-gitversion, [ploc@garoche.net])
4 4
AC_SUBST(VERSION_NUMBER, 1.7)
5
AC_SUBST(VERSION_CODENAME, "Xia/Huai-dev")
6 5

  
7 6
gitbranch=`git branch | grep \* | sed "s/\*[ ]*//"`
8 7
AC_SUBST(GITBRANCH, "$gitbranch")
......
14 13

  
15 14
# Next release will be
16 15
#AC_INIT([lustrec], [1.8], [ploc@garoche.net])
17
#AC_SUBST(VERSION_CODENAME, "Xia/Mang")
18 16
AC_MSG_NOTICE(Git branch: ${GITBRANCH})
19 17
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
20 18
AC_CONFIG_SRCDIR([src/main_lustre_testgen.ml])
21 19

  
22
AC_PATH_PROG([OCAMLC],[ocamlc],[:])
23
AC_MSG_CHECKING(OCaml version)
24
ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \  -f 1 | rev`
25
major=`echo $ocamlc_version | cut -d . -f 1`
26
minor=`echo $ocamlc_version | cut -d . -f 2`
27
if (test "$major" -lt 3 -a "$minor" -lt 11 ); then
28
  AC_MSG_ERROR([Ocaml version must be at least 3.11. You have version $ocamlc_version])
29
fi
30
AC_MSG_RESULT(valid ocaml version detected: $ocamlc_version)
31

  
32
AC_PATH_PROG([OCAMLBUILD],[ocamlbuild],[:])
33

  
34
# Handle a mismatch in available function btw 4.02 and 4.04
35
if (test $"$major" -eq 4 -a "$minor" -gt 2); then
36
   AC_SUBST(UPPERCASEFUN, "String.uppercase_ascii")
37
else
38
   AC_SUBST(UPPERCASEFUN, "String.uppercase")
39
fi
40

  
41 20
# default prefix is /usr/local
42 21
AC_PREFIX_DEFAULT(/usr/local)
43 22

  
44
dnl AC_ARG_WITH([ocamlgraph-path],
45
dnl         [AS_HELP_STRING([--ocamlgraph-path],
46
dnl               [specify the path of ocamlgraph library. graph.cmxa should be in ocamlgraph-path @<:@default=$(ocamlfind query ocamlgraph)@:>@])],
47
dnl         [AS_IF([test "x$ocamlgraph_path" = xno],
48
dnl                 [AC_MSG_ERROR([ocamlgraph library is needed])],
49
dnl                 [test "x$ocamlgraph_path" = xyes],
50
dnl                 [OCAMLGRAPH_PATH=$(ocamlfind query ocamlgraph)],
51
dnl                 [OCAMLGRAPH_PATH=$ocamlgraph_path]
52
dnl         )],
53
dnl         [OCAMLGRAPH_PATH=$(ocamlfind query ocamlgraph)]
54
dnl )
55
dnl AC_SUBST(OCAMLGRAPH_PATH)
56

  
57

  
58
# Checking libs
59
AC_CHECK_PROG(FINDLIB_CHECK,ocamlfind,yes)
60
if test x"$FINDLIB_CHECK" != x"yes" ; then
61
   AC_MSG_ERROR(ocamlfind required!)
62
fi
63
dnl AC_MSG_RESULT(Hourrah: ocamlfind found!)
64

  
65
# Checks for libraries.
66
# OCamlgraph
67
AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num)) 
68
AS_IF([ocamlfind query ocamlgraph cmdliner fmt logs num >/dev/null 2>&1],
69
    [],[AC_MSG_ERROR(A few ocaml library required. opam install ocamlgraph cmdliner fmt logs num should solve the issue)],
70
)
71
AC_MSG_RESULT(yes)
23
# Configuration
24
AC_MSG_NOTICE(******** Configuration ********)
25
AC_MSG_NOTICE(bin path:     $prefix/bin)
26
AC_MSG_NOTICE(include path: $prefix/include)
72 27

  
73
#Yojson
74
AC_MSG_CHECKING(yojson library (optional))
75
AS_IF([ocamlfind query yojson >/dev/null 2>&1],
76
    [yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_WARN(Yojson required for lustresf. opam install yojson should solve the issue)],
77
)
78 28

  
79
# Seal
80
AC_MSG_CHECKING(seal library (optional))
29
# Check seal library availability  
30
AC_MSG_CHECKING(if seal library is available)
81 31
AS_IF([ocamlfind query seal >/dev/null 2>&1],
82
    [seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
32
    [seal=yes; AC_MSG_RESULT([yes])],
33
    [seal=no; AC_MSG_RESULT([no])]
83 34
)
84
AS_IF([test "x$seal" = "xyes"], [
85
   AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);")
86
   AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)")
87
])
88 35

  
89
# Tiny
90
AC_MSG_CHECKING(tiny library (optional))
36
# Check tiny library availability  
37
AC_MSG_CHECKING([if tiny library is available]) 
91 38
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
92
    [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
39
    [tiny=yes; AC_MSG_RESULT([yes])],
40
    [tiny=no; AC_MSG_RESULT([no])],
93 41
)
94
AS_IF([test "x$tiny" = "xyes"], [
95
 dnl   AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)")
96
])
97 42

  
98
# z3 (optional)
99

  
100
AC_ARG_ENABLE(z3, [AS_HELP_STRING([--disable-z3],
101
              [disable Z3 dependencies. Enabled by default if available.])])
102

  
103
# option to rely on github version if installed
104
AC_ARG_WITH(z3_github, [AS_HELP_STRING([--with-z3-github],
105
              [Rely on Z3 as distributed by the official github
106
	       repo rather then the opam distribution. Disabled by default.])])
43
# Check z3 library availability
44
AC_MSG_CHECKING(if z3 library is available)
45
AS_IF([ocamlfind query z3 >/dev/null 2>&1],
46
    [z3=yes; AC_MSG_RESULT([yes])],
47
    [z3=no; AC_MSG_RESULT([no])]
48
)
107 49

  
108
AS_IF([test "x$with_z3_github" != "xyes"],
109
      [z3name=z3],
110
      [z3name=Z3]
111
      )
112
	
113
AC_MSG_CHECKING(z3 library)
50
# Seal plugin feature
114 51

  
52
AC_ARG_ENABLE(seal, 
53
  [AS_HELP_STRING([--disable-seal],[disable the seal plugin. Enabled by default if available.])
54
   AS_HELP_STRING([--enable-seal],[enable the seal plugin. Enabled if available by default.])])
115 55

  
116
#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
117
#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n']))
118 56

  
119
AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
120
    [z3=yes; AC_MSG_RESULT([yes])],[zustre=no; AC_MSG_RESULT(no)],
57
AS_IF([test "x$enable_seal" != "xno"],
58
  [
59
    if (test "x$seal" == "xyes" -a "x$z3" == "xyes"); then
60
      AC_MSG_RESULT([seal plugin : enabled])
61
      AC_SUBST(LUSTREV_SEAL, ["(module Seal_verifier.Verifier : Lustrec.VerifierType.S);"])
62
    else
63
      AC_MSG_RESULT([seal plugin : disabled (seal library or z3 package is not available)])
64
      if (test "x$enable_seal" == "xyes" ); then
65
        AC_MSG_ERROR([Cannot enable the seal plugin!])
66
      fi
67
    fi
68
  ], 
69
  [AC_MSG_RESULT([seal plugin disabled (you explicitely disabled it)])]
121 70
)
122 71

  
123
AS_IF([test "x$enable_z3" != "xno"], [
124
  if (test "x$z3" = xyes ); then
125
   AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
126
   AC_SUBST(LUSTREV_Z3_TAG, "<**/*verifier.native> or <tools/zustre/*.ml> or <tools/zustre/*.mli> or <tools/seal/seal_extract.ml> or <tools/seal/seal_extract.mli>: package($z3name)")
127
   AS_IF([test "x$z3name" = "xZ3"],
128
   	       [define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
129
	        AC_SUBST(Z3LIBPATH, "Z3path")],
130
 	       [define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
131
	        AC_SUBST(Z3LIBPATH, "z3path")]
132
		)
133
  fi	
134
])
135

  
72
# Zustre plugin feature
73
AC_ARG_ENABLE(zustre, 
74
  [AS_HELP_STRING([--disable-zustre],[disable the Zustre plugin. Enabled by default if available.])
75
   AS_HELP_STRING([--enable-zustre],[enable the Zustre plugin. Enabled if available by default.])])
76

  
77
AS_IF([test "x$enable_zustre" != "xno"],
78
  [
79
    if (test "x$z3" == "xyes" ); then
80
      AC_MSG_RESULT([zustre plugin : enabled])
81
      AC_SUBST(LUSTREV_ZUSTRE, ["(module Zustre_for_lustrev.Zustre_verifier.Verifier : Lustrec.VerifierType.S);"])
82
      AC_SUBST(LUSTREV_Z3_TAG, ["<**/*verifier.native> or <tools/zustre/*.ml> or <tools/zustre/*.mli> or <tools/seal/seal_extract.ml> or <tools/seal/seal_extract.mli>: package($z3name)"])
83
      define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
84
      AC_SUBST(Z3LIBPATH, "z3path")
85
    else
86
      AC_MSG_RESULT([zustre plugin : disabled (z3 is not available)])
87
      if (test "x$enable_zustre" == "xyes" ); then
88
        AC_MSG_ERROR([Cannot enable the zustre plugin!])
89
      fi
90
    fi
91
  ], 
92
  [AC_MSG_RESULT([zustre plugin disabled (you explicitely disabled it)])]
93
)
136 94

  
137
dnl # Tiny
138
dnl AC_MSG_CHECKING(tiny library (optional))
139
dnl AS_IF([ocamlfind query tiny >/dev/null 2>&1],
140
dnl     [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
141
dnl )
142
AS_IF([test "x$tiny" = "xyes"], [
143
   AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
144
   AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])
95
# Tiny plugin feature
96
AC_ARG_ENABLE(tiny, 
97
  [AS_HELP_STRING([--disable-tiny],[disable the Tiny plugin. Enabled by default if available.])
98
   AS_HELP_STRING([--enable-tiny],[enable the Tiny plugin. Enabled if available by default.])])
99

  
100
AS_IF([test "x$enable_tiny" != "xno"], [
101
  if (test "x$tiny" == "xyes" ); then
102
      AC_MSG_RESULT([tiny plugin : enabled])
103
      AC_SUBST(LUSTREV_TINY, ["(module Tiny_for_lustrev.Tiny_verifier.Verifier : Lustrec.VerifierType.S);"])
104
      AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])
105
    else
106
      AC_MSG_RESULT([tiny plugin : disabled (tiny library is not available)])
107
      if (test "x$enable_tiny" == "xyes" ); then
108
        AC_MSG_ERROR([Cannot enable the tiny plugin!])
109
      fi
110
    fi
145 111
])
146 112

  
147
# Salsa
148
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa],
149
              [disable Salsa plugin. Enabled by default if available.])])
150

  
151
AC_MSG_CHECKING(salsa library)
152
AS_IF([ocamlfind query salsa >/dev/null 2>&1],
153
    [salsa=yes; AC_MSG_RESULT(yes)],[salsa=no; AC_MSG_WARN(no)]
154
)
113
# Salsa plugin feature
114
AC_ARG_ENABLE(salsa, 
115
  [AS_HELP_STRING([--disable-salsa],[disable the salsa plugin. Enabled by default if available.])
116
   AS_HELP_STRING([--enable-salsa],[enable the salsa plugin. Enabled if available by default.])])
155 117

  
156 118

  
157 119
AS_IF([test "x$enable_salsa" != "xno"], [
158
  if (test "x$salsa" = xyes ); then
159
   AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
160
   AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)")
161
  fi
120
  if (test "x$salsa" == "xyes" ); then
121
      AC_MSG_RESULT([salsa plugin : enabled])
122
      AC_SUBST(SALSA, ["(module Salsa_plugin.Plugin : Lustrec.PluginType.S);"])
123
      AC_SUBST(SALSA_TAG, ["<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)"])
124
    else
125
      AC_MSG_RESULT([salsa plugin : disabled (salsa library is not available)])
126
      if (test "x$enable_salsa" == "xyes" ); then
127
        AC_MSG_ERROR([Cannot enable the salsa plugin!])
128
      fi
129
    fi
162 130
])
163 131

  
132

  
164 133
# GMP
165 134
AC_CHECK_LIB(gmp, __gmpz_init,
166 135
      [gmp=yes],
167 136
      [AC_MSG_RESULT([GNU MP not found])
168 137
      gmp=no])
169

  
138
#MPFR
170 139
AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
171 140
		   [AC_MSG_RESULT(
172 141
[MPFR not found])
173 142
mpfr=no])
174 143

  
175
# lustresf
176
AC_ARG_ENABLE(lustresf, [AS_HELP_STRING([--disable-lustresf],
177
              [disable lustresf compilation. Enabled by default.])])
178 144

  
179 145
AC_SUBST_FILE(lustresf)
180 146
AC_SUBST_FILE(lustresf_src)
181 147
lustresf=/dev/null
182 148
lustresf_src=/dev/null
183 149

  
184
AS_IF([test "x$enable_lustresf" != "xno"], [
185
  AC_MSG_CHECKING(yojson library for lustresf)
186
  AS_IF([ocamlfind query yojson >/dev/null 2>&1],
187
      [yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_ERROR(Yojson required for lustresf. opam install yojson should solve the issue)],
188
  )
189
  lustresf=Makefile-lustresf.in
190
  lustresf_src=src/Makefile-lustresf.in
191
  AC_SUBST(lustresf_target, "lustresf")
192
])
150

  
151
lustresf=Makefile-lustresf.in
152
lustresf_src=src/Makefile-lustresf.in
153
AC_SUBST(lustresf_target, "lustresf")
154

  
193 155

  
194 156
# Checking availability of path to regression tests
195 157
tests_path="../lustrec-tests/regression_tests"
......
235 197
# Instanciation
236 198
AC_CONFIG_FILES([opam
237 199
		 Makefile
238
		 src/Makefile
239
		 src/version.ml
240 200
		 src/pluginList.ml
241 201
		 src/verifierList.ml
242
		 src/_tags
243
		 src/ocaml_utils.ml
244 202
		 include/z3librc
245 203
		 share/FindLustre.cmake
246 204
		 ])
......
248 206
AC_OUTPUT
249 207

  
250 208

  
251
# summary
252
AC_MSG_NOTICE(******** Configuration ********)
253
AC_MSG_NOTICE(bin path:     $prefix/bin)
254
AC_MSG_NOTICE(include path: $prefix/include)
255
AC_MSG_NOTICE(********    Plugins    ********)
256

  
257
  if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
258
      AC_MSG_NOTICE([MPFR option enabled])
259
  else
260
      AC_MSG_WARN([MPFR option cannot be activated. Requires GMP and MPFR libs])
261
  fi
262

  
263
  if (test "x$salsa" = xyes -a "x$enable_salsa" != xno); then
264
      AC_MSG_NOTICE([Salsa plugin enabled])
265
  else
266
      AC_MSG_NOTICE([Salsa plugin disabled])
267
  fi
268

  
269
  if (test "x$z3" = xyes -a "x$enable_z3" != xno); then
270
      AC_MSG_NOTICE([Z3 dependencies enabled])
271
  else
272
      AC_MSG_NOTICE([Z3 dependencies disabled])
273
  fi
274

  
275
  if (test "x$yojson" = xyes -a "x$enable_lustresf" != "xno"); then
276
      AC_MSG_NOTICE([lustresf available])
277
  else
278
      if (test "x$enable_lustresf" = "xno"); then
279
        AC_MSG_NOTICE([lustresf not available (you explicitely disabled it)])
280
      else
281
        AC_MSG_NOTICE([lustresf not available])
282
      fi
283
  fi
284
AC_MSG_NOTICE(********   Verifiers    ********)
285

  
286
  if (test "x$z3" = xyes  -a "x$enable_z3" != xno); then
287
      AC_MSG_NOTICE([Zustre enabled])
288
      AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH (DYLD_LIBRARY_PATH in OSX).)
289
      dnl AC_MSG_WARN(It is currently located in "z3path")
290
      AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc")
291
      AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc)
292
else
293
      AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])
294
  fi
295

  
296
if (test "x$seal" = "xyes" -a "x$z3" = xyes  -a "x$enable_z3" != xno); then
297
      AC_MSG_NOTICE([Seal   enabled])
298
  else
299
      AC_MSG_NOTICE([Seal   disabled. Require Z3 library])
300
  fi
301

  
302 209

  
303
  if (test "x$tiny" = xyes); then
304
      AC_MSG_NOTICE([Tiny   enabled])
305
  else
306
      AC_MSG_NOTICE([Tiny   disabled. Require Tiny library])
307
  fi
308 210

  
309 211
AC_MSG_NOTICE(****** Regression Tests  ******)
310 212
if (test "x$valid_test_path" = xfalse); then
src/.merlin
1
REC
1
EXCLUDE_QUERY_DIR
2
B /home/corentin/.opam/default/lib/apron
3
B /home/corentin/.opam/default/lib/base
4
B /home/corentin/.opam/default/lib/base/base_internalhash_types
5
B /home/corentin/.opam/default/lib/base/caml
6
B /home/corentin/.opam/default/lib/base/shadow_stdlib
7
B /home/corentin/.opam/default/lib/biniou
8
B /home/corentin/.opam/default/lib/dune-build-info
9
B /home/corentin/.opam/default/lib/easy-format
10
B /home/corentin/.opam/default/lib/gmp
11
B /home/corentin/.opam/default/lib/jane-street-headers
12
B /home/corentin/.opam/default/lib/mlmpfr
13
B /home/corentin/.opam/default/lib/num
14
B /home/corentin/.opam/default/lib/ocamlgraph
15
B /home/corentin/.opam/default/lib/ppx_compare/runtime-lib
16
B /home/corentin/.opam/default/lib/ppx_enumerate/runtime-lib
17
B /home/corentin/.opam/default/lib/ppx_hash/runtime-lib
18
B /home/corentin/.opam/default/lib/ppx_inline_test/config
19
B /home/corentin/.opam/default/lib/ppx_inline_test/runtime-lib
20
B /home/corentin/.opam/default/lib/ppx_sexp_conv/runtime-lib
21
B /home/corentin/.opam/default/lib/sexplib0
22
B /home/corentin/.opam/default/lib/time_now
23
B /home/corentin/.opam/default/lib/tiny
24
B /home/corentin/.opam/default/lib/yojson
25
B /home/corentin/.opam/default/lib/z3
26
B /home/corentin/.opam/default/lib/zarith
27
B /usr/lib/ocaml
28
B ../_build/default/backends/.backends.objs/byte
29
B ../_build/default/core/.lustrec.objs/byte
30
B ../_build/default/plugins/mpfr/.lustrec_mpfr.objs/byte
31
B ../_build/default/plugins/scopes/.scopes.objs/byte
32
B ../_build/default/plugins/tiny/.tiny_for_lustrev.objs/byte
33
B ../_build/default/plugins/zustre/.zustre_for_lustrev.objs/byte
34
B ../_build/default/src/.main_lustre_compiler.eobjs/byte
35
S /home/corentin/.opam/default/lib/apron
36
S /home/corentin/.opam/default/lib/base
37
S /home/corentin/.opam/default/lib/base/base_internalhash_types
38
S /home/corentin/.opam/default/lib/base/caml
39
S /home/corentin/.opam/default/lib/base/shadow_stdlib
40
S /home/corentin/.opam/default/lib/biniou
41
S /home/corentin/.opam/default/lib/dune-build-info
42
S /home/corentin/.opam/default/lib/easy-format
43
S /home/corentin/.opam/default/lib/gmp
44
S /home/corentin/.opam/default/lib/jane-street-headers
45
S /home/corentin/.opam/default/lib/mlmpfr
46
S /home/corentin/.opam/default/lib/num
47
S /home/corentin/.opam/default/lib/ocamlgraph
48
S /home/corentin/.opam/default/lib/ppx_compare/runtime-lib
49
S /home/corentin/.opam/default/lib/ppx_enumerate/runtime-lib
50
S /home/corentin/.opam/default/lib/ppx_hash/runtime-lib
51
S /home/corentin/.opam/default/lib/ppx_inline_test/config
52
S /home/corentin/.opam/default/lib/ppx_inline_test/runtime-lib
53
S /home/corentin/.opam/default/lib/ppx_sexp_conv/runtime-lib
54
S /home/corentin/.opam/default/lib/sexplib0
55
S /home/corentin/.opam/default/lib/time_now
56
S /home/corentin/.opam/default/lib/tiny
57
S /home/corentin/.opam/default/lib/yojson
58
S /home/corentin/.opam/default/lib/z3
59
S /home/corentin/.opam/default/lib/zarith
60
S /usr/lib/ocaml
61
S ../backends/Ada
62
S ../backends/C
63
S ../backends/EMF
64
S ../backends/Horn
65
S ../backends/VHDL
66
S ../core
67
S ../core/checks
68
S ../core/features/machine_types
69
S ../core/parsers
70
S ../core/utils
71
S ../plugins/mpfr
72
S ../plugins/scopes
73
S ../plugins/tiny
74
S ../plugins/zustre
75
S .
76
S backends
77
S backends/C
78
S tools
79
S tools/importer
80
S tools/stateflow
81
S tools/stateflow/common
82
S tools/stateflow/json-parser
83
S tools/stateflow/models
84
S tools/stateflow/semantics
85
FLG -ppx '/home/corentin/n7/2A/stage/lustrec-seal/_build/default/.ppx/bfcab61e6a21ecf6d2f80029fc1ef484/ppx.exe --as-ppx --cookie '\''inline_tests="enabled"'\'''
86
FLG -open Dune__exe -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -warn-error -A -w -warn-error
src/Makefile-lustresf.in
1
lustresf:
2
	@echo Compiling binary lustresf
3
	@$(OCAMLBUILD) tools/stateflow/sf_sem.native
4
	@mkdir -p $(LOCAL_BINDIR)
5
	@mv _build/tools/stateflow/sf_sem.native $(LOCAL_BINDIR)/lustresf
6

  
7
json-parser:
8
	@echo Compiling binary json-parser-ex
9
	@$(OCAMLBUILD) tools/stateflow/json-parser/main_parse_json_file.native
10
	@mkdir -p $(LOCAL_BINDIR)
11
	@mv _build/tools/stateflow/json-parser/main_parse_json_file.native $(LOCAL_BINDIR)/json-parser
12

  
13
tests:	test-simple-var
14

  
15
test-simple-var:
16
	@echo Compiling simple tests for JSON parser -- tests on variables
17
	@$(OCAMLBUILD) tools/stateflow/json-parser/test_json_parser_variables.native
18
	@echo Lauching simple tests for JSON parser -- tests on variables
19
	./_build/tools/stateflow/json-parser/test_json_parser_variables.native
src/Makefile.in
1
OCAMLBUILD=@OCAMLBUILD@ -use-ocamlfind -no-links
2

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

  
9
LUSI_LIBS=include/math.lusi include/conv.lusi
10
LOCAL_BINDIR=../bin
11
LOCAL_DOCDIR=../doc/manual
12

  
13
all: lustrec lustret lustrev
14

  
15
lustrec:
16
	@echo Compiling binary lustrec
17
	@$(OCAMLBUILD) main_lustre_compiler.native
18
	@mkdir -p $(LOCAL_BINDIR)
19
	@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
20

  
21
lustret:
22
	@echo Compiling binary lustret
23
	@$(OCAMLBUILD) main_lustre_testgen.native
24
	@mkdir -p $(LOCAL_BINDIR)
25
	@mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
26

  
27
lustrev:
28
	@echo Compiling binary lustrev
29
	@$(OCAMLBUILD) main_lustre_verifier.native
30
	@mkdir -p $(LOCAL_BINDIR)
31
	@mv _build/main_lustre_verifier.native $(LOCAL_BINDIR)/lustrev
32

  
33
lustrei:
34
	@echo Compiling binary lustrei
35
	@$(OCAMLBUILD) tools/importer/main_lustre_importer.native
36
	@mkdir -p $(LOCAL_BINDIR)
37
	@mv _build/tools/importer/main_lustre_importer.native $(LOCAL_BINDIR)/lustrei
38

  
39
@lustresf_src@
40

  
41
doc:
42
	@echo Generating doc
43
	@$(OCAMLBUILD) lustrec.docdir/index.html
44
	@rm -rf $(LOCAL_DOCDIR)
45
	@cp -rf _build/lustrec.docdir $(LOCAL_DOCDIR)
46

  
47
dot: doc
48
	$(OCAMLBUILD) lustrec.docdir/lustrec.dot
49
	dot -T svg -o $(LOCAL_DOCDIR)/lustrec.svg _build/lustrec.docdir/lustrec.dot
50

  
51
clean:
52
	$(OCAMLBUILD) -clean
53

  
54
dist-clean: clean
55
	rm -f Makefile myocamlbuild.ml config.log config.status configure
56
	rm -f include/*.lusic include/math.h include/conv.h
57

  
58
install:
59
	make -C .. install
60

  
61
.PHONY: compile-lusi doc dot lustrec lustret lustrev lustrec.odocl clean install dist-clean tests
src/_tags.in
1
# general config
2
true: bin_annot, color(always)
3
# true: use_menhir
4

  
5
# paths to sources
6
"utils": include
7
"checks": include
8
"parsers": include
9
"backends": include
10
"backends/Ada": include
11
"backends/C": include
12
"backends/Horn": include
13
"backends/EMF": include
14
"backends/VHDL": include
15
"plugins/salsa": include
16
"plugins/scopes": include
17
"plugins/mpfr": include
18
"features/machine_types": include
19
"tools": include
20
"tools/zustre": include
21
"tools/stateflow": include
22
"tools/stateflow/common": include
23
"tools/stateflow/semantics": include
24
"tools/stateflow/models": include
25
"tools/stateflow/json-parser": include
26
"tools/importer": include
27
"tools/seal": include
28
"tools/tiny": include
29

  
30
# svn
31
<**/.svn>: -traverse
32
<**/.svn>: not_hygienic
33

  
34
# packages
35
<**/*.native> or <**/*.ml{,i}>         : package(num)
36
<**/*.native> or <**/*.ml{,i}>         : package(ocamlgraph)
37
<**/*verifier.native> or <**/*.ml{,i}> : package(yojson)
38

  
39
<**/*.native>                   : use_str
40
<**/main_lustre_compiler.native>: package(unix)
41
<**/main_lustre_testgen.native> : package(unix)
42
<**/main_lustre_verifier.native> : package(unix)
43
<**/sf_sem.native>              : package(unix)
44
<**/*>                          : package(num)
45
<**/*>                          : package(zarith)
46
<**/*.ml>                       : package(logs)
47
<**/*.native>                   : package(logs)
48
<**/json_parser.ml>             : package(yojson)
49
<**/main_parse_json_file.*>     : package(cmdliner)
50
<**/main_parse_json_file.*>     : package(fmt.tty)
51
<**/main_parse_json_file.*>     : package(fmt.cli)
52
<**/main_parse_json_file.*>     : package(logs.fmt)
53
<**/main_parse_json_file.*>     : package(logs.cli)
54
<**/main_parse_json_file.*>     : package(yojson)
55
<**/test_*.*>                   : package(oUnit)
56
<**/test_json*.*>               : package(yojson)
57

  
58
# Required for ocamldoc. Otherwise failed to build
59
<**/*.ml{,i}>: package(ocamlgraph)
60
<**/*.ml{,i}>: package(num)
61

  
62
# Plugin dependencies
63
@SALSA_TAG@
64

  
65
# Available solvers
66
@LUSTREV_SEAL_TAG@
67
@LUSTREV_TINY_TAG@
68
@LUSTREV_Z3_TAG@
69

  
70
# Local Variables:
71
# mode: conf
72
# End:
src/annotations.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
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 Lustre_types
13

  
14

  
15
(* Associate to each annotation key the pair (node, expr tag) *)
16
let expr_annotations : (string list, ident * tag) Hashtbl.t=  Hashtbl.create 13
17
let node_annotations : (string list, ident) Hashtbl.t=  Hashtbl.create 13
18

  
19
let add_expr_ann node_id expr_tag key = Hashtbl.add expr_annotations key (node_id, expr_tag)
20
let add_node_ann node_id key = Hashtbl.add node_annotations key node_id
21

  
22
let get_expr_annotations key = Hashtbl.find_all expr_annotations key
src/arrow.ml
1
open Lustre_types
2

  
3
let arrow_id = "_arrow"
4

  
5
let arrow_typ = Types.new_ty Types.Tunivar
6

  
7
let arrow_desc =
8
  {
9
    node_id = arrow_id;
10
    node_type = Type_predef.type_bin_poly_op;
11
    node_clock = Clock_predef.ck_bin_univ;
12
    node_inputs= [Corelang.dummy_var_decl "_in1" arrow_typ; Corelang.dummy_var_decl "_in2" arrow_typ];
13
    node_outputs= [Corelang.dummy_var_decl "_out" arrow_typ];
14
    node_locals= [];
15
    node_gencalls = [];
16
    node_checks = [];
17
    node_asserts = [];
18
    node_stmts= [];
19
    node_dec_stateless = false;
20
    node_stateless = Some false;
21
    node_spec = None;
22
    node_annot = [];
23
    node_iscontract = false;
24
}
25

  
26
let arrow_top_decl =
27
  {
28
    top_decl_desc = Node arrow_desc;
29
    top_decl_owner = (Options_management.core_dependency "arrow");
30
    top_decl_itf = false;
31
    top_decl_loc = Location.dummy_loc
32
  }
src/arrow.mli
1
val arrow_id: string
2
val arrow_top_decl: Lustre_types.top_decl
3
val arrow_desc: Lustre_types.node_desc
src/automata.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
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 Utils
13
open Lustre_types
14
open Corelang
15

  
16

  
17
type aut_state =
18
    {
19
      incoming_r' : var_decl;
20
      incoming_s' : var_decl;
21
      incoming_r : var_decl;
22
      incoming_s : var_decl;
23
      actual_r : var_decl;
24
      actual_s : var_decl
25
    }
26

  
27
let as_clock var_decl =
28
  let tydec = var_decl.var_dec_type in
29
  { var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
30

  
31
let mkbool loc b =
32
 mkexpr loc (Expr_const (const_of_bool b))
33

  
34
let mkident loc id =
35
 mkexpr loc (Expr_ident id)
36

  
37
let mkconst loc id =
38
 mkexpr loc (Expr_const (Const_tag id))
39

  
40
let mkfby loc e1 e2 =
41
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
42

  
43
let mkpair loc e1 e2 =
44
 mkexpr loc (Expr_tuple [e1; e2])
45

  
46
let mkidentpair loc restart state =
47
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
48

  
49
let add_branch (loc, expr, restart, st) cont =
50
 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))
51

  
52
let mkhandler loc st unless until locals (stmts, asserts, annots) =
53
 {hand_state = st;
54
  hand_unless = unless;
55
  hand_until = until;
56
  hand_locals = locals;
57
  hand_stmts = stmts;
58
  hand_asserts = asserts;
59
  hand_annots = annots;
60
  hand_loc = loc}
61

  
62
let mkautomata loc id handlers =
63
  {aut_id = id;
64
   aut_handlers = handlers;
65
   aut_loc = loc}
66

  
67
let expr_of_exit loc restart state conds tag =
68
  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
69

  
70
let rec unless_read reads handler =
71
  let res =
72
  List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_unless
73
  in
74
(
75
(*
76
Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
77
Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
78
*)
79
res
80
)
81

  
82
let rec until_read reads handler =
83
  List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_until
84

  
85
let rec handler_read reads handler =
86
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
87
  let allvars =
88
    List.fold_left (fun read stmt ->
89
      match stmt with
90
      | Eq eq -> Utils.ISet.union read (get_expr_vars eq.eq_rhs)
91
      | Aut aut -> automata_read read aut) reads handler.hand_stmts
92
  in let res = ISet.diff allvars locals
93
     in
94
(
95
(*
96
Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements allvars);
97
Format.eprintf "handler_read %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
98
*)
99
res
100
)
101

  
102
and automata_read reads aut =
103
  List.fold_left (fun read handler -> until_read (handler_read (unless_read read handler) handler) handler) reads aut.aut_handlers
104

  
105
let rec handler_write writes handler =
106
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
107
  let allvars =
108
    List.fold_left (fun write stmt ->
109
      match stmt with
110
      | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
111
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
112
  in ISet.diff allvars locals
113

  
114
let node_vars_of_idents node iset =
115
  List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) []
116

  
117
let mkautomata_state nodeid used typedef loc id =
118
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
119
  let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
120
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
121
  let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in
122
  let incoming_s' = mk_new_name used (id ^ "__next_state_in") in
123
  let incoming_r = mk_new_name used (id ^ "__restart_in") in
124
  let incoming_s = mk_new_name used (id ^ "__state_in") in
125
  let actual_r = mk_new_name used (id ^ "__restart_act") in
126
  let actual_s = mk_new_name used (id ^ "__state_act") in
127
  {
128
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
129
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
130
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
131
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
132
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false, None, Some nodeid);
133
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid)
134
  }
135

  
136
let vars_of_aut_state aut_state =
137
  [aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s]
138

  
139
let node_of_unless nused used node aut_id aut_state handler =
140
(*Format.eprintf "node_of_unless %s@." node.node_id;*)
141
  let inputs = unless_read ISet.empty handler in
142
  let var_inputs = aut_state.incoming_r (*:: aut_state.incoming_s*) :: (node_vars_of_idents node inputs) in
143
  let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in
144
  let init_expr = mkpair handler.hand_loc (mkident handler.hand_loc aut_state.incoming_r.var_id) (mkconst handler.hand_loc handler.hand_state) in
145
(*  let init_expr = mkidentpair handler.hand_loc aut_state.incoming_r.var_id aut_state.incoming_s.var_id in *)
146
  let expr_outputs = List.fold_right add_branch handler.hand_unless init_expr in
147
  let eq_outputs = Eq (mkeq handler.hand_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], expr_outputs)) in
148
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state) in
149
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.incoming_s.var_id, handler.hand_state))) var_inputs in
150
  let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in
151
  {
152
    node_id = node_id;
153
    node_type = Types.new_var ();
154
    node_clock = Clocks.new_var true;
155
    node_inputs = List.map copy_var_decl var_inputs;
156
    node_outputs = List.map copy_var_decl var_outputs;
157
    node_locals = [];
158
    node_gencalls = [];
159
    node_checks = [];
160
    node_asserts = []; 
161
    node_stmts = [ eq_outputs ];
162
    node_dec_stateless = false;
163
    node_stateless = None;
164
    node_spec = None;
165
    node_annot = [];
166
    node_iscontract = false;
167
  },
168
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
169

  
170

  
171
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
172

  
173
let rec rename_stmts_outputs frename stmts =
174
  match stmts with
175
  | []           -> []
176
  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
177
		      eq' :: rename_stmts_outputs frename q
178
  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in
179
                      let aut' = Aut { aut with aut_handlers = handlers' } in
180
		      aut' :: rename_stmts_outputs frename q
181

  
182
let mk_frename used outputs =
183
  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in
184
  (fun name -> try IMap.find name table with Not_found -> name)
185

  
186
let node_of_assign_until nused used node aut_id aut_state handler =
187
(*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
188
  let writes = handler_write ISet.empty handler in
189
  let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in
190
  let frename = mk_frename used writes in
191
  let var_inputs = aut_state.actual_r (*:: aut_state.actual_s*) :: node_vars_of_idents node inputs in
192
  let new_var_locals = node_vars_of_idents node writes in
193
  let var_outputs = List.sort IdentModule.compare (node_vars_of_idents node writes) in
194
  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
195
  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
196
  let init_until = mkpair handler.hand_loc (mkconst handler.hand_loc tag_false) (mkconst handler.hand_loc handler.hand_state) in
197
  let until_expr = List.fold_right add_branch handler.hand_until init_until in
198
  let until_eq = Eq (mkeq handler.hand_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], until_expr)) in
199
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state) in
200
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.actual_s.var_id, handler.hand_state))) var_inputs in
201
  let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in
202
  List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs,
203
  {
204
    node_id = node_id;
205
    node_type = Types.new_var ();
206
    node_clock = Clocks.new_var true;
207
    node_inputs = List.map copy_var_decl var_inputs;
208
    node_outputs = List.map copy_var_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
209
    node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
210
    node_gencalls = [];
211
    node_checks = [];
212
    node_asserts = handler.hand_asserts; 
213
    node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
214
    node_dec_stateless = false;
215
    node_stateless = None;
216
    node_spec = None;
217
    node_annot = handler.hand_annots;
218
    node_iscontract = false;
219
  },
220
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
221

  
222
let typedef_of_automata aut =
223
  let tname = Format.sprintf "%s__type" aut.aut_id in
224
  { tydef_id = tname;
225
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
226
  }
227

  
228
let expand_automata nused used owner typedef node aut =
229
  let initial = (List.hd aut.aut_handlers).hand_state in
230
  let aut_state = mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id in
231
  let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in
232
  let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in
233
  let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in
234
  let unless_handlers = List.map2 (fun h (n, c) -> (h.hand_state, c)) aut.aut_handlers unodes in
235
  let unless_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.incoming_s.var_id, unless_handlers)) in
236
  let unless_eq = mkeq aut.aut_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], unless_expr) in
237
  let assign_until_handlers = List.map2 (fun h (_, n, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in
238
  let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in
239
  let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in
240
  let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in
241
  let fby_incoming_expr = mkfby aut.aut_loc (mkpair aut.aut_loc (mkconst aut.aut_loc tag_false) (mkconst aut.aut_loc initial)) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
242
  let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in
243
  let locals' = vars_of_aut_state aut_state in
244
  let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in
245
  (  List.map2 (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers unodes
246
   @ List.map2 (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers aunodes,
247
  locals',
248
  eqs')
249

  
250
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt =
251
  match stmt with
252
  | Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs)
253
  | Aut aut ->
254
    let typedef = typedef_of_automata aut in
255
    let used' name = used name || List.exists (fun v -> v.var_id = name) locals in
256
    let nused' name =
257
      nused name ||
258
      List.exists (fun t -> match t.top_decl_desc with
259
      | ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name
260
      | _ -> false) top_nodes in
261
    let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in
262
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
263
    (top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
264

  
265
let expand_node_stmts nused used loc owner node =
266
  let (top_types', top_nodes', locals', eqs') =
267
    List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
268
  let node' = 
269
    { node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
270
  let top_node = mktop_decl loc owner false (Node node') in
271
  top_types', top_node, top_nodes'
272

  
273
let rec expand_decls_rec nused top_decls =
274
  match top_decls with
275
  | [] -> []
276
  | top_decl::q ->
277
    match top_decl.top_decl_desc with
278
    | Node nd ->
279
      let used name =
280
	   List.exists (fun v -> v.var_id = name) nd.node_inputs
281
	|| List.exists (fun v -> v.var_id = name) nd.node_outputs
282
	|| List.exists (fun v -> v.var_id = name) nd.node_locals in
283
      let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
284
      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
285
    | _       -> top_decl :: expand_decls_rec nused q
286

  
287
let expand_decls top_decls =
288
  let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
289
    | Node nd         -> ISet.add nd.node_id names
290
    | ImportedNode nd -> ISet.add nd.nodei_id names
291
    | _               -> names) ISet.empty top_decls in
292
  let nused name = ISet.mem name top_names in
293
  expand_decls_rec nused top_decls
294

  
295
(* Local Variables: *)
296
(* compile-command:"make -C .." *)
297
(* End: *)
298

  
src/backends/.merlin
1
REC
1
EXCLUDE_QUERY_DIR
2
B /home/corentin/.opam/default/lib/dune-build-info
3
B /home/corentin/.opam/default/lib/mlmpfr
4
B /home/corentin/.opam/default/lib/num
5
B /home/corentin/.opam/default/lib/ocamlgraph
6
B /home/corentin/.opam/default/lib/zarith
7
B /usr/lib/ocaml
8
B ../_build/default/backends/.backends.objs/byte
9
B ../_build/default/core/.lustrec.objs/byte
10
B ../_build/default/plugins/mpfr/.lustrec_mpfr.objs/byte
11
S /home/corentin/.opam/default/lib/dune-build-info
12
S /home/corentin/.opam/default/lib/mlmpfr
13
S /home/corentin/.opam/default/lib/num
14
S /home/corentin/.opam/default/lib/ocamlgraph
15
S /home/corentin/.opam/default/lib/zarith
16
S /usr/lib/ocaml
17
S .
18
S Ada
19
S C
20
S EMF
21
S Horn
22
S Java
23
S VHDL
24
S ../core
25
S ../core/checks
26
S ../core/features/machine_types
27
S ../core/parsers
28
S ../core/utils
29
S ../plugins/mpfr
30
FLG -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -warn-error -A
src/backends/Ada/.merlin
1
REC
src/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 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

  
src/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 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
  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.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 !Options.main_node with
153
  | "" -> None
154
  | main_node -> (
155
    match Machine_code_common.get_machine_opt filtered_machines main_node with
156
    | None -> begin
157
      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
158
      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
159
    end
160
    | Some m -> Some m
161
  )) in
162

  
163
  let destname = !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: *)
src/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 Machine_code_types
15
open Lustre_types
16
open Corelang
17
open 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: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" (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
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff