lustrec / src / causality.ml @ 32614c2d
History  View  Annotate  Download (24.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 
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule) 
32 
module TopologicalDepGraph = Topological.Make(IdentDepGraph) 
33  
34 
(*module DotGraph = Graphviz.Dot (IdentDepGraph)*) 
35 
module Bfs = Traverse.Bfs (IdentDepGraph) 
36 

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

47 
global constants are not part of the dependency graph. 
48 

49 
no_mem' = combinational(no_mem, mem); 
50 
=> (mem > no_mem' > no_mem) 
51  
52 
mem' = pre(no_mem, mem); 
53 
=> (mem' > no_mem), (mem > mem') 
54 

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

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

101 
let instance_var_cpt = ref 0 
102  
103 
(* read vars represent input/mem readonly vars, 
104 
they are not part of the program/schedule, 
105 
as they are not assigned, 
106 
but used to compute useless inputs/mems. 
107 
a mem read var represents a mem at the beginning of a cycle *) 
108 
let mk_read_var id = 
109 
Format.sprintf "#%s" id 
110  
111 
(* instance vars represent node instance calls, 
112 
they are not part of the program/schedule, 
113 
but used to simplify causality analysis 
114 
*) 
115 
let mk_instance_var id = 
116 
incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt 
117  
118 
let is_read_var v = v.[0] = '#' 
119  
120 
let is_instance_var v = v.[0] = '!' 
121  
122 
let is_ghost_var v = is_instance_var v  is_read_var v 
123  
124 
let undo_read_var id = 
125 
assert (is_read_var id); 
126 
String.sub id 1 (String.length id  1) 
127  
128 
let undo_instance_var id = 
129 
assert (is_instance_var id); 
130 
String.sub id 1 (String.length id  1) 
131  
132 
let eq_memory_variables mems eq = 
133 
let rec match_mem lhs rhs mems = 
134 
match rhs.expr_desc with 
135 
 Expr_fby _ 
136 
 Expr_pre _ > List.fold_right ISet.add lhs mems 
137 
 Expr_tuple tl > 
138 
let lhs' = (transpose_list [lhs]) in 
139 
List.fold_right2 match_mem lhs' tl mems 
140 
 _ > mems in 
141 
match_mem eq.eq_lhs eq.eq_rhs mems 
142  
143 
let node_memory_variables nd = 
144 
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd) 
145  
146 
let node_input_variables nd = 
147 
List.fold_left (fun inputs v > ISet.add v.var_id inputs) ISet.empty nd.node_inputs 
148  
149 
let node_local_variables nd = 
150 
List.fold_left (fun locals v > ISet.add v.var_id locals) ISet.empty nd.node_locals 
151  
152 
let node_constant_variables nd = 
153 
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 
154  
155 
let node_output_variables nd = 
156 
List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs 
157  
158 
let node_auxiliary_variables nd = 
159 
ISet.diff (node_local_variables nd) (node_memory_variables nd) 
160  
161 
let node_variables nd = 
162 
let inputs = node_input_variables nd in 
163 
let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in 
164 
List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals 
165  
166 
(* computes the equivalence relation relating variables 
167 
in the same equation lhs, under the form of a table 
168 
of class representatives *) 
169 
let node_eq_equiv nd = 
170 
let eq_equiv = Hashtbl.create 23 in 
171 
List.iter (fun eq > 
172 
let first = List.hd eq.eq_lhs in 
173 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 
174 
) 
175 
(get_node_eqs nd); 
176 
eq_equiv 
177  
178 
(* Create a tuple of right dimension, according to [expr] type, *) 
179 
(* filled with variable [v] *) 
180 
let adjust_tuple v expr = 
181 
match expr.expr_type.Types.tdesc with 
182 
 Types.Ttuple tl > duplicate v (List.length tl) 
183 
 _ > [v] 
184  
185  
186 
(* Add dependencies from lhs to rhs in [g, g'], *) 
187 
(* nomem/nomem and mem/nomem in g *) 
188 
(* mem/mem in g' *) 
189 
(* match (lhs_is_mem, ISet.mem x mems) with 
190 
 (false, true ) > (add_edges [x] lhs g, 
191 
g') 
192 
 (false, false) > (add_edges lhs [x] g, 
193 
g') 
194 
 (true , false) > (add_edges lhs [x] g, 
195 
g') 
196 
 (true , true ) > (g, 
197 
add_edges [x] lhs g') 
198 
*) 
199 
let add_eq_dependencies mems inputs node_vars eq (g, g') = 
200 
let add_var lhs_is_mem lhs x (g, g') = 
201 
if is_instance_var x  ISet.mem x node_vars then 
202 
if ISet.mem x mems 
203 
then 
204 
let g = add_edges lhs [mk_read_var x] g in 
205 
if lhs_is_mem 
206 
then 
207 
(g, add_edges [x] lhs g') 
208 
else 
209 
(add_edges [x] lhs g, g') 
210 
else 
211 
let x = if ISet.mem x inputs then mk_read_var x else x in 
212 
(add_edges lhs [x] g, g') 
213 
else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) 
214 
in 
215 
(* Add dependencies from [lhs] to rhs clock [ck]. *) 
216 
let rec add_clock lhs_is_mem lhs ck g = 
217 
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) 
218 
match (Clocks.repr ck).Clocks.cdesc with 
219 
 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) 
220 
 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g 
221 
 _ > g 
222 
in 
223 
let rec add_dep lhs_is_mem lhs rhs g = 
224 
(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *) 
225 
(* i.e every input is connected to every output, through a ghost var *) 
226 
let mashup_appl_dependencies f e g = 
227 
let f_var = mk_instance_var (Format.sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in 
228 
List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) 
229 
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
230 
in 
231 
match rhs.expr_desc with 
232 
 Expr_const _ > g 
233 
 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g) 
234 
 Expr_pre e > add_dep true lhs e g 
235 
 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) 
236 
 Expr_access (e1, d) 
237 
 Expr_power (e1, d) > add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g) 
238 
 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g 
239 
 Expr_tuple t > List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g 
240 
 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) 
241 
 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)) 
242 
 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) 
243 
 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) 
244 
 Expr_appl (f, e, None) > 
245 
if Basic_library.is_expr_internal_fun rhs 
246 
(* tuple componentwise dependency for internal operators *) 
247 
then 
248 
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g 
249 
(* mashed up dependency for userdefined operators *) 
250 
else 
251 
mashup_appl_dependencies f e g 
252 
 Expr_appl (f, e, Some c) > 
253 
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) 
254 
in 
255 
let g = 
256 
List.fold_left 
257 
(fun g lhs > 
258 
if ISet.mem lhs mems then 
259 
add_vertices [lhs; mk_read_var lhs] g 
260 
else 
261 
add_vertices [lhs] g 
262 
) 
263 
g eq.eq_lhs 
264 
in 
265 
add_dep false eq.eq_lhs eq.eq_rhs (g, g') 
266 

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

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

380 
) prog g in 
381 
g 
382  
383 
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) 
384 
let slice_graph gr v = 
385 
begin 
386 
let gr' = new_graph () in 
387 
IdentDepGraph.add_vertex gr' v; 
388 
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; 
389 
gr' 
390 
end 
391 

392 
let rec filter_static_inputs inputs args = 
393 
match inputs, args with 
394 
 [] , [] > [] 
395 
 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 
396 
 _ > assert false 
397  
398 
let compute_generic_calls prog = 
399 
List.iter 
400 
(fun td > 
401 
match td.top_decl_desc with 
402 
 Node nd > 
403 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
404 
nd.node_gencalls < get_calls prednode nd 
405 
 _ > () 
406 

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

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

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

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

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

684 
end 
685 

686 
(* Local Variables: *) 
687 
(* compilecommand:"make C .." *) 
688 
(* End: *) 