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

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

282 
(* (\* In order to introduce dependencies between assert expressions and the node, *) 
283 
(* we build an artificial dependency between node output and each assert *) 
284 
(* expr. While these are not valid equations, they should properly propage in *) 
285 
(* function add_eq_dependencies *\) *) 
286 
(* let g = *) 
287 
(* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *) 
288 
(* List.fold_left (fun g ae > *) 
289 
(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *) 
290 
(* add_eq_dependencies mems inputs node_vars fake_eq g *) 
291 
(* ) g n.node_asserts in *) 
292 
g 
293  
294 
end 
295  
296 
module NodeDep = struct 
297  
298 
module ExprModule = 
299 
struct 
300 
type t = expr 
301 
let compare = compare 
302 
let hash n = Hashtbl.hash n 
303 
let equal n1 n2 = n1 = n2 
304 
end 
305  
306 
module ESet = Set.Make(ExprModule) 
307  
308 
let rec get_expr_calls prednode expr = 
309 
match expr.expr_desc with 
310 
 Expr_const _ 
311 
 Expr_ident _ > ESet.empty 
312 
 Expr_access (e, _) 
313 
 Expr_power (e, _) > get_expr_calls prednode e 
314 
 Expr_array t 
315 
 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty 
316 
 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty 
317 
 Expr_fby (e1,e2) 
318 
 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) 
319 
 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) 
320 
 Expr_pre e 
321 
 Expr_when (e,_,_) > get_expr_calls prednode e 
322 
 Expr_appl (id,e, _) > 
323 
if not (Basic_library.is_expr_internal_fun expr) && prednode id 
324 
then ESet.add expr (get_expr_calls prednode e) 
325 
else (get_expr_calls prednode e) 
326  
327 
let get_callee expr = 
328 
match expr.expr_desc with 
329 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 
330 
 _ > None 
331  
332 
let get_calls prednode nd = 
333 
let accu f init objl = List.fold_left (fun accu o > ESet.union accu (f o)) init objl in 
334 
let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in 
335 
let rec get_stmt_calls s = 
336 
match s with Eq eq > get_eq_calls eq  Aut aut > get_aut_calls aut 
337 
and get_aut_calls aut = 
338 
let get_handler_calls h = 
339 
let get_cond_calls c = accu (fun (_,e,_,_) > get_expr_calls prednode e) ESet.empty c in 
340 
let until = get_cond_calls h.hand_until in 
341 
let unless = get_cond_calls h.hand_unless in 
342 
let calls = ESet.union until unless in 
343 
let calls = accu get_stmt_calls calls h.hand_stmts in 
344 
let calls = accu (fun a > get_expr_calls prednode a.assert_expr) calls h.hand_asserts in 
345 
(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *) 
346 
calls 
347 
in 
348 
accu get_handler_calls ESet.empty aut.aut_handlers 
349 
in 
350 
let eqs, auts = get_node_eqs nd in 
351 
let deps = accu get_eq_calls ESet.empty eqs in 
352 
let deps = accu get_aut_calls deps auts in 
353 
ESet.elements deps 
354  
355 
let dependence_graph prog = 
356 
let g = new_graph () in 
357 
let g = List.fold_right 
358 
(fun td accu > (* for each node we add its dependencies *) 
359 
match td.top_decl_desc with 
360 
 Node nd > 
361 
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) 
362 
let accu = add_vertices [nd.node_id] accu in 
363 
let deps = List.map 
364 
(fun e > fst (desome (get_callee e))) 
365 
(get_calls (fun _ > true) nd) 
366 
in 
367 
(* Adding assert expressions deps *) 
368 
let deps_asserts = 
369 
let prednode = (fun _ > true) in (* what is this about? *) 
370 
List.map 
371 
(fun e > fst (desome (get_callee e))) 
372 
(ESet.elements 
373 
(List.fold_left 
374 
(fun accu assert_expr > ESet.union accu (get_expr_calls prednode assert_expr)) 
375 
ESet.empty 
376 
(List.map (fun _assert > _assert.assert_expr) nd.node_asserts) 
377 
) 
378 
) 
379 
in 
380 
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) 
381 
add_edges [nd.node_id] (deps@deps_asserts) accu 
382 
 _ > assert false (* should not happen *) 
383 

384 
) prog g in 
385 
g 
386 

387 
let rec filter_static_inputs inputs args = 
388 
match inputs, args with 
389 
 [] , [] > [] 
390 
 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 
391 
 _ > assert false 
392  
393 
let compute_generic_calls prog = 
394 
List.iter 
395 
(fun td > 
396 
match td.top_decl_desc with 
397 
 Node nd > 
398 
let prednode n = is_generic_node (node_from_name n) in 
399 
nd.node_gencalls < get_calls prednode nd 
400 
 _ > () 
401 

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

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

589 
let pp_dep_graph fmt g = 
590 
begin 
591 
Format.fprintf fmt "{ /* graph */@."; 
592 
IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g; 
593 
Format.fprintf fmt "}@." 
594 
end 
595  
596 
let pp_error fmt err = 
597 
match err with 
598 
 NodeCycle trace > 
599 
Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ " 
600 
(fprintf_list ~sep:",@ " Format.pp_print_string) trace 
601 
 DataCycle traces > ( 
602 
Format.fprintf fmt "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ " 
603 
(fprintf_list ~sep:";@ " 
604 
(fun fmt trace > 
605 
Format.fprintf fmt "@[<v 0>{%a}@]" 
606 
(fprintf_list ~sep:",@ " Format.pp_print_string) 
607 
trace 
608 
)) traces 
609 
) 
610 

611 
(* Merges elements of graph [g2] into graph [g1] *) 
612 
let merge_with g1 g2 = 
613 
begin 
614 
IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2; 
615 
IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2 
616 
end 
617  
618 
let world = "!!_world" 
619  
620 
let add_external_dependency outputs mems g = 
621 
begin 
622 
IdentDepGraph.add_vertex g world; 
623 
ISet.iter (fun o > IdentDepGraph.add_edge g world o) outputs; 
624 
ISet.iter (fun m > IdentDepGraph.add_edge g world m) mems; 
625 
end 
626  
627 
let global_dependency node = 
628 
let mems = ExprDep.node_memory_variables node in 
629 
let inputs = 
630 
ISet.union 
631 
(ExprDep.node_input_variables node) 
632 
(ExprDep.node_constant_variables node) in 
633 
let outputs = ExprDep.node_output_variables node in 
634 
let node_vars = ExprDep.node_variables node in 
635 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in 
636 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
637 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
638 
try 
639 
CycleDetection.check_cycles g_non_mems; 
640 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in 
641 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
642 
begin 
643 
merge_with g_non_mems g_mems'; 
644 
add_external_dependency outputs mems g_non_mems; 
645 
{ node with node_stmts = List.map (fun eq > Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
646 
g_non_mems 
647 
end 
648 
with Error (DataCycle _ as exc) > ( 
649 
raise (Error (exc)) 
650 
) 
651  
652 
(* A module to sort dependencies among local variables when relying on clocked declarations *) 
653 
module VarClockDep = 
654 
struct 
655 
let rec get_clock_dep ck = 
656 
match ck.Clocks.cdesc with 
657 
 Clocks.Con (ck ,c ,l) > l::(get_clock_dep ck) 
658 
 Clocks.Clink ck' 
659 
 Clocks.Ccarrying (_, ck') > get_clock_dep ck' 
660 
 _ > [] 
661 

662 
let sort locals = 
663 
let g = new_graph () in 
664 
let g = List.fold_left ( 
665 
fun g var_decl > 
666 
let deps = get_clock_dep var_decl.var_clock in 
667 
add_edges [var_decl.var_id] deps g 
668 
) g locals 
669 
in 
670 
let sorted, no_deps = 
671 
TopologicalDepGraph.fold (fun vid (accu, remaining) > ( 
672 
let select v = v.var_id = vid in 
673 
let selected, not_selected = List.partition select remaining in 
674 
selected@accu, not_selected 
675 
)) g ([],locals) 
676 
in 
677 
no_deps @ sorted 
678 

679 
end 
680 

681 
(* Local Variables: *) 
682 
(* compilecommand:"make C .." *) 
683 
(* End: *) 