lustrec / src / causality.ml @ 2823bc51
History  View  Annotate  Download (21.2 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 *) 
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 userdefined 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 componentwise 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 userdefined 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 (fun e > fst (desome (get_callee e))) (get_calls (fun _ > true) (get_node_eqs nd)) in 
336 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
337 
add_edges [nd.node_id] deps accu 
338 
 _ > assert false (* should not happen *) 
339 

340 
) prog g in 
341 
g 
342  
343 
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) 
344 
let slice_graph gr v = 
345 
begin 
346 
let gr' = new_graph () in 
347 
IdentDepGraph.add_vertex gr' v; 
348 
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; 
349 
gr' 
350 
end 
351 

352 
let rec filter_static_inputs inputs args = 
353 
match inputs, args with 
354 
 [] , [] > [] 
355 
 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 
356 
 _ > assert false 
357  
358 
let compute_generic_calls prog = 
359 
List.iter 
360 
(fun td > 
361 
match td.top_decl_desc with 
362 
 Node nd > 
363 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
364 
nd.node_gencalls < get_calls prednode (get_node_eqs nd) 
365 
 _ > () 
366 

367 
) prog 
368  
369 
end 
370  
371 
module CycleDetection = struct 
372  
373 
(*  Look for cycles in a dependency graph *) 
374 
module Cycles = Graph.Components.Make (IdentDepGraph) 
375  
376 
let mk_copy_var n id = 
377 
let used name = 
378 
(List.exists (fun v > v.var_id = name) n.node_locals) 
379 
 (List.exists (fun v > v.var_id = name) n.node_inputs) 
380 
 (List.exists (fun v > v.var_id = name) n.node_outputs) 
381 
in mk_new_name used id 
382  
383 
let mk_copy_eq n var = 
384 
let var_decl = get_node_var var n in 
385 
let cp_var = mk_copy_var n var in 
386 
let expr = 
387 
{ expr_tag = Utils.new_tag (); 
388 
expr_desc = Expr_ident var; 
389 
expr_type = var_decl.var_type; 
390 
expr_clock = var_decl.var_clock; 
391 
expr_delay = Delay.new_var (); 
392 
expr_annot = None; 
393 
expr_loc = var_decl.var_loc } in 
394 
{ var_decl with var_id = cp_var; var_orig = false }, 
395 
mkeq var_decl.var_loc ([cp_var], expr) 
396  
397 
let wrong_partition g partition = 
398 
match partition with 
399 
 [id] > IdentDepGraph.mem_edge g id id 
400 
 _::_::_ > true 
401 
 [] > assert false 
402  
403 
(* Checks that the dependency graph [g] does not contain a cycle. Raises 
404 
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) 
405 
let check_cycles g = 
406 
let scc_l = Cycles.scc_list g in 
407 
List.iter (fun partition > 
408 
if wrong_partition g partition then 
409 
raise (Error (DataCycle partition)) 
410 
else () 
411 
) scc_l 
412  
413 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *) 
414 
let copy_partition g partition = 
415 
let copy_g = IdentDepGraph.create () in 
416 
IdentDepGraph.iter_edges 
417 
(fun src tgt > 
418 
if List.mem src partition && List.mem tgt partition 
419 
then IdentDepGraph.add_edge copy_g src tgt) 
420 
g 
421  
422 

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