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
|
type aut_state = {
|
17
|
incoming_r' : var_decl;
|
18
|
incoming_s' : var_decl;
|
19
|
incoming_r : var_decl;
|
20
|
incoming_s : var_decl;
|
21
|
actual_r : var_decl;
|
22
|
actual_s : var_decl;
|
23
|
}
|
24
|
|
25
|
let as_clock var_decl =
|
26
|
let tydec = var_decl.var_dec_type in
|
27
|
{
|
28
|
var_decl with
|
29
|
var_dec_type =
|
30
|
{
|
31
|
ty_dec_desc = Tydec_clock tydec.ty_dec_desc;
|
32
|
ty_dec_loc = tydec.ty_dec_loc;
|
33
|
};
|
34
|
}
|
35
|
|
36
|
let mkbool loc b = mkexpr loc (Expr_const (const_of_bool b))
|
37
|
|
38
|
let mkident loc id = mkexpr loc (Expr_ident id)
|
39
|
|
40
|
let mkconst loc id = mkexpr loc (Expr_const (Const_tag id))
|
41
|
|
42
|
let mkfby loc e1 e2 = mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
|
43
|
|
44
|
let mkpair loc e1 e2 = 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
|
51
|
(Expr_ite
|
52
|
( expr,
|
53
|
mkexpr loc (Expr_tuple [ mkbool loc restart; mkident loc st ]),
|
54
|
cont ))
|
55
|
|
56
|
let mkhandler loc st unless until locals (stmts, asserts, annots) =
|
57
|
{
|
58
|
hand_state = st;
|
59
|
hand_unless = unless;
|
60
|
hand_until = until;
|
61
|
hand_locals = locals;
|
62
|
hand_stmts = stmts;
|
63
|
hand_asserts = asserts;
|
64
|
hand_annots = annots;
|
65
|
hand_loc = loc;
|
66
|
}
|
67
|
|
68
|
let mkautomata loc id handlers =
|
69
|
{ aut_id = id; aut_handlers = handlers; aut_loc = loc }
|
70
|
|
71
|
let expr_of_exit loc restart state conds tag =
|
72
|
mkexpr loc
|
73
|
(Expr_when
|
74
|
( List.fold_right add_branch conds (mkidentpair loc restart state),
|
75
|
state,
|
76
|
tag ))
|
77
|
|
78
|
let unless_read reads handler =
|
79
|
let res =
|
80
|
List.fold_left
|
81
|
(fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c))
|
82
|
reads handler.hand_unless
|
83
|
in
|
84
|
(* Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list
|
85
|
~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
|
86
|
Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list
|
87
|
~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res); *)
|
88
|
res
|
89
|
|
90
|
let until_read reads handler =
|
91
|
List.fold_left
|
92
|
(fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c))
|
93
|
reads handler.hand_until
|
94
|
|
95
|
let rec handler_read reads handler =
|
96
|
let locals =
|
97
|
List.fold_left
|
98
|
(fun locals v -> ISet.add v.var_id locals)
|
99
|
ISet.empty handler.hand_locals
|
100
|
in
|
101
|
let allvars =
|
102
|
List.fold_left
|
103
|
(fun read stmt ->
|
104
|
match stmt with
|
105
|
| Eq eq ->
|
106
|
Utils.ISet.union read (get_expr_vars eq.eq_rhs)
|
107
|
| Aut aut ->
|
108
|
automata_read read aut)
|
109
|
reads handler.hand_stmts
|
110
|
in
|
111
|
let res = ISet.diff allvars locals in
|
112
|
(* Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list
|
113
|
~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements
|
114
|
allvars); Format.eprintf "handler_read %s = %a@." handler.hand_state
|
115
|
(fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v))
|
116
|
(ISet.elements res); *)
|
117
|
res
|
118
|
|
119
|
and automata_read reads aut =
|
120
|
List.fold_left
|
121
|
(fun read handler ->
|
122
|
until_read (handler_read (unless_read read handler) handler) handler)
|
123
|
reads aut.aut_handlers
|
124
|
|
125
|
let rec handler_write writes handler =
|
126
|
let locals =
|
127
|
List.fold_left
|
128
|
(fun locals v -> ISet.add v.var_id locals)
|
129
|
ISet.empty handler.hand_locals
|
130
|
in
|
131
|
let allvars =
|
132
|
List.fold_left
|
133
|
(fun write stmt ->
|
134
|
match stmt with
|
135
|
| Eq eq ->
|
136
|
List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
|
137
|
| Aut aut ->
|
138
|
List.fold_left handler_write write aut.aut_handlers)
|
139
|
writes handler.hand_stmts
|
140
|
in
|
141
|
ISet.diff allvars locals
|
142
|
|
143
|
let node_vars_of_idents node iset =
|
144
|
List.fold_right
|
145
|
(fun v res -> if ISet.mem v.var_id iset then v :: res else res)
|
146
|
(get_node_vars node) []
|
147
|
|
148
|
let mkautomata_state nodeid used typedef loc id =
|
149
|
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
|
150
|
let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
|
151
|
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
|
152
|
let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in
|
153
|
let incoming_s' = mk_new_name used (id ^ "__next_state_in") in
|
154
|
let incoming_r = mk_new_name used (id ^ "__restart_in") in
|
155
|
let incoming_s = mk_new_name used (id ^ "__state_in") in
|
156
|
let actual_r = mk_new_name used (id ^ "__restart_act") in
|
157
|
let actual_s = mk_new_name used (id ^ "__state_act") in
|
158
|
{
|
159
|
incoming_r' =
|
160
|
mkvar_decl loc
|
161
|
(incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
|
162
|
incoming_s' =
|
163
|
mkvar_decl loc
|
164
|
( incoming_s',
|
165
|
tydec_state typedef.tydef_id,
|
166
|
ckdec_any,
|
167
|
false,
|
168
|
None,
|
169
|
Some nodeid );
|
170
|
incoming_r =
|
171
|
mkvar_decl loc
|
172
|
(incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
|
173
|
incoming_s =
|
174
|
mkvar_decl loc
|
175
|
( incoming_s,
|
176
|
tydec_state typedef.tydef_id,
|
177
|
ckdec_any,
|
178
|
false,
|
179
|
None,
|
180
|
Some nodeid );
|
181
|
actual_r =
|
182
|
mkvar_decl loc (actual_r, tydec_bool, ckdec_any, false, None, Some nodeid);
|
183
|
actual_s =
|
184
|
mkvar_decl loc
|
185
|
( actual_s,
|
186
|
tydec_state typedef.tydef_id,
|
187
|
ckdec_any,
|
188
|
false,
|
189
|
None,
|
190
|
Some nodeid );
|
191
|
}
|
192
|
|
193
|
let vars_of_aut_state aut_state =
|
194
|
[
|
195
|
aut_state.incoming_r';
|
196
|
aut_state.incoming_r;
|
197
|
aut_state.actual_r;
|
198
|
aut_state.incoming_s';
|
199
|
as_clock aut_state.incoming_s;
|
200
|
as_clock aut_state.actual_s;
|
201
|
]
|
202
|
|
203
|
let node_of_unless nused node aut_id aut_state handler =
|
204
|
(*Format.eprintf "node_of_unless %s@." node.node_id;*)
|
205
|
let inputs = unless_read ISet.empty handler in
|
206
|
let var_inputs =
|
207
|
aut_state.incoming_r
|
208
|
(*:: aut_state.incoming_s*)
|
209
|
:: node_vars_of_idents node inputs
|
210
|
in
|
211
|
let var_outputs = [ aut_state.actual_r; aut_state.actual_s ] in
|
212
|
let init_expr =
|
213
|
mkpair handler.hand_loc
|
214
|
(mkident handler.hand_loc aut_state.incoming_r.var_id)
|
215
|
(mkconst handler.hand_loc handler.hand_state)
|
216
|
in
|
217
|
(* let init_expr = mkidentpair handler.hand_loc aut_state.incoming_r.var_id
|
218
|
aut_state.incoming_s.var_id in *)
|
219
|
let expr_outputs = List.fold_right add_branch handler.hand_unless init_expr in
|
220
|
let eq_outputs =
|
221
|
Eq
|
222
|
(mkeq handler.hand_loc
|
223
|
([ aut_state.actual_r.var_id; aut_state.actual_s.var_id ], expr_outputs))
|
224
|
in
|
225
|
let node_id =
|
226
|
mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state)
|
227
|
in
|
228
|
let args =
|
229
|
List.map
|
230
|
(fun v ->
|
231
|
mkexpr handler.hand_loc
|
232
|
(Expr_when
|
233
|
( mkident handler.hand_loc v.var_id,
|
234
|
aut_state.incoming_s.var_id,
|
235
|
handler.hand_state )))
|
236
|
var_inputs
|
237
|
in
|
238
|
let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in
|
239
|
( {
|
240
|
node_id;
|
241
|
node_type = Types.new_var ();
|
242
|
node_clock = Clocks.new_var true;
|
243
|
node_inputs = List.map copy_var_decl var_inputs;
|
244
|
node_outputs = List.map copy_var_decl var_outputs;
|
245
|
node_locals = [];
|
246
|
node_gencalls = [];
|
247
|
node_checks = [];
|
248
|
node_asserts = [];
|
249
|
node_stmts = [ eq_outputs ];
|
250
|
node_dec_stateless = false;
|
251
|
node_stateless = None;
|
252
|
node_spec = None;
|
253
|
node_annot = [];
|
254
|
node_iscontract = false;
|
255
|
},
|
256
|
mkexpr handler.hand_loc
|
257
|
(Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) )
|
258
|
|
259
|
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
|
260
|
|
261
|
let rec rename_stmts_outputs frename stmts =
|
262
|
match stmts with
|
263
|
| [] ->
|
264
|
[]
|
265
|
| Eq eq :: q ->
|
266
|
let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
|
267
|
eq' :: rename_stmts_outputs frename q
|
268
|
| Aut aut :: q ->
|
269
|
let handlers' =
|
270
|
List.map
|
271
|
(fun h ->
|
272
|
{ h with hand_stmts = rename_stmts_outputs frename h.hand_stmts })
|
273
|
aut.aut_handlers
|
274
|
in
|
275
|
let aut' = Aut { aut with aut_handlers = handlers' } in
|
276
|
aut' :: rename_stmts_outputs frename q
|
277
|
|
278
|
let mk_frename used outputs =
|
279
|
let table =
|
280
|
ISet.fold
|
281
|
(fun name table -> IMap.add name (rename_output used name) table)
|
282
|
outputs IMap.empty
|
283
|
in
|
284
|
fun name -> try IMap.find name table with Not_found -> name
|
285
|
|
286
|
let node_of_assign_until nused used node aut_id aut_state handler =
|
287
|
(*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
|
288
|
let writes = handler_write ISet.empty handler in
|
289
|
let inputs =
|
290
|
ISet.diff (handler_read (until_read ISet.empty handler) handler) writes
|
291
|
in
|
292
|
let frename = mk_frename used writes in
|
293
|
let var_inputs =
|
294
|
aut_state.actual_r
|
295
|
(*:: aut_state.actual_s*)
|
296
|
:: node_vars_of_idents node inputs
|
297
|
in
|
298
|
let new_var_locals = node_vars_of_idents node writes in
|
299
|
let var_outputs =
|
300
|
List.sort IdentModule.compare (node_vars_of_idents node writes)
|
301
|
in
|
302
|
let new_var_outputs =
|
303
|
List.map
|
304
|
(fun vdecl -> { vdecl with var_id = frename vdecl.var_id })
|
305
|
var_outputs
|
306
|
in
|
307
|
let new_output_eqs =
|
308
|
List.map2
|
309
|
(fun o o' ->
|
310
|
Eq
|
311
|
(mkeq handler.hand_loc
|
312
|
([ o'.var_id ], mkident handler.hand_loc o.var_id)))
|
313
|
var_outputs new_var_outputs
|
314
|
in
|
315
|
let init_until =
|
316
|
mkpair handler.hand_loc
|
317
|
(mkconst handler.hand_loc tag_false)
|
318
|
(mkconst handler.hand_loc handler.hand_state)
|
319
|
in
|
320
|
let until_expr = List.fold_right add_branch handler.hand_until init_until in
|
321
|
let until_eq =
|
322
|
Eq
|
323
|
(mkeq handler.hand_loc
|
324
|
( [ aut_state.incoming_r.var_id; aut_state.incoming_s.var_id ],
|
325
|
until_expr ))
|
326
|
in
|
327
|
let node_id =
|
328
|
mk_new_name nused
|
329
|
(Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state)
|
330
|
in
|
331
|
let args =
|
332
|
List.map
|
333
|
(fun v ->
|
334
|
mkexpr handler.hand_loc
|
335
|
(Expr_when
|
336
|
( mkident handler.hand_loc v.var_id,
|
337
|
aut_state.actual_s.var_id,
|
338
|
handler.hand_state )))
|
339
|
var_inputs
|
340
|
in
|
341
|
let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in
|
342
|
( List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs,
|
343
|
{
|
344
|
node_id;
|
345
|
node_type = Types.new_var ();
|
346
|
node_clock = Clocks.new_var true;
|
347
|
node_inputs = List.map copy_var_decl var_inputs;
|
348
|
node_outputs =
|
349
|
List.map copy_var_decl
|
350
|
(aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
|
351
|
node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
|
352
|
node_gencalls = [];
|
353
|
node_checks = [];
|
354
|
node_asserts = handler.hand_asserts;
|
355
|
node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
|
356
|
node_dec_stateless = false;
|
357
|
node_stateless = None;
|
358
|
node_spec = None;
|
359
|
node_annot = handler.hand_annots;
|
360
|
node_iscontract = false;
|
361
|
},
|
362
|
mkexpr handler.hand_loc
|
363
|
(Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) )
|
364
|
|
365
|
let typedef_of_automata aut =
|
366
|
let tname = Format.sprintf "%s__type" aut.aut_id in
|
367
|
{
|
368
|
tydef_id = tname;
|
369
|
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers);
|
370
|
}
|
371
|
|
372
|
let expand_automata nused used owner typedef node aut =
|
373
|
let initial = (List.hd aut.aut_handlers).hand_state in
|
374
|
let aut_state =
|
375
|
mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id
|
376
|
in
|
377
|
let unodes =
|
378
|
List.map
|
379
|
(fun h -> node_of_unless nused node aut.aut_id aut_state h)
|
380
|
aut.aut_handlers
|
381
|
in
|
382
|
let aunodes =
|
383
|
List.map
|
384
|
(fun h -> node_of_assign_until nused used node aut.aut_id aut_state h)
|
385
|
aut.aut_handlers
|
386
|
in
|
387
|
let all_outputs =
|
388
|
List.fold_left
|
389
|
(fun all (outputs, _, _) -> ISet.union outputs all)
|
390
|
ISet.empty aunodes
|
391
|
in
|
392
|
let unless_handlers =
|
393
|
List.map2 (fun h (_, c) -> h.hand_state, c) aut.aut_handlers unodes
|
394
|
in
|
395
|
let unless_expr =
|
396
|
mkexpr aut.aut_loc
|
397
|
(Expr_merge (aut_state.incoming_s.var_id, unless_handlers))
|
398
|
in
|
399
|
let unless_eq =
|
400
|
mkeq aut.aut_loc
|
401
|
([ aut_state.actual_r.var_id; aut_state.actual_s.var_id ], unless_expr)
|
402
|
in
|
403
|
let assign_until_handlers =
|
404
|
List.map2 (fun h (_, _, c) -> h.hand_state, c) aut.aut_handlers aunodes
|
405
|
in
|
406
|
let assign_until_expr =
|
407
|
mkexpr aut.aut_loc
|
408
|
(Expr_merge (aut_state.actual_s.var_id, assign_until_handlers))
|
409
|
in
|
410
|
let assign_until_vars =
|
411
|
[ aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id ]
|
412
|
@ ISet.elements all_outputs
|
413
|
in
|
414
|
let assign_until_eq =
|
415
|
mkeq aut.aut_loc (assign_until_vars, assign_until_expr)
|
416
|
in
|
417
|
let fby_incoming_expr =
|
418
|
mkfby aut.aut_loc
|
419
|
(mkpair aut.aut_loc
|
420
|
(mkconst aut.aut_loc tag_false)
|
421
|
(mkconst aut.aut_loc initial))
|
422
|
(mkidentpair aut.aut_loc aut_state.incoming_r'.var_id
|
423
|
aut_state.incoming_s'.var_id)
|
424
|
in
|
425
|
let incoming_eq =
|
426
|
mkeq aut.aut_loc
|
427
|
( [ aut_state.incoming_r.var_id; aut_state.incoming_s.var_id ],
|
428
|
fby_incoming_expr )
|
429
|
in
|
430
|
let locals' = vars_of_aut_state aut_state in
|
431
|
let eqs' = [ Eq unless_eq; Eq assign_until_eq; Eq incoming_eq ] in
|
432
|
( List.map2
|
433
|
(fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n))
|
434
|
aut.aut_handlers unodes
|
435
|
@ List.map2
|
436
|
(fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n))
|
437
|
aut.aut_handlers aunodes,
|
438
|
locals',
|
439
|
eqs' )
|
440
|
|
441
|
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs)
|
442
|
stmt =
|
443
|
match stmt with
|
444
|
| Eq eq ->
|
445
|
top_types, top_nodes, locals, Eq eq :: eqs
|
446
|
| Aut aut ->
|
447
|
let typedef = typedef_of_automata aut in
|
448
|
let used' name =
|
449
|
used name || List.exists (fun v -> v.var_id = name) locals
|
450
|
in
|
451
|
let nused' name =
|
452
|
nused name
|
453
|
|| List.exists
|
454
|
(fun t ->
|
455
|
match t.top_decl_desc with
|
456
|
| ImportedNode nd ->
|
457
|
nd.nodei_id = name
|
458
|
| Node nd ->
|
459
|
nd.node_id = name
|
460
|
| _ ->
|
461
|
false)
|
462
|
top_nodes
|
463
|
in
|
464
|
let top_decls', locals', eqs' =
|
465
|
expand_automata nused' used' owner typedef node aut
|
466
|
in
|
467
|
let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
|
468
|
( top_typedef :: top_types,
|
469
|
top_decls' @ top_nodes,
|
470
|
locals' @ locals,
|
471
|
eqs' @ eqs )
|
472
|
|
473
|
let expand_node_stmts nused used loc owner node =
|
474
|
let top_types', top_nodes', locals', eqs' =
|
475
|
List.fold_left
|
476
|
(expand_node_stmt nused used owner node)
|
477
|
([], [], [], []) node.node_stmts
|
478
|
in
|
479
|
let node' =
|
480
|
{ node with node_locals = locals' @ node.node_locals; node_stmts = eqs' }
|
481
|
in
|
482
|
let top_node = mktop_decl loc owner false (Node node') in
|
483
|
top_types', top_node, top_nodes'
|
484
|
|
485
|
let rec expand_decls_rec nused top_decls =
|
486
|
match top_decls with
|
487
|
| [] ->
|
488
|
[]
|
489
|
| top_decl :: q -> (
|
490
|
match top_decl.top_decl_desc with
|
491
|
| Node nd ->
|
492
|
let used name =
|
493
|
List.exists (fun v -> v.var_id = name) nd.node_inputs
|
494
|
|| List.exists (fun v -> v.var_id = name) nd.node_outputs
|
495
|
|| List.exists (fun v -> v.var_id = name) nd.node_locals
|
496
|
in
|
497
|
let top_types', top_decl', top_nodes' =
|
498
|
expand_node_stmts nused used top_decl.top_decl_loc
|
499
|
top_decl.top_decl_owner nd
|
500
|
in
|
501
|
top_types' @ top_decl' :: expand_decls_rec nused (top_nodes' @ q)
|
502
|
| _ ->
|
503
|
top_decl :: expand_decls_rec nused q)
|
504
|
|
505
|
let expand_decls top_decls =
|
506
|
let top_names =
|
507
|
List.fold_left
|
508
|
(fun names t ->
|
509
|
match t.top_decl_desc with
|
510
|
| Node nd ->
|
511
|
ISet.add nd.node_id names
|
512
|
| ImportedNode nd ->
|
513
|
ISet.add nd.nodei_id names
|
514
|
| _ ->
|
515
|
names)
|
516
|
ISet.empty top_decls
|
517
|
in
|
518
|
let nused name = ISet.mem name top_names in
|
519
|
expand_decls_rec nused top_decls
|
520
|
|
521
|
(* Local Variables: *)
|
522
|
(* compile-command:"make -C .." *)
|
523
|
(* End: *)
|