Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ cfe98135

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 no-mem vars.
40
   non-mem 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 (non-mem/non-mem&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 read-only 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
  (* no-mem/no-mem and mem/no-mem 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 user-defined 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 component-wise 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 user-defined 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 sub-graph 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 non-trivial 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
(* compile-command:"make -C .." *)
688
(* End: *)