Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 95944ba1

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