lustrec / src / causality.ml @ a1daa793
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 
 constants/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_constant_variables nd = 
137 
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 
138  
139 
let node_output_variables nd = 
140 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs 
141  
142 
let node_auxiliary_variables nd = 
143 
ISet.diff (node_local_variables nd) (node_memory_variables nd) 
144  
145 
let node_variables nd = 
146 
let inputs = node_input_variables nd in 
147 
let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in 
148 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals 
149  
150 
(* computes the equivalence relation relating variables 
151 
in the same equation lhs, under the form of a table 
152 
of class representatives *) 
153 
let node_eq_equiv nd = 
154 
let eq_equiv = Hashtbl.create 23 in 
155 
List.iter (fun eq > 
156 
let first = List.hd eq.eq_lhs in 
157 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 
158 
) 
159 
(get_node_eqs nd); 
160 
eq_equiv 
161  
162 
(* Create a tuple of right dimension, according to [expr] type, *) 
163 
(* filled with variable [v] *) 
164 
let adjust_tuple v expr = 
165 
match expr.expr_type.Types.tdesc with 
166 
 Types.Ttuple tl > duplicate v (List.length tl) 
167 
 _ > [v] 
168  
169  
170 
(* Add dependencies from lhs to rhs in [g, g'], *) 
171 
(* nomem/nomem and mem/nomem in g *) 
172 
(* mem/mem in g' *) 
173 
(* match (lhs_is_mem, ISet.mem x mems) with 
174 
 (false, true ) > (add_edges [x] lhs g, 
175 
g') 
176 
 (false, false) > (add_edges lhs [x] g, 
177 
g') 
178 
 (true , false) > (add_edges lhs [x] g, 
179 
g') 
180 
 (true , true ) > (g, 
181 
add_edges [x] lhs g') 
182 
*) 
183 
let add_eq_dependencies mems inputs node_vars eq (g, g') = 
184 
let add_var lhs_is_mem lhs x (g, g') = 
185 
if is_instance_var x  ISet.mem x node_vars then 
186 
if ISet.mem x mems 
187 
then 
188 
let g = add_edges lhs [mk_read_var x] g in 
189 
if lhs_is_mem 
190 
then 
191 
(g, add_edges [x] lhs g') 
192 
else 
193 
(add_edges [x] lhs g, g') 
194 
else 
195 
let x = if ISet.mem x inputs then mk_read_var x else x in 
196 
(add_edges lhs [x] g, g') 
197 
else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) in 
198 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
199 
let rec add_clock lhs_is_mem lhs ck g = 
200 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
201 
match (Clocks.repr ck).Clocks.cdesc with 
202 
 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) 
203 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
204 
 _ > g 
205 
in 
206 
let rec add_dep lhs_is_mem lhs rhs g = 
207 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
208 
(* i.e every input is connected to every output, through a ghost var *) 
209 
let mashup_appl_dependencies f e g = 
210 
let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in 
211 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) 
212 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
213 
in 
214 
match rhs.expr_desc with 
215 
 Expr_const _ > g 
216 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 
217 
 Expr_pre e > add_dep true lhs e g 
218 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 
219 
 Expr_access (e1, d) 
220 
 Expr_power (e1, d) > add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g) 
221 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
222 
 Expr_tuple t > List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
223 
 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) 
224 
 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)) 
225 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 
226 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 
227 
 Expr_appl (f, e, None) > 
228 
if Basic_library.is_internal_fun f 
229 
(* tuple componentwise dependency for internal operators *) 
230 
then 
231 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 
232 
(* mashed up dependency for userdefined operators *) 
233 
else 
234 
mashup_appl_dependencies f e g 
235 
 Expr_appl (f, e, Some c) > 
236 
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) 
237 
in 
238 
let g = 
239 
List.fold_left 
240 
(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 
241 
add_dep false eq.eq_lhs eq.eq_rhs (g, g') 
242 

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

311 
) prog g in 
312 
g 
313  
314 
let rec filter_static_inputs inputs args = 
315 
match inputs, args with 
316 
 [] , [] > [] 
317 
 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 
318 
 _ > assert false 
319  
320 
let compute_generic_calls prog = 
321 
List.iter 
322 
(fun td > 
323 
match td.top_decl_desc with 
324 
 Node nd > 
325 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
326 
nd.node_gencalls < get_calls prednode (get_node_eqs nd) 
327 
 _ > () 
328 

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

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