Project

General

Profile

Download (25.5 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 Lustre_types
19
open Corelang
20

    
21

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

    
27
exception Error of error
28

    
29

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

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

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

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

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

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

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

    
87
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
88
let slice_graph gr v =
89
  begin
90
    let gr' = new_graph () in
91
    IdentDepGraph.add_vertex gr' v;
92
    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;
93
    gr'
94
  end
95

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
195

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

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

    
300
end
301

    
302
module NodeDep = struct
303

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

    
312
  module ESet = Set.Make(ExprModule)
313

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

    
333
  let get_eexpr_calls prednode ee =
334
    get_expr_calls prednode ee.eexpr_qfexpr
335
    
336
  let get_callee expr =
337
    match expr.expr_desc with
338
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
339
    | _ -> None
340

    
341
  let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl 
342

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

    
366
  let get_contract_calls prednode c =
367
    let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in
368
    let deps = accu (get_eexpr_calls prednode) deps ( c.assume @ c.guarantees @ (List.fold_left (fun accu m -> accu @ m.require @ m.ensure ) [] c.modes)) in
369
    let id_deps = List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps) in  
370
    let id_deps = (List.fold_left (fun accu imp -> imp.import_nodeid::accu) [] c.imports) @ id_deps in  
371
    id_deps
372
    
373
  let dependence_graph prog =
374
    let g = new_graph () in
375
    let g = List.fold_right 
376
      (fun td accu -> (* for each node we add its dependencies *)
377
	match td.top_decl_desc with 
378
	| Node nd ->
379
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
380
	   let accu = add_vertices [nd.node_id] accu in
381
	   let deps = List.map
382
	     (fun e -> fst (desome (get_callee e)))
383
	     (get_calls (fun _ -> true) nd) 
384
	   in
385
	     (* Adding assert expressions deps *)
386
	   let deps_asserts =
387
	     let prednode = (fun _ -> true) in (* what is this about? *)
388
	     List.map
389
	       (fun e -> fst (desome (get_callee e)))
390
 	       (ESet.elements
391
		  (List.fold_left
392
		     (fun accu assert_expr -> ESet.union accu (get_expr_calls prednode assert_expr))
393
		     ESet.empty
394
		     (List.map (fun _assert -> _assert.assert_expr) nd.node_asserts)
395
		  )
396
	       )
397
      	   in
398
           let deps_spec = match nd.node_spec with
399
             | None -> []
400
             | Some (NodeSpec id) -> [id]
401
             | Some (Contract c) -> get_contract_calls (fun _ -> true) c
402
                                  
403
           in
404
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
405
	   add_edges [nd.node_id] (deps@deps_asserts@deps_spec) accu
406
	| _ -> assert false (* should not happen *)
407
	   
408
      ) prog g in
409
    g   
410
      
411
  let rec filter_static_inputs inputs args =
412
    match inputs, args with
413
    | []   , [] -> []
414
    | 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
415
    | _ -> assert false
416

    
417
  let compute_generic_calls prog =
418
    List.iter
419
      (fun td ->
420
	match td.top_decl_desc with 
421
	| Node nd ->
422
	   let prednode n = is_generic_node (node_from_name n) in
423
	   nd.node_gencalls <- get_calls prednode nd
424
	| _ -> ()
425
	   
426
      ) prog
427

    
428
end
429

    
430

    
431
module CycleDetection = struct
432

    
433
  (* ---- Look for cycles in a dependency graph *)
434
  module Cycles = Graph.Components.Make (IdentDepGraph)
435

    
436
  let mk_copy_var n id =
437
    let used name =
438
      (List.exists (fun v -> v.var_id = name) n.node_locals)
439
      || (List.exists (fun v -> v.var_id = name) n.node_inputs)
440
      || (List.exists (fun v -> v.var_id = name) n.node_outputs)
441
    in mk_new_name used id
442

    
443
  let mk_copy_eq n var =
444
    let var_decl = get_node_var var n in
445
    let cp_var = mk_copy_var n var in
446
    let expr =
447
      { expr_tag = Utils.new_tag ();
448
	expr_desc = Expr_ident var;
449
	expr_type = var_decl.var_type;
450
	expr_clock = var_decl.var_clock;
451
	expr_delay = Delay.new_var ();
452
	expr_annot = None;
453
	expr_loc = var_decl.var_loc } in
454
    { var_decl with var_id = cp_var; var_orig = false },
455
    mkeq var_decl.var_loc ([cp_var], expr)
456

    
457
  let wrong_partition g partition =
458
    match partition with
459
    | [id]    -> IdentDepGraph.mem_edge g id id
460
    | _::_::_ -> true
461
    | []      -> assert false
462

    
463
  (* Checks that the dependency graph [g] does not contain a cycle. Raises
464
     [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
465
  let check_cycles g =
466
    let scc_l = Cycles.scc_list g in
467
    let algebraic_loops = List.filter (wrong_partition g) scc_l in
468
    if List.length algebraic_loops > 0 then
469
      raise (Error (DataCycle algebraic_loops))
470
	(* We extract a hint to resolve the cycle: for each variable in the cycle
471
	   which is defined by a call, we return the name of the node call and
472
	   its specific id *)
473

    
474
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
475
  let copy_partition g partition =
476
    let copy_g = IdentDepGraph.create () in
477
    IdentDepGraph.iter_edges
478
      (fun src tgt ->
479
	if List.mem src partition && List.mem tgt partition
480
	then IdentDepGraph.add_edge copy_g src tgt)
481
      g
482

    
483
      
484
  (* Breaks dependency cycles in a graph [g] by inserting aux variables.
485
     [head] is a head of a non-trivial scc of [g]. 
486
     In Lustre, this is legal only for mem/mem cycles *)
487
  let break_cycle head cp_head g =
488
    let succs = IdentDepGraph.succ g head in
489
    IdentDepGraph.add_edge g head cp_head;
490
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
491
    List.iter
492
      (fun s ->
493
	IdentDepGraph.remove_edge g head s;
494
	IdentDepGraph.add_edge    g s cp_head)
495
      succs
496

    
497
  (* Breaks cycles of the dependency graph [g] of memory variables [mems]
498
     belonging in node [node]. Returns:
499
     - a list of new auxiliary variable declarations
500
     - a list of new equations
501
     - a modified acyclic version of [g]
502
  *)
503
  let break_cycles node mems g =
504
    let eqs , auts = get_node_eqs node in
505
    assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *)
506
    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in
507
    let rec break vdecls mem_eqs g =
508
      let scc_l = Cycles.scc_list g in
509
      let wrong = List.filter (wrong_partition g) scc_l in
510
      match wrong with
511
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
512
      | [head]::_       ->
513
	 begin
514
	   IdentDepGraph.remove_edge g head head;
515
	   break vdecls mem_eqs g
516
	 end
517
      | (head::part)::_ -> 
518
	 begin
519
	   let vdecl_cp_head, cp_eq = mk_copy_eq node head in
520
	   let pvar v = List.mem v part in
521
	   let fvar v = if v = head then vdecl_cp_head.var_id else v in
522
	   let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
523
	   break_cycle head vdecl_cp_head.var_id g;
524
	   break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
525
	 end
526
      | _               -> assert false
527
    in break [] mem_eqs g
528

    
529
end
530

    
531
(* Module used to compute static disjunction of variables based upon their clocks. *)
532
module Disjunction =
533
struct
534
  module ClockedIdentModule =
535
  struct
536
    type t = var_decl
537
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
538
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
539
  end
540

    
541
  module CISet = Set.Make(ClockedIdentModule)
542

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

    
547
  let pp_ciset fmt t =
548
    begin
549
      Format.fprintf fmt "{@ ";
550
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
551
      Format.fprintf fmt "}@."
552
    end
553

    
554
  let clock_disjoint_map vdecls =
555
    let map = Hashtbl.create 23 in
556
    begin
557
      List.iter
558
	(fun v1 -> let disj_v1 =
559
		     List.fold_left
560
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
561
		       CISet.empty
562
		       vdecls in
563
		   (* disjoint vdecls are stored in increasing branch length order *)
564
		   Hashtbl.add map v1.var_id disj_v1)
565
	vdecls;
566
      (map : disjoint_map)
567
    end
568

    
569
  (* merge variables [v] and [v'] in disjunction [map]. Then:
570
     - the mapping v' becomes v' |-> (map v) inter (map v')
571
     - the mapping v |-> ... then disappears
572
     - other mappings become x |-> (map x) \ (if v in x then v else v')
573
  *)
574
  let merge_in_disjoint_map map v v' =
575
    begin
576
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
577
      Hashtbl.remove map v.var_id;
578
      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;
579
    end
580

    
581
  (* replace variable [v] by [v'] in disjunction [map].
582
     [v'] is a dead variable. Then:
583
     - the mapping v' becomes v' |-> (map v)
584
     - the mapping v |-> ... then disappears
585
     - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
586
  *)
587
  let replace_in_disjoint_map map v v' =
588
    begin
589
      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
590
      Hashtbl.remove  map v.var_id;
591
      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;
592
    end
593

    
594
  (* remove variable [v] in disjunction [map]. Then:
595
     - the mapping v |-> ... then disappears
596
     - all mappings become x |-> (map x) \ { v}
597
  *)
598
  let remove_in_disjoint_map map v =
599
    begin
600
      Hashtbl.remove map v.var_id;
601
      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;
602
    end
603

    
604
  let pp_disjoint_map fmt map =
605
    begin
606
      Format.fprintf fmt "{ /* disjoint map */@.";
607
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
608
      Format.fprintf fmt "}@."
609
    end
610
end
611

    
612
  
613
let pp_dep_graph fmt g =
614
  begin
615
    Format.fprintf fmt "{ /* graph */@.";
616
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
617
    Format.fprintf fmt "}@."
618
  end
619

    
620
let pp_error fmt err =
621
  match err with
622
  | NodeCycle trace ->
623
     Format.fprintf fmt "Causality error, cyclic node calls:@   @[<v 0>%a@]@ "
624
       (fprintf_list ~sep:",@ " Format.pp_print_string) trace
625
  | DataCycle traces -> (
626
     Format.fprintf fmt "Causality error, cyclic data dependencies:@   @[<v 0>%a@]@ "
627
       (fprintf_list ~sep:";@ "
628
       (fun fmt trace ->
629
	 Format.fprintf fmt "@[<v 0>{%a}@]"
630
	   (fprintf_list ~sep:",@ " Format.pp_print_string)
631
	   trace
632
       )) traces
633
  )
634
     
635
(* Merges elements of graph [g2] into graph [g1] *)
636
let merge_with g1 g2 =
637
  begin
638
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
639
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
640
  end
641

    
642
let world = "!!_world"
643

    
644
let add_external_dependency outputs mems g =
645
  begin
646
    IdentDepGraph.add_vertex g world;
647
    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
648
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
649
  end
650

    
651
(* Takes a node and return a pair (node', graph) where node' is node
652
   rebuilt with the equations enriched with new ones introduced to
653
   "break cycles" *)
654
let global_dependency node =
655
  let mems = ExprDep.node_memory_variables node in
656
  let inputs =
657
    ISet.union
658
      (ExprDep.node_input_variables node)
659
      (ExprDep.node_constant_variables node) in
660
  let outputs = ExprDep.node_output_variables node in
661
  let node_vars = ExprDep.node_variables node in
662
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
663
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
664
    Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
665
  try
666
    CycleDetection.check_cycles g_non_mems;
667
    let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
668
    (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
669
    begin
670
      merge_with g_non_mems g_mems';
671
      add_external_dependency outputs mems g_non_mems;
672
      { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
673
      g_non_mems
674
    end
675
  with Error (DataCycle _ as exc) -> (
676
      raise (Error (exc))
677
  )
678

    
679
(* A module to sort dependencies among local variables when relying on clocked declarations *)
680
module VarClockDep =
681
struct
682
  let rec get_clock_dep ck =
683
    match ck.Clocks.cdesc with
684
    | Clocks.Con (ck , _ ,l) -> l::(get_clock_dep ck)
685
    | Clocks.Clink ck' 
686
    | Clocks.Ccarrying (_, ck') -> get_clock_dep ck'
687
    | _ -> []
688
      
689
  let sort locals =
690
    let g = new_graph () in
691
    let g = List.fold_left (
692
      fun g var_decl ->
693
	let deps = get_clock_dep var_decl.var_clock in
694
	add_edges [var_decl.var_id] deps g
695
    ) g locals
696
    in
697
    let sorted, no_deps =
698
      TopologicalDepGraph.fold (fun vid (accu, remaining) -> (
699
	let select v = v.var_id = vid in
700
	let selected, not_selected = List.partition select remaining in
701
	selected@accu, not_selected
702
      )) g ([],locals)
703
    in
704
    no_deps @ sorted
705
    
706
end
707
  
708
(* Local Variables: *)
709
(* compile-command:"make -C .." *)
710
(* End: *)
(9-9/63)