Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by Lélio Brun 7 months ago

reformatting

View differences:

src/causality.ml
6 6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7 7
(*  under the terms of the GNU Lesser General Public License        *)
8 8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
9
(*                                                                  *)
10 10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
11
(*                                                                  *)
12 12
(********************************************************************)
13 13

  
14

  
15
(** Simple modular syntactic causality analysis. Can reject correct
16
    programs, especially if the program is not flattened first. *)
17 14
open Utils
15
(** Simple modular syntactic causality analysis. Can reject correct programs,
16
    especially if the program is not flattened first. *)
17

  
18 18
open Lustre_types
19 19
open Corelang
20 20

  
21

  
22 21
type identified_call = eq * tag
22

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

  
27 28
exception Error of error
28 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
29 37

  
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 38
   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
*)
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 *)
58 48

  
59 49
(* 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
50
let is_graph_root v g = IdentDepGraph.in_degree g v = 0
62 51

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

  
69 58
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;
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;
74 62
  g
75 63

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

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

  
84 71
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
85 72
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
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'
92 84

  
93
    
94 85
module ExprDep = struct
95 86
  let get_node_eqs nd =
96 87
    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. *);
88
    if auts != [] then assert false
89
      (* No call on causality on a Lustre model with automaton. They should be
90
         expanded by now. *);
99 91
    eqs
100
      
92

  
101 93
  let instance_var_cpt = ref 0
102 94

  
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
*)
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 *)
115 102
  let mk_instance_var id =
116
    incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt
103
    incr instance_var_cpt;
104
    Format.sprintf "!%s_%d" id !instance_var_cpt
117 105

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

  
......
132 120
  let eq_memory_variables mems eq =
133 121
    let rec match_mem lhs rhs mems =
134 122
      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
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
141 131
    match_mem eq.eq_lhs eq.eq_rhs mems
142 132

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

  
146 136
  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
    
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

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

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

  
160 154
  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
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
162 159

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

  
166 163
  let node_variables nd =
167 164
    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
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
170 173

  
171
(* computes the equivalence relation relating variables 
172
   in the same equation lhs, under the form of a table 
173
   of class representatives *)
174
  (* computes the equivalence relation relating variables in the same equation
175
     lhs, under the form of a table of class representatives *)
174 176
  let eqs_eq_equiv eqs =
175 177
    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
    )
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)
180 182
      eqs;
181 183
    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] *)
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] *)
187 189
  let adjust_tuple v expr =
188 190
    match expr.expr_type.Types.tdesc with
189
    | Types.Ttuple tl -> duplicate v (List.length tl)
190
    | _         -> [v]
191

  
191
    | Types.Ttuple tl ->
192
      duplicate v (List.length tl)
193
    | _ ->
194
      [ v ]
192 195

  
193 196
  (* Add dependencies from lhs to rhs in [g, g'], *)
194 197
  (* no-mem/no-mem and mem/no-mem in g            *)
195 198
  (* 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
  *)
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') *)
206 202
  let add_eq_dependencies mems inputs node_vars eq (g, g') =
207 203
    let add_var lhs_is_mem lhs x (g, g') =
208 204
      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')
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'
217 209
        else
218 210
          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 *)
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 *)
221 214
    in
222 215
    (* Add dependencies from [lhs] to rhs clock [ck]. *)
223 216
    let rec add_clock lhs_is_mem lhs ck g =
224 217
      (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
225 218
      match (Clocks.repr ck).Clocks.cdesc with
226
      | Clocks.Con (ck', cr, _)   ->
227
        add_var lhs_is_mem lhs (Clocks.const_of_carrier cr)
219
      | Clocks.Con (ck', cr, _) ->
220
        add_var lhs_is_mem lhs
221
          (Clocks.const_of_carrier cr)
228 222
          (add_clock lhs_is_mem lhs ck' g)
229 223
      | Clocks.Ccarrying (_, ck') ->
230 224
        add_clock lhs_is_mem lhs ck' g
231
      | _                         -> g 
225
      | _ ->
226
        g
232 227
    in
233 228
    let rec add_dep lhs_is_mem lhs rhs g =
234 229
      (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
235 230
      (* i.e every input is connected to every output, through a ghost var *)
236 231
      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)
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 240
      in
241 241
      let g = add_clock lhs_is_mem lhs rhs.expr_clock g in
242 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)
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)
255 268
      | 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
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
260 273
          (* mashed up dependency for user-defined operators *)
261
        else
262
          mashup_appl_dependencies f e g
274
        else mashup_appl_dependencies f e g
263 275
      | Expr_appl (f, e, Some c) ->
264 276
        mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
265 277
    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
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
272 284
    in
273 285
    add_dep false eq.eq_lhs eq.eq_rhs (g, g')
274 286

  
275

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

  
283 298
    (* 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 *)
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 *)
290 307
    (*    function add_eq_dependencies *\) *)
291 308
    (* let g = *)
292 309
    (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
293 310
    (*   List.fold_left (fun g ae -> *)
294
    (*     let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)
311
    (* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs,
312
       ae.assert_expr) in *)
295 313
    (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
296 314
    (* ) g n.node_asserts in  *)
297 315
    g
298

  
299 316
end
300 317

  
301 318
module NodeDep = struct
302

  
303
  module ExprModule =
304
  struct
319
  module ExprModule = struct
305 320
    type t = expr
321

  
306 322
    let compare = compare
323

  
307 324
    let hash n = Hashtbl.hash n
325

  
308 326
    let equal n1 n2 = n1 = n2
309 327
  end
310 328

  
311
  module ESet = Set.Make(ExprModule)
329
  module ESet = Set.Make (ExprModule)
312 330

  
313
  let rec get_expr_calls prednode expr = 
331
  let rec get_expr_calls prednode expr =
314 332
    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
    
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

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

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

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

  
344 372
  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 
373
    match s with
374
    | Eq eq ->
375
      get_eq_calls prednode eq
376
    | Aut aut ->
377
      get_aut_calls prednode aut
378

  
346 379
  and get_aut_calls prednode aut =
347 380
    let get_handler_calls prednode h =
348
      let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in
381
      let get_cond_calls c =
382
        accu (fun (_, e, _, _) -> get_expr_calls prednode e) ESet.empty c
383
      in
349 384
      let until = get_cond_calls h.hand_until in
350 385
      let unless = get_cond_calls h.hand_unless in
351
      let calls = ESet.union until unless in 
386
      let calls = ESet.union until unless in
352 387
      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 *)
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 *)
355 395
      calls
356 396
    in
357 397
    accu (get_handler_calls prednode) ESet.empty aut.aut_handlers
358
    
398

  
359 399
  let get_calls prednode nd =
360 400
    let eqs, auts = get_node_eqs nd in
361 401
    let deps = accu (get_eq_calls prednode) ESet.empty eqs in
......
364 404

  
365 405
  let get_contract_calls prednode c =
366 406
    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  
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
370 420
    id_deps
371
    
421

  
372 422
  let dependence_graph prog =
373 423
    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
      
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

  
410 472
  let rec filter_static_inputs inputs args =
411 473
    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
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
415 482

  
416 483
  let compute_generic_calls prog =
417 484
    List.iter
418 485
      (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

  
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
427 493
end
428 494

  
429

  
430 495
module CycleDetection = struct
431

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

  
435 499
  let mk_copy_var n id =
436 500
    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
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
441 506

  
442 507
  let mk_copy_eq n var =
443 508
    let var_decl = get_node_var var n in
444 509
    let cp_var = mk_copy_var n var in
445 510
    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)
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) )
455 523

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

  
462 533
  (* Checks that the dependency graph [g] does not contain a cycle. Raises
463
     [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
534
     [Cycle partition] if the succession of dependencies [partition] forms a
535
     cycle *)
464 536
  let check_cycles g =
465 537
    let scc_l = Cycles.scc_list g in
466 538
    let algebraic_loops = List.filter (wrong_partition g) scc_l in
467 539
    if List.length algebraic_loops > 0 then
468 540
      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 *)
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 *)
472 544

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

  
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 *)
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 *)
486 557
  let break_cycle head cp_head g =
487 558
    let succs = IdentDepGraph.succ g head in
488 559
    IdentDepGraph.add_edge g head cp_head;
489 560
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
490 561
    List.iter
491 562
      (fun s ->
492
	IdentDepGraph.remove_edge g head s;
493
	IdentDepGraph.add_edge    g s cp_head)
563
        IdentDepGraph.remove_edge g head s;
564
        IdentDepGraph.add_edge g s cp_head)
494 565
      succs
495 566

  
496 567
  (* 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
  *)
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] *)
502 570
  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
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
506 579
    let rec break vdecls mem_eqs g =
507 580
      let scc_l = Cycles.scc_list g in
508 581
      let wrong = List.filter (wrong_partition g) scc_l in
509 582
      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

  
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
528 599
end
529 600

  
530
(* Module used to compute static disjunction of variables based upon their clocks. *)
531
module Disjunction =
532
struct
533
  module ClockedIdentModule =
534
  struct
601
(* Module used to compute static disjunction of variables based upon their
602
   clocks. *)
603
module Disjunction = struct
604
  module ClockedIdentModule = struct
535 605
    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)
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)
538 612
  end
539 613

  
540
  module CISet = Set.Make(ClockedIdentModule)
614
  module CISet = Set.Make (ClockedIdentModule)
541 615

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

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

  
550 625
  let clock_disjoint_map vdecls =
551 626
    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
  *)
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') *)
570 645
  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
  *)
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) *)
583 659
  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
  *)
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} *)
594 671
  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
672
    Hashtbl.remove map v.var_id;
673
    Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map
599 674

  
600 675
  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))
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))
607 684
end
608 685

  
609
  
610 686
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)
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)
614 691

  
615 692
let pp_error fmt err =
616 693
  match err with
617 694
  | 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
     
695
    Format.fprintf fmt "Causality error, cyclic node calls:@   @[<v 0>%a@]@ "
696
      (fprintf_list ~sep:",@ " Format.pp_print_string)
697
      trace
698
  | DataCycle traces ->
699
    Format.fprintf fmt
700
      "Causality error, cyclic data dependencies:@   @[<v 0>%a@]@ "
701
      (fprintf_list ~sep:";@ " (fun fmt trace ->
702
           Format.fprintf fmt "@[<v 0>{%a}@]"
703
             (fprintf_list ~sep:",@ " Format.pp_print_string)
704
             trace))
705
      traces
706

  
630 707
(* Merges elements of graph [g2] into graph [g1] *)
631 708
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
709
  IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
710
  IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
636 711

  
637 712
let world = "!!_world"
638 713

  
639 714
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
715
  IdentDepGraph.add_vertex g world;
716
  ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
717
  ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems
645 718

  
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" *)
719
(* Takes a node and return a pair (node', graph) where node' is node rebuilt
720
   with the equations enriched with new ones introduced to "break cycles" *)
649 721
let global_dependency node =
650 722
  let mems = ExprDep.node_memory_variables node in
651 723
  let inputs =
652 724
    ISet.union
653 725
      (ExprDep.node_input_variables node)
654
      (ExprDep.node_constant_variables node) in
726
      (ExprDep.node_constant_variables node)
727
  in
655 728
  let outputs = ExprDep.node_output_variables node in
656 729
  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;*)
730
  let g_non_mems, g_mems =
731
    ExprDep.dependence_graph mems inputs node_vars node
732
  in
733
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; Format.eprintf
734
    "g_mems: %a" pp_dep_graph g_mems;*)
660 735
  try
661 736
    CycleDetection.check_cycles g_non_mems;
662
    let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
737
    let vdecls', eqs', g_mems' = CycleDetection.break_cycles node mems g_mems in
663 738
    (*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
739
    merge_with g_non_mems g_mems';
740
    add_external_dependency outputs mems g_non_mems;
741
    ( {
742
        node with
668 743
        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
744
        node_locals = vdecls' @ node.node_locals;
745
      },
746
      g_non_mems )
747
  with Error (DataCycle _ as exc) -> raise (Error exc)
748

  
749
(* A module to sort dependencies among local variables when relying on clocked
750
   declarations *)
751
module VarClockDep = struct
678 752
  let rec get_clock_dep ck =
679 753
    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
      
754
    | Clocks.Con (ck, _, l) ->
755
      l :: get_clock_dep ck
756
    | Clocks.Clink ck' | Clocks.Ccarrying (_, ck') ->
757
      get_clock_dep ck'
758
    | _ ->
759
      []
760

  
685 761
  let sort locals =
686 762
    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
763
    let g =
764
      List.fold_left
765
        (fun g var_decl ->
766
          let deps = get_clock_dep var_decl.var_clock in
767
          add_edges [ var_decl.var_id ] deps g)
768
        g locals
692 769
    in
693 770
    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)
771
      TopologicalDepGraph.fold
772
        (fun vid (accu, remaining) ->
773
          let select v = v.var_id = vid in
774
          let selected, not_selected = List.partition select remaining in
775
          selected @ accu, not_selected)
776
        g ([], locals)
699 777
    in
700 778
    no_deps @ sorted
701
    
702 779
end
703
  
780

  
704 781
(* Local Variables: *)
705 782
(* compile-command:"make -C .." *)
706 783
(* End: *)

Also available in: Unified diff