lustrec / src / causality.ml @ 7d640c88
History  View  Annotate  Download (20.4 KB)
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 nomem vars. 
37 
nonmem 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 (nonmem/nonmem&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 readonly 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 
(* nomem/nomem and mem/nomem 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 *) in 
205 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
206 
let rec add_clock lhs_is_mem lhs ck g = 
207 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
208 
match (Clocks.repr ck).Clocks.cdesc with 
209 
 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) 
210 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
211 
 _ > g 
212 
in 
213 
let rec add_dep lhs_is_mem lhs rhs g = 
214 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
215 
(* i.e every input is connected to every output, through a ghost var *) 
216 
let mashup_appl_dependencies f e g = 
217 
let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in 
218 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) 
219 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
220 
in 
221 
match rhs.expr_desc with 
222 
 Expr_const _ > g 
223 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 
224 
 Expr_pre e > add_dep true lhs e g 
225 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 
226 
 Expr_access (e1, d) 
227 
 Expr_power (e1, d) > add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g) 
228 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
229 
 Expr_tuple t > List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
230 
 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) 
231 
 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)) 
232 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 
233 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 
234 
 Expr_appl (f, e, None) > 
235 
if Basic_library.is_expr_internal_fun rhs 
236 
(* tuple componentwise dependency for internal operators *) 
237 
then 
238 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 
239 
(* mashed up dependency for userdefined operators *) 
240 
else 
241 
mashup_appl_dependencies f e g 
242 
 Expr_appl (f, e, Some c) > 
243 
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) 
244 
in 
245 
let g = 
246 
List.fold_left 
247 
(fun g lhs > if ISet.mem lhs mems then add_vertices [lhs; mk_read_var lhs] g else add_vertices [lhs] g) g eq.eq_lhs in 
248 
add_dep false eq.eq_lhs eq.eq_rhs (g, g') 
249 

250  
251 
(* Returns the dependence graph for node [n] *) 
252 
let dependence_graph mems inputs node_vars n = 
253 
instance_var_cpt := 0; 
254 
let g = new_graph (), new_graph () in 
255 
(* Basic dependencies *) 
256 
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in 
257 
g 
258  
259 
end 
260  
261 
module NodeDep = struct 
262  
263 
module ExprModule = 
264 
struct 
265 
type t = expr 
266 
let compare = compare 
267 
let hash n = Hashtbl.hash n 
268 
let equal n1 n2 = n1 = n2 
269 
end 
270  
271 
module ESet = Set.Make(ExprModule) 
272  
273 
let rec get_expr_calls prednode expr = 
274 
match expr.expr_desc with 
275 
 Expr_const _ 
276 
 Expr_ident _ > ESet.empty 
277 
 Expr_access (e, _) 
278 
 Expr_power (e, _) > get_expr_calls prednode e 
279 
 Expr_array t 
280 
 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty 
281 
 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty 
282 
 Expr_fby (e1,e2) 
283 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 
284 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 
285 
 Expr_pre e 
286 
 Expr_when (e,_,_) > get_expr_calls prednode e 
287 
 Expr_appl (id,e, _) > 
288 
if not (Basic_library.is_expr_internal_fun expr) && prednode id 
289 
then ESet.add expr (get_expr_calls prednode e) 
290 
else (get_expr_calls prednode e) 
291  
292 
let get_callee expr = 
293 
match expr.expr_desc with 
294 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 
295 
 _ > None 
296  
297 
let get_calls prednode eqs = 
298 
let deps = 
299 
List.fold_left 
300 
(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs)) 
301 
ESet.empty 
302 
eqs in 
303 
ESet.elements deps 
304  
305 
let dependence_graph prog = 
306 
let g = new_graph () in 
307 
let g = List.fold_right 
308 
(fun td accu > (* for each node we add its dependencies *) 
309 
match td.top_decl_desc with 
310 
 Node nd > 
311 
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) 
312 
let accu = add_vertices [nd.node_id] accu in 
313 
let deps = List.map (fun e > fst (desome (get_callee e))) (get_calls (fun _ > true) (get_node_eqs nd)) in 
314 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
315 
add_edges [nd.node_id] deps accu 
316 
 _ > assert false (* should not happen *) 
317 

318 
) prog g in 
319 
g 
320  
321 
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) 
322 
let slice_graph gr v = 
323 
begin 
324 
let gr' = new_graph () in 
325 
IdentDepGraph.add_vertex gr' v; 
326 
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; 
327 
gr' 
328 
end 
329 

330 
let rec filter_static_inputs inputs args = 
331 
match inputs, args with 
332 
 [] , [] > [] 
333 
 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 
334 
 _ > assert false 
335  
336 
let compute_generic_calls prog = 
337 
List.iter 
338 
(fun td > 
339 
match td.top_decl_desc with 
340 
 Node nd > 
341 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
342 
nd.node_gencalls < get_calls prednode (get_node_eqs nd) 
343 
 _ > () 
344 

345 
) prog 
346  
347 
end 
348  
349 
module CycleDetection = struct 
350  
351 
(*  Look for cycles in a dependency graph *) 
352 
module Cycles = Graph.Components.Make (IdentDepGraph) 
353  
354 
let mk_copy_var n id = 
355 
let used name = 
356 
(List.exists (fun v > v.var_id = name) n.node_locals) 
357 
 (List.exists (fun v > v.var_id = name) n.node_inputs) 
358 
 (List.exists (fun v > v.var_id = name) n.node_outputs) 
359 
in mk_new_name used id 
360  
361 
let mk_copy_eq n var = 
362 
let var_decl = get_node_var var n in 
363 
let cp_var = mk_copy_var n var in 
364 
let expr = 
365 
{ expr_tag = Utils.new_tag (); 
366 
expr_desc = Expr_ident var; 
367 
expr_type = var_decl.var_type; 
368 
expr_clock = var_decl.var_clock; 
369 
expr_delay = Delay.new_var (); 
370 
expr_annot = None; 
371 
expr_loc = var_decl.var_loc } in 
372 
{ var_decl with var_id = cp_var; var_orig = false }, 
373 
mkeq var_decl.var_loc ([cp_var], expr) 
374  
375 
let wrong_partition g partition = 
376 
match partition with 
377 
 [id] > IdentDepGraph.mem_edge g id id 
378 
 _::_::_ > true 
379 
 [] > assert false 
380  
381 
(* Checks that the dependency graph [g] does not contain a cycle. Raises 
382 
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) 
383 
let check_cycles g = 
384 
let scc_l = Cycles.scc_list g in 
385 
List.iter (fun partition > 
386 
if wrong_partition g partition then 
387 
raise (Error (DataCycle partition)) 
388 
else () 
389 
) scc_l 
390  
391 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *) 
392 
let copy_partition g partition = 
393 
let copy_g = IdentDepGraph.create () in 
394 
IdentDepGraph.iter_edges 
395 
(fun src tgt > 
396 
if List.mem src partition && List.mem tgt partition 
397 
then IdentDepGraph.add_edge copy_g src tgt) 
398 
g 
399  
400 

401 
(* Breaks dependency cycles in a graph [g] by inserting aux variables. 
402 
[head] is a head of a nontrivial scc of [g]. 
403 
In Lustre, this is legal only for mem/mem cycles *) 
404 
let break_cycle head cp_head g = 
405 
let succs = IdentDepGraph.succ g head in 
406 
IdentDepGraph.add_edge g head cp_head; 
407 
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); 
408 
List.iter 
409 
(fun s > 
410 
IdentDepGraph.remove_edge g head s; 
411 
IdentDepGraph.add_edge g s cp_head) 
412 
succs 
413  
414 
(* Breaks cycles of the dependency graph [g] of memory variables [mems] 
415 
belonging in node [node]. Returns: 
416 
 a list of new auxiliary variable declarations 
417 
 a list of new equations 
418 
 a modified acyclic version of [g] 
419 
*) 
420 
let break_cycles node mems g = 
421 
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 
422 
let rec break vdecls mem_eqs g = 
423 
let scc_l = Cycles.scc_list g in 
424 
let wrong = List.filter (wrong_partition g) scc_l in 
425 
match wrong with 
426 
 [] > (vdecls, non_mem_eqs@mem_eqs, g) 
427 
 [head]::_ > 
428 
begin 
429 
IdentDepGraph.remove_edge g head head; 
430 
break vdecls mem_eqs g 
431 
end 
432 
 (head::part)::_ > 
433 
begin 
434 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in 
435 
let pvar v = List.mem v part in 
436 
let fvar v = if v = head then vdecl_cp_head.var_id else v in 
437 
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in 
438 
break_cycle head vdecl_cp_head.var_id g; 
439 
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g 
440 
end 
441 
 _ > assert false 
442 
in break [] mem_eqs g 
443  
444 
end 
445  
446 
(* Module used to compute static disjunction of variables based upon their clocks. *) 
447 
module Disjunction = 
448 
struct 
449 
module ClockedIdentModule = 
450 
struct 
451 
type t = var_decl 
452 
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock 
453 
let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id) 
454 
end 
455  
456 
module CISet = Set.Make(ClockedIdentModule) 
457  
458 
(* map: var > list of disjoint vars, sorted in increasing branch length order, 
459 
maybe removing shorter branches *) 
460 
type disjoint_map = (ident, CISet.t) Hashtbl.t 
461  
462 
let pp_ciset fmt t = 
463 
begin 
464 
Format.fprintf fmt "{@ "; 
465 
CISet.iter (fun s > Format.fprintf fmt "%a@ " Printers.pp_var_name s) t; 
466 
Format.fprintf fmt "}@." 
467 
end 
468  
469 
let clock_disjoint_map vdecls = 
470 
let map = Hashtbl.create 23 in 
471 
begin 
472 
List.iter 
473 
(fun v1 > let disj_v1 = 
474 
List.fold_left 
475 
(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res) 
476 
CISet.empty 
477 
vdecls in 
478 
(* disjoint vdecls are stored in increasing branch length order *) 
479 
Hashtbl.add map v1.var_id disj_v1) 
480 
vdecls; 
481 
(map : disjoint_map) 
482 
end 
483  
484 
(* merge variables [v] and [v'] in disjunction [map]. Then: 
485 
 the mapping v' becomes v' > (map v) inter (map v') 
486 
 the mapping v > ... then disappears 
487 
 other mappings become x > (map x) \ (if v in x then v else v') 
488 
*) 
489 
let merge_in_disjoint_map map v v' = 
490 
begin 
491 
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); 
492 
Hashtbl.remove map v.var_id; 
493 
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; 
494 
end 
495  
496 
(* replace variable [v] by [v'] in disjunction [map]. 
497 
[v'] is a dead variable. Then: 
498 
 the mapping v' becomes v' > (map v) 
499 
 the mapping v > ... then disappears 
500 
 all mappings become x > ((map x) \ { v}) union ({v'} if v in map x) 
501 
*) 
502 
let replace_in_disjoint_map map v v' = 
503 
begin 
504 
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); 
505 
Hashtbl.remove map v.var_id; 
506 
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; 
507 
end 
508  
509 
(* remove variable [v] in disjunction [map]. Then: 
510 
 the mapping v > ... then disappears 
511 
 all mappings become x > (map x) \ { v} 
512 
*) 
513 
let remove_in_disjoint_map map v = 
514 
begin 
515 
Hashtbl.remove map v.var_id; 
516 
Hashtbl.iter (fun x mapx > Hashtbl.replace map x (CISet.remove v mapx)) map; 
517 
end 
518  
519 
let pp_disjoint_map fmt map = 
520 
begin 
521 
Format.fprintf fmt "{ /* disjoint map */@."; 
522 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; 
523 
Format.fprintf fmt "}@." 
524 
end 
525 
end 
526  
527 
let pp_dep_graph fmt g = 
528 
begin 
529 
Format.fprintf fmt "{ /* graph */@."; 
530 
IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g; 
531 
Format.fprintf fmt "}@." 
532 
end 
533  
534 
let pp_error fmt err = 
535 
match err with 
536 
 DataCycle trace > 
537 
fprintf fmt "@.Causality error, cyclic data dependencies: %a@." 
538 
(fprintf_list ~sep:", " pp_print_string) trace 
539 
 NodeCycle trace > 
540 
fprintf fmt "@.Causality error, cyclic node calls: %a@." 
541 
(fprintf_list ~sep:", " pp_print_string) trace 
542  
543 
(* Merges elements of graph [g2] into graph [g1] *) 
544 
let merge_with g1 g2 = 
545 
begin 
546 
IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2; 
547 
IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2 
548 
end 
549  
550 
let world = "!!_world" 
551  
552 
let add_external_dependency outputs mems g = 
553 
begin 
554 
IdentDepGraph.add_vertex g world; 
555 
ISet.iter (fun o > IdentDepGraph.add_edge g world o) outputs; 
556 
ISet.iter (fun m > IdentDepGraph.add_edge g world m) mems; 
557 
end 
558  
559 
let global_dependency node = 
560 
let mems = ExprDep.node_memory_variables node in 
561 
let inputs = 
562 
ISet.union 
563 
(ExprDep.node_input_variables node) 
564 
(ExprDep.node_constant_variables node) in 
565 
let outputs = ExprDep.node_output_variables node in 
566 
let node_vars = ExprDep.node_variables node in 
567 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in 
568 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
569 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
570 
CycleDetection.check_cycles g_non_mems; 
571 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in 
572 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
573 
begin 
574 
merge_with g_non_mems g_mems'; 
575 
add_external_dependency outputs mems g_non_mems; 
576 
{ node with node_stmts = List.map (fun eq > Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
577 
g_non_mems 
578 
end 
579  
580 
(* Local Variables: *) 
581 
(* compilecommand:"make C .." *) 
582 
(* End: *) 