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
|
open Options
|
12
|
|
13
|
let print_version () =
|
14
|
let open Utils.Format in
|
15
|
printf
|
16
|
"@[<v>Lustrec compiler, version %s (%s)@,\
|
17
|
Standard lib: %s@,\
|
18
|
User provided include directory: @[<h>%a@]@]@." version codename
|
19
|
Version.include_path
|
20
|
(pp_print_list ~pp_sep:pp_print_space pp_print_string)
|
21
|
!include_dirs
|
22
|
|
23
|
let add_include_dir dir =
|
24
|
let removed_slash_suffix =
|
25
|
let len = String.length dir in
|
26
|
if dir.[len - 1] = '/' then String.sub dir 0 (len - 1) else dir
|
27
|
in
|
28
|
include_dirs := removed_slash_suffix :: !include_dirs
|
29
|
|
30
|
(** Solving the path of required library: If local: look in the folders
|
31
|
described in !Options.include_dirs If non local: look first as a local, then
|
32
|
in Version.include_path: ie. in Version.include_path::!Options.include_dirs
|
33
|
Note that in options.ml, include folder are added as heads. One need to
|
34
|
perform a fold_right to respect the order *)
|
35
|
let search_lib_path (local, full_file_name) =
|
36
|
let paths =
|
37
|
if local then !include_dirs else Version.include_path :: !include_dirs
|
38
|
in
|
39
|
let name =
|
40
|
List.fold_right
|
41
|
(fun dir res ->
|
42
|
match res with
|
43
|
| Some _ ->
|
44
|
res
|
45
|
| None ->
|
46
|
let path_to_lib = dir ^ "/" ^ full_file_name in
|
47
|
if Sys.file_exists path_to_lib then Some dir else None)
|
48
|
paths None
|
49
|
in
|
50
|
match name with
|
51
|
| None ->
|
52
|
Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name
|
53
|
(Utils.fprintf_list ~sep:", " Format.pp_print_string)
|
54
|
paths;
|
55
|
raise Not_found
|
56
|
| Some s ->
|
57
|
s
|
58
|
|
59
|
(* Search for path of core libs (without lusic: arrow and io_frontend *)
|
60
|
let core_dependency lib_name = search_lib_path (false, lib_name ^ ".h")
|
61
|
|
62
|
let name_dependency (_, dep) ext =
|
63
|
let dir = search_lib_path (false, dep ^ ext) in
|
64
|
dir ^ "/" ^ dep
|
65
|
|
66
|
let set_mpfr prec =
|
67
|
if prec > 0 then (
|
68
|
mpfr := true;
|
69
|
mpfr_prec := prec;
|
70
|
real_type := "mpfr"
|
71
|
(* salsa_enabled := false; (* We deactivate salsa *) TODO *))
|
72
|
else failwith "mpfr requires a positive integer"
|
73
|
|
74
|
let set_real_type s =
|
75
|
match s with
|
76
|
| "mpfr" ->
|
77
|
mpfr := true;
|
78
|
real_type := "mpfr"
|
79
|
| _ ->
|
80
|
real_type := s
|
81
|
|
82
|
let setup () = Backends.setup ()
|
83
|
|
84
|
let set_backend s = output := s
|
85
|
|
86
|
let common_options =
|
87
|
[
|
88
|
( "-d",
|
89
|
Arg.Set_string dest_dir,
|
90
|
"uses the specified \x1b[4mdirectory\x1b[0m as root for \
|
91
|
generated/imported object and C files <default: .>" );
|
92
|
"-I", Arg.String add_include_dir, "sets include \x1b[4mdirectory\x1b[0m";
|
93
|
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
|
94
|
"-print-types", Arg.Set print_types, "prints node types";
|
95
|
"-print-clocks", Arg.Set print_clocks, "prints node clocks";
|
96
|
"-print-nodes", Arg.Set print_nodes, "prints node list";
|
97
|
"-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
|
98
|
( "-algebraic-loop-max",
|
99
|
Arg.Set_int al_nb_max,
|
100
|
"try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>" );
|
101
|
"-kind2", Arg.Set kind2_print, "active kind2 output";
|
102
|
( "-verbose",
|
103
|
Arg.Set_int verbose_level,
|
104
|
"changes verbose \x1b[4mlevel\x1b[0m <default: 1>" );
|
105
|
"-version", Arg.Unit print_version, " displays the version";
|
106
|
]
|
107
|
|
108
|
let lustrec_options =
|
109
|
common_options
|
110
|
@ [
|
111
|
( "-init",
|
112
|
Arg.Set delay_calculus,
|
113
|
"performs an initialisation analysis for Lustre nodes <default: no \
|
114
|
analysis>" );
|
115
|
( "-dynamic",
|
116
|
Arg.Clear static_mem,
|
117
|
"specifies a dynamic allocation scheme for main Lustre node <default: \
|
118
|
static>" );
|
119
|
( "-check-access",
|
120
|
Arg.Set check,
|
121
|
"checks at runtime that array accesses always lie within bounds \
|
122
|
<default: no check>" );
|
123
|
( "-mpfr",
|
124
|
Arg.Int set_mpfr,
|
125
|
"replaces FP numbers by the MPFR library multiple precision numbers \
|
126
|
with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP \
|
127
|
numbers>" );
|
128
|
( "-lusi",
|
129
|
Arg.Set lusi,
|
130
|
"only generates a .lusi interface source file from a Lustre source \
|
131
|
<default: no generation>" );
|
132
|
( "-no-spec",
|
133
|
Arg.Unit (fun () -> spec := "no"),
|
134
|
"do not generate any specification" );
|
135
|
( "-acsl-spec",
|
136
|
Arg.Unit (fun () -> spec := "acsl"),
|
137
|
"generates an ACSL encoding of the specification. Only meaningful for \
|
138
|
the C backend <default>" );
|
139
|
( "-c-spec",
|
140
|
Arg.Unit (fun () -> spec := "c"),
|
141
|
"generates a C encoding of the specification instead of ACSL contracts \
|
142
|
and annotations. Only meaningful for the C backend" );
|
143
|
(* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output
|
144
|
instead of C"; *)
|
145
|
( "-ada",
|
146
|
Arg.Unit (fun () -> set_backend "Ada"),
|
147
|
"generates Ada encoding output instead of C" );
|
148
|
( "-horn",
|
149
|
Arg.Unit (fun () -> set_backend "horn"),
|
150
|
"generates Horn clauses encoding output instead of C" );
|
151
|
( "-horn-traces",
|
152
|
Arg.Unit
|
153
|
(fun () ->
|
154
|
set_backend "horn";
|
155
|
traces := true),
|
156
|
"produce traceability file for Horn backend. Enable the horn backend." );
|
157
|
( "-horn-cex",
|
158
|
Arg.Unit
|
159
|
(fun () ->
|
160
|
set_backend "horn";
|
161
|
horn_cex := true),
|
162
|
"generate cex enumeration. Enable the horn backend (work in progress)" );
|
163
|
( "-horn-query",
|
164
|
Arg.Unit
|
165
|
(fun () ->
|
166
|
set_backend "horn";
|
167
|
horn_query := true),
|
168
|
"generate queries in generated Horn file. Enable the horn backend \
|
169
|
(work in progress)" );
|
170
|
( "-horn-sfunction",
|
171
|
Arg.Set_string sfunction,
|
172
|
"Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m" );
|
173
|
"-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
|
174
|
( "-lustre",
|
175
|
Arg.Unit (fun () -> output := "lustre"),
|
176
|
"generates Lustre output, performing all active optimizations" );
|
177
|
( "-emf",
|
178
|
Arg.Unit (fun () -> set_backend "emf"),
|
179
|
"generates EMF output, to be used by CocoSim" );
|
180
|
( "-inline",
|
181
|
Arg.Unit
|
182
|
(fun () ->
|
183
|
global_inline := true;
|
184
|
const_unfold := true),
|
185
|
"inlines all node calls (require a main node). Implies constant \
|
186
|
unfolding" );
|
187
|
( "-witnesses",
|
188
|
Arg.Set witnesses,
|
189
|
"enables production of witnesses during compilation" );
|
190
|
( "-O",
|
191
|
Arg.Set_int optimization,
|
192
|
"changes optimization \x1b[4mlevel\x1b[0m <default: 2>" );
|
193
|
"-c++", Arg.Set cpp, "c++ backend";
|
194
|
( "-int",
|
195
|
Arg.Set_string int_type,
|
196
|
"specifies the integer type (default=\"int\")" );
|
197
|
( "-real",
|
198
|
Arg.String set_real_type,
|
199
|
"specifies the real type (default=\"double\" without mpfr option)" );
|
200
|
( "-real-print-prec",
|
201
|
Arg.Set_int print_prec_double,
|
202
|
"specifies the number of digits to be printed for real values \
|
203
|
(default=15)" );
|
204
|
( "-int_div_euclidean",
|
205
|
Arg.Set integer_div_euclidean,
|
206
|
"interprets integer division as Euclidean (default : C division \
|
207
|
semantics)" );
|
208
|
( "-int_div_C",
|
209
|
Arg.Clear integer_div_euclidean,
|
210
|
"interprets integer division as C division (default)" );
|
211
|
( "-mauve",
|
212
|
Arg.String
|
213
|
(fun node ->
|
214
|
mauve := node;
|
215
|
cpp := true;
|
216
|
static_mem := false),
|
217
|
"generates the mauve code" );
|
218
|
]
|
219
|
|
220
|
let lustret_options =
|
221
|
common_options
|
222
|
@ [
|
223
|
( "-nb-mutants",
|
224
|
Arg.Set_int nb_mutants,
|
225
|
"\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>" );
|
226
|
"-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage";
|
227
|
( "-no-mutation-suffix",
|
228
|
Arg.Set no_mutation_suffix,
|
229
|
"does not rename node with the _mutant suffix" );
|
230
|
]
|
231
|
|
232
|
let lustrev_options =
|
233
|
common_options
|
234
|
@ [
|
235
|
( "-inline",
|
236
|
Arg.Unit
|
237
|
(fun () ->
|
238
|
global_inline := true;
|
239
|
const_unfold := true),
|
240
|
"inlines all node calls (require a main node). Implies constant \
|
241
|
unfolding" );
|
242
|
( "-O",
|
243
|
Arg.Set_int optimization,
|
244
|
"changes optimization \x1b[4mlevel\x1b[0m <default: 2>" );
|
245
|
]
|
246
|
|
247
|
let plugin_opt (name, activate, usage, options) =
|
248
|
let usage () =
|
249
|
Format.printf "@[<v 2>Plugin %s:@ %t@]@." name usage;
|
250
|
exit 0
|
251
|
in
|
252
|
("-" ^ name, Arg.Unit activate, "activate plugin " ^ name)
|
253
|
::
|
254
|
("-" ^ name ^ "-help", Arg.Unit usage, "plugin " ^ name ^ " help")
|
255
|
:: List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options
|
256
|
|
257
|
let verifier_opt (name, activate, options) =
|
258
|
("-" ^ name, Arg.Unit activate, "run verifier " ^ name)
|
259
|
:: List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options
|
260
|
|
261
|
let get_witness_dir filename =
|
262
|
(* Make sure the directory exists *)
|
263
|
let dir = !dest_dir ^ "/" ^ Filename.basename filename ^ "_witnesses" in
|
264
|
let _ =
|
265
|
try
|
266
|
if not (Sys.is_directory dir) then (
|
267
|
Format.eprintf "File of name %s exists. It should be a directory.@." dir;
|
268
|
exit 1)
|
269
|
with Sys_error _ -> Unix.mkdir dir 0o750
|
270
|
in
|
271
|
dir
|