Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ f4cba4b8

History | View | Annotate | Download (24.6 KB)

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

    
14

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

    
22

    
23
type identified_call = eq * tag
24
type error =
25
  | DataCycle of ident list list (* multiple failed partitions at once *) 
26
  | NodeCycle of ident list
27

    
28
exception Error of error
29

    
30

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

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

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

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

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

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

    
85
let new_graph () =
86
  IdentDepGraph.create ()
87

    
88
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
89
let slice_graph gr v =
90
  begin
91
    let gr' = new_graph () in
92
    IdentDepGraph.add_vertex gr' v;
93
    Bfs.iter_component (fun v -> IdentDepGraph.iter_succ (fun s -> IdentDepGraph.add_vertex gr' s; IdentDepGraph.add_edge gr' v s) gr v) gr v;
94
    gr'
95
  end
96

    
97
    
98
module ExprDep = struct
99
  let get_node_eqs nd =
100
    let eqs, auts = get_node_eqs nd in
101
    if auts != [] then assert false (* No call on causality on a Lustre model
102
				       with automaton. They should be expanded by now. *);
103
    eqs
104
      
105
  let instance_var_cpt = ref 0
106

    
107
(* read vars represent input/mem read-only vars,
108
   they are not part of the program/schedule,
109
   as they are not assigned,
110
   but used to compute useless inputs/mems.
111
   a mem read var represents a mem at the beginning of a cycle  *)
112
  let mk_read_var id =
113
    Format.sprintf "#%s" id
114

    
115
(* instance vars represent node instance calls,
116
   they are not part of the program/schedule,
117
   but used to simplify causality analysis
118
*)
119
  let mk_instance_var id =
120
    incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt
121

    
122
  let is_read_var v = v.[0] = '#'
123

    
124
  let is_instance_var v = v.[0] = '!'
125

    
126
  let is_ghost_var v = is_instance_var v || is_read_var v
127

    
128
  let undo_read_var id =
129
    assert (is_read_var id);
130
    String.sub id 1 (String.length id - 1)
131

    
132
  let undo_instance_var id =
133
    assert (is_instance_var id);
134
    String.sub id 1 (String.length id - 1)
135

    
136
  let eq_memory_variables mems eq =
137
    let rec match_mem lhs rhs mems =
138
      match rhs.expr_desc with
139
      | Expr_fby _
140
      | Expr_pre _    -> List.fold_right ISet.add lhs mems
141
      | Expr_tuple tl -> 
142
	 let lhs' = (transpose_list [lhs]) in
143
	 List.fold_right2 match_mem lhs' tl mems
144
      | _             -> mems in
145
    match_mem eq.eq_lhs eq.eq_rhs mems
146

    
147
  let node_memory_variables nd =
148
    List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
149

    
150
  let node_input_variables nd =
151
    List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty 
152
      (if nd.node_iscontract then
153
         nd.node_inputs@nd.node_outputs
154
       else
155
         nd.node_inputs)
156
    
157
  let node_output_variables nd =
158
    List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty
159
      (if nd.node_iscontract then [] else nd.node_outputs)
160

    
161
  let node_local_variables nd =
162
    List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
163

    
164
  let node_constant_variables nd =
165
    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
166

    
167
  let node_auxiliary_variables nd =
168
    ISet.diff (node_local_variables nd) (node_memory_variables nd)
169

    
170
  let node_variables nd =
171
    let inputs = node_input_variables nd in
172
    let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in
173
    List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals
174

    
175
(* computes the equivalence relation relating variables 
176
   in the same equation lhs, under the form of a table 
177
   of class representatives *)
178
  let eqs_eq_equiv eqs =
179
    let eq_equiv = Hashtbl.create 23 in
180
    List.iter (fun eq ->
181
      let first = List.hd eq.eq_lhs in
182
      List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
183
    )
184
      eqs;
185
    eq_equiv
186
    
187
  let node_eq_equiv nd = eqs_eq_equiv  (get_node_eqs nd)
188
  
189
(* Create a tuple of right dimension, according to [expr] type, *)
190
(* filled with variable [v] *)
191
  let adjust_tuple v expr =
192
    match expr.expr_type.Types.tdesc with
193
    | Types.Ttuple tl -> duplicate v (List.length tl)
194
    | _         -> [v]
195

    
196

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

    
279
  (* Returns the dependence graph for node [n] *)
280
  let dependence_graph mems inputs node_vars n =
281
    instance_var_cpt := 0;
282
    let g = new_graph (), new_graph () in
283
    (* Basic dependencies *)
284
    let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
285
    (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
286
       faut imposer que les outputs dépendent des asserts pour identifier que les
287
       fcn calls des asserts sont évalués avant le noeuds *)
288
    
289
    (* (\* In order to introduce dependencies between assert expressions and the node, *)
290
    (*    we build an artificial dependency between node output and each assert *)
291
    (*    expr. While these are not valid equations, they should properly propage in *)
292
    (*    function add_eq_dependencies *\) *)
293
    (* let g = *)
294
    (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
295
    (*   List.fold_left (fun g ae -> *)
296
    (*     let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)
297
    (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
298
    (* ) g n.node_asserts in  *)
299
    g
300

    
301
end
302

    
303
module NodeDep = struct
304

    
305
  module ExprModule =
306
  struct
307
    type t = expr
308
    let compare = compare
309
    let hash n = Hashtbl.hash n
310
    let equal n1 n2 = n1 = n2
311
  end
312

    
313
  module ESet = Set.Make(ExprModule)
314

    
315
  let rec get_expr_calls prednode expr = 
316
    match expr.expr_desc with
317
    | Expr_const _ 
318
    | Expr_ident _ -> ESet.empty
319
    | Expr_access (e, _)
320
    | Expr_power (e, _) -> get_expr_calls prednode e
321
    | Expr_array t
322
    | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
323
    | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
324
    | Expr_fby (e1,e2)
325
    | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
326
    | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
327
    | Expr_pre e 
328
    | Expr_when (e,_,_) -> get_expr_calls prednode e
329
    | Expr_appl (id,e, _) ->
330
       if not (Basic_library.is_expr_internal_fun expr) && prednode id
331
       then ESet.add expr (get_expr_calls prednode e)
332
       else (get_expr_calls prednode e)
333

    
334
  let get_callee expr =
335
    match expr.expr_desc with
336
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
337
    | _ -> None
338

    
339
  let get_calls prednode nd =
340
    let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl in
341
    let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in
342
    let rec get_stmt_calls s =
343
      match s with Eq eq -> get_eq_calls eq | Aut aut -> get_aut_calls aut 
344
    and get_aut_calls aut =
345
      let get_handler_calls h =
346
	let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in
347
	let until = get_cond_calls h.hand_until in
348
	let unless = get_cond_calls h.hand_unless in
349
	let calls = ESet.union until unless in 
350
	let calls = accu get_stmt_calls calls h.hand_stmts in
351
	let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in
352
	(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *)
353
	calls
354
      in
355
      accu get_handler_calls ESet.empty aut.aut_handlers
356
    in
357
    let eqs, auts = get_node_eqs nd in
358
    let deps = accu get_eq_calls ESet.empty eqs in
359
    let deps = accu get_aut_calls deps auts in
360
    ESet.elements deps
361

    
362
  let dependence_graph prog =
363
    let g = new_graph () in
364
    let g = List.fold_right 
365
      (fun td accu -> (* for each node we add its dependencies *)
366
	match td.top_decl_desc with 
367
	| Node nd ->
368
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
369
	   let accu = add_vertices [nd.node_id] accu in
370
	   let deps = List.map
371
	     (fun e -> fst (desome (get_callee e)))
372
	     (get_calls (fun _ -> true) nd) 
373
	   in
374
	     (* Adding assert expressions deps *)
375
	   let deps_asserts =
376
	     let prednode = (fun _ -> true) in (* what is this about? *)
377
	     List.map
378
	       (fun e -> fst (desome (get_callee e)))
379
 	       (ESet.elements
380
		  (List.fold_left
381
		     (fun accu assert_expr -> ESet.union accu (get_expr_calls prednode assert_expr))
382
		     ESet.empty
383
		     (List.map (fun _assert -> _assert.assert_expr) nd.node_asserts)
384
		  )
385
	       )
386
      	   in
387
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
388
	   add_edges [nd.node_id] (deps@deps_asserts) accu
389
	| _ -> assert false (* should not happen *)
390
	   
391
      ) prog g in
392
    g   
393
      
394
  let rec filter_static_inputs inputs args =
395
    match inputs, args with
396
    | []   , [] -> []
397
    | 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
398
    | _ -> assert false
399

    
400
  let compute_generic_calls prog =
401
    List.iter
402
      (fun td ->
403
	match td.top_decl_desc with 
404
	| Node nd ->
405
	   let prednode n = is_generic_node (node_from_name n) in
406
	   nd.node_gencalls <- get_calls prednode nd
407
	| _ -> ()
408
	   
409
      ) prog
410

    
411
end
412

    
413

    
414
module CycleDetection = struct
415

    
416
  (* ---- Look for cycles in a dependency graph *)
417
  module Cycles = Graph.Components.Make (IdentDepGraph)
418

    
419
  let mk_copy_var n id =
420
    let used name =
421
      (List.exists (fun v -> v.var_id = name) n.node_locals)
422
      || (List.exists (fun v -> v.var_id = name) n.node_inputs)
423
      || (List.exists (fun v -> v.var_id = name) n.node_outputs)
424
    in mk_new_name used id
425

    
426
  let mk_copy_eq n var =
427
    let var_decl = get_node_var var n in
428
    let cp_var = mk_copy_var n var in
429
    let expr =
430
      { expr_tag = Utils.new_tag ();
431
	expr_desc = Expr_ident var;
432
	expr_type = var_decl.var_type;
433
	expr_clock = var_decl.var_clock;
434
	expr_delay = Delay.new_var ();
435
	expr_annot = None;
436
	expr_loc = var_decl.var_loc } in
437
    { var_decl with var_id = cp_var; var_orig = false },
438
    mkeq var_decl.var_loc ([cp_var], expr)
439

    
440
  let wrong_partition g partition =
441
    match partition with
442
    | [id]    -> IdentDepGraph.mem_edge g id id
443
    | _::_::_ -> true
444
    | []      -> assert false
445

    
446
  (* Checks that the dependency graph [g] does not contain a cycle. Raises
447
     [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
448
  let check_cycles g =
449
    let scc_l = Cycles.scc_list g in
450
    let algebraic_loops = List.filter (wrong_partition g) scc_l in
451
    if List.length algebraic_loops > 0 then
452
      raise (Error (DataCycle algebraic_loops))
453
	(* We extract a hint to resolve the cycle: for each variable in the cycle
454
	   which is defined by a call, we return the name of the node call and
455
	   its specific id *)
456

    
457
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
458
  let copy_partition g partition =
459
    let copy_g = IdentDepGraph.create () in
460
    IdentDepGraph.iter_edges
461
      (fun src tgt ->
462
	if List.mem src partition && List.mem tgt partition
463
	then IdentDepGraph.add_edge copy_g src tgt)
464
      g
465

    
466
      
467
  (* Breaks dependency cycles in a graph [g] by inserting aux variables.
468
     [head] is a head of a non-trivial scc of [g]. 
469
     In Lustre, this is legal only for mem/mem cycles *)
470
  let break_cycle head cp_head g =
471
    let succs = IdentDepGraph.succ g head in
472
    IdentDepGraph.add_edge g head cp_head;
473
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
474
    List.iter
475
      (fun s ->
476
	IdentDepGraph.remove_edge g head s;
477
	IdentDepGraph.add_edge    g s cp_head)
478
      succs
479

    
480
  (* Breaks cycles of the dependency graph [g] of memory variables [mems]
481
     belonging in node [node]. Returns:
482
     - a list of new auxiliary variable declarations
483
     - a list of new equations
484
     - a modified acyclic version of [g]
485
  *)
486
  let break_cycles node mems g =
487
    let eqs , auts = get_node_eqs node in
488
    assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *)
489
    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in
490
    let rec break vdecls mem_eqs g =
491
      let scc_l = Cycles.scc_list g in
492
      let wrong = List.filter (wrong_partition g) scc_l in
493
      match wrong with
494
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
495
      | [head]::_       ->
496
	 begin
497
	   IdentDepGraph.remove_edge g head head;
498
	   break vdecls mem_eqs g
499
	 end
500
      | (head::part)::_ -> 
501
	 begin
502
	   let vdecl_cp_head, cp_eq = mk_copy_eq node head in
503
	   let pvar v = List.mem v part in
504
	   let fvar v = if v = head then vdecl_cp_head.var_id else v in
505
	   let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
506
	   break_cycle head vdecl_cp_head.var_id g;
507
	   break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
508
	 end
509
      | _               -> assert false
510
    in break [] mem_eqs g
511

    
512
end
513

    
514
(* Module used to compute static disjunction of variables based upon their clocks. *)
515
module Disjunction =
516
struct
517
  module ClockedIdentModule =
518
  struct
519
    type t = var_decl
520
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
521
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
522
  end
523

    
524
  module CISet = Set.Make(ClockedIdentModule)
525

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

    
530
  let pp_ciset fmt t =
531
    begin
532
      Format.fprintf fmt "{@ ";
533
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
534
      Format.fprintf fmt "}@."
535
    end
536

    
537
  let clock_disjoint_map vdecls =
538
    let map = Hashtbl.create 23 in
539
    begin
540
      List.iter
541
	(fun v1 -> let disj_v1 =
542
		     List.fold_left
543
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
544
		       CISet.empty
545
		       vdecls in
546
		   (* disjoint vdecls are stored in increasing branch length order *)
547
		   Hashtbl.add map v1.var_id disj_v1)
548
	vdecls;
549
      (map : disjoint_map)
550
    end
551

    
552
  (* merge variables [v] and [v'] in disjunction [map]. Then:
553
     - the mapping v' becomes v' |-> (map v) inter (map v')
554
     - the mapping v |-> ... then disappears
555
     - other mappings become x |-> (map x) \ (if v in x then v else v')
556
  *)
557
  let merge_in_disjoint_map map v v' =
558
    begin
559
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
560
      Hashtbl.remove map v.var_id;
561
      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;
562
    end
563

    
564
  (* replace variable [v] by [v'] in disjunction [map].
565
     [v'] is a dead variable. Then:
566
     - the mapping v' becomes v' |-> (map v)
567
     - the mapping v |-> ... then disappears
568
     - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
569
  *)
570
  let replace_in_disjoint_map map v v' =
571
    begin
572
      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
573
      Hashtbl.remove  map v.var_id;
574
      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;
575
    end
576

    
577
  (* remove variable [v] in disjunction [map]. Then:
578
     - the mapping v |-> ... then disappears
579
     - all mappings become x |-> (map x) \ { v}
580
  *)
581
  let remove_in_disjoint_map map v =
582
    begin
583
      Hashtbl.remove map v.var_id;
584
      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;
585
    end
586

    
587
  let pp_disjoint_map fmt map =
588
    begin
589
      Format.fprintf fmt "{ /* disjoint map */@.";
590
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
591
      Format.fprintf fmt "}@."
592
    end
593
end
594

    
595
  
596
let pp_dep_graph fmt g =
597
  begin
598
    Format.fprintf fmt "{ /* graph */@.";
599
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
600
    Format.fprintf fmt "}@."
601
  end
602

    
603
let pp_error fmt err =
604
  match err with
605
  | NodeCycle trace ->
606
     Format.fprintf fmt "Causality error, cyclic node calls:@   @[<v 0>%a@]@ "
607
       (fprintf_list ~sep:",@ " Format.pp_print_string) trace
608
  | DataCycle traces -> (
609
     Format.fprintf fmt "Causality error, cyclic data dependencies:@   @[<v 0>%a@]@ "
610
       (fprintf_list ~sep:";@ "
611
       (fun fmt trace ->
612
	 Format.fprintf fmt "@[<v 0>{%a}@]"
613
	   (fprintf_list ~sep:",@ " Format.pp_print_string)
614
	   trace
615
       )) traces
616
  )
617
     
618
(* Merges elements of graph [g2] into graph [g1] *)
619
let merge_with g1 g2 =
620
  begin
621
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
622
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
623
  end
624

    
625
let world = "!!_world"
626

    
627
let add_external_dependency outputs mems g =
628
  begin
629
    IdentDepGraph.add_vertex g world;
630
    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
631
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
632
  end
633

    
634
(* Takes a node and return a pair (node', graph) where node' is node
635
   rebuilt with the equations enriched with new ones introduced to
636
   "break cycles" *)
637
let global_dependency node =
638
  let mems = ExprDep.node_memory_variables node in
639
  let inputs =
640
    ISet.union
641
      (ExprDep.node_input_variables node)
642
      (ExprDep.node_constant_variables node) in
643
  let outputs = ExprDep.node_output_variables node in
644
  let node_vars = ExprDep.node_variables node in
645
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
646
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
647
    Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
648
  try
649
    CycleDetection.check_cycles g_non_mems;
650
    let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
651
    (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
652
    begin
653
      merge_with g_non_mems g_mems';
654
      add_external_dependency outputs mems g_non_mems;
655
      { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
656
      g_non_mems
657
    end
658
  with Error (DataCycle _ as exc) -> (
659
      raise (Error (exc))
660
  )
661

    
662
(* A module to sort dependencies among local variables when relying on clocked declarations *)
663
module VarClockDep =
664
struct
665
  let rec get_clock_dep ck =
666
    match ck.Clocks.cdesc with
667
    | Clocks.Con (ck ,c ,l) -> l::(get_clock_dep ck)
668
    | Clocks.Clink ck' 
669
    | Clocks.Ccarrying (_, ck') -> get_clock_dep ck'
670
    | _ -> []
671
      
672
  let sort locals =
673
    let g = new_graph () in
674
    let g = List.fold_left (
675
      fun g var_decl ->
676
	let deps = get_clock_dep var_decl.var_clock in
677
	add_edges [var_decl.var_id] deps g
678
    ) g locals
679
    in
680
    let sorted, no_deps =
681
      TopologicalDepGraph.fold (fun vid (accu, remaining) -> (
682
	let select v = v.var_id = vid in
683
	let selected, not_selected = List.partition select remaining in
684
	selected@accu, not_selected
685
      )) g ([],locals)
686
    in
687
    no_deps @ sorted
688
    
689
end
690
  
691
(* Local Variables: *)
692
(* compile-command:"make -C .." *)
693
(* End: *)