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 Format
|
14
|
open Lustre_types
|
15
|
open Corelang
|
16
|
|
17
|
let check_main () =
|
18
|
if !Options.main_node = "" then (
|
19
|
eprintf "Code generation error: %a@." Error.pp Error.No_main_specified;
|
20
|
raise (Error.Error (Location.dummy, Error.No_main_specified)))
|
21
|
|
22
|
let create_dest_dir () =
|
23
|
if not (Sys.file_exists !Options.dest_dir) then (
|
24
|
Log.report ~level:1 (fun fmt ->
|
25
|
fprintf fmt ".. creating destination directory@ ");
|
26
|
Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm);
|
27
|
if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then (
|
28
|
eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir;
|
29
|
exit 1)
|
30
|
|
31
|
(* Loading Lus/Lusi file and filling type tables with parsed functions/nodes *)
|
32
|
let parse filename extension =
|
33
|
(* Location.set_input filename; *)
|
34
|
(* let f_in = open_in filename in *)
|
35
|
(* let lexbuf = Lexing.from_channel f_in in *)
|
36
|
(* Location.init lexbuf filename; *)
|
37
|
(* Parsing *)
|
38
|
let prog =
|
39
|
try
|
40
|
Parse.(
|
41
|
parse_filename
|
42
|
(module Lexer_lustre)
|
43
|
filename
|
44
|
(match extension with
|
45
|
| ".lusi" ->
|
46
|
Log.report ~level:1 (fun fmt ->
|
47
|
fprintf fmt ".. parsing header file %s@ " filename);
|
48
|
Header
|
49
|
| ".lus" ->
|
50
|
Log.report ~level:1 (fun fmt ->
|
51
|
fprintf fmt ".. parsing source file %s@ " filename);
|
52
|
Program
|
53
|
| _ ->
|
54
|
assert false))
|
55
|
with
|
56
|
(* | (Parse.Error err) as exc ->
|
57
|
* Parse.report_error err;
|
58
|
* raise exc *)
|
59
|
| Error.Error (loc, err) as exc ->
|
60
|
eprintf "Parsing error: %a%a@." Error.pp err Location.pp loc;
|
61
|
raise exc
|
62
|
in
|
63
|
(* close_in f_in; *)
|
64
|
prog
|
65
|
|
66
|
let expand_automata decls =
|
67
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
|
68
|
try Automata.expand_decls decls
|
69
|
with Error.Error (loc, err) as exc ->
|
70
|
eprintf "Automata error: %a%a@." Error.pp err Location.pp loc;
|
71
|
raise exc
|
72
|
|
73
|
let check_stateless_decls decls =
|
74
|
Log.report ~level:1 (fun fmt ->
|
75
|
fprintf fmt "@ .. checking stateless/stateful status@ ");
|
76
|
try Stateless.check_prog decls
|
77
|
with Stateless.Error (loc, err) as exc ->
|
78
|
eprintf
|
79
|
"Stateless status error: %a%a@."
|
80
|
Stateless.pp_error
|
81
|
err
|
82
|
Location.pp
|
83
|
loc;
|
84
|
raise exc
|
85
|
|
86
|
let force_stateful_decls decls =
|
87
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. forcing stateful status@ ");
|
88
|
try Stateless.force_prog decls
|
89
|
with Stateless.Error (loc, err) as exc ->
|
90
|
eprintf
|
91
|
"Stateless status error: %a%a@."
|
92
|
Stateless.pp_error
|
93
|
err
|
94
|
Location.pp
|
95
|
loc;
|
96
|
raise exc
|
97
|
|
98
|
let type_decls env decls =
|
99
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. typing@ ");
|
100
|
let new_env =
|
101
|
try Typing.type_prog env decls
|
102
|
with Types.Error (loc, err) as exc ->
|
103
|
eprintf "Typing error: %a%a@." Types.pp_error err Location.pp loc;
|
104
|
raise exc
|
105
|
in
|
106
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
|
107
|
if !Options.print_types || !Options.verbose_level > 2 then
|
108
|
Log.report ~level:1 (fun fmt ->
|
109
|
fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_type decls);
|
110
|
new_env
|
111
|
|
112
|
let clock_decls env decls =
|
113
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. clock calculus@ ");
|
114
|
let new_env =
|
115
|
try Clock_calculus.clock_prog env decls
|
116
|
with Clocks.Error (loc, err) as exc ->
|
117
|
eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp loc;
|
118
|
raise exc
|
119
|
in
|
120
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
|
121
|
if !Options.print_clocks || !Options.verbose_level > 2 then
|
122
|
Log.report ~level:1 (fun fmt ->
|
123
|
fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_clock decls);
|
124
|
new_env
|
125
|
|
126
|
(* XXX: UNUSED *)
|
127
|
(* Typing/Clocking with an empty env *)
|
128
|
(* let check_top_decls header =
|
129
|
* let new_tenv = type_decls Basic_library.type_env header in
|
130
|
* (\* Typing *\)
|
131
|
* let new_cenv = clock_decls Basic_library.clock_env header in
|
132
|
* (\* Clock calculus *\)
|
133
|
* header, new_tenv, new_cenv *)
|
134
|
|
135
|
(* List.fold_right (fun top_decl (ty_env, ck_env) -> match
|
136
|
top_decl.top_decl_desc with | Node nd -> (Env.add_value ty_env nd.node_id
|
137
|
nd.node_type, Env.add_value ck_env nd.node_id nd.node_clock) | ImportedNode
|
138
|
ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type, Env.add_value
|
139
|
ck_env ind.nodei_id ind.nodei_clock) | Const c -> get_envs_from_const c
|
140
|
(ty_env, ck_env) | TypeDef _ -> List.fold_left (fun envs top ->
|
141
|
consts_of_enum_type top_decl | Open _ -> (ty_env, ck_env)) header
|
142
|
(Env.initial, Env.initial) *)
|
143
|
|
144
|
let check_compatibility (_, computed_types_env, computed_clocks_env)
|
145
|
(header, declared_types_env, declared_clocks_env) =
|
146
|
try
|
147
|
(* checking defined types are compatible with declared types*)
|
148
|
Typing.check_typedef_compat header;
|
149
|
|
150
|
(* checking type compatibility with computed types*)
|
151
|
Typing.check_env_compat header declared_types_env computed_types_env;
|
152
|
|
153
|
(* checking clocks compatibility with computed clocks*)
|
154
|
Clock_calculus.check_env_compat
|
155
|
header
|
156
|
declared_clocks_env
|
157
|
computed_clocks_env;
|
158
|
|
159
|
(* checking stateless status compatibility *)
|
160
|
Stateless.check_compat header
|
161
|
with
|
162
|
| Types.Error (loc, err) as exc ->
|
163
|
eprintf
|
164
|
"Type mismatch between computed type and declared type in lustre \
|
165
|
interface file: %a%a@."
|
166
|
Types.pp_error
|
167
|
err
|
168
|
Location.pp
|
169
|
loc;
|
170
|
raise exc
|
171
|
| Clocks.Error (loc, err) as exc ->
|
172
|
eprintf
|
173
|
"Clock mismatch between computed clock and declared clock in lustre \
|
174
|
interface file: %a%a@."
|
175
|
Clocks.pp_error
|
176
|
err
|
177
|
Location.pp
|
178
|
loc;
|
179
|
raise exc
|
180
|
| Stateless.Error (loc, err) as exc ->
|
181
|
eprintf
|
182
|
"Stateless status mismatch between defined status and declared status in \
|
183
|
lustre interface file: %a%a@."
|
184
|
Stateless.pp_error
|
185
|
err
|
186
|
Location.pp
|
187
|
loc;
|
188
|
raise exc
|
189
|
|
190
|
(* Process each node/imported node and introduce the associated contract node *)
|
191
|
let resolve_contracts prog =
|
192
|
(* Bind a fresh node with a new name according to existing nodes and freshly
|
193
|
binded contract node. Clean the contract to remove the stmts *)
|
194
|
let process_contract new_contracts c =
|
195
|
(* Format.eprintf "Process contract@."; *)
|
196
|
(* Resolve first the imports *)
|
197
|
let stmts, locals, c =
|
198
|
List.fold_left
|
199
|
(fun (stmts, locals, c) import ->
|
200
|
(* Search for contract in prog. The node have to be processed already.
|
201
|
Otherwise raise an error. Each stmts in injected with a fresh name
|
202
|
Inputs are renamed and associated to the expression in1 Same thing
|
203
|
for outputs.
|
204
|
|
205
|
Last the contracts elements are replaced with the renamed vars and
|
206
|
merged with c contract. *)
|
207
|
let name = import.import_nodeid in
|
208
|
(* Format.eprintf "Process contract import %s@." name; *)
|
209
|
let loc = import.import_loc in
|
210
|
try
|
211
|
let imp_nd = get_node name new_contracts in
|
212
|
(* Get the contract node in process contracts *)
|
213
|
(* checking that it's actually a (processed) contract *)
|
214
|
let _ =
|
215
|
if not (is_node_contract imp_nd) then assert false
|
216
|
(* should be a contract *)
|
217
|
else
|
218
|
let imp_c = get_node_contract imp_nd in
|
219
|
if
|
220
|
not
|
221
|
(imp_c.imports = [] && imp_c.locals = []
|
222
|
&& imp_c.consts = [] && imp_c.stmts = [])
|
223
|
then (
|
224
|
Format.eprintf
|
225
|
"Invalid processed contract: %i %i %i %i@.@?"
|
226
|
(List.length imp_c.imports)
|
227
|
(List.length imp_c.locals)
|
228
|
(List.length imp_c.consts)
|
229
|
(List.length imp_c.stmts);
|
230
|
assert false (* should be processed *))
|
231
|
in
|
232
|
let name_prefix x = "__" ^ name ^ "__" ^ x in
|
233
|
let imp_nd =
|
234
|
rename_node
|
235
|
(fun x -> x (* not changing node names *))
|
236
|
name_prefix
|
237
|
imp_nd
|
238
|
in
|
239
|
let imp_in = imp_nd.node_inputs in
|
240
|
let imp_out = imp_nd.node_outputs in
|
241
|
let imp_locals = imp_nd.node_locals in
|
242
|
let locals = imp_in @ imp_out @ imp_locals @ locals in
|
243
|
let imp_c = get_node_contract imp_nd in
|
244
|
(* Assigning in and out *)
|
245
|
let mk_def vars_l e =
|
246
|
let lhs = List.map (fun v -> v.var_id) vars_l in
|
247
|
Eq (mkeq loc (lhs, e))
|
248
|
in
|
249
|
let in_assigns = mk_def imp_in import.inputs in
|
250
|
let out_assigns = mk_def imp_out import.outputs in
|
251
|
let stmts =
|
252
|
in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts
|
253
|
in
|
254
|
let c = merge_contracts c imp_c in
|
255
|
stmts, locals, c
|
256
|
with Not_found ->
|
257
|
Format.eprintf "Where is contract %s@.@?" name;
|
258
|
raise (Error.Error (loc, Error.Unbound_symbol ("contract " ^ name))))
|
259
|
([], c.consts @ c.locals, c)
|
260
|
c.imports
|
261
|
in
|
262
|
let stmts = stmts @ c.stmts in
|
263
|
(* Other contract elements will be normalized later *)
|
264
|
let c =
|
265
|
{
|
266
|
c with
|
267
|
(* we erase locals and stmts sinced they are now in the parent node *)
|
268
|
locals = [];
|
269
|
consts = [];
|
270
|
stmts = [];
|
271
|
imports = [];
|
272
|
}
|
273
|
in
|
274
|
|
275
|
(* Format.eprintf "Processed stmts: %a@." Printers.pp_node_stmts stmts;
|
276
|
* Format.eprintf "Processed locals: %a@." Printers.pp_vars locals; *)
|
277
|
stmts, locals, c
|
278
|
in
|
279
|
|
280
|
let process_contract_new_node accu_contracts prog top =
|
281
|
let id, spec, inputs, outputs =
|
282
|
match top.top_decl_desc with
|
283
|
| Node nd ->
|
284
|
nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
|
285
|
| ImportedNode ind ->
|
286
|
ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
|
287
|
| _ ->
|
288
|
assert false
|
289
|
in
|
290
|
|
291
|
(* Format.eprintf "Process contract new node for node %s@." id; *)
|
292
|
let node_stmts, node_locals, c =
|
293
|
match spec with
|
294
|
| None | Some (NodeSpec _) ->
|
295
|
assert false
|
296
|
| Some (Contract c) ->
|
297
|
(* Format.eprintf "Processing contract of node %s@." id; *)
|
298
|
process_contract accu_contracts c
|
299
|
in
|
300
|
(* Create a fresh name *)
|
301
|
let used v =
|
302
|
List.exists
|
303
|
(fun top ->
|
304
|
match top.top_decl_desc with
|
305
|
| Node _ | ImportedNode _ ->
|
306
|
node_name top = v
|
307
|
| _ ->
|
308
|
false)
|
309
|
(accu_contracts @ prog)
|
310
|
in
|
311
|
let nd = {
|
312
|
node_id = mk_new_name used (id ^ "_contract");
|
313
|
node_type = Types.new_var ();
|
314
|
node_clock = Clocks.new_var true;
|
315
|
node_inputs = inputs @ outputs;
|
316
|
node_outputs = [];
|
317
|
node_locals;
|
318
|
node_gencalls = [];
|
319
|
node_checks = [];
|
320
|
node_asserts = [];
|
321
|
node_stmts;
|
322
|
node_dec_stateless = false;
|
323
|
node_stateless = None;
|
324
|
node_spec = Some (Contract c);
|
325
|
node_annot = [];
|
326
|
node_iscontract = true;
|
327
|
} in
|
328
|
(* let stateless = Stateless.compute_node nd in *)
|
329
|
mktop_decl
|
330
|
c.spec_loc
|
331
|
top.top_decl_owner
|
332
|
top.top_decl_itf
|
333
|
(Node nd)
|
334
|
(* { nd with
|
335
|
* node_dec_stateless = stateless;
|
336
|
* node_stateless = Some stateless;
|
337
|
* }) *)
|
338
|
in
|
339
|
(* Processing nodes in order. Should have been sorted by now
|
340
|
|
341
|
Each top level contract is processed: stmts pushed in node
|
342
|
|
343
|
Each regular imported node or node associated with a contract is replaced
|
344
|
with a simplidfied contract and its contract is bound to a fresh node. *)
|
345
|
let new_contracts, prog =
|
346
|
List.fold_left
|
347
|
(fun (accu_contracts, accu_nodes) top ->
|
348
|
match top.top_decl_desc with
|
349
|
| Node nd when nd.node_iscontract -> (
|
350
|
match nd.node_spec with
|
351
|
| None | Some (NodeSpec _) ->
|
352
|
assert false
|
353
|
| Some (Contract c) ->
|
354
|
(* Format.eprintf "Processing top contract %s@." nd.node_id; *)
|
355
|
let stmts, locals, c = process_contract accu_contracts c in
|
356
|
let nd =
|
357
|
{
|
358
|
nd with
|
359
|
node_locals = nd.node_locals @ locals;
|
360
|
node_stmts = nd.node_stmts @ stmts;
|
361
|
node_spec = Some (Contract c);
|
362
|
}
|
363
|
in
|
364
|
{ top with top_decl_desc = Node nd } :: accu_contracts, accu_nodes)
|
365
|
| Node nd -> (
|
366
|
match nd.node_spec with
|
367
|
| None ->
|
368
|
accu_contracts, top :: accu_nodes (* A boring node: no contract *)
|
369
|
| Some (NodeSpec _) ->
|
370
|
(* shall not happen, its too early *)
|
371
|
assert false
|
372
|
| Some (Contract _) ->
|
373
|
(* A contract: processing it *)
|
374
|
(* we bind a fresh node *)
|
375
|
let new_nd = process_contract_new_node accu_contracts prog top in
|
376
|
(* Format.eprintf "Creating new contract node %s@." (node_name
|
377
|
new_nd); *)
|
378
|
let nd =
|
379
|
{ nd with node_spec = Some (NodeSpec (node_name new_nd)) }
|
380
|
in
|
381
|
( new_nd :: accu_contracts,
|
382
|
{ top with top_decl_desc = Node nd } :: accu_nodes ))
|
383
|
| ImportedNode ind -> (
|
384
|
(* Similar treatment for imported nodes *)
|
385
|
match ind.nodei_spec with
|
386
|
| None ->
|
387
|
accu_contracts, top :: accu_nodes (* A boring node: no contract *)
|
388
|
| Some (NodeSpec _) ->
|
389
|
(* shall not happen, its too early *)
|
390
|
assert false
|
391
|
| Some (Contract _) ->
|
392
|
(* A contract: processing it *)
|
393
|
(* we bind a fresh node *)
|
394
|
let new_nd = process_contract_new_node accu_contracts prog top in
|
395
|
let ind =
|
396
|
{ ind with nodei_spec = Some (NodeSpec (node_name new_nd)) }
|
397
|
in
|
398
|
( new_nd :: accu_contracts,
|
399
|
{ top with top_decl_desc = ImportedNode ind } :: accu_nodes ))
|
400
|
| _ ->
|
401
|
accu_contracts, top :: accu_nodes)
|
402
|
([], [])
|
403
|
prog
|
404
|
in
|
405
|
List.rev new_contracts @ List.rev prog
|
406
|
|
407
|
let track_exception () =
|
408
|
if !Options.track_exceptions then (
|
409
|
Printexc.print_backtrace stdout;
|
410
|
flush stdout)
|
411
|
else ()
|
412
|
|
413
|
let update_vdecl_parents_prog prog =
|
414
|
let update_vdecl_parents parent v = v.var_parent_nodeid <- Some parent in
|
415
|
List.iter
|
416
|
(fun top ->
|
417
|
match top.top_decl_desc with
|
418
|
| Node nd ->
|
419
|
List.iter
|
420
|
(update_vdecl_parents nd.node_id)
|
421
|
(nd.node_inputs @ nd.node_outputs @ nd.node_locals)
|
422
|
| ImportedNode ind ->
|
423
|
List.iter
|
424
|
(update_vdecl_parents ind.nodei_id)
|
425
|
(ind.nodei_inputs @ ind.nodei_outputs)
|
426
|
| _ ->
|
427
|
())
|
428
|
prog
|