1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
|
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
|
(* This file was originally from the Prelude compiler *)
|
11
|
(* *)
|
12
|
(********************************************************************)
|
13
|
|
14
|
open Utils
|
15
|
(** Simple modular syntactic causality analysis. Can reject correct programs,
|
16
|
especially if the program is not flattened first. *)
|
17
|
|
18
|
open Lustre_types
|
19
|
open Corelang
|
20
|
|
21
|
type identified_call = eq * tag
|
22
|
|
23
|
type error =
|
24
|
| DataCycle of ident list list
|
25
|
(* multiple failed partitions at once *)
|
26
|
| NodeCycle of ident list
|
27
|
|
28
|
exception Error of error
|
29
|
|
30
|
(* Dependency of mem variables on mem variables is cut off by duplication of
|
31
|
some mem vars into local node vars. Thus, cylic dependency errors may only
|
32
|
arise between no-mem vars. non-mem variables are: - constants/inputs: not
|
33
|
needed for causality/scheduling, needed only for detecting useless vars -
|
34
|
read mems (fake vars): same remark as above. - outputs: decoupled from mems,
|
35
|
if necessary - locals - instance vars (fake vars): simplify causality
|
36
|
analysis
|
37
|
|
38
|
global constants are not part of the dependency graph.
|
39
|
|
40
|
no_mem' = combinational(no_mem, mem); => (mem -> no_mem' -> no_mem)
|
41
|
|
42
|
mem' = pre(no_mem, mem); => (mem' -> no_mem), (mem -> mem')
|
43
|
|
44
|
Global roadmap: - compute two dep graphs g (non-mem/non-mem&mem) and g'
|
45
|
(mem/mem) - check cycles in g (a cycle means a dependency error) - break
|
46
|
cycles in g' (it's legal !): - check cycles in g' - if any, introduce aux var
|
47
|
to break cycle, then start afresh - insert g' into g - return g *)
|
48
|
|
49
|
(* Tests whether [v] is a root of graph [g], i.e. a source *)
|
50
|
let is_graph_root v g = IdentDepGraph.in_degree g v = 0
|
51
|
|
52
|
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
|
53
|
let graph_roots g =
|
54
|
IdentDepGraph.fold_vertex
|
55
|
(fun v roots -> if is_graph_root v g then v :: roots else roots)
|
56
|
g []
|
57
|
|
58
|
let add_edges src tgt g =
|
59
|
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t)
|
60
|
tgt) src;*)
|
61
|
List.iter (fun s -> List.iter (IdentDepGraph.add_edge g s) tgt) src;
|
62
|
g
|
63
|
|
64
|
let add_vertices vtc g =
|
65
|
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
|
66
|
List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
|
67
|
g
|
68
|
|
69
|
let new_graph () = IdentDepGraph.create ()
|
70
|
|
71
|
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
|
72
|
let slice_graph gr v =
|
73
|
let gr' = new_graph () in
|
74
|
IdentDepGraph.add_vertex gr' v;
|
75
|
Bfs.iter_component
|
76
|
(fun v ->
|
77
|
IdentDepGraph.iter_succ
|
78
|
(fun s ->
|
79
|
IdentDepGraph.add_vertex gr' s;
|
80
|
IdentDepGraph.add_edge gr' v s)
|
81
|
gr v)
|
82
|
gr v;
|
83
|
gr'
|
84
|
|
85
|
module ExprDep = struct
|
86
|
let get_node_eqs nd =
|
87
|
let eqs, auts = get_node_eqs nd in
|
88
|
if auts != [] then assert false
|
89
|
(* No call on causality on a Lustre model with automaton. They should be
|
90
|
expanded by now. *);
|
91
|
eqs
|
92
|
|
93
|
let instance_var_cpt = ref 0
|
94
|
|
95
|
(* read vars represent input/mem read-only vars, they are not part of the
|
96
|
program/schedule, as they are not assigned, but used to compute useless
|
97
|
inputs/mems. a mem read var represents a mem at the beginning of a cycle *)
|
98
|
let mk_read_var id = Format.sprintf "#%s" id
|
99
|
|
100
|
(* instance vars represent node instance calls, they are not part of the
|
101
|
program/schedule, but used to simplify causality analysis *)
|
102
|
let mk_instance_var id =
|
103
|
incr instance_var_cpt;
|
104
|
Format.sprintf "!%s_%d" id !instance_var_cpt
|
105
|
|
106
|
let is_read_var v = v.[0] = '#'
|
107
|
|
108
|
let is_instance_var v = v.[0] = '!'
|
109
|
|
110
|
let is_ghost_var v = is_instance_var v || is_read_var v
|
111
|
|
112
|
let undo_read_var id =
|
113
|
assert (is_read_var id);
|
114
|
String.sub id 1 (String.length id - 1)
|
115
|
|
116
|
let undo_instance_var id =
|
117
|
assert (is_instance_var id);
|
118
|
String.sub id 1 (String.length id - 1)
|
119
|
|
120
|
let eq_memory_variables mems eq =
|
121
|
let rec match_mem lhs rhs mems =
|
122
|
match rhs.expr_desc with
|
123
|
| Expr_fby _ | Expr_pre _ ->
|
124
|
List.fold_right ISet.add lhs mems
|
125
|
| Expr_tuple tl ->
|
126
|
let lhs' = transpose_list [ lhs ] in
|
127
|
List.fold_right2 match_mem lhs' tl mems
|
128
|
| _ ->
|
129
|
mems
|
130
|
in
|
131
|
match_mem eq.eq_lhs eq.eq_rhs mems
|
132
|
|
133
|
let node_memory_variables nd =
|
134
|
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
|
135
|
|
136
|
let node_input_variables nd =
|
137
|
List.fold_left
|
138
|
(fun inputs v -> ISet.add v.var_id inputs)
|
139
|
ISet.empty
|
140
|
(if nd.node_iscontract then nd.node_inputs @ nd.node_outputs
|
141
|
else nd.node_inputs)
|
142
|
|
143
|
let node_output_variables nd =
|
144
|
List.fold_left
|
145
|
(fun outputs v -> ISet.add v.var_id outputs)
|
146
|
ISet.empty
|
147
|
(if nd.node_iscontract then [] else nd.node_outputs)
|
148
|
|
149
|
let node_local_variables nd =
|
150
|
List.fold_left
|
151
|
(fun locals v -> ISet.add v.var_id locals)
|
152
|
ISet.empty nd.node_locals
|
153
|
|
154
|
let node_constant_variables nd =
|
155
|
List.fold_left
|
156
|
(fun locals v ->
|
157
|
if v.var_dec_const then ISet.add v.var_id locals else locals)
|
158
|
ISet.empty nd.node_locals
|
159
|
|
160
|
let node_auxiliary_variables nd =
|
161
|
ISet.diff (node_local_variables nd) (node_memory_variables nd)
|
162
|
|
163
|
let node_variables nd =
|
164
|
let inputs = node_input_variables nd in
|
165
|
let inoutputs =
|
166
|
List.fold_left
|
167
|
(fun inoutputs v -> ISet.add v.var_id inoutputs)
|
168
|
inputs nd.node_outputs
|
169
|
in
|
170
|
List.fold_left
|
171
|
(fun vars v -> ISet.add v.var_id vars)
|
172
|
inoutputs nd.node_locals
|
173
|
|
174
|
(* computes the equivalence relation relating variables in the same equation
|
175
|
lhs, under the form of a table of class representatives *)
|
176
|
let eqs_eq_equiv eqs =
|
177
|
let eq_equiv = Hashtbl.create 23 in
|
178
|
List.iter
|
179
|
(fun eq ->
|
180
|
let first = List.hd eq.eq_lhs in
|
181
|
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs)
|
182
|
eqs;
|
183
|
eq_equiv
|
184
|
|
185
|
let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)
|
186
|
|
187
|
(* Create a tuple of right dimension, according to [expr] type, *)
|
188
|
(* filled with variable [v] *)
|
189
|
let adjust_tuple v expr =
|
190
|
match expr.expr_type.Types.tdesc with
|
191
|
| Types.Ttuple tl ->
|
192
|
duplicate v (List.length tl)
|
193
|
| _ ->
|
194
|
[ v ]
|
195
|
|
196
|
(* Add dependencies from lhs to rhs in [g, g'], *)
|
197
|
(* no-mem/no-mem and mem/no-mem in g *)
|
198
|
(* mem/mem in g' *)
|
199
|
(* match (lhs_is_mem, ISet.mem x mems) with | (false, true ) -> (add_edges [x]
|
200
|
lhs g, g') | (false, false) -> (add_edges lhs [x] g, g') | (true , false)
|
201
|
-> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs g') *)
|
202
|
let add_eq_dependencies mems inputs node_vars eq (g, g') =
|
203
|
let add_var lhs_is_mem lhs x (g, g') =
|
204
|
if is_instance_var x || ISet.mem x node_vars then
|
205
|
if ISet.mem x mems then
|
206
|
let g = add_edges lhs [ mk_read_var x ] g in
|
207
|
if lhs_is_mem then g, add_edges [ x ] lhs g'
|
208
|
else add_edges [ x ] lhs g, g'
|
209
|
else
|
210
|
let x = if ISet.mem x inputs then mk_read_var x else x in
|
211
|
add_edges lhs [ x ] g, g'
|
212
|
else add_edges lhs [ mk_read_var x ] g, g'
|
213
|
(* x is a global constant, treated as a read var *)
|
214
|
in
|
215
|
(* Add dependencies from [lhs] to rhs clock [ck]. *)
|
216
|
let rec add_clock lhs_is_mem lhs ck g =
|
217
|
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
|
218
|
match (Clocks.repr ck).Clocks.cdesc with
|
219
|
| Clocks.Con (ck', cr, _) ->
|
220
|
add_var lhs_is_mem lhs
|
221
|
(Clocks.const_of_carrier cr)
|
222
|
(add_clock lhs_is_mem lhs ck' g)
|
223
|
| Clocks.Ccarrying (_, ck') ->
|
224
|
add_clock lhs_is_mem lhs ck' g
|
225
|
| _ ->
|
226
|
g
|
227
|
in
|
228
|
let rec add_dep lhs_is_mem lhs rhs g =
|
229
|
(* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
|
230
|
(* i.e every input is connected to every output, through a ghost var *)
|
231
|
let mashup_appl_dependencies f e g =
|
232
|
let f_var =
|
233
|
mk_instance_var
|
234
|
(Format.sprintf "%s_%d" f (fst eq.eq_loc).Lexing.pos_lnum)
|
235
|
in
|
236
|
List.fold_right
|
237
|
(fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
|
238
|
(expr_list_of_expr e)
|
239
|
(add_var lhs_is_mem lhs f_var g)
|
240
|
in
|
241
|
let g = add_clock lhs_is_mem lhs rhs.expr_clock g in
|
242
|
match rhs.expr_desc with
|
243
|
| Expr_const _ ->
|
244
|
g
|
245
|
| Expr_fby (e1, e2) ->
|
246
|
add_dep true lhs e2 (add_dep false lhs e1 g)
|
247
|
| Expr_pre e ->
|
248
|
add_dep true lhs e g
|
249
|
| Expr_ident x ->
|
250
|
add_var lhs_is_mem lhs x g
|
251
|
| Expr_access (e1, d) | Expr_power (e1, d) ->
|
252
|
add_dep lhs_is_mem lhs e1
|
253
|
(add_dep lhs_is_mem lhs (expr_of_dimension d) g)
|
254
|
| Expr_array a ->
|
255
|
List.fold_right (add_dep lhs_is_mem lhs) a g
|
256
|
| Expr_tuple t ->
|
257
|
List.fold_right2 (fun l r -> add_dep lhs_is_mem [ l ] r) lhs t g
|
258
|
| Expr_merge (c, hl) ->
|
259
|
add_var lhs_is_mem lhs c
|
260
|
(List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
|
261
|
| Expr_ite (c, t, e) ->
|
262
|
add_dep lhs_is_mem lhs c
|
263
|
(add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))
|
264
|
| Expr_arrow (e1, e2) ->
|
265
|
add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
|
266
|
| Expr_when (e, c, _) ->
|
267
|
add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
|
268
|
| Expr_appl (f, e, None) ->
|
269
|
if
|
270
|
Basic_library.is_expr_internal_fun rhs
|
271
|
(* tuple component-wise dependency for internal operators *)
|
272
|
then List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
|
273
|
(* mashed up dependency for user-defined operators *)
|
274
|
else mashup_appl_dependencies f e g
|
275
|
| Expr_appl (f, e, Some c) ->
|
276
|
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
|
277
|
in
|
278
|
let g =
|
279
|
List.fold_left
|
280
|
(fun g lhs ->
|
281
|
if ISet.mem lhs mems then add_vertices [ lhs; mk_read_var lhs ] g
|
282
|
else add_vertices [ lhs ] g)
|
283
|
g eq.eq_lhs
|
284
|
in
|
285
|
add_dep false eq.eq_lhs eq.eq_rhs (g, g')
|
286
|
|
287
|
(* Returns the dependence graph for node [n] *)
|
288
|
let dependence_graph mems inputs node_vars n =
|
289
|
instance_var_cpt := 0;
|
290
|
let g = new_graph (), new_graph () in
|
291
|
(* Basic dependencies *)
|
292
|
let g =
|
293
|
List.fold_right
|
294
|
(add_eq_dependencies mems inputs node_vars)
|
295
|
(get_node_eqs n) g
|
296
|
in
|
297
|
|
298
|
(* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
|
299
|
faut imposer que les outputs dépendent des asserts pour identifier que
|
300
|
les fcn calls des asserts sont évalués avant le noeuds *)
|
301
|
|
302
|
(* (\* In order to introduce dependencies between assert expressions and the
|
303
|
node, *)
|
304
|
(* we build an artificial dependency between node output and each assert *)
|
305
|
(* expr. While these are not valid equations, they should properly propage
|
306
|
in *)
|
307
|
(* function add_eq_dependencies *\) *)
|
308
|
(* let g = *)
|
309
|
(* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
|
310
|
(* List.fold_left (fun g ae -> *)
|
311
|
(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs,
|
312
|
ae.assert_expr) in *)
|
313
|
(* add_eq_dependencies mems inputs node_vars fake_eq g *)
|
314
|
(* ) g n.node_asserts in *)
|
315
|
g
|
316
|
end
|
317
|
|
318
|
module NodeDep = struct
|
319
|
module ExprModule = struct
|
320
|
type t = expr
|
321
|
|
322
|
let compare = compare
|
323
|
|
324
|
let hash n = Hashtbl.hash n
|
325
|
|
326
|
let equal n1 n2 = n1 = n2
|
327
|
end
|
328
|
|
329
|
module ESet = Set.Make (ExprModule)
|
330
|
|
331
|
let rec get_expr_calls prednode expr =
|
332
|
match expr.expr_desc with
|
333
|
| Expr_const _ | Expr_ident _ ->
|
334
|
ESet.empty
|
335
|
| Expr_access (e, _) | Expr_power (e, _) ->
|
336
|
get_expr_calls prednode e
|
337
|
| Expr_array t | Expr_tuple t ->
|
338
|
List.fold_right
|
339
|
(fun x set -> ESet.union (get_expr_calls prednode x) set)
|
340
|
t ESet.empty
|
341
|
| Expr_merge (_, hl) ->
|
342
|
List.fold_right
|
343
|
(fun (_, h) set -> ESet.union (get_expr_calls prednode h) set)
|
344
|
hl ESet.empty
|
345
|
| Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
|
346
|
ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
|
347
|
| Expr_ite (c, t, e) ->
|
348
|
ESet.union
|
349
|
(get_expr_calls prednode c)
|
350
|
(ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
|
351
|
| Expr_pre e | Expr_when (e, _, _) ->
|
352
|
get_expr_calls prednode e
|
353
|
| Expr_appl (id, e, _) ->
|
354
|
if (not (Basic_library.is_expr_internal_fun expr)) && prednode id then
|
355
|
ESet.add expr (get_expr_calls prednode e)
|
356
|
else get_expr_calls prednode e
|
357
|
|
358
|
let get_eexpr_calls prednode ee = get_expr_calls prednode ee.eexpr_qfexpr
|
359
|
|
360
|
let get_callee expr =
|
361
|
match expr.expr_desc with
|
362
|
| Expr_appl (id, args, _) ->
|
363
|
Some (id, expr_list_of_expr args)
|
364
|
| _ ->
|
365
|
None
|
366
|
|
367
|
let accu f init objl =
|
368
|
List.fold_left (fun accu o -> ESet.union accu (f o)) init objl
|
369
|
|
370
|
let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs
|
371
|
|
372
|
let rec get_stmt_calls prednode s =
|
373
|
match s with
|
374
|
| Eq eq ->
|
375
|
get_eq_calls prednode eq
|
376
|
| Aut aut ->
|
377
|
get_aut_calls prednode aut
|
378
|
|
379
|
and get_aut_calls prednode aut =
|
380
|
let get_handler_calls prednode h =
|
381
|
let get_cond_calls c =
|
382
|
accu (fun (_, e, _, _) -> get_expr_calls prednode e) ESet.empty c
|
383
|
in
|
384
|
let until = get_cond_calls h.hand_until in
|
385
|
let unless = get_cond_calls h.hand_unless in
|
386
|
let calls = ESet.union until unless in
|
387
|
let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in
|
388
|
let calls =
|
389
|
accu
|
390
|
(fun a -> get_expr_calls prednode a.assert_expr)
|
391
|
calls h.hand_asserts
|
392
|
in
|
393
|
(* let calls = accu xx calls h.hand_annots in *)
|
394
|
(* TODO: search for calls in eexpr *)
|
395
|
calls
|
396
|
in
|
397
|
accu (get_handler_calls prednode) ESet.empty aut.aut_handlers
|
398
|
|
399
|
let get_calls prednode nd =
|
400
|
let eqs, auts = get_node_eqs nd in
|
401
|
let deps = accu (get_eq_calls prednode) ESet.empty eqs in
|
402
|
let deps = accu (get_aut_calls prednode) deps auts in
|
403
|
ESet.elements deps
|
404
|
|
405
|
let get_contract_calls prednode c =
|
406
|
let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in
|
407
|
let deps =
|
408
|
accu (get_eexpr_calls prednode) deps
|
409
|
(c.assume @ c.guarantees
|
410
|
@ List.fold_left (fun accu m -> accu @ m.require @ m.ensure) [] c.modes
|
411
|
)
|
412
|
in
|
413
|
let id_deps =
|
414
|
List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps)
|
415
|
in
|
416
|
let id_deps =
|
417
|
List.fold_left (fun accu imp -> imp.import_nodeid :: accu) [] c.imports
|
418
|
@ id_deps
|
419
|
in
|
420
|
id_deps
|
421
|
|
422
|
let dependence_graph prog =
|
423
|
let g = new_graph () in
|
424
|
let g =
|
425
|
List.fold_right
|
426
|
(fun td accu ->
|
427
|
(* for each node we add its dependencies *)
|
428
|
match td.top_decl_desc with
|
429
|
| Node nd ->
|
430
|
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
|
431
|
let accu = add_vertices [ nd.node_id ] accu in
|
432
|
let deps =
|
433
|
List.map
|
434
|
(fun e -> fst (desome (get_callee e)))
|
435
|
(get_calls (fun _ -> true) nd)
|
436
|
in
|
437
|
(* Adding assert expressions deps *)
|
438
|
let deps_asserts =
|
439
|
let prednode _ = true in
|
440
|
(* what is this about? *)
|
441
|
List.map
|
442
|
(fun e -> fst (desome (get_callee e)))
|
443
|
(ESet.elements
|
444
|
(List.fold_left
|
445
|
(fun accu assert_expr ->
|
446
|
ESet.union accu (get_expr_calls prednode assert_expr))
|
447
|
ESet.empty
|
448
|
(List.map
|
449
|
(fun _assert -> _assert.assert_expr)
|
450
|
nd.node_asserts)))
|
451
|
in
|
452
|
let deps_spec =
|
453
|
match nd.node_spec with
|
454
|
| None ->
|
455
|
[]
|
456
|
| Some (NodeSpec id) ->
|
457
|
[ id ]
|
458
|
| Some (Contract c) ->
|
459
|
get_contract_calls (fun _ -> true) c
|
460
|
in
|
461
|
|
462
|
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@."
|
463
|
Format.pp_print_string) deps; *)
|
464
|
add_edges [ nd.node_id ] (deps @ deps_asserts @ deps_spec) accu
|
465
|
| _ ->
|
466
|
assert false
|
467
|
(* should not happen *))
|
468
|
prog g
|
469
|
in
|
470
|
g
|
471
|
|
472
|
let rec filter_static_inputs inputs args =
|
473
|
match inputs, args with
|
474
|
| [], [] ->
|
475
|
[]
|
476
|
| v :: vq, a :: aq ->
|
477
|
if v.var_dec_const && Types.is_dimension_type v.var_type then
|
478
|
dimension_of_expr a :: filter_static_inputs vq aq
|
479
|
else filter_static_inputs vq aq
|
480
|
| _ ->
|
481
|
assert false
|
482
|
|
483
|
let compute_generic_calls prog =
|
484
|
List.iter
|
485
|
(fun td ->
|
486
|
match td.top_decl_desc with
|
487
|
| Node nd ->
|
488
|
let prednode n = is_generic_node (node_from_name n) in
|
489
|
nd.node_gencalls <- get_calls prednode nd
|
490
|
| _ ->
|
491
|
())
|
492
|
prog
|
493
|
end
|
494
|
|
495
|
module CycleDetection = struct
|
496
|
(* ---- Look for cycles in a dependency graph *)
|
497
|
module Cycles = Graph.Components.Make (IdentDepGraph)
|
498
|
|
499
|
let mk_copy_var n id =
|
500
|
let used name =
|
501
|
List.exists (fun v -> v.var_id = name) n.node_locals
|
502
|
|| List.exists (fun v -> v.var_id = name) n.node_inputs
|
503
|
|| List.exists (fun v -> v.var_id = name) n.node_outputs
|
504
|
in
|
505
|
mk_new_name used id
|
506
|
|
507
|
let mk_copy_eq n var =
|
508
|
let var_decl = get_node_var var n in
|
509
|
let cp_var = mk_copy_var n var in
|
510
|
let expr =
|
511
|
{
|
512
|
expr_tag = Utils.new_tag ();
|
513
|
expr_desc = Expr_ident var;
|
514
|
expr_type = var_decl.var_type;
|
515
|
expr_clock = var_decl.var_clock;
|
516
|
expr_delay = Delay.new_var ();
|
517
|
expr_annot = None;
|
518
|
expr_loc = var_decl.var_loc;
|
519
|
}
|
520
|
in
|
521
|
( { var_decl with var_id = cp_var; var_orig = false },
|
522
|
mkeq var_decl.var_loc ([ cp_var ], expr) )
|
523
|
|
524
|
let wrong_partition g partition =
|
525
|
match partition with
|
526
|
| [ id ] ->
|
527
|
IdentDepGraph.mem_edge g id id
|
528
|
| _ :: _ :: _ ->
|
529
|
true
|
530
|
| [] ->
|
531
|
assert false
|
532
|
|
533
|
(* Checks that the dependency graph [g] does not contain a cycle. Raises
|
534
|
[Cycle partition] if the succession of dependencies [partition] forms a
|
535
|
cycle *)
|
536
|
let check_cycles g =
|
537
|
let scc_l = Cycles.scc_list g in
|
538
|
let algebraic_loops = List.filter (wrong_partition g) scc_l in
|
539
|
if List.length algebraic_loops > 0 then
|
540
|
raise (Error (DataCycle algebraic_loops))
|
541
|
(* We extract a hint to resolve the cycle: for each variable in the cycle
|
542
|
which is defined by a call, we return the name of the node call and its
|
543
|
specific id *)
|
544
|
|
545
|
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
|
546
|
let copy_partition g partition =
|
547
|
let copy_g = IdentDepGraph.create () in
|
548
|
IdentDepGraph.iter_edges
|
549
|
(fun src tgt ->
|
550
|
if List.mem src partition && List.mem tgt partition then
|
551
|
IdentDepGraph.add_edge copy_g src tgt)
|
552
|
g
|
553
|
|
554
|
(* Breaks dependency cycles in a graph [g] by inserting aux variables. [head]
|
555
|
is a head of a non-trivial scc of [g]. In Lustre, this is legal only for
|
556
|
mem/mem cycles *)
|
557
|
let break_cycle head cp_head g =
|
558
|
let succs = IdentDepGraph.succ g head in
|
559
|
IdentDepGraph.add_edge g head cp_head;
|
560
|
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
|
561
|
List.iter
|
562
|
(fun s ->
|
563
|
IdentDepGraph.remove_edge g head s;
|
564
|
IdentDepGraph.add_edge g s cp_head)
|
565
|
succs
|
566
|
|
567
|
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
|
568
|
belonging in node [node]. Returns: - a list of new auxiliary variable
|
569
|
declarations - a list of new equations - a modified acyclic version of [g] *)
|
570
|
let break_cycles node mems g =
|
571
|
let eqs, auts = get_node_eqs node in
|
572
|
assert (auts = []);
|
573
|
(* TODO: check: For the moment we assume that auts are expanded by now *)
|
574
|
let mem_eqs, non_mem_eqs =
|
575
|
List.partition
|
576
|
(fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs)
|
577
|
eqs
|
578
|
in
|
579
|
let rec break vdecls mem_eqs g =
|
580
|
let scc_l = Cycles.scc_list g in
|
581
|
let wrong = List.filter (wrong_partition g) scc_l in
|
582
|
match wrong with
|
583
|
| [] ->
|
584
|
vdecls, non_mem_eqs @ mem_eqs, g
|
585
|
| [ head ] :: _ ->
|
586
|
IdentDepGraph.remove_edge g head head;
|
587
|
break vdecls mem_eqs g
|
588
|
| (head :: part) :: _ ->
|
589
|
let vdecl_cp_head, cp_eq = mk_copy_eq node head in
|
590
|
let pvar v = List.mem v part in
|
591
|
let fvar v = if v = head then vdecl_cp_head.var_id else v in
|
592
|
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
|
593
|
break_cycle head vdecl_cp_head.var_id g;
|
594
|
break (vdecl_cp_head :: vdecls) (cp_eq :: mem_eqs') g
|
595
|
| _ ->
|
596
|
assert false
|
597
|
in
|
598
|
break [] mem_eqs g
|
599
|
end
|
600
|
|
601
|
(* Module used to compute static disjunction of variables based upon their
|
602
|
clocks. *)
|
603
|
module Disjunction = struct
|
604
|
module ClockedIdentModule = struct
|
605
|
type t = var_decl
|
606
|
|
607
|
let root_branch vdecl =
|
608
|
Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
|
609
|
|
610
|
let compare v1 v2 =
|
611
|
compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
|
612
|
end
|
613
|
|
614
|
module CISet = Set.Make (ClockedIdentModule)
|
615
|
|
616
|
(* map: var |-> list of disjoint vars, sorted in increasing branch length
|
617
|
order, maybe removing shorter branches *)
|
618
|
type disjoint_map = (ident, CISet.t) Hashtbl.t
|
619
|
|
620
|
let pp_ciset fmt t =
|
621
|
let open Format in
|
622
|
pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt
|
623
|
(CISet.elements t)
|
624
|
|
625
|
let clock_disjoint_map vdecls =
|
626
|
let map = Hashtbl.create 23 in
|
627
|
List.iter
|
628
|
(fun v1 ->
|
629
|
let disj_v1 =
|
630
|
List.fold_left
|
631
|
(fun res v2 ->
|
632
|
if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res
|
633
|
else res)
|
634
|
CISet.empty vdecls
|
635
|
in
|
636
|
(* disjoint vdecls are stored in increasing branch length order *)
|
637
|
Hashtbl.add map v1.var_id disj_v1)
|
638
|
vdecls;
|
639
|
(map : disjoint_map)
|
640
|
|
641
|
(* merge variables [v] and [v'] in disjunction [map]. Then: - the mapping v'
|
642
|
becomes v' |-> (map v) inter (map v') - the mapping v |-> ... then
|
643
|
disappears - other mappings become x |-> (map x) \ (if v in x then v else
|
644
|
v') *)
|
645
|
let merge_in_disjoint_map map v v' =
|
646
|
Hashtbl.replace map v'.var_id
|
647
|
(CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
|
648
|
Hashtbl.remove map v.var_id;
|
649
|
Hashtbl.iter
|
650
|
(fun x map_x ->
|
651
|
Hashtbl.replace map x
|
652
|
(CISet.remove (if CISet.mem v map_x then v else v') map_x))
|
653
|
map
|
654
|
|
655
|
(* replace variable [v] by [v'] in disjunction [map]. [v'] is a dead variable.
|
656
|
Then: - the mapping v' becomes v' |-> (map v) - the mapping v |-> ... then
|
657
|
disappears - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in
|
658
|
map x) *)
|
659
|
let replace_in_disjoint_map map v v' =
|
660
|
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
|
661
|
Hashtbl.remove map v.var_id;
|
662
|
Hashtbl.iter
|
663
|
(fun x mapx ->
|
664
|
Hashtbl.replace map x
|
665
|
(if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx)
|
666
|
else CISet.remove v' mapx))
|
667
|
map
|
668
|
|
669
|
(* remove variable [v] in disjunction [map]. Then: - the mapping v |-> ...
|
670
|
then disappears - all mappings become x |-> (map x) \ { v} *)
|
671
|
let remove_in_disjoint_map map v =
|
672
|
Hashtbl.remove map v.var_id;
|
673
|
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map
|
674
|
|
675
|
let pp_disjoint_map fmt map =
|
676
|
Format.(
|
677
|
fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }" (fun fmt ->
|
678
|
Hashtbl.iter
|
679
|
(fun k v ->
|
680
|
fprintf fmt "@,%s # %a" k
|
681
|
(pp_print_braced' Printers.pp_var_name)
|
682
|
(CISet.elements v))
|
683
|
map))
|
684
|
end
|
685
|
|
686
|
let pp_dep_graph fmt g =
|
687
|
Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]" (fun fmt ->
|
688
|
IdentDepGraph.iter_edges
|
689
|
(fun s t -> Format.fprintf fmt "@ %s -> %s" s t)
|
690
|
g)
|
691
|
|
692
|
let pp_error fmt err =
|
693
|
match err with
|
694
|
| NodeCycle trace ->
|
695
|
Format.(fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ "
|
696
|
(pp_comma_list Format.pp_print_string) trace)
|
697
|
| DataCycle traces ->
|
698
|
Format.(fprintf fmt
|
699
|
"Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ "
|
700
|
(pp_print_list ~pp_sep:pp_print_semicolon (fun fmt trace ->
|
701
|
fprintf fmt "@[<v 0>{%a}@]"
|
702
|
(pp_comma_list Format.pp_print_string) trace))
|
703
|
traces)
|
704
|
|
705
|
(* Merges elements of graph [g2] into graph [g1] *)
|
706
|
let merge_with g1 g2 =
|
707
|
IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
|
708
|
IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
|
709
|
|
710
|
let world = "!!_world"
|
711
|
|
712
|
let add_external_dependency outputs mems g =
|
713
|
IdentDepGraph.add_vertex g world;
|
714
|
ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
|
715
|
ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems
|
716
|
|
717
|
(* Takes a node and return a pair (node', graph) where node' is node rebuilt
|
718
|
with the equations enriched with new ones introduced to "break cycles" *)
|
719
|
let global_dependency node =
|
720
|
let mems = ExprDep.node_memory_variables node in
|
721
|
let inputs =
|
722
|
ISet.union
|
723
|
(ExprDep.node_input_variables node)
|
724
|
(ExprDep.node_constant_variables node)
|
725
|
in
|
726
|
let outputs = ExprDep.node_output_variables node in
|
727
|
let node_vars = ExprDep.node_variables node in
|
728
|
let g_non_mems, g_mems =
|
729
|
ExprDep.dependence_graph mems inputs node_vars node
|
730
|
in
|
731
|
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; Format.eprintf
|
732
|
"g_mems: %a" pp_dep_graph g_mems;*)
|
733
|
try
|
734
|
CycleDetection.check_cycles g_non_mems;
|
735
|
let vdecls', eqs', g_mems' = CycleDetection.break_cycles node mems g_mems in
|
736
|
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
|
737
|
merge_with g_non_mems g_mems';
|
738
|
add_external_dependency outputs mems g_non_mems;
|
739
|
( {
|
740
|
node with
|
741
|
node_stmts = List.map (fun eq -> Eq eq) eqs';
|
742
|
node_locals = vdecls' @ node.node_locals;
|
743
|
},
|
744
|
g_non_mems )
|
745
|
with Error (DataCycle _ as exc) -> raise (Error exc)
|
746
|
|
747
|
(* A module to sort dependencies among local variables when relying on clocked
|
748
|
declarations *)
|
749
|
module VarClockDep = struct
|
750
|
let rec get_clock_dep ck =
|
751
|
match ck.Clocks.cdesc with
|
752
|
| Clocks.Con (ck, _, l) ->
|
753
|
l :: get_clock_dep ck
|
754
|
| Clocks.Clink ck' | Clocks.Ccarrying (_, ck') ->
|
755
|
get_clock_dep ck'
|
756
|
| _ ->
|
757
|
[]
|
758
|
|
759
|
let sort locals =
|
760
|
let g = new_graph () in
|
761
|
let g =
|
762
|
List.fold_left
|
763
|
(fun g var_decl ->
|
764
|
let deps = get_clock_dep var_decl.var_clock in
|
765
|
add_edges [ var_decl.var_id ] deps g)
|
766
|
g locals
|
767
|
in
|
768
|
let sorted, no_deps =
|
769
|
TopologicalDepGraph.fold
|
770
|
(fun vid (accu, remaining) ->
|
771
|
let select v = v.var_id = vid in
|
772
|
let selected, not_selected = List.partition select remaining in
|
773
|
selected @ accu, not_selected)
|
774
|
g ([], locals)
|
775
|
in
|
776
|
no_deps @ sorted
|
777
|
end
|
778
|
|
779
|
(* Local Variables: *)
|
780
|
(* compile-command:"make -C .." *)
|
781
|
(* End: *)
|