lustrec / src / causality.ml @ 6a1a01d2
History  View  Annotate  Download (19.7 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 
exception Cycle of ident list 
24  
25 
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule) 
26  
27 
(* Dependency of mem variables on mem variables is cut off 
28 
by duplication of some mem vars into local node vars. 
29 
Thus, cylic dependency errors may only arise between nomem vars. 
30 
nonmem variables are: 
31 
 inputs: not needed for causality/scheduling, needed only for detecting useless vars 
32 
 read mems (fake vars): same remark as above. 
33 
 outputs: decoupled from mems, if necessary 
34 
 locals 
35 
 instance vars (fake vars): simplify causality analysis 
36  
37 
global constants are not part of the dependency graph. 
38  
39 
no_mem' = combinational(no_mem, mem); 
40 
=> (mem > no_mem' > no_mem) 
41  
42 
mem' = pre(no_mem, mem); 
43 
=> (mem' > no_mem), (mem > mem') 
44  
45 
Global roadmap: 
46 
 compute two dep graphs g (nonmem/nonmem&mem) and g' (mem/mem) 
47 
 check cycles in g (a cycle means a dependency error) 
48 
 break cycles in g' (it's legal !): 
49 
 check cycles in g' 
50 
 if any, introduce aux var to break cycle, then start afresh 
51 
 insert g' into g 
52 
 return g 
53 
*) 
54  
55 
(* Tests whether [v] is a root of graph [g], i.e. a source *) 
56 
let is_graph_root v g = 
57 
IdentDepGraph.in_degree g v = 0 
58  
59 
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) 
60 
let graph_roots g = 
61 
IdentDepGraph.fold_vertex 
62 
(fun v roots > if is_graph_root v g then v::roots else roots) 
63 
g [] 
64  
65 
let add_edges src tgt g = 
66 
(*List.iter (fun s > List.iter (fun t > Format.eprintf "add %s > %s@." s t) tgt) src;*) 
67 
List.iter 
68 
(fun s > 
69 
List.iter 
70 
(fun t > IdentDepGraph.add_edge g s t) 
71 
tgt) 
72 
src; 
73 
g 
74  
75 
let add_vertices vtc g = 
76 
(*List.iter (fun t > Format.eprintf "add %s@." t) vtc;*) 
77 
List.iter (fun v > IdentDepGraph.add_vertex g v) vtc; 
78 
g 
79  
80 
let new_graph () = 
81 
IdentDepGraph.create () 
82  
83 
module ExprDep = struct 
84  
85 
let instance_var_cpt = ref 0 
86  
87 
(* read vars represent input/mem readonly vars, 
88 
they are not part of the program/schedule, 
89 
as they are not assigned, 
90 
but used to compute useless inputs/mems. 
91 
a mem read var represents a mem at the beginning of a cycle *) 
92 
let mk_read_var id = 
93 
sprintf "#%s" id 
94  
95 
(* instance vars represent node instance calls, 
96 
they are not part of the program/schedule, 
97 
but used to simplify causality analysis 
98 
*) 
99 
let mk_instance_var id = 
100 
incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt 
101  
102 
let is_read_var v = v.[0] = '#' 
103  
104 
let is_instance_var v = v.[0] = '!' 
105  
106 
let is_ghost_var v = is_instance_var v  is_read_var v 
107  
108 
let undo_read_var id = 
109 
assert (is_read_var id); 
110 
String.sub id 1 (String.length id  1) 
111  
112 
let undo_instance_var id = 
113 
assert (is_instance_var id); 
114 
String.sub id 1 (String.length id  1) 
115  
116 
let eq_memory_variables mems eq = 
117 
let rec match_mem lhs rhs mems = 
118 
match rhs.expr_desc with 
119 
 Expr_fby _ 
120 
 Expr_pre _ > List.fold_right ISet.add lhs mems 
121 
 Expr_tuple tl > 
122 
let lhs' = (transpose_list [lhs]) in 
123 
List.fold_right2 match_mem lhs' tl mems 
124 
 _ > mems in 
125 
match_mem eq.eq_lhs eq.eq_rhs mems 
126  
127 
let node_memory_variables nd = 
128 
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd) 
129  
130 
let node_input_variables nd = 
131 
List.fold_left (fun inputs v > ISet.add v.var_id inputs) ISet.empty nd.node_inputs 
132  
133 
let node_local_variables nd = 
134 
List.fold_left (fun locals v > ISet.add v.var_id locals) ISet.empty nd.node_locals 
135  
136 
let node_output_variables nd = 
137 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs 
138  
139 
let node_auxiliary_variables nd = 
140 
ISet.diff (node_local_variables nd) (node_memory_variables nd) 
141  
142 
let node_variables nd = 
143 
let inputs = node_input_variables nd in 
144 
let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in 
145 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals 
146  
147 
(* computes the equivalence relation relating variables 
148 
in the same equation lhs, under the form of a table 
149 
of class representatives *) 
150 
let node_eq_equiv nd = 
151 
let eq_equiv = Hashtbl.create 23 in 
152 
List.iter (fun eq > 
153 
let first = List.hd eq.eq_lhs in 
154 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 
155 
) 
156 
(get_node_eqs nd); 
157 
eq_equiv 
158  
159 
(* Create a tuple of right dimension, according to [expr] type, *) 
160 
(* filled with variable [v] *) 
161 
let adjust_tuple v expr = 
162 
match expr.expr_type.Types.tdesc with 
163 
 Types.Ttuple tl > duplicate v (List.length tl) 
164 
 _ > [v] 
165  
166  
167 
(* Add dependencies from lhs to rhs in [g, g'], *) 
168 
(* nomem/nomem and mem/nomem in g *) 
169 
(* mem/mem in g' *) 
170 
(* match (lhs_is_mem, ISet.mem x mems) with 
171 
 (false, true ) > (add_edges [x] lhs g, 
172 
g') 
173 
 (false, false) > (add_edges lhs [x] g, 
174 
g') 
175 
 (true , false) > (add_edges lhs [x] g, 
176 
g') 
177 
 (true , true ) > (g, 
178 
add_edges [x] lhs g') 
179 
*) 
180 
let add_eq_dependencies mems inputs node_vars eq (g, g') = 
181 
let add_var lhs_is_mem lhs x (g, g') = 
182 
if is_instance_var x  ISet.mem x node_vars then 
183 
if ISet.mem x mems 
184 
then 
185 
let g = add_edges lhs [mk_read_var x] g in 
186 
if lhs_is_mem 
187 
then 
188 
(g, add_edges [x] lhs g') 
189 
else 
190 
(add_edges [x] lhs g, g') 
191 
else 
192 
let x = if ISet.mem x inputs then mk_read_var x else x in 
193 
(add_edges lhs [x] g, g') 
194 
else (g, g') in 
195 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
196 
let rec add_clock lhs_is_mem lhs ck g = 
197 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
198 
match (Clocks.repr ck).Clocks.cdesc with 
199 
 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) 
200 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
201 
 _ > g 
202 
in 
203 
let rec add_dep lhs_is_mem lhs rhs g = 
204 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
205 
(* i.e every input is connected to every output, through a ghost var *) 
206 
let mashup_appl_dependencies f e g = 
207 
let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in 
208 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) 
209 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
210 
in 
211 
match rhs.expr_desc with 
212 
 Expr_const _ > g 
213 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 
214 
 Expr_pre e > add_dep true lhs e g 
215 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 
216 
 Expr_access (e1, _) 
217 
 Expr_power (e1, _) > add_dep lhs_is_mem lhs e1 g 
218 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
219 
 Expr_tuple t > 
220 
(* 
221 
if List.length t <> List.length lhs then ( 
222 
match lhs with 
223 
 [l] > List.fold_right (fun r > add_dep lhs_is_mem [l] r) t g 
224 
 _ > 
225 
Format.eprintf "Incompatible tuple assign: %a (%i) vs %a (%i)@.@?" 
226 
(Utils.fprintf_list ~sep:"," (Format.pp_print_string)) lhs 
227 
(List.length lhs) 
228 
Printers.pp_expr rhs 
229 
(List.length t) 
230 
; 
231 
assert false 
232 
) 
233 
else 
234 
*) 
235 
List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
236 
 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) 
237 
 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)) 
238 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 
239 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 
240 
 Expr_appl (f, e, None) > 
241 
if Basic_library.is_internal_fun f 
242 
(* tuple componentwise dependency for internal operators *) 
243 
then 
244 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 
245 
(* mashed up dependency for userdefined operators *) 
246 
else 
247 
mashup_appl_dependencies f e g 
248 
 Expr_appl (f, e, Some c) > 
249 
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) 
250 
in 
251 
let g = 
252 
List.fold_left 
253 
(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 
254 
add_dep false eq.eq_lhs eq.eq_rhs (g, g') 
255 

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

324 
) prog g in 
325 
g 
326  
327 
let rec filter_static_inputs inputs args = 
328 
match inputs, args with 
329 
 [] , [] > [] 
330 
 v::vq, a::aq > if v.var_dec_const then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq 
331 
 _ > assert false 
332  
333 
let compute_generic_calls prog = 
334 
List.iter 
335 
(fun td > 
336 
match td.top_decl_desc with 
337 
 Node nd > 
338 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
339 
nd.node_gencalls < get_calls prednode (get_node_eqs nd) 
340 
 _ > () 
341 

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

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