1
|
open Format
|
2
|
open Compiler_common
|
3
|
open Lustre_types
|
4
|
module Mpfr = Lustrec_mpfr
|
5
|
|
6
|
exception StopPhase1 of program_t
|
7
|
|
8
|
let dynamic_checks () =
|
9
|
let open Options in
|
10
|
match !output, !spec with OutC, SpecC -> true | _ -> false
|
11
|
|
12
|
let generate_c_header = ref false
|
13
|
|
14
|
(* check whether a source file has a compiled header, if not, generate the
|
15
|
compiled header *)
|
16
|
let compile_source_to_header prog computed_types_env computed_clocks_env dirname
|
17
|
basename extension =
|
18
|
let destname = !Options.dest_dir ^ "/" ^ basename in
|
19
|
let lusic_ext = ".lusic" in
|
20
|
let header_name = destname ^ lusic_ext in
|
21
|
let from_lusi = extension = ".lusi" in
|
22
|
if
|
23
|
(* Generating the lusic file *)
|
24
|
(* because input is a lusi *)
|
25
|
from_lusi
|
26
|
(* or because it is a lus but no lusic exists *)
|
27
|
|| (extension = ".lus" && not (Sys.file_exists header_name))
|
28
|
(* or the lusic exists but is not generated from a lusi, hence it has te be
|
29
|
regenerated *)
|
30
|
||
|
31
|
let lusic = Lusic.read_lusic destname lusic_ext in
|
32
|
not lusic.Lusic.from_lusi
|
33
|
then (
|
34
|
Log.report ~level:1 (fun fmt ->
|
35
|
fprintf fmt "@ .. generating compiled header file %s@," header_name);
|
36
|
Lusic.write_lusic from_lusi
|
37
|
(* is it a lusi file ? *)
|
38
|
(if from_lusi then prog else Lusic.extract_header dirname basename prog)
|
39
|
destname lusic_ext;
|
40
|
generate_c_header := !Options.output = Options.OutC)
|
41
|
else (
|
42
|
(* Lusic exists and is usable. Checking compatibility *)
|
43
|
Log.report ~level:1 (fun fmt ->
|
44
|
fprintf fmt "@ .. loading compiled header file %s@," header_name);
|
45
|
let lusic = Lusic.read_lusic destname lusic_ext in
|
46
|
Lusic.check_obsolete lusic destname;
|
47
|
let header = lusic.Lusic.contents in
|
48
|
let declared_types_env, declared_clocks_env =
|
49
|
Modules.get_envs_from_top_decls header
|
50
|
in
|
51
|
check_compatibility
|
52
|
(prog, computed_types_env, computed_clocks_env)
|
53
|
(header, declared_types_env, declared_clocks_env))
|
54
|
|
55
|
(* From prog to prog *)
|
56
|
let stage1 params prog dirname basename extension =
|
57
|
(* Updating parent node information for variables *)
|
58
|
Compiler_common.update_vdecl_parents_prog prog;
|
59
|
|
60
|
(* Removing automata *)
|
61
|
let prog = expand_automata prog in
|
62
|
Log.report ~level:4 (fun fmt ->
|
63
|
fprintf fmt "@[<v 2>.. after automata expansion:@ %a@]@ " Printers.pp_prog
|
64
|
prog
|
65
|
(* Utils.Format.pp_print_nothing () *));
|
66
|
|
67
|
(* Importing source *)
|
68
|
let prog, dependencies, (typ_env, clk_env) =
|
69
|
Modules.load ~is_header:(extension = ".lusi") prog
|
70
|
in
|
71
|
(* Registering types and clocks for future checks *)
|
72
|
Global.type_env := Env.overwrite !Global.type_env typ_env;
|
73
|
Global.clock_env := Env.overwrite !Global.clock_env clk_env;
|
74
|
|
75
|
(* (\* Extracting dependencies (and updating Global.(type_env/clock_env) *\)
|
76
|
* let dependencies = import_dependencies prog in *)
|
77
|
|
78
|
(* Sorting nodes *)
|
79
|
let prog = SortProg.sort prog in
|
80
|
(* Consolidating contracts *)
|
81
|
let prog = resolve_contracts prog in
|
82
|
let prog = SortProg.sort prog in
|
83
|
Log.report ~level:3 (fun fmt ->
|
84
|
Format.fprintf fmt "@ @[<v 2>.. contracts resolved:@ %a@ @]@ "
|
85
|
Printers.pp_prog prog);
|
86
|
|
87
|
(* Consolidating main node *)
|
88
|
let _ =
|
89
|
match !Options.main_node with
|
90
|
| "" ->
|
91
|
()
|
92
|
| main_node -> (
|
93
|
Global.main_node := main_node;
|
94
|
try ignore (Corelang.node_from_name main_node)
|
95
|
with Not_found ->
|
96
|
Format.eprintf "Code generation error: %a@." Error.pp
|
97
|
Error.Main_not_found;
|
98
|
raise (Error.Error (Location.dummy, Error.Main_not_found)))
|
99
|
in
|
100
|
|
101
|
(* Perform inlining before any analysis *)
|
102
|
let _, prog =
|
103
|
if !Options.global_inline && !Global.main_node <> "" then
|
104
|
(if !Options.witnesses then prog else []), Inliner.global_inline prog
|
105
|
else (* if !Option.has_local_inline *)
|
106
|
[], Inliner.local_inline prog
|
107
|
(* type_env clock_env *)
|
108
|
in
|
109
|
|
110
|
(* Checking stateless/stateful status *)
|
111
|
if Plugins.check_force_stateful () then force_stateful_decls prog
|
112
|
else check_stateless_decls prog;
|
113
|
|
114
|
(* Typing *)
|
115
|
Global.type_env := type_decls !Global.type_env prog;
|
116
|
|
117
|
(* Clock calculus *)
|
118
|
Global.clock_env := clock_decls !Global.clock_env prog;
|
119
|
|
120
|
(* Registering and checking machine types *)
|
121
|
if Machine_types.is_active then Machine_types.load prog;
|
122
|
|
123
|
(* Generating a .lusi header file only *)
|
124
|
if !Options.lusi || !Options.print_nodes then
|
125
|
(* We stop here the processing and produce the current prog. It will be
|
126
|
exported as a lusi *)
|
127
|
raise (StopPhase1 prog);
|
128
|
|
129
|
(* Optimization of prog: - Unfold consts - eliminate trivial expressions *)
|
130
|
let prog =
|
131
|
if !Options.const_unfold || !Options.optimization >= 5 then (
|
132
|
Log.report ~level:1 (fun fmt ->
|
133
|
fprintf fmt ".. eliminating constants and aliases@,");
|
134
|
Optimize_prog.prog_unfold_consts prog)
|
135
|
else prog
|
136
|
in
|
137
|
|
138
|
(* Delay calculus *)
|
139
|
(* TO BE DONE LATER (Xavier) if(!Options.delay_calculus) then begin Log.report
|
140
|
~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?"); try
|
141
|
Delay_calculus.delay_prog Basic_library.delay_env prog with (Delay.Error
|
142
|
(loc,err)) as exc -> Location.print loc; eprintf "%a" Delay.pp_error err;
|
143
|
Utils.track_exception (); raise exc end; *)
|
144
|
|
145
|
(* Creating destination directory if needed *)
|
146
|
create_dest_dir ();
|
147
|
|
148
|
Typing.uneval_prog_generics prog;
|
149
|
Clock_calculus.uneval_prog_generics prog;
|
150
|
|
151
|
(* Disabling witness option. Could but reactivated later if
|
152
|
!Options.global_inline && !Options.main_node <> "" && !Options.witnesses
|
153
|
then begin let orig = Corelang.copy_prog orig in Log.report ~level:1 (fun
|
154
|
fmt -> fprintf fmt ".. generating witness file@,"); check_stateless_decls
|
155
|
orig; let _ = Typing.type_prog type_env orig in let _ =
|
156
|
Clock_calculus.clock_prog clock_env orig in Typing.uneval_prog_generics
|
157
|
orig; Clock_calculus.uneval_prog_generics orig; Inliner.witness basename
|
158
|
!Options.main_node orig prog type_env clock_env end; *)
|
159
|
|
160
|
(* Computes and stores generic calls for each node, only useful for ANSI C90
|
161
|
compliant generic node compilation *)
|
162
|
if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
|
163
|
|
164
|
(*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
|
165
|
Corelang.Node nd -> Format.eprintf "%s calls %a" id
|
166
|
Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
|
167
|
|
168
|
(* If some backend involving dynamic checks are active, then node annotations
|
169
|
become runtime checks *)
|
170
|
let prog = if dynamic_checks () then Spec.enforce_spec_prog prog else prog in
|
171
|
|
172
|
(* (\* Registering and checking machine types *\) *)
|
173
|
(* Machine_types.load prog; *)
|
174
|
|
175
|
(* Normalization phase *)
|
176
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. normalization@ ");
|
177
|
let prog = Normalization.normalize_prog params prog in
|
178
|
Log.report ~level:2 (fun fmt ->
|
179
|
fprintf fmt "@[<v 2>@ %a@]@ " Printers.pp_prog_short prog);
|
180
|
Log.report ~level:3 (fun fmt ->
|
181
|
fprintf fmt "@[<v 2>@ %a@]@ " Printers.pp_prog prog);
|
182
|
|
183
|
(* Compatibility with Lusi *)
|
184
|
(* If compiling a lusi, generate the lusic. If this is a lus file, Check the
|
185
|
existence of a lusi (Lustre Interface file) *)
|
186
|
if !Options.compile_header then
|
187
|
compile_source_to_header prog !Global.type_env !Global.clock_env dirname
|
188
|
basename extension;
|
189
|
|
190
|
let prog =
|
191
|
if !Options.mpfr then (
|
192
|
Log.report ~level:1 (fun fmt ->
|
193
|
fprintf fmt "@ .. targetting MPFR library@,");
|
194
|
Mpfr.inject_prog prog)
|
195
|
else (
|
196
|
Log.report ~level:1 (fun fmt ->
|
197
|
fprintf fmt "@ .. keeping floating-point numbers@,");
|
198
|
prog)
|
199
|
in
|
200
|
Log.report ~level:3 (fun fmt ->
|
201
|
fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
|
202
|
|
203
|
(* Checking array accesses *)
|
204
|
if !Options.check then (
|
205
|
Log.report ~level:1 (fun fmt ->
|
206
|
fprintf fmt "@ .. checking array accesses@,");
|
207
|
Access.check_prog prog);
|
208
|
|
209
|
let prog = SortProg.sort_nodes_locals prog in
|
210
|
|
211
|
prog, dependencies
|
212
|
|
213
|
(* from source to machine code, with optimization *)
|
214
|
let stage2 params prog =
|
215
|
(* Computation of node equation scheduling. It also breaks dependency cycles
|
216
|
and warns about unused input or memory variables *)
|
217
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. scheduling@ ");
|
218
|
let prog, node_schs =
|
219
|
try Scheduling.schedule_prog prog
|
220
|
with Causality.Error _ ->
|
221
|
(* Error is not kept. It is recomputed in a more systemtic way in
|
222
|
AlgebraicLoop module *)
|
223
|
AlgebraicLoop.analyze prog
|
224
|
in
|
225
|
Scheduling.(
|
226
|
Log.report ~level:1 (fun fmt -> pp_warning_unused fmt node_schs);
|
227
|
Log.report ~level:3 (fun fmt -> fprintf fmt "@ %a" pp_schedule node_schs);
|
228
|
Log.report ~level:3 (fun fmt -> fprintf fmt "@ %a" pp_fanin_table node_schs);
|
229
|
Log.report ~level:5 (fun fmt -> fprintf fmt "@ %a" pp_dep_graph node_schs);
|
230
|
Log.report ~level:3 (fun fmt -> fprintf fmt "@ %a" Printers.pp_prog prog);
|
231
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "));
|
232
|
|
233
|
(* TODO Salsa optimize prog: - emits warning for programs with pre inside
|
234
|
expressions - make sure each node arguments and memory is bounded by a
|
235
|
local annotation - introduce fresh local variables for each real pure
|
236
|
subexpression *)
|
237
|
(* DFS with modular code generation *)
|
238
|
Log.report ~level:1 (fun fmt ->
|
239
|
fprintf fmt "@ @[<v 2>.. machines generation@ ");
|
240
|
let machine_code = Machine_code.translate_prog prog node_schs in
|
241
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
|
242
|
|
243
|
Log.report ~level:3 (fun fmt ->
|
244
|
fprintf fmt "@ @[<v 2>.. generated machines (unoptimized):@ %a@]@ "
|
245
|
Machine_code_common.pp_machines machine_code);
|
246
|
|
247
|
(* Optimize machine code *)
|
248
|
Optimize_machine.optimize params prog node_schs machine_code
|
249
|
|
250
|
(* printing code *)
|
251
|
let stage3 prog machine_code dependencies basename extension =
|
252
|
let open Options in
|
253
|
let basename = Filename.basename basename in
|
254
|
match !output, extension with
|
255
|
| OutC, ".lus" ->
|
256
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
|
257
|
C_backend.translate_to_c !generate_c_header
|
258
|
(* alloc_header_file source_lib_file source_main_file makefile_file *)
|
259
|
basename prog machine_code dependencies
|
260
|
(* | "acsl", ".lus" -> begin Log.report ~level:1 (fun fmt -> fprintf fmt "..
|
261
|
ACSL annotations generation@,"); ACSL_backend.translate_to_acsl (*
|
262
|
alloc_header_file source_lib_file source_main_file makefile_file *)
|
263
|
basename prog machine_code dependencies end *)
|
264
|
| OutC, _ ->
|
265
|
C_backend.print_c_header basename;
|
266
|
Log.report ~level:1 (fun fmt ->
|
267
|
fprintf fmt ".. no C code generation for lusi@,")
|
268
|
| OutJava, _ ->
|
269
|
Format.eprintf "internal error: sorry, but not yet supported !";
|
270
|
assert false
|
271
|
(*let source_file = basename ^ ".java" in Log.report ~level:1 (fun fmt ->
|
272
|
fprintf fmt ".. opening file %s@,@?" source_file); let source_out = open_out
|
273
|
source_file in let source_fmt = formatter_of_out_channel source_out in
|
274
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
|
275
|
Java_backend.translate_to_java source_fmt basename normalized_prog
|
276
|
machine_code;*)
|
277
|
| OutAda, _ ->
|
278
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
|
279
|
Ada_backend.translate_to_ada basename
|
280
|
(Machine_code_common.arrow_machine :: machine_code)
|
281
|
| OutHorn, _ ->
|
282
|
let destname = !Options.dest_dir ^ "/" ^ basename in
|
283
|
let source_file = destname ^ ".smt2" in
|
284
|
(* Could be changed *)
|
285
|
let source_out = open_out source_file in
|
286
|
let fmt = formatter_of_out_channel source_out in
|
287
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
|
288
|
Horn_backend.translate fmt prog
|
289
|
(Machine_code_common.arrow_machine :: machine_code);
|
290
|
(* Tracability file if option is activated *)
|
291
|
if !Options.traces then (
|
292
|
let traces_file = destname ^ ".traces.xml" in
|
293
|
(* Could be changed *)
|
294
|
let traces_out = open_out traces_file in
|
295
|
let fmt = formatter_of_out_channel traces_out in
|
296
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
|
297
|
Horn_backend_traces.traces_file fmt machine_code)
|
298
|
| OutLustre, _ ->
|
299
|
let destname = !Options.dest_dir ^ "/" ^ basename in
|
300
|
let source_file = destname ^ ".lustrec" ^ extension in
|
301
|
(* Could be changed *)
|
302
|
Log.report ~level:1 (fun fmt ->
|
303
|
fprintf fmt ".. exporting processed file as %s@," source_file);
|
304
|
let source_out = open_out source_file in
|
305
|
let fmt = formatter_of_out_channel source_out in
|
306
|
Printers.pp_prog fmt prog;
|
307
|
Format.fprintf fmt "@.@?";
|
308
|
(* Lustre_backend.translate fmt basename normalized_prog machine_code *)
|
309
|
()
|
310
|
| OutEMF, _ ->
|
311
|
let destname = !Options.dest_dir ^ "/" ^ basename in
|
312
|
let source_file = destname ^ ".json" in
|
313
|
(* Could be changed *)
|
314
|
let source_out = open_out source_file in
|
315
|
let fmt = formatter_of_out_channel source_out in
|
316
|
EMF_backend.translate fmt basename prog machine_code;
|
317
|
()
|