Project

General

Profile

Download (25.7 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 -> List.iter (IdentDepGraph.add_edge g s) tgt)
73
    src;
74
  g
75

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

    
81
let new_graph () =
82
  IdentDepGraph.create ()
83

    
84
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
85
let slice_graph gr v =
86
  begin
87
    let gr' = new_graph () in
88
    IdentDepGraph.add_vertex gr' v;
89
    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;
90
    gr'
91
  end
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 
148
      (if nd.node_iscontract then
149
         nd.node_inputs@nd.node_outputs
150
       else
151
         nd.node_inputs)
152
    
153
  let node_output_variables nd =
154
    List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty
155
      (if nd.node_iscontract then [] else nd.node_outputs)
156

    
157
  let node_local_variables nd =
158
    List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
159

    
160
  let node_constant_variables nd =
161
    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
162

    
163
  let node_auxiliary_variables nd =
164
    ISet.diff (node_local_variables nd) (node_memory_variables nd)
165

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

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

    
192

    
193
  (* Add dependencies from lhs to rhs in [g, g'], *)
194
  (* no-mem/no-mem and mem/no-mem in g            *)
195
  (* mem/mem in g'                                *)
196
  (*     match (lhs_is_mem, ISet.mem x mems) with
197
	 | (false, true ) -> (add_edges [x] lhs g,
198
	 g')
199
	 | (false, false) -> (add_edges lhs [x] g,
200
	 g')
201
	 | (true , false) -> (add_edges lhs [x] g,
202
	 g')
203
	 | (true , true ) -> (g,
204
	 add_edges [x] lhs g')
205
  *)
206
  let add_eq_dependencies mems inputs node_vars eq (g, g') =
207
    let add_var lhs_is_mem lhs x (g, g') =
208
      if is_instance_var x || ISet.mem x node_vars then
209
        if ISet.mem x mems
210
        then
211
          let g = add_edges lhs [mk_read_var x] g in
212
          if lhs_is_mem
213
          then
214
            (g, add_edges [x] lhs g')
215
          else
216
            (add_edges [x] lhs g, g')
217
        else
218
          let x = if ISet.mem x inputs then mk_read_var x else x in
219
          (add_edges lhs [x] g, g')
220
      else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)
221
    in
222
    (* Add dependencies from [lhs] to rhs clock [ck]. *)
223
    let rec add_clock lhs_is_mem lhs ck g =
224
      (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
225
      match (Clocks.repr ck).Clocks.cdesc with
226
      | Clocks.Con (ck', cr, _)   ->
227
        add_var lhs_is_mem lhs (Clocks.const_of_carrier cr)
228
          (add_clock lhs_is_mem lhs ck' g)
229
      | Clocks.Ccarrying (_, ck') ->
230
        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 (fst eq.eq_loc).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
      let g = add_clock lhs_is_mem lhs rhs.expr_clock g 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 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 = List.fold_left (fun g lhs ->
267
        if ISet.mem lhs mems then
268
          add_vertices [lhs; mk_read_var lhs] g
269
        else
270
	      add_vertices [lhs] g)
271
	    g eq.eq_lhs
272
    in
273
    add_dep false eq.eq_lhs eq.eq_rhs (g, g')
274

    
275

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

    
299
end
300

    
301
module NodeDep = struct
302

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

    
311
  module ESet = Set.Make(ExprModule)
312

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

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

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

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

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

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

    
427
end
428

    
429

    
430
module CycleDetection = struct
431

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

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

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

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

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

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

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

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

    
528
end
529

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

    
540
  module CISet = Set.Make(ClockedIdentModule)
541

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

    
546
  let pp_ciset fmt t = let open Format in
547
    pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt
548
      (CISet.elements t)
549

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

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

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

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

    
600
  let pp_disjoint_map fmt map =
601
    Format.(fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }"
602
              (fun fmt ->
603
                 Hashtbl.iter (fun k v ->
604
                     fprintf fmt "@,%s # %a"
605
                       k (pp_print_braced' Printers.pp_var_name)
606
                       (CISet.elements v)) map))
607
end
608

    
609
  
610
let pp_dep_graph fmt g =
611
  Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]"
612
    (fun fmt ->
613
       IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "@ %s -> %s" s t) g)
614

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

    
637
let world = "!!_world"
638

    
639
let add_external_dependency outputs mems g =
640
  begin
641
    IdentDepGraph.add_vertex g world;
642
    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
643
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
644
  end
645

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

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