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