Project

General

Profile

Download (26.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
open Utils
15
(** Simple modular syntactic causality analysis. Can reject correct programs,
16
    especially if the program is not flattened first. *)
17

    
18
open Lustre_types
19
open Corelang
20

    
21
type identified_call = eq * tag
22

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

    
28
exception Error of error
29

    
30
(* Dependency of mem variables on mem variables is cut off by duplication of
31
   some mem vars into local node vars. Thus, cylic dependency errors may only
32
   arise between no-mem vars. non-mem variables are: - constants/inputs: not
33
   needed for causality/scheduling, needed only for detecting useless vars -
34
   read mems (fake vars): same remark as above. - outputs: decoupled from mems,
35
   if necessary - locals - instance vars (fake vars): simplify causality
36
   analysis
37

    
38
   global constants are not part of the dependency graph.
39

    
40
   no_mem' = combinational(no_mem, mem); => (mem -> no_mem' -> no_mem)
41

    
42
   mem' = pre(no_mem, mem); => (mem' -> no_mem), (mem -> mem')
43

    
44
   Global roadmap: - compute two dep graphs g (non-mem/non-mem&mem) and g'
45
   (mem/mem) - check cycles in g (a cycle means a dependency error) - break
46
   cycles in g' (it's legal !): - check cycles in g' - if any, introduce aux var
47
   to break cycle, then start afresh - insert g' into g - return g *)
48

    
49
(* Tests whether [v] is a root of graph [g], i.e. a source *)
50
let is_graph_root v g = IdentDepGraph.in_degree g v = 0
51

    
52
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
53
let graph_roots g =
54
  IdentDepGraph.fold_vertex
55
    (fun v roots -> if is_graph_root v g then v :: roots else roots)
56
    g []
57

    
58
let add_edges src tgt g =
59
  (*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t)
60
    tgt) src;*)
61
  List.iter (fun s -> List.iter (IdentDepGraph.add_edge g s) tgt) src;
62
  g
63

    
64
let add_vertices vtc g =
65
  (*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
66
  List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
67
  g
68

    
69
let new_graph () = IdentDepGraph.create ()
70

    
71
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
72
let slice_graph gr v =
73
  let gr' = new_graph () in
74
  IdentDepGraph.add_vertex gr' v;
75
  Bfs.iter_component
76
    (fun v ->
77
      IdentDepGraph.iter_succ
78
        (fun s ->
79
          IdentDepGraph.add_vertex gr' s;
80
          IdentDepGraph.add_edge gr' v s)
81
        gr v)
82
    gr v;
83
  gr'
84

    
85
module ExprDep = struct
86
  let get_node_eqs nd =
87
    let eqs, auts = get_node_eqs nd in
88
    if auts != [] then assert false
89
      (* No call on causality on a Lustre model with automaton. They should be
90
         expanded by now. *);
91
    eqs
92

    
93
  let instance_var_cpt = ref 0
94

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

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

    
106
  let is_read_var v = v.[0] = '#'
107

    
108
  let is_instance_var v = v.[0] = '!'
109

    
110
  let is_ghost_var v = is_instance_var v || is_read_var v
111

    
112
  let undo_read_var id =
113
    assert (is_read_var id);
114
    String.sub id 1 (String.length id - 1)
115

    
116
  let undo_instance_var id =
117
    assert (is_instance_var id);
118
    String.sub id 1 (String.length id - 1)
119

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

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

    
136
  let node_input_variables nd =
137
    List.fold_left
138
      (fun inputs v -> ISet.add v.var_id inputs)
139
      ISet.empty
140
      (if nd.node_iscontract then nd.node_inputs @ nd.node_outputs
141
      else nd.node_inputs)
142

    
143
  let node_output_variables nd =
144
    List.fold_left
145
      (fun outputs v -> ISet.add v.var_id outputs)
146
      ISet.empty
147
      (if nd.node_iscontract then [] else nd.node_outputs)
148

    
149
  let node_local_variables nd =
150
    List.fold_left
151
      (fun locals v -> ISet.add v.var_id locals)
152
      ISet.empty nd.node_locals
153

    
154
  let node_constant_variables nd =
155
    List.fold_left
156
      (fun locals v ->
157
        if v.var_dec_const then ISet.add v.var_id locals else locals)
158
      ISet.empty nd.node_locals
159

    
160
  let node_auxiliary_variables nd =
161
    ISet.diff (node_local_variables nd) (node_memory_variables nd)
162

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

    
174
  (* computes the equivalence relation relating variables in the same equation
175
     lhs, under the form of a table of class representatives *)
176
  let eqs_eq_equiv eqs =
177
    let eq_equiv = Hashtbl.create 23 in
178
    List.iter
179
      (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
      eqs;
183
    eq_equiv
184

    
185
  let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)
186

    
187
  (* Create a tuple of right dimension, according to [expr] type, *)
188
  (* filled with variable [v] *)
189
  let adjust_tuple v expr =
190
    match expr.expr_type.Types.tdesc with
191
    | Types.Ttuple tl ->
192
      duplicate v (List.length tl)
193
    | _ ->
194
      [ v ]
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 | (false, true ) -> (add_edges [x]
200
     lhs g, g') | (false, false) -> (add_edges lhs [x] g, g') | (true , false)
201
     -> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs g') *)
202
  let add_eq_dependencies mems inputs node_vars eq (g, g') =
203
    let add_var lhs_is_mem lhs x (g, g') =
204
      if is_instance_var x || ISet.mem x node_vars then
205
        if ISet.mem x mems then
206
          let g = add_edges lhs [ mk_read_var x ] g in
207
          if lhs_is_mem then g, add_edges [ x ] lhs g'
208
          else add_edges [ x ] lhs g, g'
209
        else
210
          let x = if ISet.mem x inputs then mk_read_var x else x in
211
          add_edges lhs [ x ] g, g'
212
      else add_edges lhs [ mk_read_var x ] g, g'
213
      (* 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, _) ->
220
        add_var lhs_is_mem lhs
221
          (Clocks.const_of_carrier cr)
222
          (add_clock lhs_is_mem lhs ck' g)
223
      | Clocks.Ccarrying (_, ck') ->
224
        add_clock lhs_is_mem lhs ck' g
225
      | _ ->
226
        g
227
    in
228
    let rec add_dep lhs_is_mem lhs rhs g =
229
      (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
230
      (* i.e every input is connected to every output, through a ghost var *)
231
      let mashup_appl_dependencies f e g =
232
        let f_var =
233
          mk_instance_var
234
            (Format.sprintf "%s_%d" f (fst eq.eq_loc).Lexing.pos_lnum)
235
        in
236
        List.fold_right
237
          (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
238
          (expr_list_of_expr e)
239
          (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 _ ->
244
        g
245
      | Expr_fby (e1, e2) ->
246
        add_dep true lhs e2 (add_dep false lhs e1 g)
247
      | Expr_pre e ->
248
        add_dep true lhs e g
249
      | Expr_ident x ->
250
        add_var lhs_is_mem lhs x g
251
      | Expr_access (e1, d) | Expr_power (e1, d) ->
252
        add_dep lhs_is_mem lhs e1
253
          (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
254
      | Expr_array a ->
255
        List.fold_right (add_dep lhs_is_mem lhs) a g
256
      | Expr_tuple t ->
257
        List.fold_right2 (fun l r -> add_dep lhs_is_mem [ l ] r) lhs t g
258
      | Expr_merge (c, hl) ->
259
        add_var lhs_is_mem lhs c
260
          (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
261
      | Expr_ite (c, t, e) ->
262
        add_dep lhs_is_mem lhs c
263
          (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))
264
      | Expr_arrow (e1, e2) ->
265
        add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
266
      | Expr_when (e, c, _) ->
267
        add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
268
      | Expr_appl (f, e, None) ->
269
        if
270
          Basic_library.is_expr_internal_fun rhs
271
          (* tuple component-wise dependency for internal operators *)
272
        then List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
273
          (* mashed up dependency for user-defined operators *)
274
        else mashup_appl_dependencies f e g
275
      | Expr_appl (f, e, Some c) ->
276
        mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
277
    in
278
    let g =
279
      List.fold_left
280
        (fun g lhs ->
281
          if ISet.mem lhs mems then add_vertices [ lhs; mk_read_var lhs ] g
282
          else add_vertices [ lhs ] g)
283
        g eq.eq_lhs
284
    in
285
    add_dep false eq.eq_lhs eq.eq_rhs (g, g')
286

    
287
  (* Returns the dependence graph for node [n] *)
288
  let dependence_graph mems inputs node_vars n =
289
    instance_var_cpt := 0;
290
    let g = new_graph (), new_graph () in
291
    (* Basic dependencies *)
292
    let g =
293
      List.fold_right
294
        (add_eq_dependencies mems inputs node_vars)
295
        (get_node_eqs n) g
296
    in
297

    
298
    (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
299
       faut imposer que les outputs dépendent des asserts pour identifier que
300
       les fcn calls des asserts sont évalués avant le noeuds *)
301

    
302
    (* (\* In order to introduce dependencies between assert expressions and the
303
       node, *)
304
    (* we build an artificial dependency between node output and each assert *)
305
    (* expr. While these are not valid equations, they should properly propage
306
       in *)
307
    (*    function add_eq_dependencies *\) *)
308
    (* let g = *)
309
    (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
310
    (*   List.fold_left (fun g ae -> *)
311
    (* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs,
312
       ae.assert_expr) in *)
313
    (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
314
    (* ) g n.node_asserts in  *)
315
    g
316
end
317

    
318
module NodeDep = struct
319
  module ExprModule = struct
320
    type t = expr
321

    
322
    let compare = compare
323

    
324
    let hash n = Hashtbl.hash n
325

    
326
    let equal n1 n2 = n1 = n2
327
  end
328

    
329
  module ESet = Set.Make (ExprModule)
330

    
331
  let rec get_expr_calls prednode expr =
332
    match expr.expr_desc with
333
    | Expr_const _ | Expr_ident _ ->
334
      ESet.empty
335
    | Expr_access (e, _) | Expr_power (e, _) ->
336
      get_expr_calls prednode e
337
    | Expr_array t | Expr_tuple t ->
338
      List.fold_right
339
        (fun x set -> ESet.union (get_expr_calls prednode x) set)
340
        t ESet.empty
341
    | Expr_merge (_, hl) ->
342
      List.fold_right
343
        (fun (_, h) set -> ESet.union (get_expr_calls prednode h) set)
344
        hl ESet.empty
345
    | Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
346
      ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
347
    | Expr_ite (c, t, e) ->
348
      ESet.union
349
        (get_expr_calls prednode c)
350
        (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
351
    | Expr_pre e | Expr_when (e, _, _) ->
352
      get_expr_calls prednode e
353
    | Expr_appl (id, e, _) ->
354
      if (not (Basic_library.is_expr_internal_fun expr)) && prednode id then
355
        ESet.add expr (get_expr_calls prednode e)
356
      else get_expr_calls prednode e
357

    
358
  let get_eexpr_calls prednode ee = get_expr_calls prednode ee.eexpr_qfexpr
359

    
360
  let get_callee expr =
361
    match expr.expr_desc with
362
    | Expr_appl (id, args, _) ->
363
      Some (id, expr_list_of_expr args)
364
    | _ ->
365
      None
366

    
367
  let accu f init objl =
368
    List.fold_left (fun accu o -> ESet.union accu (f o)) init objl
369

    
370
  let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs
371

    
372
  let rec get_stmt_calls prednode s =
373
    match s with
374
    | Eq eq ->
375
      get_eq_calls prednode eq
376
    | Aut aut ->
377
      get_aut_calls prednode aut
378

    
379
  and get_aut_calls prednode aut =
380
    let get_handler_calls prednode h =
381
      let get_cond_calls c =
382
        accu (fun (_, e, _, _) -> get_expr_calls prednode e) ESet.empty c
383
      in
384
      let until = get_cond_calls h.hand_until in
385
      let unless = get_cond_calls h.hand_unless in
386
      let calls = ESet.union until unless in
387
      let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in
388
      let calls =
389
        accu
390
          (fun a -> get_expr_calls prednode a.assert_expr)
391
          calls h.hand_asserts
392
      in
393
      (* let calls = accu xx calls h.hand_annots in *)
394
      (* TODO: search for calls in eexpr *)
395
      calls
396
    in
397
    accu (get_handler_calls prednode) ESet.empty aut.aut_handlers
398

    
399
  let get_calls prednode nd =
400
    let eqs, auts = get_node_eqs nd in
401
    let deps = accu (get_eq_calls prednode) ESet.empty eqs in
402
    let deps = accu (get_aut_calls prednode) deps auts in
403
    ESet.elements deps
404

    
405
  let get_contract_calls prednode c =
406
    let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in
407
    let deps =
408
      accu (get_eexpr_calls prednode) deps
409
        (c.assume @ c.guarantees
410
        @ List.fold_left (fun accu m -> accu @ m.require @ m.ensure) [] c.modes
411
        )
412
    in
413
    let id_deps =
414
      List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps)
415
    in
416
    let id_deps =
417
      List.fold_left (fun accu imp -> imp.import_nodeid :: accu) [] c.imports
418
      @ id_deps
419
    in
420
    id_deps
421

    
422
  let dependence_graph prog =
423
    let g = new_graph () in
424
    let g =
425
      List.fold_right
426
        (fun td accu ->
427
          (* for each node we add its dependencies *)
428
          match td.top_decl_desc with
429
          | Node nd ->
430
            (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
431
            let accu = add_vertices [ nd.node_id ] accu in
432
            let deps =
433
              List.map
434
                (fun e -> fst (desome (get_callee e)))
435
                (get_calls (fun _ -> true) nd)
436
            in
437
            (* Adding assert expressions deps *)
438
            let deps_asserts =
439
              let prednode _ = true in
440
              (* what is this about? *)
441
              List.map
442
                (fun e -> fst (desome (get_callee e)))
443
                (ESet.elements
444
                   (List.fold_left
445
                      (fun accu assert_expr ->
446
                        ESet.union accu (get_expr_calls prednode assert_expr))
447
                      ESet.empty
448
                      (List.map
449
                         (fun _assert -> _assert.assert_expr)
450
                         nd.node_asserts)))
451
            in
452
            let deps_spec =
453
              match nd.node_spec with
454
              | None ->
455
                []
456
              | Some (NodeSpec id) ->
457
                [ id ]
458
              | Some (Contract c) ->
459
                get_contract_calls (fun _ -> true) c
460
            in
461

    
462
            (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@."
463
              Format.pp_print_string) deps; *)
464
            add_edges [ nd.node_id ] (deps @ deps_asserts @ deps_spec) accu
465
          | _ ->
466
            assert false
467
          (* should not happen *))
468
        prog g
469
    in
470
    g
471

    
472
  let rec filter_static_inputs inputs args =
473
    match inputs, args with
474
    | [], [] ->
475
      []
476
    | v :: vq, a :: aq ->
477
      if v.var_dec_const && Types.is_dimension_type v.var_type then
478
        dimension_of_expr a :: filter_static_inputs vq aq
479
      else filter_static_inputs vq aq
480
    | _ ->
481
      assert false
482

    
483
  let compute_generic_calls prog =
484
    List.iter
485
      (fun td ->
486
        match td.top_decl_desc with
487
        | Node nd ->
488
          let prednode n = is_generic_node (node_from_name n) in
489
          nd.node_gencalls <- get_calls prednode nd
490
        | _ ->
491
          ())
492
      prog
493
end
494

    
495
module CycleDetection = struct
496
  (* ---- Look for cycles in a dependency graph *)
497
  module Cycles = Graph.Components.Make (IdentDepGraph)
498

    
499
  let mk_copy_var n id =
500
    let used name =
501
      List.exists (fun v -> v.var_id = name) n.node_locals
502
      || List.exists (fun v -> v.var_id = name) n.node_inputs
503
      || List.exists (fun v -> v.var_id = name) n.node_outputs
504
    in
505
    mk_new_name used id
506

    
507
  let mk_copy_eq n var =
508
    let var_decl = get_node_var var n in
509
    let cp_var = mk_copy_var n var in
510
    let expr =
511
      {
512
        expr_tag = Utils.new_tag ();
513
        expr_desc = Expr_ident var;
514
        expr_type = var_decl.var_type;
515
        expr_clock = var_decl.var_clock;
516
        expr_delay = Delay.new_var ();
517
        expr_annot = None;
518
        expr_loc = var_decl.var_loc;
519
      }
520
    in
521
    ( { var_decl with var_id = cp_var; var_orig = false },
522
      mkeq var_decl.var_loc ([ cp_var ], expr) )
523

    
524
  let wrong_partition g partition =
525
    match partition with
526
    | [ id ] ->
527
      IdentDepGraph.mem_edge g id id
528
    | _ :: _ :: _ ->
529
      true
530
    | [] ->
531
      assert false
532

    
533
  (* Checks that the dependency graph [g] does not contain a cycle. Raises
534
     [Cycle partition] if the succession of dependencies [partition] forms a
535
     cycle *)
536
  let check_cycles g =
537
    let scc_l = Cycles.scc_list g in
538
    let algebraic_loops = List.filter (wrong_partition g) scc_l in
539
    if List.length algebraic_loops > 0 then
540
      raise (Error (DataCycle algebraic_loops))
541
  (* We extract a hint to resolve the cycle: for each variable in the cycle
542
     which is defined by a call, we return the name of the node call and its
543
     specific id *)
544

    
545
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
546
  let copy_partition g partition =
547
    let copy_g = IdentDepGraph.create () in
548
    IdentDepGraph.iter_edges
549
      (fun src tgt ->
550
        if List.mem src partition && List.mem tgt partition then
551
          IdentDepGraph.add_edge copy_g src tgt)
552
      g
553

    
554
  (* Breaks dependency cycles in a graph [g] by inserting aux variables. [head]
555
     is a head of a non-trivial scc of [g]. In Lustre, this is legal only for
556
     mem/mem cycles *)
557
  let break_cycle head cp_head g =
558
    let succs = IdentDepGraph.succ g head in
559
    IdentDepGraph.add_edge g head cp_head;
560
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
561
    List.iter
562
      (fun s ->
563
        IdentDepGraph.remove_edge g head s;
564
        IdentDepGraph.add_edge g s cp_head)
565
      succs
566

    
567
  (* Breaks cycles of the dependency graph [g] of memory variables [mems]
568
     belonging in node [node]. Returns: - a list of new auxiliary variable
569
     declarations - a list of new equations - a modified acyclic version of [g] *)
570
  let break_cycles node mems g =
571
    let eqs, auts = get_node_eqs node in
572
    assert (auts = []);
573
    (* TODO: check: For the moment we assume that auts are expanded by now *)
574
    let mem_eqs, non_mem_eqs =
575
      List.partition
576
        (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs)
577
        eqs
578
    in
579
    let rec break vdecls mem_eqs g =
580
      let scc_l = Cycles.scc_list g in
581
      let wrong = List.filter (wrong_partition g) scc_l in
582
      match wrong with
583
      | [] ->
584
        vdecls, non_mem_eqs @ mem_eqs, g
585
      | [ head ] :: _ ->
586
        IdentDepGraph.remove_edge g head head;
587
        break vdecls mem_eqs g
588
      | (head :: part) :: _ ->
589
        let vdecl_cp_head, cp_eq = mk_copy_eq node head in
590
        let pvar v = List.mem v part in
591
        let fvar v = if v = head then vdecl_cp_head.var_id else v in
592
        let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
593
        break_cycle head vdecl_cp_head.var_id g;
594
        break (vdecl_cp_head :: vdecls) (cp_eq :: mem_eqs') g
595
      | _ ->
596
        assert false
597
    in
598
    break [] mem_eqs g
599
end
600

    
601
(* Module used to compute static disjunction of variables based upon their
602
   clocks. *)
603
module Disjunction = struct
604
  module ClockedIdentModule = struct
605
    type t = var_decl
606

    
607
    let root_branch vdecl =
608
      Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
609

    
610
    let compare v1 v2 =
611
      compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
612
  end
613

    
614
  module CISet = Set.Make (ClockedIdentModule)
615

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

    
620
  let pp_ciset fmt t =
621
    let open Format in
622
    pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt
623
      (CISet.elements t)
624

    
625
  let clock_disjoint_map vdecls =
626
    let map = Hashtbl.create 23 in
627
    List.iter
628
      (fun v1 ->
629
        let disj_v1 =
630
          List.fold_left
631
            (fun res v2 ->
632
              if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res
633
              else res)
634
            CISet.empty vdecls
635
        in
636
        (* disjoint vdecls are stored in increasing branch length order *)
637
        Hashtbl.add map v1.var_id disj_v1)
638
      vdecls;
639
    (map : disjoint_map)
640

    
641
  (* merge variables [v] and [v'] in disjunction [map]. Then: - the mapping v'
642
     becomes v' |-> (map v) inter (map v') - the mapping v |-> ... then
643
     disappears - other mappings become x |-> (map x) \ (if v in x then v else
644
     v') *)
645
  let merge_in_disjoint_map map v v' =
646
    Hashtbl.replace map v'.var_id
647
      (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
648
    Hashtbl.remove map v.var_id;
649
    Hashtbl.iter
650
      (fun x map_x ->
651
        Hashtbl.replace map x
652
          (CISet.remove (if CISet.mem v map_x then v else v') map_x))
653
      map
654

    
655
  (* replace variable [v] by [v'] in disjunction [map]. [v'] is a dead variable.
656
     Then: - the mapping v' becomes v' |-> (map v) - the mapping v |-> ... then
657
     disappears - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in
658
     map x) *)
659
  let replace_in_disjoint_map map v v' =
660
    Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
661
    Hashtbl.remove map v.var_id;
662
    Hashtbl.iter
663
      (fun x mapx ->
664
        Hashtbl.replace map x
665
          (if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx)
666
          else CISet.remove v' mapx))
667
      map
668

    
669
  (* remove variable [v] in disjunction [map]. Then: - the mapping v |-> ...
670
     then disappears - all mappings become x |-> (map x) \ { v} *)
671
  let remove_in_disjoint_map map v =
672
    Hashtbl.remove map v.var_id;
673
    Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map
674

    
675
  let pp_disjoint_map fmt map =
676
    Format.(
677
      fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }" (fun fmt ->
678
          Hashtbl.iter
679
            (fun k v ->
680
              fprintf fmt "@,%s # %a" k
681
                (pp_print_braced' Printers.pp_var_name)
682
                (CISet.elements v))
683
            map))
684
end
685

    
686
let pp_dep_graph fmt g =
687
  Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]" (fun fmt ->
688
      IdentDepGraph.iter_edges
689
        (fun s t -> Format.fprintf fmt "@ %s -> %s" s t)
690
        g)
691

    
692
let pp_error fmt err =
693
  match err with
694
  | NodeCycle trace ->
695
    Format.(fprintf fmt "Causality error, cyclic node calls:@   @[<v 0>%a@]@ "
696
              (pp_comma_list Format.pp_print_string) trace)
697
  | DataCycle traces ->
698
    Format.(fprintf fmt
699
              "Causality error, cyclic data dependencies:@   @[<v 0>%a@]@ "
700
              (pp_print_list ~pp_sep:pp_print_semicolon (fun fmt trace ->
701
                   fprintf fmt "@[<v 0>{%a}@]"
702
                     (pp_comma_list Format.pp_print_string) trace))
703
              traces)
704

    
705
(* Merges elements of graph [g2] into graph [g1] *)
706
let merge_with g1 g2 =
707
  IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
708
  IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
709

    
710
let world = "!!_world"
711

    
712
let add_external_dependency outputs mems g =
713
  IdentDepGraph.add_vertex g world;
714
  ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
715
  ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems
716

    
717
(* Takes a node and return a pair (node', graph) where node' is node rebuilt
718
   with the equations enriched with new ones introduced to "break cycles" *)
719
let global_dependency node =
720
  let mems = ExprDep.node_memory_variables node in
721
  let inputs =
722
    ISet.union
723
      (ExprDep.node_input_variables node)
724
      (ExprDep.node_constant_variables node)
725
  in
726
  let outputs = ExprDep.node_output_variables node in
727
  let node_vars = ExprDep.node_variables node in
728
  let g_non_mems, g_mems =
729
    ExprDep.dependence_graph mems inputs node_vars node
730
  in
731
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; Format.eprintf
732
    "g_mems: %a" pp_dep_graph g_mems;*)
733
  try
734
    CycleDetection.check_cycles g_non_mems;
735
    let vdecls', eqs', g_mems' = CycleDetection.break_cycles node mems g_mems in
736
    (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
737
    merge_with g_non_mems g_mems';
738
    add_external_dependency outputs mems g_non_mems;
739
    ( {
740
        node with
741
        node_stmts = List.map (fun eq -> Eq eq) eqs';
742
        node_locals = vdecls' @ node.node_locals;
743
      },
744
      g_non_mems )
745
  with Error (DataCycle _ as exc) -> raise (Error exc)
746

    
747
(* A module to sort dependencies among local variables when relying on clocked
748
   declarations *)
749
module VarClockDep = struct
750
  let rec get_clock_dep ck =
751
    match ck.Clocks.cdesc with
752
    | Clocks.Con (ck, _, l) ->
753
      l :: get_clock_dep ck
754
    | Clocks.Clink ck' | Clocks.Ccarrying (_, ck') ->
755
      get_clock_dep ck'
756
    | _ ->
757
      []
758

    
759
  let sort locals =
760
    let g = new_graph () in
761
    let g =
762
      List.fold_left
763
        (fun g var_decl ->
764
          let deps = get_clock_dep var_decl.var_clock in
765
          add_edges [ var_decl.var_id ] deps g)
766
        g locals
767
    in
768
    let sorted, no_deps =
769
      TopologicalDepGraph.fold
770
        (fun vid (accu, remaining) ->
771
          let select v = v.var_id = vid in
772
          let selected, not_selected = List.partition select remaining in
773
          selected @ accu, not_selected)
774
        g ([], locals)
775
    in
776
    no_deps @ sorted
777
end
778

    
779
(* Local Variables: *)
780
(* compile-command:"make -C .." *)
781
(* End: *)
(12-12/111)