Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ e7cc5186

History | View | Annotate | Download (22.5 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
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 e7cc5186 ploc
23
type identified_call = eq * tag
24 eb837d74 xthirioux
type error =
25 e7cc5186 ploc
  | DataCycle of ident list list (* multiple failed partitions at once *) 
26 eb837d74 xthirioux
  | NodeCycle of ident list
27
28
exception Error of error
29 22fe1c93 ploc
30
31 eb837d74 xthirioux
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
32
(*module DotGraph = Graphviz.Dot (IdentDepGraph)*)
33
module Bfs = Traverse.Bfs (IdentDepGraph)
34
  
35 22fe1c93 ploc
(* 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 no-mem vars.
38 3bfed7f9 xthirioux
   non-mem variables are:
39 ec433d69 xthirioux
   - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
40 3bfed7f9 xthirioux
   - 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 7352a936 ploc
   
45 3bfed7f9 xthirioux
   global constants are not part of the dependency graph.
46 7352a936 ploc
   
47
   no_mem' = combinational(no_mem, mem);
48
   => (mem -> no_mem' -> no_mem)
49 3bfed7f9 xthirioux
50 7352a936 ploc
   mem' = pre(no_mem, mem);
51
   => (mem' -> no_mem), (mem -> mem')
52
   
53 22fe1c93 ploc
   Global roadmap:
54
   - compute two dep graphs g (non-mem/non-mem&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 695d6f2f xthirioux
(* Tests whether [v] is a root of graph [g], i.e. a source *)
64
let is_graph_root v g =
65 7352a936 ploc
  IdentDepGraph.in_degree g v = 0
66 695d6f2f xthirioux
67
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
68
let graph_roots g =
69 7352a936 ploc
  IdentDepGraph.fold_vertex
70
    (fun v roots -> if is_graph_root v g then v::roots else roots)
71
    g []
72 695d6f2f xthirioux
73 22fe1c93 ploc
let add_edges src tgt g =
74 7352a936 ploc
 (*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 22fe1c93 ploc
  g
82
83
let add_vertices vtc g =
84 7352a936 ploc
 (*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
85
  List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
86 22fe1c93 ploc
  g
87
88
let new_graph () =
89 7352a936 ploc
  IdentDepGraph.create ()
90 22fe1c93 ploc
91
module ExprDep = struct
92
93 7352a936 ploc
  let instance_var_cpt = ref 0
94 22fe1c93 ploc
95 3bfed7f9 xthirioux
(* read vars represent input/mem read-only 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 7352a936 ploc
  let mk_read_var id =
101 e7cc5186 ploc
    Format.sprintf "#%s" id
102 3bfed7f9 xthirioux
103
(* instance vars represent node instance calls,
104
   they are not part of the program/schedule,
105
   but used to simplify causality analysis
106 7352a936 ploc
*)
107
  let mk_instance_var id =
108 e7cc5186 ploc
    incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt
109 22fe1c93 ploc
110 7352a936 ploc
  let is_read_var v = v.[0] = '#'
111 22fe1c93 ploc
112 7352a936 ploc
  let is_instance_var v = v.[0] = '!'
113 22fe1c93 ploc
114 7352a936 ploc
  let is_ghost_var v = is_instance_var v || is_read_var v
115 3bfed7f9 xthirioux
116 7352a936 ploc
  let undo_read_var id =
117
    assert (is_read_var id);
118
    String.sub id 1 (String.length id - 1)
119 22fe1c93 ploc
120 7352a936 ploc
  let undo_instance_var id =
121
    assert (is_instance_var id);
122
    String.sub id 1 (String.length id - 1)
123 54d032f5 xthirioux
124 7352a936 ploc
  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 22fe1c93 ploc
135 7352a936 ploc
  let node_memory_variables nd =
136
    List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
137 22fe1c93 ploc
138 7352a936 ploc
  let node_input_variables nd =
139
    List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
140 8a183477 xthirioux
141 7352a936 ploc
  let node_local_variables nd =
142
    List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
143 3bfed7f9 xthirioux
144 7352a936 ploc
  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 ec433d69 xthirioux
147 7352a936 ploc
  let node_output_variables nd =
148
    List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
149 3bfed7f9 xthirioux
150 7352a936 ploc
  let node_auxiliary_variables nd =
151
    ISet.diff (node_local_variables nd) (node_memory_variables nd)
152 bb2ca5f4 xthirioux
153 7352a936 ploc
  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 d4807c3d xthirioux
158 22fe1c93 ploc
(* computes the equivalence relation relating variables 
159
   in the same equation lhs, under the form of a table 
160
   of class representatives *)
161 7352a936 ploc
  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 22fe1c93 ploc
170
(* Create a tuple of right dimension, according to [expr] type, *)
171
(* filled with variable [v] *)
172 7352a936 ploc
  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
  (* no-mem/no-mem and mem/no-mem 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 3bfed7f9 xthirioux
	then
196 7352a936 ploc
	  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 3bfed7f9 xthirioux
	else
203 7352a936 ploc
	  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 c9043042 ploc
  (* Add dependencies from [lhs] to rhs clock [ck]. *)
208 7352a936 ploc
    let rec add_clock lhs_is_mem lhs ck g =
209 d4807c3d xthirioux
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
210 7352a936 ploc
      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 1b01da98 ploc
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
217
    (* i.e every input is connected to every output, through a ghost var *)
218 7352a936 ploc
      let mashup_appl_dependencies f e g =
219 e7cc5186 ploc
	let f_var = mk_instance_var (Format.sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
220 7352a936 ploc
	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 1b01da98 ploc
      (* tuple component-wise dependency for internal operators *)
239 7352a936 ploc
	 then
240
	   List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
241 1b01da98 ploc
      (* mashed up dependency for user-defined operators *)
242 7352a936 ploc
	 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 22fe1c93 ploc
260 7352a936 ploc
  (* 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 22fe1c93 ploc
286 7352a936 ploc
  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 22fe1c93 ploc
	| Node nd ->
334
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
335 7352a936 ploc
	   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 22fe1c93 ploc
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
354 7352a936 ploc
	   add_edges [nd.node_id] (deps@deps_asserts) accu
355 22fe1c93 ploc
	| _ -> assert false (* should not happen *)
356 7352a936 ploc
	   
357
      ) prog g in
358
    g   
359 22fe1c93 ploc
360 eb837d74 xthirioux
  (* 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 7352a936 ploc
      
369 22fe1c93 ploc
  let rec filter_static_inputs inputs args =
370 7352a936 ploc
    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 22fe1c93 ploc
375
  let compute_generic_calls prog =
376
    List.iter
377
      (fun td ->
378
	match td.top_decl_desc with 
379
	| Node nd ->
380 7352a936 ploc
	   let prednode n = is_generic_node (Hashtbl.find node_table n) in
381
	   nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
382 22fe1c93 ploc
	| _ -> ()
383 7352a936 ploc
	   
384 22fe1c93 ploc
      ) prog
385
386
end
387
388 e7cc5186 ploc
389 22fe1c93 ploc
module CycleDetection = struct
390
391 7352a936 ploc
  (* ---- Look for cycles in a dependency graph *)
392 22fe1c93 ploc
  module Cycles = Graph.Components.Make (IdentDepGraph)
393
394
  let mk_copy_var n id =
395 b08ffca7 xthirioux
    let used name =
396 7352a936 ploc
      (List.exists (fun v -> v.var_id = name) n.node_locals)
397 b08ffca7 xthirioux
      || (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 22fe1c93 ploc
401
  let mk_copy_eq n var =
402 01c7d5e1 ploc
    let var_decl = get_node_var var n in
403 22fe1c93 ploc
    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 54d032f5 xthirioux
    { var_decl with var_id = cp_var; var_orig = false },
413 22fe1c93 ploc
    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 7352a936 ploc
  (* 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 22fe1c93 ploc
  let check_cycles g =
424
    let scc_l = Cycles.scc_list g in
425 e7cc5186 ploc
    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 22fe1c93 ploc
432 7352a936 ploc
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
433 22fe1c93 ploc
  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 7352a936 ploc
      
442
  (* Breaks dependency cycles in a graph [g] by inserting aux variables.
443
     [head] is a head of a non-trivial scc of [g]. 
444
     In Lustre, this is legal only for mem/mem cycles *)
445 22fe1c93 ploc
  let break_cycle head cp_head g =
446
    let succs = IdentDepGraph.succ g head in
447
    IdentDepGraph.add_edge g head cp_head;
448 3bfed7f9 xthirioux
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
449 22fe1c93 ploc
    List.iter
450
      (fun s ->
451
	IdentDepGraph.remove_edge g head s;
452
	IdentDepGraph.add_edge    g s cp_head)
453
      succs
454
455 7352a936 ploc
  (* 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 22fe1c93 ploc
  let break_cycles node mems g =
462 b08ffca7 xthirioux
    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 22fe1c93 ploc
    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 7352a936 ploc
	 begin
470
	   IdentDepGraph.remove_edge g head head;
471
	   break vdecls mem_eqs g
472
	 end
473 22fe1c93 ploc
      | (head::part)::_ -> 
474 7352a936 ploc
	 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 22fe1c93 ploc
      | _               -> assert false
483
    in break [] mem_eqs g
484
485
end
486
487 8f89eba8 xthirioux
(* Module used to compute static disjunction of variables based upon their clocks. *)
488
module Disjunction =
489
struct
490 add75bcb xthirioux
  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 28c58de1 xthirioux
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
495 add75bcb xthirioux
  end
496
497
  module CISet = Set.Make(ClockedIdentModule)
498 8f89eba8 xthirioux
499 add75bcb xthirioux
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
500
     maybe removing shorter branches *)
501 b6a94a4e xthirioux
  type disjoint_map = (ident, CISet.t) Hashtbl.t
502 8f89eba8 xthirioux
503 a38c681e xthirioux
  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 b1a97ade xthirioux
  let clock_disjoint_map vdecls =
511 8f89eba8 xthirioux
    let map = Hashtbl.create 23 in
512
    begin
513 add75bcb xthirioux
      List.iter
514
	(fun v1 -> let disj_v1 =
515
		     List.fold_left
516 b6a94a4e xthirioux
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
517
		       CISet.empty
518 add75bcb xthirioux
		       vdecls in
519
		   (* disjoint vdecls are stored in increasing branch length order *)
520
		   Hashtbl.add map v1.var_id disj_v1)
521
	vdecls;
522 b6a94a4e xthirioux
      (map : disjoint_map)
523 8f89eba8 xthirioux
    end
524 b1a97ade xthirioux
525 45c13277 xthirioux
  (* merge variables [v] and [v'] in disjunction [map]. Then:
526 7352a936 ploc
     - 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 add75bcb xthirioux
  *)
530 45c13277 xthirioux
  let merge_in_disjoint_map map v v' =
531 add75bcb xthirioux
    begin
532 b6a94a4e xthirioux
      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 add75bcb xthirioux
    end
536
537 45c13277 xthirioux
  (* replace variable [v] by [v'] in disjunction [map].
538 7352a936 ploc
     [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 45c13277 xthirioux
  *)
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 7352a936 ploc
     - the mapping v |-> ... then disappears
552
     - all mappings become x |-> (map x) \ { v}
553 45c13277 xthirioux
  *)
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 b1a97ade xthirioux
  let pp_disjoint_map fmt map =
561
    begin
562
      Format.fprintf fmt "{ /* disjoint map */@.";
563 b6a94a4e xthirioux
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
564 b1a97ade xthirioux
      Format.fprintf fmt "}@."
565
    end
566 8f89eba8 xthirioux
end
567
568 e7cc5186 ploc
  
569 22fe1c93 ploc
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 eb837d74 xthirioux
let pp_error fmt err =
577
  match err with
578
  | NodeCycle trace ->
579 e7cc5186 ploc
     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 22fe1c93 ploc
(* Merges elements of graph [g2] into graph [g1] *)
592 b1a97ade xthirioux
let merge_with g1 g2 =
593 45c13277 xthirioux
  begin
594 22fe1c93 ploc
    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 45c13277 xthirioux
  end
597
598 57115ec0 xthirioux
let world = "!!_world"
599
600 45c13277 xthirioux
let add_external_dependency outputs mems g =
601
  begin
602 57115ec0 xthirioux
    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 45c13277 xthirioux
  end
606 22fe1c93 ploc
607
let global_dependency node =
608
  let mems = ExprDep.node_memory_variables node in
609 ec433d69 xthirioux
  let inputs =
610
    ISet.union
611
      (ExprDep.node_input_variables node)
612
      (ExprDep.node_constant_variables node) in
613 45c13277 xthirioux
  let outputs = ExprDep.node_output_variables node in
614 3bfed7f9 xthirioux
  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 22fe1c93 ploc
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
617 7352a936 ploc
    Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
618 e7cc5186 ploc
  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 22fe1c93 ploc
632
(* Local Variables: *)
633
(* compile-command:"make -C .." *)
634
(* End: *)