Project

General

Profile

Download (21.9 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
12
(********************************************************************)
13

    
14

    
15
(** Simple modular syntactic causality analysis. Can reject correct
16
    programs, especially if the program is not flattened first. *)
17
open Utils
18
open LustreSpec
19
open Corelang
20
open Graph
21
open Format
22

    
23
type error =
24
  | DataCycle of ident list
25
  | NodeCycle of ident list
26

    
27
exception Error of error
28

    
29

    
30
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
31
(*module DotGraph = Graphviz.Dot (IdentDepGraph)*)
32
module Bfs = Traverse.Bfs (IdentDepGraph)
33
  
34
(* Dependency of mem variables on mem variables is cut off 
35
   by duplication of some mem vars into local node vars.
36
   Thus, cylic dependency errors may only arise between no-mem vars.
37
   non-mem variables are:
38
   - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
39
   - read mems (fake vars): same remark as above.
40
   - outputs: decoupled from mems, if necessary
41
   - locals
42
   - instance vars (fake vars): simplify causality analysis
43
   
44
   global constants are not part of the dependency graph.
45
   
46
   no_mem' = combinational(no_mem, mem);
47
   => (mem -> no_mem' -> no_mem)
48

    
49
   mem' = pre(no_mem, mem);
50
   => (mem' -> no_mem), (mem -> mem')
51
   
52
   Global roadmap:
53
   - compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem)
54
   - check cycles in g (a cycle means a dependency error)
55
   - break cycles in g' (it's legal !):
56
     - check cycles in g'
57
     - if any, introduce aux var to break cycle, then start afresh
58
   - insert g' into g
59
   - return g
60
*)
61

    
62
(* Tests whether [v] is a root of graph [g], i.e. a source *)
63
let is_graph_root v g =
64
  IdentDepGraph.in_degree g v = 0
65

    
66
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
67
let graph_roots g =
68
  IdentDepGraph.fold_vertex
69
    (fun v roots -> if is_graph_root v g then v::roots else roots)
70
    g []
71

    
72
let add_edges src tgt g =
73
 (*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)
74
  List.iter
75
    (fun s ->
76
      List.iter
77
	(fun t -> IdentDepGraph.add_edge g s t)
78
	tgt)
79
    src;
80
  g
81

    
82
let add_vertices vtc g =
83
 (*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
84
  List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
85
  g
86

    
87
let new_graph () =
88
  IdentDepGraph.create ()
89

    
90
module ExprDep = struct
91

    
92
  let instance_var_cpt = ref 0
93

    
94
(* read vars represent input/mem read-only vars,
95
   they are not part of the program/schedule,
96
   as they are not assigned,
97
   but used to compute useless inputs/mems.
98
   a mem read var represents a mem at the beginning of a cycle  *)
99
  let mk_read_var id =
100
    sprintf "#%s" id
101

    
102
(* instance vars represent node instance calls,
103
   they are not part of the program/schedule,
104
   but used to simplify causality analysis
105
*)
106
  let mk_instance_var id =
107
    incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt
108

    
109
  let is_read_var v = v.[0] = '#'
110

    
111
  let is_instance_var v = v.[0] = '!'
112

    
113
  let is_ghost_var v = is_instance_var v || is_read_var v
114

    
115
  let undo_read_var id =
116
    assert (is_read_var id);
117
    String.sub id 1 (String.length id - 1)
118

    
119
  let undo_instance_var id =
120
    assert (is_instance_var id);
121
    String.sub id 1 (String.length id - 1)
122

    
123
  let eq_memory_variables mems eq =
124
    let rec match_mem lhs rhs mems =
125
      match rhs.expr_desc with
126
      | Expr_fby _
127
      | Expr_pre _    -> List.fold_right ISet.add lhs mems
128
      | Expr_tuple tl -> 
129
	 let lhs' = (transpose_list [lhs]) in
130
	 List.fold_right2 match_mem lhs' tl mems
131
      | _             -> mems in
132
    match_mem eq.eq_lhs eq.eq_rhs mems
133

    
134
  let node_memory_variables nd =
135
    List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
136

    
137
  let node_input_variables nd =
138
    List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
139

    
140
  let node_local_variables nd =
141
    List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
142

    
143
  let node_constant_variables nd =
144
    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
145

    
146
  let node_output_variables nd =
147
    List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
148

    
149
  let node_auxiliary_variables nd =
150
    ISet.diff (node_local_variables nd) (node_memory_variables nd)
151

    
152
  let node_variables nd =
153
    let inputs = node_input_variables nd in
154
    let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in
155
    List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals
156

    
157
(* computes the equivalence relation relating variables 
158
   in the same equation lhs, under the form of a table 
159
   of class representatives *)
160
  let node_eq_equiv nd =
161
    let eq_equiv = Hashtbl.create 23 in
162
    List.iter (fun eq ->
163
      let first = List.hd eq.eq_lhs in
164
      List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
165
    )
166
      (get_node_eqs nd);
167
    eq_equiv
168

    
169
(* Create a tuple of right dimension, according to [expr] type, *)
170
(* filled with variable [v] *)
171
  let adjust_tuple v expr =
172
    match expr.expr_type.Types.tdesc with
173
    | Types.Ttuple tl -> duplicate v (List.length tl)
174
    | _         -> [v]
175

    
176

    
177
  (* Add dependencies from lhs to rhs in [g, g'], *)
178
  (* no-mem/no-mem and mem/no-mem in g            *)
179
  (* mem/mem in g'                                *)
180
  (*     match (lhs_is_mem, ISet.mem x mems) with
181
	 | (false, true ) -> (add_edges [x] lhs g,
182
	 g')
183
	 | (false, false) -> (add_edges lhs [x] g,
184
	 g')
185
	 | (true , false) -> (add_edges lhs [x] g,
186
	 g')
187
	 | (true , true ) -> (g,
188
	 add_edges [x] lhs g')
189
  *)
190
  let add_eq_dependencies mems inputs node_vars eq (g, g') =
191
    let add_var lhs_is_mem lhs x (g, g') =
192
      if is_instance_var x || ISet.mem x node_vars then
193
	if ISet.mem x mems
194
	then
195
	  let g = add_edges lhs [mk_read_var x] g in
196
	  if lhs_is_mem
197
	  then
198
	    (g, add_edges [x] lhs g')
199
	  else
200
	    (add_edges [x] lhs g, g')
201
	else
202
	  let x = if ISet.mem x inputs then mk_read_var x else x in
203
	  (add_edges lhs [x] g, g')
204
      else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)
205
    in
206
  (* Add dependencies from [lhs] to rhs clock [ck]. *)
207
    let rec add_clock lhs_is_mem lhs ck g =
208
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
209
      match (Clocks.repr ck).Clocks.cdesc with
210
      | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
211
      | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
212
      | _                         -> g 
213
    in
214
    let rec add_dep lhs_is_mem lhs rhs g =
215
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
216
    (* i.e every input is connected to every output, through a ghost var *)
217
      let mashup_appl_dependencies f e g =
218
	let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
219
	List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
220
	  (expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
221
      in
222
      match rhs.expr_desc with
223
      | Expr_const _    -> g
224
      | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
225
      | Expr_pre e      -> add_dep true lhs e g
226
      | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
227
      | Expr_access (e1, d)
228
      | Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
229
      | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
230
      | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
231
      | 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)
232
      | 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))
233
      | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
234
      | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
235
      | Expr_appl (f, e, None) ->
236
	 if Basic_library.is_expr_internal_fun rhs
237
      (* tuple component-wise dependency for internal operators *)
238
	 then
239
	   List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
240
      (* mashed up dependency for user-defined operators *)
241
	 else
242
	   mashup_appl_dependencies f e g
243
      | Expr_appl (f, e, Some c) ->
244
	 mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
245
    in
246
    let g =
247
      List.fold_left
248
	(fun g lhs ->
249
	  if ISet.mem lhs mems then
250
	    add_vertices [lhs; mk_read_var lhs] g
251
	  else
252
	    add_vertices [lhs] g
253
	)
254
	g eq.eq_lhs
255
    in
256
    add_dep false eq.eq_lhs eq.eq_rhs (g, g')
257
      
258

    
259
  (* Returns the dependence graph for node [n] *)
260
  let dependence_graph mems inputs node_vars n =
261
    instance_var_cpt := 0;
262
    let g = new_graph (), new_graph () in
263
    (* Basic dependencies *)
264
    let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
265
    (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
266
       faut imposer que les outputs dépendent des asserts pour identifier que les
267
       fcn calls des asserts sont évalués avant le noeuds *)
268
    
269
    (* (\* In order to introduce dependencies between assert expressions and the node, *)
270
    (*    we build an artificial dependency between node output and each assert *)
271
    (*    expr. While these are not valid equations, they should properly propage in *)
272
    (*    function add_eq_dependencies *\) *)
273
    (* let g = *)
274
    (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
275
    (*   List.fold_left (fun g ae -> *)
276
    (*     let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)
277
    (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
278
    (* ) g n.node_asserts in  *)
279
    g
280

    
281
end
282

    
283
module NodeDep = struct
284

    
285
  module ExprModule =
286
  struct
287
    type t = expr
288
    let compare = compare
289
    let hash n = Hashtbl.hash n
290
    let equal n1 n2 = n1 = n2
291
  end
292

    
293
  module ESet = Set.Make(ExprModule)
294

    
295
  let rec get_expr_calls prednode expr = 
296
    match expr.expr_desc with
297
    | Expr_const _ 
298
    | Expr_ident _ -> ESet.empty
299
    | Expr_access (e, _)
300
    | Expr_power (e, _) -> get_expr_calls prednode e
301
    | Expr_array t
302
    | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
303
    | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
304
    | Expr_fby (e1,e2)
305
    | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
306
    | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
307
    | Expr_pre e 
308
    | Expr_when (e,_,_) -> get_expr_calls prednode e
309
    | Expr_appl (id,e, _) ->
310
       if not (Basic_library.is_expr_internal_fun expr) && prednode id
311
       then ESet.add expr (get_expr_calls prednode e)
312
       else (get_expr_calls prednode e)
313

    
314
  let get_callee expr =
315
    match expr.expr_desc with
316
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
317
    | _ -> None
318

    
319
  let get_calls prednode eqs =
320
    let deps =
321
      List.fold_left 
322
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
323
	ESet.empty
324
	eqs in
325
    ESet.elements deps
326

    
327
  let dependence_graph prog =
328
    let g = new_graph () in
329
    let g = List.fold_right 
330
      (fun td accu -> (* for each node we add its dependencies *)
331
	match td.top_decl_desc with 
332
	| Node nd ->
333
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
334
	   let accu = add_vertices [nd.node_id] accu in
335
	   let deps = List.map
336
	     (fun e -> fst (desome (get_callee e)))
337
	     (get_calls (fun _ -> true) (get_node_eqs nd)) 
338
	   in
339
	     (* Adding assert expressions deps *)
340
	   let deps_asserts =
341
	     let prednode = (fun _ -> true) in (* what is this about? *)
342
	     List.map
343
	       (fun e -> fst (desome (get_callee e)))
344
 	       (ESet.elements
345
		  (List.fold_left
346
		     (fun accu assert_expr -> ESet.union accu (get_expr_calls prednode assert_expr))
347
		     ESet.empty
348
		     (List.map (fun _assert -> _assert.assert_expr) nd.node_asserts)
349
		  )
350
	       )
351
      	   in
352
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
353
	   add_edges [nd.node_id] (deps@deps_asserts) accu
354
	| _ -> assert false (* should not happen *)
355
	   
356
      ) prog g in
357
    g   
358

    
359
  (* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
360
  let slice_graph gr v =
361
    begin
362
      let gr' = new_graph () in
363
      IdentDepGraph.add_vertex gr' v;
364
      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;
365
      gr'
366
    end
367
      
368
  let rec filter_static_inputs inputs args =
369
    match inputs, args with
370
    | []   , [] -> []
371
    | 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
372
    | _ -> assert false
373

    
374
  let compute_generic_calls prog =
375
    List.iter
376
      (fun td ->
377
	match td.top_decl_desc with 
378
	| Node nd ->
379
	   let prednode n = is_generic_node (Hashtbl.find node_table n) in
380
	   nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
381
	| _ -> ()
382
	   
383
      ) prog
384

    
385
end
386

    
387
module CycleDetection = struct
388

    
389
  (* ---- Look for cycles in a dependency graph *)
390
  module Cycles = Graph.Components.Make (IdentDepGraph)
391

    
392
  let mk_copy_var n id =
393
    let used name =
394
      (List.exists (fun v -> v.var_id = name) n.node_locals)
395
      || (List.exists (fun v -> v.var_id = name) n.node_inputs)
396
      || (List.exists (fun v -> v.var_id = name) n.node_outputs)
397
    in mk_new_name used id
398

    
399
  let mk_copy_eq n var =
400
    let var_decl = get_node_var var n in
401
    let cp_var = mk_copy_var n var in
402
    let expr =
403
      { expr_tag = Utils.new_tag ();
404
	expr_desc = Expr_ident var;
405
	expr_type = var_decl.var_type;
406
	expr_clock = var_decl.var_clock;
407
	expr_delay = Delay.new_var ();
408
	expr_annot = None;
409
	expr_loc = var_decl.var_loc } in
410
    { var_decl with var_id = cp_var; var_orig = false },
411
    mkeq var_decl.var_loc ([cp_var], expr)
412

    
413
  let wrong_partition g partition =
414
    match partition with
415
    | [id]    -> IdentDepGraph.mem_edge g id id
416
    | _::_::_ -> true
417
    | []      -> assert false
418

    
419
  (* Checks that the dependency graph [g] does not contain a cycle. Raises
420
     [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
421
  let check_cycles g =
422
    let scc_l = Cycles.scc_list g in
423
    List.iter (fun partition ->
424
      if wrong_partition g partition then
425
	raise (Error (DataCycle partition))
426
      else ()
427
    ) scc_l
428

    
429
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
430
  let copy_partition g partition =
431
    let copy_g = IdentDepGraph.create () in
432
    IdentDepGraph.iter_edges
433
      (fun src tgt ->
434
	if List.mem src partition && List.mem tgt partition
435
	then IdentDepGraph.add_edge copy_g src tgt)
436
      g
437

    
438
      
439
  (* Breaks dependency cycles in a graph [g] by inserting aux variables.
440
     [head] is a head of a non-trivial scc of [g]. 
441
     In Lustre, this is legal only for mem/mem cycles *)
442
  let break_cycle head cp_head g =
443
    let succs = IdentDepGraph.succ g head in
444
    IdentDepGraph.add_edge g head cp_head;
445
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
446
    List.iter
447
      (fun s ->
448
	IdentDepGraph.remove_edge g head s;
449
	IdentDepGraph.add_edge    g s cp_head)
450
      succs
451

    
452
  (* Breaks cycles of the dependency graph [g] of memory variables [mems]
453
     belonging in node [node]. Returns:
454
     - a list of new auxiliary variable declarations
455
     - a list of new equations
456
     - a modified acyclic version of [g]
457
  *)
458
  let break_cycles node mems g =
459
    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
460
    let rec break vdecls mem_eqs g =
461
      let scc_l = Cycles.scc_list g in
462
      let wrong = List.filter (wrong_partition g) scc_l in
463
      match wrong with
464
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
465
      | [head]::_       ->
466
	 begin
467
	   IdentDepGraph.remove_edge g head head;
468
	   break vdecls mem_eqs g
469
	 end
470
      | (head::part)::_ -> 
471
	 begin
472
	   let vdecl_cp_head, cp_eq = mk_copy_eq node head in
473
	   let pvar v = List.mem v part in
474
	   let fvar v = if v = head then vdecl_cp_head.var_id else v in
475
	   let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
476
	   break_cycle head vdecl_cp_head.var_id g;
477
	   break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
478
	 end
479
      | _               -> assert false
480
    in break [] mem_eqs g
481

    
482
end
483

    
484
(* Module used to compute static disjunction of variables based upon their clocks. *)
485
module Disjunction =
486
struct
487
  module ClockedIdentModule =
488
  struct
489
    type t = var_decl
490
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
491
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
492
  end
493

    
494
  module CISet = Set.Make(ClockedIdentModule)
495

    
496
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
497
     maybe removing shorter branches *)
498
  type disjoint_map = (ident, CISet.t) Hashtbl.t
499

    
500
  let pp_ciset fmt t =
501
    begin
502
      Format.fprintf fmt "{@ ";
503
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
504
      Format.fprintf fmt "}@."
505
    end
506

    
507
  let clock_disjoint_map vdecls =
508
    let map = Hashtbl.create 23 in
509
    begin
510
      List.iter
511
	(fun v1 -> let disj_v1 =
512
		     List.fold_left
513
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
514
		       CISet.empty
515
		       vdecls in
516
		   (* disjoint vdecls are stored in increasing branch length order *)
517
		   Hashtbl.add map v1.var_id disj_v1)
518
	vdecls;
519
      (map : disjoint_map)
520
    end
521

    
522
  (* merge variables [v] and [v'] in disjunction [map]. Then:
523
     - the mapping v' becomes v' |-> (map v) inter (map v')
524
     - the mapping v |-> ... then disappears
525
     - other mappings become x |-> (map x) \ (if v in x then v else v')
526
  *)
527
  let merge_in_disjoint_map map v v' =
528
    begin
529
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
530
      Hashtbl.remove map v.var_id;
531
      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;
532
    end
533

    
534
  (* replace variable [v] by [v'] in disjunction [map].
535
     [v'] is a dead variable. Then:
536
     - the mapping v' becomes v' |-> (map v)
537
     - the mapping v |-> ... then disappears
538
     - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
539
  *)
540
  let replace_in_disjoint_map map v v' =
541
    begin
542
      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
543
      Hashtbl.remove  map v.var_id;
544
      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;
545
    end
546

    
547
  (* remove variable [v] in disjunction [map]. Then:
548
     - the mapping v |-> ... then disappears
549
     - all mappings become x |-> (map x) \ { v}
550
  *)
551
  let remove_in_disjoint_map map v =
552
    begin
553
      Hashtbl.remove map v.var_id;
554
      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;
555
    end
556

    
557
  let pp_disjoint_map fmt map =
558
    begin
559
      Format.fprintf fmt "{ /* disjoint map */@.";
560
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
561
      Format.fprintf fmt "}@."
562
    end
563
end
564

    
565
let pp_dep_graph fmt g =
566
  begin
567
    Format.fprintf fmt "{ /* graph */@.";
568
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
569
    Format.fprintf fmt "}@."
570
  end
571

    
572
let pp_error fmt err =
573
  match err with
574
  | DataCycle trace ->
575
     fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
576
       (fprintf_list ~sep:", " pp_print_string) trace
577
  | NodeCycle trace ->
578
     fprintf fmt "@.Causality error, cyclic node calls: %a@."
579
       (fprintf_list ~sep:", " pp_print_string) trace
580

    
581
(* Merges elements of graph [g2] into graph [g1] *)
582
let merge_with g1 g2 =
583
  begin
584
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
585
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
586
  end
587

    
588
let world = "!!_world"
589

    
590
let add_external_dependency outputs mems g =
591
  begin
592
    IdentDepGraph.add_vertex g world;
593
    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
594
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
595
  end
596

    
597
let global_dependency node =
598
  let mems = ExprDep.node_memory_variables node in
599
  let inputs =
600
    ISet.union
601
      (ExprDep.node_input_variables node)
602
      (ExprDep.node_constant_variables node) in
603
  let outputs = ExprDep.node_output_variables node in
604
  let node_vars = ExprDep.node_variables node in
605
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
606
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
607
    Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
608
  CycleDetection.check_cycles g_non_mems;
609
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
610
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
611
  begin
612
    merge_with g_non_mems g_mems';
613
    add_external_dependency outputs mems g_non_mems;
614
    { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
615
    g_non_mems
616
  end
617

    
618
(* Local Variables: *)
619
(* compile-command:"make -C .." *)
620
(* End: *)
(7-7/61)