Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ ae7d913d

History | View | Annotate | Download (24.5 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
14
15
(** Simple modular syntactic causality analysis. Can reject correct
16
    programs, especially if the program is not flattened first. *)
17
open Utils
18 8446bf03 ploc
open Lustre_types
19 22fe1c93 ploc
open Corelang
20
open Graph
21
22 e7cc5186 ploc
23
type identified_call = eq * tag
24 eb837d74 xthirioux
type error =
25 e7cc5186 ploc
  | DataCycle of ident list list (* multiple failed partitions at once *) 
26 eb837d74 xthirioux
  | NodeCycle of ident list
27
28
exception Error of error
29 22fe1c93 ploc
30
31 eb837d74 xthirioux
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
32 70466917 ploc
module TopologicalDepGraph = Topological.Make(IdentDepGraph)
33
34 eb837d74 xthirioux
(*module DotGraph = Graphviz.Dot (IdentDepGraph)*)
35
module Bfs = Traverse.Bfs (IdentDepGraph)
36
  
37 22fe1c93 ploc
(* Dependency of mem variables on mem variables is cut off 
38
   by duplication of some mem vars into local node vars.
39
   Thus, cylic dependency errors may only arise between no-mem vars.
40 3bfed7f9 xthirioux
   non-mem variables are:
41 ec433d69 xthirioux
   - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
42 3bfed7f9 xthirioux
   - read mems (fake vars): same remark as above.
43
   - outputs: decoupled from mems, if necessary
44
   - locals
45
   - instance vars (fake vars): simplify causality analysis
46 7352a936 ploc
   
47 3bfed7f9 xthirioux
   global constants are not part of the dependency graph.
48 7352a936 ploc
   
49
   no_mem' = combinational(no_mem, mem);
50
   => (mem -> no_mem' -> no_mem)
51 3bfed7f9 xthirioux
52 7352a936 ploc
   mem' = pre(no_mem, mem);
53
   => (mem' -> no_mem), (mem -> mem')
54
   
55 22fe1c93 ploc
   Global roadmap:
56
   - compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem)
57
   - check cycles in g (a cycle means a dependency error)
58
   - break cycles in g' (it's legal !):
59
     - check cycles in g'
60
     - if any, introduce aux var to break cycle, then start afresh
61
   - insert g' into g
62
   - return g
63
*)
64
65 695d6f2f xthirioux
(* Tests whether [v] is a root of graph [g], i.e. a source *)
66
let is_graph_root v g =
67 7352a936 ploc
  IdentDepGraph.in_degree g v = 0
68 695d6f2f xthirioux
69
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
70
let graph_roots g =
71 7352a936 ploc
  IdentDepGraph.fold_vertex
72
    (fun v roots -> if is_graph_root v g then v::roots else roots)
73
    g []
74 695d6f2f xthirioux
75 22fe1c93 ploc
let add_edges src tgt g =
76 7352a936 ploc
 (*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)
77
  List.iter
78
    (fun s ->
79
      List.iter
80
	(fun t -> IdentDepGraph.add_edge g s t)
81
	tgt)
82
    src;
83 22fe1c93 ploc
  g
84
85
let add_vertices vtc g =
86 7352a936 ploc
 (*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
87
  List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
88 22fe1c93 ploc
  g
89
90
let new_graph () =
91 7352a936 ploc
  IdentDepGraph.create ()
92 22fe1c93 ploc
93 333e3a25 ploc
    
94 22fe1c93 ploc
module ExprDep = struct
95 333e3a25 ploc
  let get_node_eqs nd =
96
    let eqs, auts = get_node_eqs nd in
97
    if auts != [] then assert false (* No call on causality on a Lustre model
98
				       with automaton. They should be expanded by now. *);
99
    eqs
100
      
101 7352a936 ploc
  let instance_var_cpt = ref 0
102 22fe1c93 ploc
103 3bfed7f9 xthirioux
(* 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 7352a936 ploc
  let mk_read_var id =
109 e7cc5186 ploc
    Format.sprintf "#%s" id
110 3bfed7f9 xthirioux
111
(* instance vars represent node instance calls,
112
   they are not part of the program/schedule,
113
   but used to simplify causality analysis
114 7352a936 ploc
*)
115
  let mk_instance_var id =
116 e7cc5186 ploc
    incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt
117 22fe1c93 ploc
118 7352a936 ploc
  let is_read_var v = v.[0] = '#'
119 22fe1c93 ploc
120 7352a936 ploc
  let is_instance_var v = v.[0] = '!'
121 22fe1c93 ploc
122 7352a936 ploc
  let is_ghost_var v = is_instance_var v || is_read_var v
123 3bfed7f9 xthirioux
124 7352a936 ploc
  let undo_read_var id =
125
    assert (is_read_var id);
126
    String.sub id 1 (String.length id - 1)
127 22fe1c93 ploc
128 7352a936 ploc
  let undo_instance_var id =
129
    assert (is_instance_var id);
130
    String.sub id 1 (String.length id - 1)
131 54d032f5 xthirioux
132 7352a936 ploc
  let eq_memory_variables mems eq =
133
    let rec match_mem lhs rhs mems =
134
      match rhs.expr_desc with
135
      | Expr_fby _
136
      | Expr_pre _    -> List.fold_right ISet.add lhs mems
137
      | Expr_tuple tl -> 
138
	 let lhs' = (transpose_list [lhs]) in
139
	 List.fold_right2 match_mem lhs' tl mems
140
      | _             -> mems in
141
    match_mem eq.eq_lhs eq.eq_rhs mems
142 22fe1c93 ploc
143 7352a936 ploc
  let node_memory_variables nd =
144
    List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
145 22fe1c93 ploc
146 7352a936 ploc
  let node_input_variables nd =
147
    List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
148 8a183477 xthirioux
149 7352a936 ploc
  let node_local_variables nd =
150
    List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
151 3bfed7f9 xthirioux
152 7352a936 ploc
  let node_constant_variables nd =
153
    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
154 ec433d69 xthirioux
155 7352a936 ploc
  let node_output_variables nd =
156
    List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
157 3bfed7f9 xthirioux
158 7352a936 ploc
  let node_auxiliary_variables nd =
159
    ISet.diff (node_local_variables nd) (node_memory_variables nd)
160 bb2ca5f4 xthirioux
161 7352a936 ploc
  let node_variables nd =
162
    let inputs = node_input_variables nd in
163
    let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in
164
    List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals
165 d4807c3d xthirioux
166 22fe1c93 ploc
(* computes the equivalence relation relating variables 
167
   in the same equation lhs, under the form of a table 
168
   of class representatives *)
169 7352a936 ploc
  let node_eq_equiv nd =
170
    let eq_equiv = Hashtbl.create 23 in
171
    List.iter (fun eq ->
172
      let first = List.hd eq.eq_lhs in
173
      List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
174
    )
175
      (get_node_eqs nd);
176
    eq_equiv
177 22fe1c93 ploc
178
(* Create a tuple of right dimension, according to [expr] type, *)
179
(* filled with variable [v] *)
180 7352a936 ploc
  let adjust_tuple v expr =
181
    match expr.expr_type.Types.tdesc with
182
    | Types.Ttuple tl -> duplicate v (List.length tl)
183
    | _         -> [v]
184
185
186
  (* Add dependencies from lhs to rhs in [g, g'], *)
187
  (* no-mem/no-mem and mem/no-mem in g            *)
188
  (* mem/mem in g'                                *)
189
  (*     match (lhs_is_mem, ISet.mem x mems) with
190
	 | (false, true ) -> (add_edges [x] lhs g,
191
	 g')
192
	 | (false, false) -> (add_edges lhs [x] g,
193
	 g')
194
	 | (true , false) -> (add_edges lhs [x] g,
195
	 g')
196
	 | (true , true ) -> (g,
197
	 add_edges [x] lhs g')
198
  *)
199
  let add_eq_dependencies mems inputs node_vars eq (g, g') =
200
    let add_var lhs_is_mem lhs x (g, g') =
201
      if is_instance_var x || ISet.mem x node_vars then
202
	if ISet.mem x mems
203 3bfed7f9 xthirioux
	then
204 7352a936 ploc
	  let g = add_edges lhs [mk_read_var x] g in
205
	  if lhs_is_mem
206
	  then
207
	    (g, add_edges [x] lhs g')
208
	  else
209
	    (add_edges [x] lhs g, g')
210 3bfed7f9 xthirioux
	else
211 7352a936 ploc
	  let x = if ISet.mem x inputs then mk_read_var x else x in
212
	  (add_edges lhs [x] g, g')
213
      else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)
214
    in
215 c9043042 ploc
  (* Add dependencies from [lhs] to rhs clock [ck]. *)
216 7352a936 ploc
    let rec add_clock lhs_is_mem lhs ck g =
217 d4807c3d xthirioux
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
218 7352a936 ploc
      match (Clocks.repr ck).Clocks.cdesc with
219
      | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
220
      | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
221
      | _                         -> g 
222
    in
223
    let rec add_dep lhs_is_mem lhs rhs g =
224 1b01da98 ploc
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
225
    (* i.e every input is connected to every output, through a ghost var *)
226 7352a936 ploc
      let mashup_appl_dependencies f e g =
227 e7cc5186 ploc
	let f_var = mk_instance_var (Format.sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
228 7352a936 ploc
	List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
229
	  (expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
230
      in
231
      match rhs.expr_desc with
232
      | Expr_const _    -> g
233
      | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
234
      | Expr_pre e      -> add_dep true lhs e g
235
      | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
236
      | Expr_access (e1, d)
237
      | Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
238
      | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
239
      | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
240
      | 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)
241
      | 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))
242
      | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
243
      | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
244
      | Expr_appl (f, e, None) ->
245
	 if Basic_library.is_expr_internal_fun rhs
246 1b01da98 ploc
      (* tuple component-wise dependency for internal operators *)
247 7352a936 ploc
	 then
248
	   List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
249 1b01da98 ploc
      (* mashed up dependency for user-defined operators *)
250 7352a936 ploc
	 else
251
	   mashup_appl_dependencies f e g
252
      | Expr_appl (f, e, Some c) ->
253
	 mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
254
    in
255
    let g =
256
      List.fold_left
257
	(fun g lhs ->
258
	  if ISet.mem lhs mems then
259
	    add_vertices [lhs; mk_read_var lhs] g
260
	  else
261
	    add_vertices [lhs] g
262
	)
263
	g eq.eq_lhs
264
    in
265
    add_dep false eq.eq_lhs eq.eq_rhs (g, g')
266
      
267 22fe1c93 ploc
268 7352a936 ploc
  (* Returns the dependence graph for node [n] *)
269
  let dependence_graph mems inputs node_vars n =
270
    instance_var_cpt := 0;
271
    let g = new_graph (), new_graph () in
272
    (* Basic dependencies *)
273
    let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
274
    (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
275
       faut imposer que les outputs dépendent des asserts pour identifier que les
276
       fcn calls des asserts sont évalués avant le noeuds *)
277
    
278
    (* (\* In order to introduce dependencies between assert expressions and the node, *)
279
    (*    we build an artificial dependency between node output and each assert *)
280
    (*    expr. While these are not valid equations, they should properly propage in *)
281
    (*    function add_eq_dependencies *\) *)
282
    (* let g = *)
283
    (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
284
    (*   List.fold_left (fun g ae -> *)
285
    (*     let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)
286
    (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
287
    (* ) g n.node_asserts in  *)
288
    g
289
290
end
291
292
module NodeDep = struct
293 22fe1c93 ploc
294 7352a936 ploc
  module ExprModule =
295
  struct
296
    type t = expr
297
    let compare = compare
298
    let hash n = Hashtbl.hash n
299
    let equal n1 n2 = n1 = n2
300
  end
301
302
  module ESet = Set.Make(ExprModule)
303
304
  let rec get_expr_calls prednode expr = 
305
    match expr.expr_desc with
306
    | Expr_const _ 
307
    | Expr_ident _ -> ESet.empty
308
    | Expr_access (e, _)
309
    | Expr_power (e, _) -> get_expr_calls prednode e
310
    | Expr_array t
311
    | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
312
    | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
313
    | Expr_fby (e1,e2)
314
    | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
315
    | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
316
    | Expr_pre e 
317
    | Expr_when (e,_,_) -> get_expr_calls prednode e
318
    | Expr_appl (id,e, _) ->
319
       if not (Basic_library.is_expr_internal_fun expr) && prednode id
320
       then ESet.add expr (get_expr_calls prednode e)
321
       else (get_expr_calls prednode e)
322
323
  let get_callee expr =
324
    match expr.expr_desc with
325
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
326
    | _ -> None
327
328 333e3a25 ploc
  let get_calls prednode nd =
329
    let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl in
330
    let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in
331
    let rec get_stmt_calls s =
332
      match s with Eq eq -> get_eq_calls eq | Aut aut -> get_aut_calls aut 
333
    and get_aut_calls aut =
334
      let get_handler_calls h =
335
	let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in
336
	let until = get_cond_calls h.hand_until in
337
	let unless = get_cond_calls h.hand_unless in
338
	let calls = ESet.union until unless in 
339
	let calls = accu get_stmt_calls calls h.hand_stmts in
340
	let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in
341
	(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *)
342
	calls
343
      in
344
      accu get_handler_calls ESet.empty aut.aut_handlers
345
    in
346
    let eqs, auts = get_node_eqs nd in
347
    let deps = accu get_eq_calls ESet.empty eqs in
348
    let deps = accu get_aut_calls deps auts in
349 7352a936 ploc
    ESet.elements deps
350
351
  let dependence_graph prog =
352
    let g = new_graph () in
353
    let g = List.fold_right 
354
      (fun td accu -> (* for each node we add its dependencies *)
355
	match td.top_decl_desc with 
356 22fe1c93 ploc
	| Node nd ->
357
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
358 7352a936 ploc
	   let accu = add_vertices [nd.node_id] accu in
359
	   let deps = List.map
360
	     (fun e -> fst (desome (get_callee e)))
361 333e3a25 ploc
	     (get_calls (fun _ -> true) nd) 
362 7352a936 ploc
	   in
363
	     (* Adding assert expressions deps *)
364
	   let deps_asserts =
365
	     let prednode = (fun _ -> true) in (* what is this about? *)
366
	     List.map
367
	       (fun e -> fst (desome (get_callee e)))
368
 	       (ESet.elements
369
		  (List.fold_left
370
		     (fun accu assert_expr -> ESet.union accu (get_expr_calls prednode assert_expr))
371
		     ESet.empty
372
		     (List.map (fun _assert -> _assert.assert_expr) nd.node_asserts)
373
		  )
374
	       )
375
      	   in
376 22fe1c93 ploc
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
377 7352a936 ploc
	   add_edges [nd.node_id] (deps@deps_asserts) accu
378 22fe1c93 ploc
	| _ -> assert false (* should not happen *)
379 7352a936 ploc
	   
380
      ) prog g in
381
    g   
382 22fe1c93 ploc
383 eb837d74 xthirioux
  (* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
384
  let slice_graph gr v =
385
    begin
386
      let gr' = new_graph () in
387
      IdentDepGraph.add_vertex gr' v;
388
      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;
389
      gr'
390
    end
391 7352a936 ploc
      
392 22fe1c93 ploc
  let rec filter_static_inputs inputs args =
393 7352a936 ploc
    match inputs, args with
394
    | []   , [] -> []
395
    | 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
396
    | _ -> assert false
397 22fe1c93 ploc
398
  let compute_generic_calls prog =
399
    List.iter
400
      (fun td ->
401
	match td.top_decl_desc with 
402
	| Node nd ->
403 7352a936 ploc
	   let prednode n = is_generic_node (Hashtbl.find node_table n) in
404 333e3a25 ploc
	   nd.node_gencalls <- get_calls prednode nd
405 22fe1c93 ploc
	| _ -> ()
406 7352a936 ploc
	   
407 22fe1c93 ploc
      ) prog
408
409
end
410
411 e7cc5186 ploc
412 22fe1c93 ploc
module CycleDetection = struct
413
414 7352a936 ploc
  (* ---- Look for cycles in a dependency graph *)
415 22fe1c93 ploc
  module Cycles = Graph.Components.Make (IdentDepGraph)
416
417
  let mk_copy_var n id =
418 b08ffca7 xthirioux
    let used name =
419 7352a936 ploc
      (List.exists (fun v -> v.var_id = name) n.node_locals)
420 b08ffca7 xthirioux
      || (List.exists (fun v -> v.var_id = name) n.node_inputs)
421
      || (List.exists (fun v -> v.var_id = name) n.node_outputs)
422
    in mk_new_name used id
423 22fe1c93 ploc
424
  let mk_copy_eq n var =
425 01c7d5e1 ploc
    let var_decl = get_node_var var n in
426 22fe1c93 ploc
    let cp_var = mk_copy_var n var in
427
    let expr =
428
      { expr_tag = Utils.new_tag ();
429
	expr_desc = Expr_ident var;
430
	expr_type = var_decl.var_type;
431
	expr_clock = var_decl.var_clock;
432
	expr_delay = Delay.new_var ();
433
	expr_annot = None;
434
	expr_loc = var_decl.var_loc } in
435 54d032f5 xthirioux
    { var_decl with var_id = cp_var; var_orig = false },
436 22fe1c93 ploc
    mkeq var_decl.var_loc ([cp_var], expr)
437
438
  let wrong_partition g partition =
439
    match partition with
440
    | [id]    -> IdentDepGraph.mem_edge g id id
441
    | _::_::_ -> true
442
    | []      -> assert false
443
444 7352a936 ploc
  (* Checks that the dependency graph [g] does not contain a cycle. Raises
445
     [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
446 22fe1c93 ploc
  let check_cycles g =
447
    let scc_l = Cycles.scc_list g in
448 e7cc5186 ploc
    let algebraic_loops = List.filter (wrong_partition g) scc_l in
449
    if List.length algebraic_loops > 0 then
450
      raise (Error (DataCycle algebraic_loops))
451
	(* We extract a hint to resolve the cycle: for each variable in the cycle
452
	   which is defined by a call, we return the name of the node call and
453
	   its specific id *)
454 22fe1c93 ploc
455 7352a936 ploc
  (* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
456 22fe1c93 ploc
  let copy_partition g partition =
457
    let copy_g = IdentDepGraph.create () in
458
    IdentDepGraph.iter_edges
459
      (fun src tgt ->
460
	if List.mem src partition && List.mem tgt partition
461
	then IdentDepGraph.add_edge copy_g src tgt)
462
      g
463
464 7352a936 ploc
      
465
  (* Breaks dependency cycles in a graph [g] by inserting aux variables.
466
     [head] is a head of a non-trivial scc of [g]. 
467
     In Lustre, this is legal only for mem/mem cycles *)
468 22fe1c93 ploc
  let break_cycle head cp_head g =
469
    let succs = IdentDepGraph.succ g head in
470
    IdentDepGraph.add_edge g head cp_head;
471 3bfed7f9 xthirioux
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
472 22fe1c93 ploc
    List.iter
473
      (fun s ->
474
	IdentDepGraph.remove_edge g head s;
475
	IdentDepGraph.add_edge    g s cp_head)
476
      succs
477
478 7352a936 ploc
  (* Breaks cycles of the dependency graph [g] of memory variables [mems]
479
     belonging in node [node]. Returns:
480
     - a list of new auxiliary variable declarations
481
     - a list of new equations
482
     - a modified acyclic version of [g]
483
  *)
484 22fe1c93 ploc
  let break_cycles node mems g =
485 333e3a25 ploc
    let eqs , auts = get_node_eqs node in
486
    assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *)
487
    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in
488 22fe1c93 ploc
    let rec break vdecls mem_eqs g =
489
      let scc_l = Cycles.scc_list g in
490
      let wrong = List.filter (wrong_partition g) scc_l in
491
      match wrong with
492
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
493
      | [head]::_       ->
494 7352a936 ploc
	 begin
495
	   IdentDepGraph.remove_edge g head head;
496
	   break vdecls mem_eqs g
497
	 end
498 22fe1c93 ploc
      | (head::part)::_ -> 
499 7352a936 ploc
	 begin
500
	   let vdecl_cp_head, cp_eq = mk_copy_eq node head in
501
	   let pvar v = List.mem v part in
502
	   let fvar v = if v = head then vdecl_cp_head.var_id else v in
503
	   let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
504
	   break_cycle head vdecl_cp_head.var_id g;
505
	   break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
506
	 end
507 22fe1c93 ploc
      | _               -> assert false
508
    in break [] mem_eqs g
509
510
end
511
512 8f89eba8 xthirioux
(* Module used to compute static disjunction of variables based upon their clocks. *)
513
module Disjunction =
514
struct
515 add75bcb xthirioux
  module ClockedIdentModule =
516
  struct
517
    type t = var_decl
518
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
519 28c58de1 xthirioux
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
520 add75bcb xthirioux
  end
521
522
  module CISet = Set.Make(ClockedIdentModule)
523 8f89eba8 xthirioux
524 add75bcb xthirioux
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
525
     maybe removing shorter branches *)
526 b6a94a4e xthirioux
  type disjoint_map = (ident, CISet.t) Hashtbl.t
527 8f89eba8 xthirioux
528 a38c681e xthirioux
  let pp_ciset fmt t =
529
    begin
530
      Format.fprintf fmt "{@ ";
531
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
532
      Format.fprintf fmt "}@."
533
    end
534
535 b1a97ade xthirioux
  let clock_disjoint_map vdecls =
536 8f89eba8 xthirioux
    let map = Hashtbl.create 23 in
537
    begin
538 add75bcb xthirioux
      List.iter
539
	(fun v1 -> let disj_v1 =
540
		     List.fold_left
541 b6a94a4e xthirioux
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
542
		       CISet.empty
543 add75bcb xthirioux
		       vdecls in
544
		   (* disjoint vdecls are stored in increasing branch length order *)
545
		   Hashtbl.add map v1.var_id disj_v1)
546
	vdecls;
547 b6a94a4e xthirioux
      (map : disjoint_map)
548 8f89eba8 xthirioux
    end
549 b1a97ade xthirioux
550 45c13277 xthirioux
  (* merge variables [v] and [v'] in disjunction [map]. Then:
551 7352a936 ploc
     - the mapping v' becomes v' |-> (map v) inter (map v')
552
     - the mapping v |-> ... then disappears
553
     - other mappings become x |-> (map x) \ (if v in x then v else v')
554 add75bcb xthirioux
  *)
555 45c13277 xthirioux
  let merge_in_disjoint_map map v v' =
556 add75bcb xthirioux
    begin
557 b6a94a4e xthirioux
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
558
      Hashtbl.remove map v.var_id;
559
      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;
560 add75bcb xthirioux
    end
561
562 45c13277 xthirioux
  (* replace variable [v] by [v'] in disjunction [map].
563 7352a936 ploc
     [v'] is a dead variable. Then:
564
     - the mapping v' becomes v' |-> (map v)
565
     - the mapping v |-> ... then disappears
566
     - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
567 45c13277 xthirioux
  *)
568
  let replace_in_disjoint_map map v v' =
569
    begin
570
      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
571
      Hashtbl.remove  map v.var_id;
572
      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;
573
    end
574
575
  (* remove variable [v] in disjunction [map]. Then:
576 7352a936 ploc
     - the mapping v |-> ... then disappears
577
     - all mappings become x |-> (map x) \ { v}
578 45c13277 xthirioux
  *)
579
  let remove_in_disjoint_map map v =
580
    begin
581
      Hashtbl.remove map v.var_id;
582
      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;
583
    end
584
585 b1a97ade xthirioux
  let pp_disjoint_map fmt map =
586
    begin
587
      Format.fprintf fmt "{ /* disjoint map */@.";
588 b6a94a4e xthirioux
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
589 b1a97ade xthirioux
      Format.fprintf fmt "}@."
590
    end
591 8f89eba8 xthirioux
end
592
593 e7cc5186 ploc
  
594 22fe1c93 ploc
let pp_dep_graph fmt g =
595
  begin
596
    Format.fprintf fmt "{ /* graph */@.";
597
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
598
    Format.fprintf fmt "}@."
599
  end
600
601 eb837d74 xthirioux
let pp_error fmt err =
602
  match err with
603
  | NodeCycle trace ->
604 e7cc5186 ploc
     Format.fprintf fmt "Causality error, cyclic node calls:@   @[<v 0>%a@]@ "
605
       (fprintf_list ~sep:",@ " Format.pp_print_string) trace
606
  | DataCycle traces -> (
607
     Format.fprintf fmt "Causality error, cyclic data dependencies:@   @[<v 0>%a@]@ "
608
       (fprintf_list ~sep:";@ "
609
       (fun fmt trace ->
610
	 Format.fprintf fmt "@[<v 0>{%a}@]"
611
	   (fprintf_list ~sep:",@ " Format.pp_print_string)
612
	   trace
613
       )) traces
614
  )
615
     
616 22fe1c93 ploc
(* Merges elements of graph [g2] into graph [g1] *)
617 b1a97ade xthirioux
let merge_with g1 g2 =
618 45c13277 xthirioux
  begin
619 22fe1c93 ploc
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
620
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
621 45c13277 xthirioux
  end
622
623 57115ec0 xthirioux
let world = "!!_world"
624
625 45c13277 xthirioux
let add_external_dependency outputs mems g =
626
  begin
627 57115ec0 xthirioux
    IdentDepGraph.add_vertex g world;
628
    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
629
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
630 45c13277 xthirioux
  end
631 22fe1c93 ploc
632
let global_dependency node =
633
  let mems = ExprDep.node_memory_variables node in
634 ec433d69 xthirioux
  let inputs =
635
    ISet.union
636
      (ExprDep.node_input_variables node)
637
      (ExprDep.node_constant_variables node) in
638 45c13277 xthirioux
  let outputs = ExprDep.node_output_variables node in
639 3bfed7f9 xthirioux
  let node_vars = ExprDep.node_variables node in
640
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
641 22fe1c93 ploc
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
642 7352a936 ploc
    Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
643 e7cc5186 ploc
  try
644
    CycleDetection.check_cycles g_non_mems;
645
    let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
646
    (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
647
    begin
648
      merge_with g_non_mems g_mems';
649
      add_external_dependency outputs mems g_non_mems;
650
      { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
651
      g_non_mems
652
    end
653
  with Error (DataCycle _ as exc) -> (
654
      raise (Error (exc))
655
  )
656 22fe1c93 ploc
657 70466917 ploc
(* A module to sort dependencies among local variables when relying on clocked declarations *)
658
module VarClockDep =
659
struct
660
  let rec get_clock_dep ck =
661
    match ck.Clocks.cdesc with
662
    | Clocks.Con (ck ,c ,l) -> l::(get_clock_dep ck)
663
    | Clocks.Clink ck' 
664
    | Clocks.Ccarrying (_, ck') -> get_clock_dep ck'
665
    | _ -> []
666
      
667
  let sort locals =
668
    let g = new_graph () in
669
    let g = List.fold_left (
670
      fun g var_decl ->
671
	let deps = get_clock_dep var_decl.var_clock in
672
	add_edges [var_decl.var_id] deps g
673
    ) g locals
674
    in
675
    let sorted, no_deps =
676
      TopologicalDepGraph.fold (fun vid (accu, remaining) -> (
677
	let select v = v.var_id = vid in
678
	let selected, not_selected = List.partition select remaining in
679
	selected@accu, not_selected
680
      )) g ([],locals)
681
    in
682
    no_deps @ sorted
683
    
684
end
685
  
686 22fe1c93 ploc
(* Local Variables: *)
687
(* compile-command:"make -C .." *)
688
(* End: *)