lustrec / src / causality.ml @ e7cc5186
History  View  Annotate  Download (22.5 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  
22  
23 
type identified_call = eq * tag 
24 
type error = 
25 
 DataCycle of ident list list (* multiple failed partitions at once *) 
26 
 NodeCycle of ident list 
27  
28 
exception Error of error 
29  
30  
31 
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule) 
32 
(*module DotGraph = Graphviz.Dot (IdentDepGraph)*) 
33 
module Bfs = Traverse.Bfs (IdentDepGraph) 
34 

35 
(* Dependency of mem variables on mem variables is cut off 
36 
by duplication of some mem vars into local node vars. 
37 
Thus, cylic dependency errors may only arise between nomem vars. 
38 
nonmem variables are: 
39 
 constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars 
40 
 read mems (fake vars): same remark as above. 
41 
 outputs: decoupled from mems, if necessary 
42 
 locals 
43 
 instance vars (fake vars): simplify causality analysis 
44 

45 
global constants are not part of the dependency graph. 
46 

47 
no_mem' = combinational(no_mem, mem); 
48 
=> (mem > no_mem' > no_mem) 
49  
50 
mem' = pre(no_mem, mem); 
51 
=> (mem' > no_mem), (mem > mem') 
52 

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

259  
260 
(* Returns the dependence graph for node [n] *) 
261 
let dependence_graph mems inputs node_vars n = 
262 
instance_var_cpt := 0; 
263 
let g = new_graph (), new_graph () in 
264 
(* Basic dependencies *) 
265 
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in 
266 
(* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il 
267 
faut imposer que les outputs dépendent des asserts pour identifier que les 
268 
fcn calls des asserts sont évalués avant le noeuds *) 
269 

270 
(* (\* In order to introduce dependencies between assert expressions and the node, *) 
271 
(* we build an artificial dependency between node output and each assert *) 
272 
(* expr. While these are not valid equations, they should properly propage in *) 
273 
(* function add_eq_dependencies *\) *) 
274 
(* let g = *) 
275 
(* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *) 
276 
(* List.fold_left (fun g ae > *) 
277 
(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *) 
278 
(* add_eq_dependencies mems inputs node_vars fake_eq g *) 
279 
(* ) g n.node_asserts in *) 
280 
g 
281  
282 
end 
283  
284 
module NodeDep = struct 
285  
286 
module ExprModule = 
287 
struct 
288 
type t = expr 
289 
let compare = compare 
290 
let hash n = Hashtbl.hash n 
291 
let equal n1 n2 = n1 = n2 
292 
end 
293  
294 
module ESet = Set.Make(ExprModule) 
295  
296 
let rec get_expr_calls prednode expr = 
297 
match expr.expr_desc with 
298 
 Expr_const _ 
299 
 Expr_ident _ > ESet.empty 
300 
 Expr_access (e, _) 
301 
 Expr_power (e, _) > get_expr_calls prednode e 
302 
 Expr_array t 
303 
 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty 
304 
 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty 
305 
 Expr_fby (e1,e2) 
306 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 
307 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 
308 
 Expr_pre e 
309 
 Expr_when (e,_,_) > get_expr_calls prednode e 
310 
 Expr_appl (id,e, _) > 
311 
if not (Basic_library.is_expr_internal_fun expr) && prednode id 
312 
then ESet.add expr (get_expr_calls prednode e) 
313 
else (get_expr_calls prednode e) 
314  
315 
let get_callee expr = 
316 
match expr.expr_desc with 
317 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 
318 
 _ > None 
319  
320 
let get_calls prednode eqs = 
321 
let deps = 
322 
List.fold_left 
323 
(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs)) 
324 
ESet.empty 
325 
eqs in 
326 
ESet.elements deps 
327  
328 
let dependence_graph prog = 
329 
let g = new_graph () in 
330 
let g = List.fold_right 
331 
(fun td accu > (* for each node we add its dependencies *) 
332 
match td.top_decl_desc with 
333 
 Node nd > 
334 
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) 
335 
let accu = add_vertices [nd.node_id] accu in 
336 
let deps = List.map 
337 
(fun e > fst (desome (get_callee e))) 
338 
(get_calls (fun _ > true) (get_node_eqs nd)) 
339 
in 
340 
(* Adding assert expressions deps *) 
341 
let deps_asserts = 
342 
let prednode = (fun _ > true) in (* what is this about? *) 
343 
List.map 
344 
(fun e > fst (desome (get_callee e))) 
345 
(ESet.elements 
346 
(List.fold_left 
347 
(fun accu assert_expr > ESet.union accu (get_expr_calls prednode assert_expr)) 
348 
ESet.empty 
349 
(List.map (fun _assert > _assert.assert_expr) nd.node_asserts) 
350 
) 
351 
) 
352 
in 
353 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
354 
add_edges [nd.node_id] (deps@deps_asserts) accu 
355 
 _ > assert false (* should not happen *) 
356 

357 
) prog g in 
358 
g 
359  
360 
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) 
361 
let slice_graph gr v = 
362 
begin 
363 
let gr' = new_graph () in 
364 
IdentDepGraph.add_vertex gr' v; 
365 
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; 
366 
gr' 
367 
end 
368 

369 
let rec filter_static_inputs inputs args = 
370 
match inputs, args with 
371 
 [] , [] > [] 
372 
 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 
373 
 _ > assert false 
374  
375 
let compute_generic_calls prog = 
376 
List.iter 
377 
(fun td > 
378 
match td.top_decl_desc with 
379 
 Node nd > 
380 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
381 
nd.node_gencalls < get_calls prednode (get_node_eqs nd) 
382 
 _ > () 
383 

384 
) prog 
385  
386 
end 
387  
388  
389 
module CycleDetection = struct 
390  
391 
(*  Look for cycles in a dependency graph *) 
392 
module Cycles = Graph.Components.Make (IdentDepGraph) 
393  
394 
let mk_copy_var n id = 
395 
let used name = 
396 
(List.exists (fun v > v.var_id = name) n.node_locals) 
397 
 (List.exists (fun v > v.var_id = name) n.node_inputs) 
398 
 (List.exists (fun v > v.var_id = name) n.node_outputs) 
399 
in mk_new_name used id 
400  
401 
let mk_copy_eq n var = 
402 
let var_decl = get_node_var var n in 
403 
let cp_var = mk_copy_var n var in 
404 
let expr = 
405 
{ expr_tag = Utils.new_tag (); 
406 
expr_desc = Expr_ident var; 
407 
expr_type = var_decl.var_type; 
408 
expr_clock = var_decl.var_clock; 
409 
expr_delay = Delay.new_var (); 
410 
expr_annot = None; 
411 
expr_loc = var_decl.var_loc } in 
412 
{ var_decl with var_id = cp_var; var_orig = false }, 
413 
mkeq var_decl.var_loc ([cp_var], expr) 
414  
415 
let wrong_partition g partition = 
416 
match partition with 
417 
 [id] > IdentDepGraph.mem_edge g id id 
418 
 _::_::_ > true 
419 
 [] > assert false 
420  
421 
(* Checks that the dependency graph [g] does not contain a cycle. Raises 
422 
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) 
423 
let check_cycles g = 
424 
let scc_l = Cycles.scc_list g in 
425 
let algebraic_loops = List.filter (wrong_partition g) scc_l in 
426 
if List.length algebraic_loops > 0 then 
427 
raise (Error (DataCycle algebraic_loops)) 
428 
(* We extract a hint to resolve the cycle: for each variable in the cycle 
429 
which is defined by a call, we return the name of the node call and 
430 
its specific id *) 
431  
432 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *) 
433 
let copy_partition g partition = 
434 
let copy_g = IdentDepGraph.create () in 
435 
IdentDepGraph.iter_edges 
436 
(fun src tgt > 
437 
if List.mem src partition && List.mem tgt partition 
438 
then IdentDepGraph.add_edge copy_g src tgt) 
439 
g 
440  
441 

442 
(* Breaks dependency cycles in a graph [g] by inserting aux variables. 
443 
[head] is a head of a nontrivial scc of [g]. 
444 
In Lustre, this is legal only for mem/mem cycles *) 
445 
let break_cycle head cp_head g = 
446 
let succs = IdentDepGraph.succ g head in 
447 
IdentDepGraph.add_edge g head cp_head; 
448 
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); 
449 
List.iter 
450 
(fun s > 
451 
IdentDepGraph.remove_edge g head s; 
452 
IdentDepGraph.add_edge g s cp_head) 
453 
succs 
454  
455 
(* Breaks cycles of the dependency graph [g] of memory variables [mems] 
456 
belonging in node [node]. Returns: 
457 
 a list of new auxiliary variable declarations 
458 
 a list of new equations 
459 
 a modified acyclic version of [g] 
460 
*) 
461 
let break_cycles node mems g = 
462 
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 
463 
let rec break vdecls mem_eqs g = 
464 
let scc_l = Cycles.scc_list g in 
465 
let wrong = List.filter (wrong_partition g) scc_l in 
466 
match wrong with 
467 
 [] > (vdecls, non_mem_eqs@mem_eqs, g) 
468 
 [head]::_ > 
469 
begin 
470 
IdentDepGraph.remove_edge g head head; 
471 
break vdecls mem_eqs g 
472 
end 
473 
 (head::part)::_ > 
474 
begin 
475 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in 
476 
let pvar v = List.mem v part in 
477 
let fvar v = if v = head then vdecl_cp_head.var_id else v in 
478 
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in 
479 
break_cycle head vdecl_cp_head.var_id g; 
480 
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g 
481 
end 
482 
 _ > assert false 
483 
in break [] mem_eqs g 
484  
485 
end 
486  
487 
(* Module used to compute static disjunction of variables based upon their clocks. *) 
488 
module Disjunction = 
489 
struct 
490 
module ClockedIdentModule = 
491 
struct 
492 
type t = var_decl 
493 
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock 
494 
let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id) 
495 
end 
496  
497 
module CISet = Set.Make(ClockedIdentModule) 
498  
499 
(* map: var > list of disjoint vars, sorted in increasing branch length order, 
500 
maybe removing shorter branches *) 
501 
type disjoint_map = (ident, CISet.t) Hashtbl.t 
502  
503 
let pp_ciset fmt t = 
504 
begin 
505 
Format.fprintf fmt "{@ "; 
506 
CISet.iter (fun s > Format.fprintf fmt "%a@ " Printers.pp_var_name s) t; 
507 
Format.fprintf fmt "}@." 
508 
end 
509  
510 
let clock_disjoint_map vdecls = 
511 
let map = Hashtbl.create 23 in 
512 
begin 
513 
List.iter 
514 
(fun v1 > let disj_v1 = 
515 
List.fold_left 
516 
(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res) 
517 
CISet.empty 
518 
vdecls in 
519 
(* disjoint vdecls are stored in increasing branch length order *) 
520 
Hashtbl.add map v1.var_id disj_v1) 
521 
vdecls; 
522 
(map : disjoint_map) 
523 
end 
524  
525 
(* merge variables [v] and [v'] in disjunction [map]. Then: 
526 
 the mapping v' becomes v' > (map v) inter (map v') 
527 
 the mapping v > ... then disappears 
528 
 other mappings become x > (map x) \ (if v in x then v else v') 
529 
*) 
530 
let merge_in_disjoint_map map v v' = 
531 
begin 
532 
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); 
533 
Hashtbl.remove map v.var_id; 
534 
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; 
535 
end 
536  
537 
(* replace variable [v] by [v'] in disjunction [map]. 
538 
[v'] is a dead variable. Then: 
539 
 the mapping v' becomes v' > (map v) 
540 
 the mapping v > ... then disappears 
541 
 all mappings become x > ((map x) \ { v}) union ({v'} if v in map x) 
542 
*) 
543 
let replace_in_disjoint_map map v v' = 
544 
begin 
545 
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); 
546 
Hashtbl.remove map v.var_id; 
547 
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; 
548 
end 
549  
550 
(* remove variable [v] in disjunction [map]. Then: 
551 
 the mapping v > ... then disappears 
552 
 all mappings become x > (map x) \ { v} 
553 
*) 
554 
let remove_in_disjoint_map map v = 
555 
begin 
556 
Hashtbl.remove map v.var_id; 
557 
Hashtbl.iter (fun x mapx > Hashtbl.replace map x (CISet.remove v mapx)) map; 
558 
end 
559  
560 
let pp_disjoint_map fmt map = 
561 
begin 
562 
Format.fprintf fmt "{ /* disjoint map */@."; 
563 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; 
564 
Format.fprintf fmt "}@." 
565 
end 
566 
end 
567  
568 

569 
let pp_dep_graph fmt g = 
570 
begin 
571 
Format.fprintf fmt "{ /* graph */@."; 
572 
IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g; 
573 
Format.fprintf fmt "}@." 
574 
end 
575  
576 
let pp_error fmt err = 
577 
match err with 
578 
 NodeCycle trace > 
579 
Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ " 
580 
(fprintf_list ~sep:",@ " Format.pp_print_string) trace 
581 
 DataCycle traces > ( 
582 
Format.fprintf fmt "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ " 
583 
(fprintf_list ~sep:";@ " 
584 
(fun fmt trace > 
585 
Format.fprintf fmt "@[<v 0>{%a}@]" 
586 
(fprintf_list ~sep:",@ " Format.pp_print_string) 
587 
trace 
588 
)) traces 
589 
) 
590 

591 
(* Merges elements of graph [g2] into graph [g1] *) 
592 
let merge_with g1 g2 = 
593 
begin 
594 
IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2; 
595 
IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2 
596 
end 
597  
598 
let world = "!!_world" 
599  
600 
let add_external_dependency outputs mems g = 
601 
begin 
602 
IdentDepGraph.add_vertex g world; 
603 
ISet.iter (fun o > IdentDepGraph.add_edge g world o) outputs; 
604 
ISet.iter (fun m > IdentDepGraph.add_edge g world m) mems; 
605 
end 
606  
607 
let global_dependency node = 
608 
let mems = ExprDep.node_memory_variables node in 
609 
let inputs = 
610 
ISet.union 
611 
(ExprDep.node_input_variables node) 
612 
(ExprDep.node_constant_variables node) in 
613 
let outputs = ExprDep.node_output_variables node in 
614 
let node_vars = ExprDep.node_variables node in 
615 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in 
616 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
617 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
618 
try 
619 
CycleDetection.check_cycles g_non_mems; 
620 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in 
621 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
622 
begin 
623 
merge_with g_non_mems g_mems'; 
624 
add_external_dependency outputs mems g_non_mems; 
625 
{ node with node_stmts = List.map (fun eq > Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
626 
g_non_mems 
627 
end 
628 
with Error (DataCycle _ as exc) > ( 
629 
raise (Error (exc)) 
630 
) 
631  
632 
(* Local Variables: *) 
633 
(* compilecommand:"make C .." *) 
634 
(* End: *) 