lustrec / src / causality.ml @ 861f327f
History  View  Annotate  Download (25.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 Lustre_types 
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 

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

42 
global constants are not part of the dependency graph. 
43 

44 
no_mem' = combinational(no_mem, mem); 
45 
=> (mem > no_mem' > no_mem) 
46  
47 
mem' = pre(no_mem, mem); 
48 
=> (mem' > no_mem), (mem > mem') 
49 

50 
Global roadmap: 
51 
 compute two dep graphs g (nonmem/nonmem&mem) and g' (mem/mem) 
52 
 check cycles in g (a cycle means a dependency error) 
53 
 break cycles in g' (it's legal !): 
54 
 check cycles in g' 
55 
 if any, introduce aux var to break cycle, then start afresh 
56 
 insert g' into g 
57 
 return g 
58 
*) 
59  
60 
(* Tests whether [v] is a root of graph [g], i.e. a source *) 
61 
let is_graph_root v g = 
62 
IdentDepGraph.in_degree g v = 0 
63  
64 
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) 
65 
let graph_roots g = 
66 
IdentDepGraph.fold_vertex 
67 
(fun v roots > if is_graph_root v g then v::roots else roots) 
68 
g [] 
69  
70 
let add_edges src tgt g = 
71 
(*List.iter (fun s > List.iter (fun t > Format.eprintf "add %s > %s@." s t) tgt) src;*) 
72 
List.iter 
73 
(fun s > 
74 
List.iter 
75 
(fun t > IdentDepGraph.add_edge g s t) 
76 
tgt) 
77 
src; 
78 
g 
79  
80 
let add_vertices vtc g = 
81 
(*List.iter (fun t > Format.eprintf "add %s@." t) vtc;*) 
82 
List.iter (fun v > IdentDepGraph.add_vertex g v) vtc; 
83 
g 
84  
85 
let new_graph () = 
86 
IdentDepGraph.create () 
87  
88 
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) 
89 
let slice_graph gr v = 
90 
begin 
91 
let gr' = new_graph () in 
92 
IdentDepGraph.add_vertex gr' v; 
93 
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; 
94 
gr' 
95 
end 
96  
97 

98 
module ExprDep = struct 
99 
let get_node_eqs nd = 
100 
let eqs, auts = get_node_eqs nd in 
101 
if auts != [] then assert false (* No call on causality on a Lustre model 
102 
with automaton. They should be expanded by now. *); 
103 
eqs 
104 

105 
let instance_var_cpt = ref 0 
106  
107 
(* read vars represent input/mem readonly vars, 
108 
they are not part of the program/schedule, 
109 
as they are not assigned, 
110 
but used to compute useless inputs/mems. 
111 
a mem read var represents a mem at the beginning of a cycle *) 
112 
let mk_read_var id = 
113 
Format.sprintf "#%s" id 
114  
115 
(* instance vars represent node instance calls, 
116 
they are not part of the program/schedule, 
117 
but used to simplify causality analysis 
118 
*) 
119 
let mk_instance_var id = 
120 
incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt 
121  
122 
let is_read_var v = v.[0] = '#' 
123  
124 
let is_instance_var v = v.[0] = '!' 
125  
126 
let is_ghost_var v = is_instance_var v  is_read_var v 
127  
128 
let undo_read_var id = 
129 
assert (is_read_var id); 
130 
String.sub id 1 (String.length id  1) 
131  
132 
let undo_instance_var id = 
133 
assert (is_instance_var id); 
134 
String.sub id 1 (String.length id  1) 
135  
136 
let eq_memory_variables mems eq = 
137 
let rec match_mem lhs rhs mems = 
138 
match rhs.expr_desc with 
139 
 Expr_fby _ 
140 
 Expr_pre _ > List.fold_right ISet.add lhs mems 
141 
 Expr_tuple tl > 
142 
let lhs' = (transpose_list [lhs]) in 
143 
List.fold_right2 match_mem lhs' tl mems 
144 
 _ > mems in 
145 
match_mem eq.eq_lhs eq.eq_rhs mems 
146  
147 
let node_memory_variables nd = 
148 
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd) 
149  
150 
let node_input_variables nd = 
151 
List.fold_left (fun inputs v > ISet.add v.var_id inputs) ISet.empty 
152 
(if nd.node_iscontract then 
153 
nd.node_inputs@nd.node_outputs 
154 
else 
155 
nd.node_inputs) 
156 

157 
let node_output_variables nd = 
158 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty 
159 
(if nd.node_iscontract then [] else nd.node_outputs) 
160  
161 
let node_local_variables nd = 
162 
List.fold_left (fun locals v > ISet.add v.var_id locals) ISet.empty nd.node_locals 
163  
164 
let node_constant_variables nd = 
165 
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 
166  
167 
let node_auxiliary_variables nd = 
168 
ISet.diff (node_local_variables nd) (node_memory_variables nd) 
169  
170 
let node_variables nd = 
171 
let inputs = node_input_variables nd in 
172 
let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in 
173 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals 
174  
175 
(* computes the equivalence relation relating variables 
176 
in the same equation lhs, under the form of a table 
177 
of class representatives *) 
178 
let eqs_eq_equiv eqs = 
179 
let eq_equiv = Hashtbl.create 23 in 
180 
List.iter (fun eq > 
181 
let first = List.hd eq.eq_lhs in 
182 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 
183 
) 
184 
eqs; 
185 
eq_equiv 
186 

187 
let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd) 
188 

189 
(* Create a tuple of right dimension, according to [expr] type, *) 
190 
(* filled with variable [v] *) 
191 
let adjust_tuple v expr = 
192 
match expr.expr_type.Types.tdesc with 
193 
 Types.Ttuple tl > duplicate v (List.length tl) 
194 
 _ > [v] 
195  
196  
197 
(* Add dependencies from lhs to rhs in [g, g'], *) 
198 
(* nomem/nomem and mem/nomem in g *) 
199 
(* mem/mem in g' *) 
200 
(* match (lhs_is_mem, ISet.mem x mems) with 
201 
 (false, true ) > (add_edges [x] lhs g, 
202 
g') 
203 
 (false, false) > (add_edges lhs [x] g, 
204 
g') 
205 
 (true , false) > (add_edges lhs [x] g, 
206 
g') 
207 
 (true , true ) > (g, 
208 
add_edges [x] lhs g') 
209 
*) 
210 
let add_eq_dependencies mems inputs node_vars eq (g, g') = 
211 
let add_var lhs_is_mem lhs x (g, g') = 
212 
if is_instance_var x  ISet.mem x node_vars then 
213 
if ISet.mem x mems 
214 
then 
215 
let g = add_edges lhs [mk_read_var x] g in 
216 
if lhs_is_mem 
217 
then 
218 
(g, add_edges [x] lhs g') 
219 
else 
220 
(add_edges [x] lhs g, g') 
221 
else 
222 
let x = if ISet.mem x inputs then mk_read_var x else x in 
223 
(add_edges lhs [x] g, g') 
224 
else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) 
225 
in 
226 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
227 
let rec add_clock lhs_is_mem lhs ck g = 
228 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
229 
match (Clocks.repr ck).Clocks.cdesc with 
230 
 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) 
231 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
232 
 _ > g 
233 
in 
234 
let rec add_dep lhs_is_mem lhs rhs g = 
235 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
236 
(* i.e every input is connected to every output, through a ghost var *) 
237 
let mashup_appl_dependencies f e g = 
238 
let f_var = mk_instance_var (Format.sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in 
239 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) 
240 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
241 
in 
242 
match rhs.expr_desc with 
243 
 Expr_const _ > g 
244 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 
245 
 Expr_pre e > add_dep true lhs e g 
246 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 
247 
 Expr_access (e1, d) 
248 
 Expr_power (e1, d) > add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g) 
249 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
250 
 Expr_tuple t > List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
251 
 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) 
252 
 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)) 
253 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 
254 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 
255 
 Expr_appl (f, e, None) > 
256 
if Basic_library.is_expr_internal_fun rhs 
257 
(* tuple componentwise dependency for internal operators *) 
258 
then 
259 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 
260 
(* mashed up dependency for userdefined operators *) 
261 
else 
262 
mashup_appl_dependencies f e g 
263 
 Expr_appl (f, e, Some c) > 
264 
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) 
265 
in 
266 
let g = 
267 
List.fold_left 
268 
(fun g lhs > 
269 
if ISet.mem lhs mems then 
270 
add_vertices [lhs; mk_read_var lhs] g 
271 
else 
272 
add_vertices [lhs] g 
273 
) 
274 
g eq.eq_lhs 
275 
in 
276 
add_dep false eq.eq_lhs eq.eq_rhs (g, g') 
277 

278  
279 
(* Returns the dependence graph for node [n] *) 
280 
let dependence_graph mems inputs node_vars n = 
281 
instance_var_cpt := 0; 
282 
let g = new_graph (), new_graph () in 
283 
(* Basic dependencies *) 
284 
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in 
285 
(* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il 
286 
faut imposer que les outputs dépendent des asserts pour identifier que les 
287 
fcn calls des asserts sont évalués avant le noeuds *) 
288 

289 
(* (\* In order to introduce dependencies between assert expressions and the node, *) 
290 
(* we build an artificial dependency between node output and each assert *) 
291 
(* expr. While these are not valid equations, they should properly propage in *) 
292 
(* function add_eq_dependencies *\) *) 
293 
(* let g = *) 
294 
(* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *) 
295 
(* List.fold_left (fun g ae > *) 
296 
(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *) 
297 
(* add_eq_dependencies mems inputs node_vars fake_eq g *) 
298 
(* ) g n.node_asserts in *) 
299 
g 
300  
301 
end 
302  
303 
module NodeDep = struct 
304  
305 
module ExprModule = 
306 
struct 
307 
type t = expr 
308 
let compare = compare 
309 
let hash n = Hashtbl.hash n 
310 
let equal n1 n2 = n1 = n2 
311 
end 
312  
313 
module ESet = Set.Make(ExprModule) 
314  
315 
let rec get_expr_calls prednode expr = 
316 
match expr.expr_desc with 
317 
 Expr_const _ 
318 
 Expr_ident _ > ESet.empty 
319 
 Expr_access (e, _) 
320 
 Expr_power (e, _) > get_expr_calls prednode e 
321 
 Expr_array t 
322 
 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty 
323 
 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty 
324 
 Expr_fby (e1,e2) 
325 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 
326 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 
327 
 Expr_pre e 
328 
 Expr_when (e,_,_) > get_expr_calls prednode e 
329 
 Expr_appl (id,e, _) > 
330 
if not (Basic_library.is_expr_internal_fun expr) && prednode id 
331 
then ESet.add expr (get_expr_calls prednode e) 
332 
else (get_expr_calls prednode e) 
333  
334 
let get_eexpr_calls prednode ee = 
335 
get_expr_calls prednode ee.eexpr_qfexpr 
336 

337 
let get_callee expr = 
338 
match expr.expr_desc with 
339 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 
340 
 _ > None 
341  
342 
let accu f init objl = List.fold_left (fun accu o > ESet.union accu (f o)) init objl 
343  
344 
let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs 
345 

346 
let rec get_stmt_calls prednode s = 
347 
match s with Eq eq > get_eq_calls prednode eq  Aut aut > get_aut_calls prednode aut 
348 
and get_aut_calls prednode aut = 
349 
let get_handler_calls prednode h = 
350 
let get_cond_calls c = accu (fun (_,e,_,_) > get_expr_calls prednode e) ESet.empty c in 
351 
let until = get_cond_calls h.hand_until in 
352 
let unless = get_cond_calls h.hand_unless in 
353 
let calls = ESet.union until unless in 
354 
let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in 
355 
let calls = accu (fun a > get_expr_calls prednode a.assert_expr) calls h.hand_asserts in 
356 
(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *) 
357 
calls 
358 
in 
359 
accu (get_handler_calls prednode) ESet.empty aut.aut_handlers 
360 

361 
let get_calls prednode nd = 
362 
let eqs, auts = get_node_eqs nd in 
363 
let deps = accu (get_eq_calls prednode) ESet.empty eqs in 
364 
let deps = accu (get_aut_calls prednode) deps auts in 
365 
ESet.elements deps 
366  
367 
let get_contract_calls prednode c = 
368 
let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in 
369 
let deps = accu (get_eexpr_calls prednode) deps ( c.assume @ c.guarantees @ (List.fold_left (fun accu m > accu @ m.require @ m.ensure ) [] c.modes)) in 
370 
let id_deps = List.map (fun e > fst (desome (get_callee e))) (ESet.elements deps) in 
371 
let id_deps = (List.fold_left (fun accu imp > imp.import_nodeid::accu) [] c.imports) @ id_deps in 
372 
id_deps 
373 

374 
let dependence_graph prog = 
375 
let g = new_graph () in 
376 
let g = List.fold_right 
377 
(fun td accu > (* for each node we add its dependencies *) 
378 
match td.top_decl_desc with 
379 
 Node nd > 
380 
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) 
381 
let accu = add_vertices [nd.node_id] accu in 
382 
let deps = List.map 
383 
(fun e > fst (desome (get_callee e))) 
384 
(get_calls (fun _ > true) nd) 
385 
in 
386 
(* Adding assert expressions deps *) 
387 
let deps_asserts = 
388 
let prednode = (fun _ > true) in (* what is this about? *) 
389 
List.map 
390 
(fun e > fst (desome (get_callee e))) 
391 
(ESet.elements 
392 
(List.fold_left 
393 
(fun accu assert_expr > ESet.union accu (get_expr_calls prednode assert_expr)) 
394 
ESet.empty 
395 
(List.map (fun _assert > _assert.assert_expr) nd.node_asserts) 
396 
) 
397 
) 
398 
in 
399 
let deps_spec = match nd.node_spec with 
400 
 None > [] 
401 
 Some (NodeSpec id) > [id] 
402 
 Some (Contract c) > get_contract_calls (fun _ > true) c 
403 

404 
in 
405 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
406 
add_edges [nd.node_id] (deps@deps_asserts@deps_spec) accu 
407 
 _ > assert false (* should not happen *) 
408 

409 
) prog g in 
410 
g 
411 

412 
let rec filter_static_inputs inputs args = 
413 
match inputs, args with 
414 
 [] , [] > [] 
415 
 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 
416 
 _ > assert false 
417  
418 
let compute_generic_calls prog = 
419 
List.iter 
420 
(fun td > 
421 
match td.top_decl_desc with 
422 
 Node nd > 
423 
let prednode n = is_generic_node (node_from_name n) in 
424 
nd.node_gencalls < get_calls prednode nd 
425 
 _ > () 
426 

427 
) prog 
428  
429 
end 
430  
431  
432 
module CycleDetection = struct 
433  
434 
(*  Look for cycles in a dependency graph *) 
435 
module Cycles = Graph.Components.Make (IdentDepGraph) 
436  
437 
let mk_copy_var n id = 
438 
let used name = 
439 
(List.exists (fun v > v.var_id = name) n.node_locals) 
440 
 (List.exists (fun v > v.var_id = name) n.node_inputs) 
441 
 (List.exists (fun v > v.var_id = name) n.node_outputs) 
442 
in mk_new_name used id 
443  
444 
let mk_copy_eq n var = 
445 
let var_decl = get_node_var var n in 
446 
let cp_var = mk_copy_var n var in 
447 
let expr = 
448 
{ expr_tag = Utils.new_tag (); 
449 
expr_desc = Expr_ident var; 
450 
expr_type = var_decl.var_type; 
451 
expr_clock = var_decl.var_clock; 
452 
expr_delay = Delay.new_var (); 
453 
expr_annot = None; 
454 
expr_loc = var_decl.var_loc } in 
455 
{ var_decl with var_id = cp_var; var_orig = false }, 
456 
mkeq var_decl.var_loc ([cp_var], expr) 
457  
458 
let wrong_partition g partition = 
459 
match partition with 
460 
 [id] > IdentDepGraph.mem_edge g id id 
461 
 _::_::_ > true 
462 
 [] > assert false 
463  
464 
(* Checks that the dependency graph [g] does not contain a cycle. Raises 
465 
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) 
466 
let check_cycles g = 
467 
let scc_l = Cycles.scc_list g in 
468 
let algebraic_loops = List.filter (wrong_partition g) scc_l in 
469 
if List.length algebraic_loops > 0 then 
470 
raise (Error (DataCycle algebraic_loops)) 
471 
(* We extract a hint to resolve the cycle: for each variable in the cycle 
472 
which is defined by a call, we return the name of the node call and 
473 
its specific id *) 
474  
475 
(* Creates the subgraph of [g] restricted to vertices and edges in partition *) 
476 
let copy_partition g partition = 
477 
let copy_g = IdentDepGraph.create () in 
478 
IdentDepGraph.iter_edges 
479 
(fun src tgt > 
480 
if List.mem src partition && List.mem tgt partition 
481 
then IdentDepGraph.add_edge copy_g src tgt) 
482 
g 
483  
484 

485 
(* Breaks dependency cycles in a graph [g] by inserting aux variables. 
486 
[head] is a head of a nontrivial scc of [g]. 
487 
In Lustre, this is legal only for mem/mem cycles *) 
488 
let break_cycle head cp_head g = 
489 
let succs = IdentDepGraph.succ g head in 
490 
IdentDepGraph.add_edge g head cp_head; 
491 
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); 
492 
List.iter 
493 
(fun s > 
494 
IdentDepGraph.remove_edge g head s; 
495 
IdentDepGraph.add_edge g s cp_head) 
496 
succs 
497  
498 
(* Breaks cycles of the dependency graph [g] of memory variables [mems] 
499 
belonging in node [node]. Returns: 
500 
 a list of new auxiliary variable declarations 
501 
 a list of new equations 
502 
 a modified acyclic version of [g] 
503 
*) 
504 
let break_cycles node mems g = 
505 
let eqs , auts = get_node_eqs node in 
506 
assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *) 
507 
let (mem_eqs, non_mem_eqs) = List.partition (fun eq > List.exists (fun v > ISet.mem v mems) eq.eq_lhs) eqs in 
508 
let rec break vdecls mem_eqs g = 
509 
let scc_l = Cycles.scc_list g in 
510 
let wrong = List.filter (wrong_partition g) scc_l in 
511 
match wrong with 
512 
 [] > (vdecls, non_mem_eqs@mem_eqs, g) 
513 
 [head]::_ > 
514 
begin 
515 
IdentDepGraph.remove_edge g head head; 
516 
break vdecls mem_eqs g 
517 
end 
518 
 (head::part)::_ > 
519 
begin 
520 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in 
521 
let pvar v = List.mem v part in 
522 
let fvar v = if v = head then vdecl_cp_head.var_id else v in 
523 
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in 
524 
break_cycle head vdecl_cp_head.var_id g; 
525 
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g 
526 
end 
527 
 _ > assert false 
528 
in break [] mem_eqs g 
529  
530 
end 
531  
532 
(* Module used to compute static disjunction of variables based upon their clocks. *) 
533 
module Disjunction = 
534 
struct 
535 
module ClockedIdentModule = 
536 
struct 
537 
type t = var_decl 
538 
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock 
539 
let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id) 
540 
end 
541  
542 
module CISet = Set.Make(ClockedIdentModule) 
543  
544 
(* map: var > list of disjoint vars, sorted in increasing branch length order, 
545 
maybe removing shorter branches *) 
546 
type disjoint_map = (ident, CISet.t) Hashtbl.t 
547  
548 
let pp_ciset fmt t = 
549 
begin 
550 
Format.fprintf fmt "{@ "; 
551 
CISet.iter (fun s > Format.fprintf fmt "%a@ " Printers.pp_var_name s) t; 
552 
Format.fprintf fmt "}@." 
553 
end 
554  
555 
let clock_disjoint_map vdecls = 
556 
let map = Hashtbl.create 23 in 
557 
begin 
558 
List.iter 
559 
(fun v1 > let disj_v1 = 
560 
List.fold_left 
561 
(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res) 
562 
CISet.empty 
563 
vdecls in 
564 
(* disjoint vdecls are stored in increasing branch length order *) 
565 
Hashtbl.add map v1.var_id disj_v1) 
566 
vdecls; 
567 
(map : disjoint_map) 
568 
end 
569  
570 
(* merge variables [v] and [v'] in disjunction [map]. Then: 
571 
 the mapping v' becomes v' > (map v) inter (map v') 
572 
 the mapping v > ... then disappears 
573 
 other mappings become x > (map x) \ (if v in x then v else v') 
574 
*) 
575 
let merge_in_disjoint_map map v v' = 
576 
begin 
577 
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); 
578 
Hashtbl.remove map v.var_id; 
579 
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; 
580 
end 
581  
582 
(* replace variable [v] by [v'] in disjunction [map]. 
583 
[v'] is a dead variable. Then: 
584 
 the mapping v' becomes v' > (map v) 
585 
 the mapping v > ... then disappears 
586 
 all mappings become x > ((map x) \ { v}) union ({v'} if v in map x) 
587 
*) 
588 
let replace_in_disjoint_map map v v' = 
589 
begin 
590 
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); 
591 
Hashtbl.remove map v.var_id; 
592 
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; 
593 
end 
594  
595 
(* remove variable [v] in disjunction [map]. Then: 
596 
 the mapping v > ... then disappears 
597 
 all mappings become x > (map x) \ { v} 
598 
*) 
599 
let remove_in_disjoint_map map v = 
600 
begin 
601 
Hashtbl.remove map v.var_id; 
602 
Hashtbl.iter (fun x mapx > Hashtbl.replace map x (CISet.remove v mapx)) map; 
603 
end 
604  
605 
let pp_disjoint_map fmt map = 
606 
begin 
607 
Format.fprintf fmt "{ /* disjoint map */@."; 
608 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; 
609 
Format.fprintf fmt "}@." 
610 
end 
611 
end 
612  
613 

614 
let pp_dep_graph fmt g = 
615 
begin 
616 
Format.fprintf fmt "{ /* graph */@."; 
617 
IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g; 
618 
Format.fprintf fmt "}@." 
619 
end 
620  
621 
let pp_error fmt err = 
622 
match err with 
623 
 NodeCycle trace > 
624 
Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ " 
625 
(fprintf_list ~sep:",@ " Format.pp_print_string) trace 
626 
 DataCycle traces > ( 
627 
Format.fprintf fmt "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ " 
628 
(fprintf_list ~sep:";@ " 
629 
(fun fmt trace > 
630 
Format.fprintf fmt "@[<v 0>{%a}@]" 
631 
(fprintf_list ~sep:",@ " Format.pp_print_string) 
632 
trace 
633 
)) traces 
634 
) 
635 

636 
(* Merges elements of graph [g2] into graph [g1] *) 
637 
let merge_with g1 g2 = 
638 
begin 
639 
IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2; 
640 
IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2 
641 
end 
642  
643 
let world = "!!_world" 
644  
645 
let add_external_dependency outputs mems g = 
646 
begin 
647 
IdentDepGraph.add_vertex g world; 
648 
ISet.iter (fun o > IdentDepGraph.add_edge g world o) outputs; 
649 
ISet.iter (fun m > IdentDepGraph.add_edge g world m) mems; 
650 
end 
651  
652 
(* Takes a node and return a pair (node', graph) where node' is node 
653 
rebuilt with the equations enriched with new ones introduced to 
654 
"break cycles" *) 
655 
let global_dependency node = 
656 
let mems = ExprDep.node_memory_variables node in 
657 
let inputs = 
658 
ISet.union 
659 
(ExprDep.node_input_variables node) 
660 
(ExprDep.node_constant_variables node) in 
661 
let outputs = ExprDep.node_output_variables node in 
662 
let node_vars = ExprDep.node_variables node in 
663 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in 
664 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
665 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
666 
try 
667 
CycleDetection.check_cycles g_non_mems; 
668 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in 
669 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
670 
begin 
671 
merge_with g_non_mems g_mems'; 
672 
add_external_dependency outputs mems g_non_mems; 
673 
{ node with node_stmts = List.map (fun eq > Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
674 
g_non_mems 
675 
end 
676 
with Error (DataCycle _ as exc) > ( 
677 
raise (Error (exc)) 
678 
) 
679  
680 
(* A module to sort dependencies among local variables when relying on clocked declarations *) 
681 
module VarClockDep = 
682 
struct 
683 
let rec get_clock_dep ck = 
684 
match ck.Clocks.cdesc with 
685 
 Clocks.Con (ck ,c ,l) > l::(get_clock_dep ck) 
686 
 Clocks.Clink ck' 
687 
 Clocks.Ccarrying (_, ck') > get_clock_dep ck' 
688 
 _ > [] 
689 

690 
let sort locals = 
691 
let g = new_graph () in 
692 
let g = List.fold_left ( 
693 
fun g var_decl > 
694 
let deps = get_clock_dep var_decl.var_clock in 
695 
add_edges [var_decl.var_id] deps g 
696 
) g locals 
697 
in 
698 
let sorted, no_deps = 
699 
TopologicalDepGraph.fold (fun vid (accu, remaining) > ( 
700 
let select v = v.var_id = vid in 
701 
let selected, not_selected = List.partition select remaining in 
702 
selected@accu, not_selected 
703 
)) g ([],locals) 
704 
in 
705 
no_deps @ sorted 
706 

707 
end 
708 

709 
(* Local Variables: *) 
710 
(* compilecommand:"make C .." *) 
711 
(* End: *) 