Project

General

Profile

Download (27.2 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
(* XXX: UNUSED *)
22
(* type identified_call = eq * tag *)
23

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

    
29
exception Error of error
30

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

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

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

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

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

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

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

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

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

    
71
let new_graph () = IdentDepGraph.create ()
72

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

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

    
96
  let instance_var_cpt = ref 0
97

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

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

    
109
  let is_read_var v = v.[0] = '#'
110

    
111
  let is_instance_var v = v.[0] = '!'
112

    
113
  let is_ghost_var v = is_instance_var v || is_read_var v
114

    
115
  let undo_read_var id =
116
    assert (is_read_var id);
117
    String.sub id 1 (String.length id - 1)
118

    
119
  let undo_instance_var id =
120
    assert (is_instance_var id);
121
    String.sub id 1 (String.length id - 1)
122

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

    
136
  let node_memory_variables nd =
137
    List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
138

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

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

    
152
  let node_local_variables nd =
153
    List.fold_left
154
      (fun locals v -> ISet.add v.var_id locals)
155
      ISet.empty
156
      nd.node_locals
157

    
158
  let node_constant_variables nd =
159
    List.fold_left
160
      (fun locals v ->
161
        if v.var_dec_const then ISet.add v.var_id locals else locals)
162
      ISet.empty
163
      nd.node_locals
164

    
165
  (* XXX: UNUSED *)
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 =
172
      List.fold_left
173
        (fun inoutputs v -> ISet.add v.var_id inoutputs)
174
        inputs
175
        nd.node_outputs
176
    in
177
    List.fold_left
178
      (fun vars v -> ISet.add v.var_id vars)
179
      inoutputs
180
      nd.node_locals
181

    
182
  (* computes the equivalence relation relating variables in the same equation
183
     lhs, under the form of a table of class representatives *)
184
  let eqs_eq_equiv eqs =
185
    let eq_equiv = Hashtbl.create 23 in
186
    List.iter
187
      (fun eq ->
188
        let first = List.hd eq.eq_lhs in
189
        List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs)
190
      eqs;
191
    eq_equiv
192

    
193
  let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)
194

    
195
  (* Create a tuple of right dimension, according to [expr] type, *)
196
  (* filled with variable [v] *)
197
  let adjust_tuple v expr =
198
    match expr.expr_type.Types.tdesc with
199
    | Types.Ttuple tl ->
200
      duplicate v (List.length tl)
201
    | _ ->
202
      [ v ]
203

    
204
  (* Add dependencies from lhs to rhs in [g, g'], *)
205
  (* no-mem/no-mem and mem/no-mem in g            *)
206
  (* mem/mem in g'                                *)
207
  (* match (lhs_is_mem, ISet.mem x mems) with | (false, true ) -> (add_edges [x]
208
     lhs g, g') | (false, false) -> (add_edges lhs [x] g, g') | (true , false)
209
     -> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs g') *)
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 then
214
          let g = add_edges lhs [ mk_read_var x ] g in
215
          if lhs_is_mem then g, add_edges [ x ] lhs g'
216
          else 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'
221
      (* x is a global constant, treated as a read var *)
222
    in
223
    (* Add dependencies from [lhs] to rhs clock [ck]. *)
224
    let rec add_clock lhs_is_mem lhs ck g =
225
      (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
226
      match (Clocks.repr ck).Clocks.cdesc with
227
      | Clocks.Con (ck', cr, _) ->
228
        add_var
229
          lhs_is_mem
230
          lhs
231
          (Clocks.const_of_carrier cr)
232
          (add_clock lhs_is_mem lhs ck' g)
233
      | Clocks.Ccarrying (_, ck') ->
234
        add_clock lhs_is_mem lhs ck' g
235
      | _ ->
236
        g
237
    in
238
    let rec add_dep lhs_is_mem lhs rhs g =
239
      (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
240
      (* i.e every input is connected to every output, through a ghost var *)
241
      let mashup_appl_dependencies f e g =
242
        let f_var =
243
          mk_instance_var
244
            (Format.sprintf "%s_%d" f (fst eq.eq_loc).Lexing.pos_lnum)
245
        in
246
        List.fold_right
247
          (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
248
          (expr_list_of_expr e)
249
          (add_var lhs_is_mem lhs f_var g)
250
      in
251
      let g = add_clock lhs_is_mem lhs rhs.expr_clock g in
252
      match rhs.expr_desc with
253
      | Expr_const _ ->
254
        g
255
      | Expr_fby (e1, e2) ->
256
        add_dep true lhs e2 (add_dep false lhs e1 g)
257
      | Expr_pre e ->
258
        add_dep true lhs e g
259
      | Expr_ident x ->
260
        add_var lhs_is_mem lhs x g
261
      | Expr_access (e1, d) | Expr_power (e1, d) ->
262
        add_dep
263
          lhs_is_mem
264
          lhs
265
          e1
266
          (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
267
      | Expr_array a ->
268
        List.fold_right (add_dep lhs_is_mem lhs) a g
269
      | Expr_tuple t ->
270
        List.fold_right2 (fun l r -> add_dep lhs_is_mem [ l ] r) lhs t g
271
      | Expr_merge (c, hl) ->
272
        add_var
273
          lhs_is_mem
274
          lhs
275
          c
276
          (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
277
      | Expr_ite (c, t, e) ->
278
        add_dep
279
          lhs_is_mem
280
          lhs
281
          c
282
          (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))
283
      | Expr_arrow (e1, e2) ->
284
        add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
285
      | Expr_when (e, c, _) ->
286
        add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
287
      | Expr_appl (f, e, None) ->
288
        if
289
          Basic_library.is_expr_internal_fun rhs
290
          (* tuple component-wise dependency for internal operators *)
291
        then List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
292
          (* mashed up dependency for user-defined operators *)
293
        else mashup_appl_dependencies f e g
294
      | Expr_appl (f, e, Some c) ->
295
        mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
296
    in
297
    let g =
298
      List.fold_left
299
        (fun g lhs ->
300
          if ISet.mem lhs mems then add_vertices [ lhs; mk_read_var lhs ] g
301
          else add_vertices [ lhs ] g)
302
        g
303
        eq.eq_lhs
304
    in
305
    add_dep false eq.eq_lhs eq.eq_rhs (g, g')
306

    
307
  (* Returns the dependence graph for node [n] *)
308
  let dependence_graph mems inputs node_vars n =
309
    instance_var_cpt := 0;
310
    let g = new_graph (), new_graph () in
311
    (* Basic dependencies *)
312
    let g =
313
      List.fold_right
314
        (add_eq_dependencies mems inputs node_vars)
315
        (get_node_eqs n)
316
        g
317
    in
318

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

    
323
    (* (\* In order to introduce dependencies between assert expressions and the
324
       node, *)
325
    (* we build an artificial dependency between node output and each assert *)
326
    (* expr. While these are not valid equations, they should properly propage
327
       in *)
328
    (*    function add_eq_dependencies *\) *)
329
    (* let g = *)
330
    (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
331
    (*   List.fold_left (fun g ae -> *)
332
    (* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs,
333
       ae.assert_expr) in *)
334
    (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
335
    (* ) g n.node_asserts in  *)
336
    g
337
end
338

    
339
module NodeDep = struct
340
  module ExprModule = struct
341
    type t = expr
342

    
343
    let compare = compare
344
  end
345

    
346
  module ESet = Set.Make (ExprModule)
347

    
348
  let rec get_expr_calls prednode expr =
349
    match expr.expr_desc with
350
    | Expr_const _ | Expr_ident _ ->
351
      ESet.empty
352
    | Expr_access (e, _) | Expr_power (e, _) ->
353
      get_expr_calls prednode e
354
    | Expr_array t | Expr_tuple t ->
355
      List.fold_right
356
        (fun x set -> ESet.union (get_expr_calls prednode x) set)
357
        t
358
        ESet.empty
359
    | Expr_merge (_, hl) ->
360
      List.fold_right
361
        (fun (_, h) set -> ESet.union (get_expr_calls prednode h) set)
362
        hl
363
        ESet.empty
364
    | Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
365
      ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
366
    | Expr_ite (c, t, e) ->
367
      ESet.union
368
        (get_expr_calls prednode c)
369
        (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
370
    | Expr_pre e | Expr_when (e, _, _) ->
371
      get_expr_calls prednode e
372
    | Expr_appl (id, e, _) ->
373
      if (not (Basic_library.is_expr_internal_fun expr)) && prednode id then
374
        ESet.add expr (get_expr_calls prednode e)
375
      else get_expr_calls prednode e
376

    
377
  let get_eexpr_calls prednode ee = get_expr_calls prednode ee.eexpr_qfexpr
378

    
379
  let get_callee expr =
380
    match expr.expr_desc with
381
    | Expr_appl (id, args, _) ->
382
      Some (id, expr_list_of_expr args)
383
    | _ ->
384
      None
385

    
386
  let accu f init objl =
387
    List.fold_left (fun accu o -> ESet.union accu (f o)) init objl
388

    
389
  let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs
390

    
391
  let rec get_stmt_calls prednode s =
392
    match s with
393
    | Eq eq ->
394
      get_eq_calls prednode eq
395
    | Aut aut ->
396
      get_aut_calls prednode aut
397

    
398
  and get_aut_calls prednode aut =
399
    let get_handler_calls prednode h =
400
      let get_cond_calls c =
401
        accu (fun (_, e, _, _) -> get_expr_calls prednode e) ESet.empty c
402
      in
403
      let until = get_cond_calls h.hand_until in
404
      let unless = get_cond_calls h.hand_unless in
405
      let calls = ESet.union until unless in
406
      let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in
407
      let calls =
408
        accu
409
          (fun a -> get_expr_calls prednode a.assert_expr)
410
          calls
411
          h.hand_asserts
412
      in
413
      (* let calls = accu xx calls h.hand_annots in *)
414
      (* TODO: search for calls in eexpr *)
415
      calls
416
    in
417
    accu (get_handler_calls prednode) ESet.empty aut.aut_handlers
418

    
419
  let get_calls prednode nd =
420
    let eqs, auts = get_node_eqs nd in
421
    let deps = accu (get_eq_calls prednode) ESet.empty eqs in
422
    let deps = accu (get_aut_calls prednode) deps auts in
423
    ESet.elements deps
424

    
425
  let get_contract_calls prednode c =
426
    let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in
427
    let deps =
428
      accu
429
        (get_eexpr_calls prednode)
430
        deps
431
        (c.assume @ c.guarantees
432
        @ List.fold_left (fun accu m -> accu @ m.require @ m.ensure) [] c.modes
433
        )
434
    in
435
    let id_deps =
436
      List.map (fun e -> fst (desome (get_callee e))) (ESet.elements deps)
437
    in
438
    let id_deps =
439
      List.fold_left (fun accu imp -> imp.import_nodeid :: accu) [] c.imports
440
      @ id_deps
441
    in
442
    id_deps
443

    
444
  let dependence_graph prog =
445
    let g = new_graph () in
446
    let g =
447
      List.fold_right
448
        (fun td accu ->
449
          (* for each node we add its dependencies *)
450
          match td.top_decl_desc with
451
          | Node nd ->
452
            (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
453
            let accu = add_vertices [ nd.node_id ] accu in
454
            let deps =
455
              List.map
456
                (fun e -> fst (desome (get_callee e)))
457
                (get_calls (fun _ -> true) nd)
458
            in
459
            (* Adding assert expressions deps *)
460
            let deps_asserts =
461
              let prednode _ = true in
462
              (* what is this about? *)
463
              List.map
464
                (fun e -> fst (desome (get_callee e)))
465
                (ESet.elements
466
                   (List.fold_left
467
                      (fun accu assert_expr ->
468
                        ESet.union accu (get_expr_calls prednode assert_expr))
469
                      ESet.empty
470
                      (List.map
471
                         (fun _assert -> _assert.assert_expr)
472
                         nd.node_asserts)))
473
            in
474
            let deps_spec =
475
              match nd.node_spec with
476
              | None ->
477
                []
478
              | Some (NodeSpec id) ->
479
                [ id ]
480
              | Some (Contract c) ->
481
                get_contract_calls (fun _ -> true) c
482
            in
483

    
484
            (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@."
485
              Format.pp_print_string) deps; *)
486
            add_edges [ nd.node_id ] (deps @ deps_asserts @ deps_spec) accu
487
          | _ ->
488
            assert false
489
          (* should not happen *))
490
        prog
491
        g
492
    in
493
    g
494

    
495
  let rec filter_static_inputs inputs args =
496
    match inputs, args with
497
    | [], [] ->
498
      []
499
    | v :: vq, a :: aq ->
500
      if v.var_dec_const && Types.is_dimension_type v.var_type then
501
        dimension_of_expr a :: filter_static_inputs vq aq
502
      else filter_static_inputs vq aq
503
    | _ ->
504
      assert false
505

    
506
  let compute_generic_calls prog =
507
    List.iter
508
      (fun td ->
509
        match td.top_decl_desc with
510
        | Node nd ->
511
          let prednode n = is_generic_node (node_from_name n) in
512
          nd.node_gencalls <- get_calls prednode nd
513
        | _ ->
514
          ())
515
      prog
516
end
517

    
518
module CycleDetection = struct
519
  (* ---- Look for cycles in a dependency graph *)
520
  module Cycles = Graph.Components.Make (IdentDepGraph)
521

    
522
  let mk_copy_var n id =
523
    let used name =
524
      List.exists (fun v -> v.var_id = name) n.node_locals
525
      || List.exists (fun v -> v.var_id = name) n.node_inputs
526
      || List.exists (fun v -> v.var_id = name) n.node_outputs
527
    in
528
    mk_new_name used id
529

    
530
  let mk_copy_eq n var =
531
    let var_decl = get_node_var var n in
532
    let cp_var = mk_copy_var n var in
533
    let expr =
534
      {
535
        expr_tag = Utils.new_tag ();
536
        expr_desc = Expr_ident var;
537
        expr_type = var_decl.var_type;
538
        expr_clock = var_decl.var_clock;
539
        expr_delay = Delay.new_var ();
540
        expr_annot = None;
541
        expr_loc = var_decl.var_loc;
542
      }
543
    in
544
    ( { var_decl with var_id = cp_var; var_orig = false },
545
      mkeq var_decl.var_loc ([ cp_var ], expr) )
546

    
547
  let wrong_partition g partition =
548
    match partition with
549
    | [ id ] ->
550
      IdentDepGraph.mem_edge g id id
551
    | _ :: _ :: _ ->
552
      true
553
    | [] ->
554
      assert false
555

    
556
  (* Checks that the dependency graph [g] does not contain a cycle. Raises
557
     [Cycle partition] if the succession of dependencies [partition] forms a
558
     cycle *)
559
  let check_cycles g =
560
    let scc_l = Cycles.scc_list g in
561
    let algebraic_loops = List.filter (wrong_partition g) scc_l in
562
    if List.length algebraic_loops > 0 then
563
      raise (Error (DataCycle algebraic_loops))
564
  (* We extract a hint to resolve the cycle: for each variable in the cycle
565
     which is defined by a call, we return the name of the node call and its
566
     specific id *)
567

    
568
  (* XXX: UNUSED *)
569
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
570
  (* let copy_partition g partition =
571
   *   let copy_g = IdentDepGraph.create () in
572
   *   IdentDepGraph.iter_edges
573
   *     (fun src tgt ->
574
   *       if List.mem src partition && List.mem tgt partition then
575
   *         IdentDepGraph.add_edge copy_g src tgt)
576
   *     g *)
577

    
578
  (* Breaks dependency cycles in a graph [g] by inserting aux variables. [head]
579
     is a head of a non-trivial scc of [g]. In Lustre, this is legal only for
580
     mem/mem cycles *)
581
  let break_cycle head cp_head g =
582
    let succs = IdentDepGraph.succ g head in
583
    IdentDepGraph.add_edge g head cp_head;
584
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
585
    List.iter
586
      (fun s ->
587
        IdentDepGraph.remove_edge g head s;
588
        IdentDepGraph.add_edge g s cp_head)
589
      succs
590

    
591
  (* Breaks cycles of the dependency graph [g] of memory variables [mems]
592
     belonging in node [node]. Returns: - a list of new auxiliary variable
593
     declarations - a list of new equations - a modified acyclic version of [g] *)
594
  let break_cycles node mems g =
595
    let eqs, auts = get_node_eqs node in
596
    assert (auts = []);
597
    (* TODO: check: For the moment we assume that auts are expanded by now *)
598
    let mem_eqs, non_mem_eqs =
599
      List.partition
600
        (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs)
601
        eqs
602
    in
603
    let rec break vdecls mem_eqs g =
604
      let scc_l = Cycles.scc_list g in
605
      let wrong = List.filter (wrong_partition g) scc_l in
606
      match wrong with
607
      | [] ->
608
        vdecls, non_mem_eqs @ mem_eqs, g
609
      | [ head ] :: _ ->
610
        IdentDepGraph.remove_edge g head head;
611
        break vdecls mem_eqs g
612
      | (head :: part) :: _ ->
613
        let vdecl_cp_head, cp_eq = mk_copy_eq node head in
614
        let pvar v = List.mem v part in
615
        let fvar v = if v = head then vdecl_cp_head.var_id else v in
616
        let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
617
        break_cycle head vdecl_cp_head.var_id g;
618
        break (vdecl_cp_head :: vdecls) (cp_eq :: mem_eqs') g
619
      | _ ->
620
        assert false
621
    in
622
    break [] mem_eqs g
623
end
624

    
625
(* Module used to compute static disjunction of variables based upon their
626
   clocks. *)
627
module Disjunction = struct
628
  module ClockedIdentModule = struct
629
    type t = var_decl
630

    
631
    let root_branch vdecl =
632
      Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
633

    
634
    let compare v1 v2 =
635
      compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
636
  end
637

    
638
  module CISet = Set.Make (ClockedIdentModule)
639

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

    
644
  let pp_ciset fmt t =
645
    let open Format in
646
    pp_print_braced'
647
      ~pp_sep:pp_print_space
648
      Printers.pp_var_name
649
      fmt
650
      (CISet.elements t)
651

    
652
  let clock_disjoint_map vdecls =
653
    let map = Hashtbl.create 23 in
654
    List.iter
655
      (fun v1 ->
656
        let disj_v1 =
657
          List.fold_left
658
            (fun res v2 ->
659
              if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res
660
              else res)
661
            CISet.empty
662
            vdecls
663
        in
664
        (* disjoint vdecls are stored in increasing branch length order *)
665
        Hashtbl.add map v1.var_id disj_v1)
666
      vdecls;
667
    (map : disjoint_map)
668

    
669
  (* XXX: UNUSED *)
670
  (* merge variables [v] and [v'] in disjunction [map]. Then: - the mapping v'
671
     becomes v' |-> (map v) inter (map v') - the mapping v |-> ... then
672
     disappears - other mappings become x |-> (map x) \ (if v in x then v else
673
     v') *)
674
  (* let merge_in_disjoint_map map v v' =
675
   *   Hashtbl.replace map v'.var_id
676
   *     (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
677
   *   Hashtbl.remove map v.var_id;
678
   *   Hashtbl.iter
679
   *     (fun x map_x ->
680
   *       Hashtbl.replace map x
681
   *         (CISet.remove (if CISet.mem v map_x then v else v') map_x))
682
   *     map *)
683

    
684
  (* XXX: UNUSED *)
685
  (* replace variable [v] by [v'] in disjunction [map]. [v'] is a dead variable.
686
     Then: - the mapping v' becomes v' |-> (map v) - the mapping v |-> ... then
687
     disappears - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in
688
     map x) *)
689
  (* let replace_in_disjoint_map map v v' =
690
   *   Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
691
   *   Hashtbl.remove map v.var_id;
692
   *   Hashtbl.iter
693
   *     (fun x mapx ->
694
   *       Hashtbl.replace map x
695
   *         (if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx)
696
   *         else CISet.remove v' mapx))
697
   *     map *)
698

    
699
  (* XXX: UNUSED *)
700
  (* remove variable [v] in disjunction [map]. Then: - the mapping v |-> ...
701
     then disappears - all mappings become x |-> (map x) \ { v} *)
702
  (* let remove_in_disjoint_map map v =
703
   *   Hashtbl.remove map v.var_id;
704
   *   Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map *)
705

    
706
  let pp_disjoint_map fmt map =
707
    Format.(
708
      fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }" (fun fmt ->
709
          Hashtbl.iter
710
            (fun k v ->
711
              fprintf
712
                fmt
713
                "@,%s # %a"
714
                k
715
                (pp_print_braced' Printers.pp_var_name)
716
                (CISet.elements v))
717
            map))
718
end
719

    
720
let pp_dep_graph fmt g =
721
  Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]" (fun fmt ->
722
      IdentDepGraph.iter_edges
723
        (fun s t -> Format.fprintf fmt "@ %s -> %s" s t)
724
        g)
725

    
726
let pp_error fmt err =
727
  match err with
728
  | NodeCycle trace ->
729
    Format.(
730
      fprintf
731
        fmt
732
        "Causality error, cyclic node calls:@   @[<v 0>%a@]@ "
733
        (pp_comma_list Format.pp_print_string)
734
        trace)
735
  | DataCycle traces ->
736
    Format.(
737
      fprintf
738
        fmt
739
        "Causality error, cyclic data dependencies:@   @[<v 0>%a@]@ "
740
        (pp_print_list ~pp_sep:pp_print_semicolon (fun fmt trace ->
741
             fprintf
742
               fmt
743
               "@[<v 0>{%a}@]"
744
               (pp_comma_list Format.pp_print_string)
745
               trace))
746
        traces)
747

    
748
(* Merges elements of graph [g2] into graph [g1] *)
749
let merge_with g1 g2 =
750
  IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
751
  IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
752

    
753
let world = "!!_world"
754

    
755
let add_external_dependency outputs mems g =
756
  IdentDepGraph.add_vertex g world;
757
  ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
758
  ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems
759

    
760
(* Takes a node and return a pair (node', graph) where node' is node rebuilt
761
   with the equations enriched with new ones introduced to "break cycles" *)
762
let global_dependency node =
763
  let mems = ExprDep.node_memory_variables node in
764
  let inputs =
765
    ISet.union
766
      (ExprDep.node_input_variables node)
767
      (ExprDep.node_constant_variables node)
768
  in
769
  let outputs = ExprDep.node_output_variables node in
770
  let node_vars = ExprDep.node_variables node in
771
  let g_non_mems, g_mems =
772
    ExprDep.dependence_graph mems inputs node_vars node
773
  in
774
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; Format.eprintf
775
    "g_mems: %a" pp_dep_graph g_mems;*)
776
  try
777
    CycleDetection.check_cycles g_non_mems;
778
    let vdecls', eqs', g_mems' = CycleDetection.break_cycles node mems g_mems in
779
    (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
780
    merge_with g_non_mems g_mems';
781
    add_external_dependency outputs mems g_non_mems;
782
    ( {
783
        node with
784
        node_stmts = List.map (fun eq -> Eq eq) eqs';
785
        node_locals = vdecls' @ node.node_locals;
786
      },
787
      g_non_mems )
788
  with Error (DataCycle _ as exc) -> raise (Error exc)
789

    
790
(* A module to sort dependencies among local variables when relying on clocked
791
   declarations *)
792
module VarClockDep = struct
793
  let rec get_clock_dep ck =
794
    match ck.Clocks.cdesc with
795
    | Clocks.Con (ck, _, l) ->
796
      l :: get_clock_dep ck
797
    | Clocks.Clink ck' | Clocks.Ccarrying (_, ck') ->
798
      get_clock_dep ck'
799
    | _ ->
800
      []
801

    
802
  let sort locals =
803
    let g = new_graph () in
804
    let g =
805
      List.fold_left
806
        (fun g var_decl ->
807
          let deps = get_clock_dep var_decl.var_clock in
808
          add_edges [ var_decl.var_id ] deps g)
809
        g
810
        locals
811
    in
812
    let sorted, no_deps =
813
      TopologicalDepGraph.fold
814
        (fun vid (accu, remaining) ->
815
          let select v = v.var_id = vid in
816
          let selected, not_selected = List.partition select remaining in
817
          selected @ accu, not_selected)
818
        g
819
        ([], locals)
820
    in
821
    no_deps @ sorted
822
end
823

    
824
(* Local Variables: *)
825
(* compile-command:"make -C .." *)
826
(* End: *)
(12-12/99)