Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 58a463e7

History | View | Annotate | Download (19.4 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
open LustreSpec
19
open Corelang
20
open Graph
21
open Format
22
23
exception Cycle of ident list
24
25
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
26
27
(* Dependency of mem variables on mem variables is cut off 
28
   by duplication of some mem vars into local node vars.
29
   Thus, cylic dependency errors may only arise between no-mem vars.
30 3bfed7f9 xthirioux
   non-mem variables are:
31
   - inputs: not needed for causality/scheduling, needed only for detecting useless vars
32
   - read mems (fake vars): same remark as above.
33
   - outputs: decoupled from mems, if necessary
34
   - locals
35
   - instance vars (fake vars): simplify causality analysis
36
37
   global constants are not part of the dependency graph.
38
39 22fe1c93 ploc
no_mem' = combinational(no_mem, mem);
40
=> (mem -> no_mem' -> no_mem)
41
42
mem' = pre(no_mem, mem);
43
=> (mem' -> no_mem), (mem -> mem')
44
45
   Global roadmap:
46
   - compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem)
47
   - check cycles in g (a cycle means a dependency error)
48
   - break cycles in g' (it's legal !):
49
     - check cycles in g'
50
     - if any, introduce aux var to break cycle, then start afresh
51
   - insert g' into g
52
   - return g
53
*)
54
55 695d6f2f xthirioux
(* Tests whether [v] is a root of graph [g], i.e. a source *)
56
let is_graph_root v g =
57
 IdentDepGraph.in_degree g v = 0
58
59
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
60
let graph_roots g =
61
 IdentDepGraph.fold_vertex
62
   (fun v roots -> if is_graph_root v g then v::roots else roots)
63
   g []
64
65 22fe1c93 ploc
let add_edges src tgt g =
66
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)
67
 List.iter
68
   (fun s ->
69
     List.iter
70
       (fun t -> IdentDepGraph.add_edge g s t)
71
       tgt)
72
   src;
73
  g
74
75
let add_vertices vtc g =
76
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
77
 List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
78
  g
79
80
let new_graph () =
81
 IdentDepGraph.create ()
82
83
module ExprDep = struct
84
85
let instance_var_cpt = ref 0
86
87 3bfed7f9 xthirioux
(* read vars represent input/mem read-only vars,
88
   they are not part of the program/schedule,
89
   as they are not assigned,
90
   but used to compute useless inputs/mems.
91
   a mem read var represents a mem at the beginning of a cycle  *)
92
let mk_read_var id =
93
 sprintf "#%s" id
94
95
(* instance vars represent node instance calls,
96
   they are not part of the program/schedule,
97
   but used to simplify causality analysis
98
    *)
99 22fe1c93 ploc
let mk_instance_var id =
100
 incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt
101
102 3bfed7f9 xthirioux
let is_read_var v = v.[0] = '#'
103 22fe1c93 ploc
104
let is_instance_var v = v.[0] = '!'
105
106 3bfed7f9 xthirioux
let is_ghost_var v = is_instance_var v || is_read_var v
107
108
let undo_read_var id =
109
 assert (is_read_var id);
110
 String.sub id 1 (String.length id - 1)
111 22fe1c93 ploc
112 54d032f5 xthirioux
let undo_instance_var id =
113
 assert (is_instance_var id);
114
 String.sub id 1 (String.length id - 1)
115
116 22fe1c93 ploc
let eq_memory_variables mems eq =
117
  let rec match_mem lhs rhs mems =
118
    match rhs.expr_desc with
119
    | Expr_fby _
120
    | Expr_pre _    -> List.fold_right ISet.add lhs mems
121 1b01da98 ploc
    | Expr_tuple tl -> 
122
      let lhs' = (transpose_list [lhs]) in
123
      List.fold_right2 match_mem lhs' tl mems
124 22fe1c93 ploc
    | _             -> mems in
125
  match_mem eq.eq_lhs eq.eq_rhs mems
126
127
let node_memory_variables nd =
128 b08ffca7 xthirioux
 List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
129 22fe1c93 ploc
130 3bfed7f9 xthirioux
let node_input_variables nd =
131
 List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
132 8a183477 xthirioux
133
let node_local_variables nd =
134
 List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
135 3bfed7f9 xthirioux
136
let node_output_variables nd =
137
 List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
138
139 bb2ca5f4 xthirioux
let node_auxiliary_variables nd =
140
 ISet.diff (node_local_variables nd) (node_memory_variables nd)
141
142 3bfed7f9 xthirioux
let node_variables nd =
143
  let inputs = node_input_variables nd in
144
  let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in
145
  List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals
146 d4807c3d xthirioux
147 22fe1c93 ploc
(* computes the equivalence relation relating variables 
148
   in the same equation lhs, under the form of a table 
149
   of class representatives *)
150
let node_eq_equiv nd =
151
  let eq_equiv = Hashtbl.create 23 in
152
  List.iter (fun eq ->
153
    let first = List.hd eq.eq_lhs in
154
    List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
155
  )
156 b08ffca7 xthirioux
    (get_node_eqs nd);
157 22fe1c93 ploc
  eq_equiv
158
159
(* Create a tuple of right dimension, according to [expr] type, *)
160
(* filled with variable [v] *)
161
let adjust_tuple v expr =
162
 match expr.expr_type.Types.tdesc with
163
 | Types.Ttuple tl -> duplicate v (List.length tl)
164
 | _         -> [v]
165
166 d4807c3d xthirioux
167 22fe1c93 ploc
(* Add dependencies from lhs to rhs in [g, g'], *)
168
(* no-mem/no-mem and mem/no-mem in g            *)
169
(* mem/mem in g'                                *)
170 3bfed7f9 xthirioux
(*     match (lhs_is_mem, ISet.mem x mems) with
171
      | (false, true ) -> (add_edges [x] lhs g,
172
			   g')
173
      | (false, false) -> (add_edges lhs [x] g,
174
			   g')
175
      | (true , false) -> (add_edges lhs [x] g,
176
			   g')
177
      | (true , true ) -> (g,
178
			   add_edges [x] lhs g')
179
*)
180
let add_eq_dependencies mems inputs node_vars eq (g, g') =
181 d4807c3d xthirioux
  let add_var lhs_is_mem lhs x (g, g') =
182 3bfed7f9 xthirioux
    if is_instance_var x || ISet.mem x node_vars then
183
      if ISet.mem x mems
184
      then
185
	let g = add_edges lhs [mk_read_var x] g in
186
	if lhs_is_mem
187
	then
188
	  (g, add_edges [x] lhs g')
189
	else
190
	  (add_edges [x] lhs g, g')
191
      else
192
	let x = if ISet.mem x inputs then mk_read_var x else x in
193
	(add_edges lhs [x] g, g')
194 d0b1ec56 xthirioux
    else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) in
195 d4807c3d xthirioux
(* Add dependencies from [lhs] to rhs clock [ck]. *)
196
  let rec add_clock lhs_is_mem lhs ck g =
197
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
198
    match (Clocks.repr ck).Clocks.cdesc with
199
    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
200
    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
201 1b01da98 ploc
    | _                         -> g 
202
  in
203 d4807c3d xthirioux
  let rec add_dep lhs_is_mem lhs rhs g =
204 1b01da98 ploc
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
205
    (* i.e every input is connected to every output, through a ghost var *)
206 22fe1c93 ploc
    let mashup_appl_dependencies f e g =
207
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
208
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
209 1b01da98 ploc
	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
210
    in
211 22fe1c93 ploc
    match rhs.expr_desc with
212
    | Expr_const _    -> g
213
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
214
    | Expr_pre e      -> add_dep true lhs e g
215 d4807c3d xthirioux
    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
216 22fe1c93 ploc
    | Expr_access (e1, _)
217
    | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
218
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
219 df39e35a xthirioux
    | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
220 d4807c3d xthirioux
    | 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)
221 22fe1c93 ploc
    | 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))
222
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
223 d4807c3d xthirioux
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
224 22fe1c93 ploc
    | Expr_appl (f, e, None) ->
225
      if Basic_library.is_internal_fun f
226 1b01da98 ploc
      (* tuple component-wise dependency for internal operators *)
227 22fe1c93 ploc
      then
228
	List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
229 1b01da98 ploc
      (* mashed up dependency for user-defined operators *)
230 22fe1c93 ploc
      else
231
	mashup_appl_dependencies f e g
232 54d032f5 xthirioux
    | Expr_appl (f, e, Some c) ->
233
      mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
234 22fe1c93 ploc
  in
235 3bfed7f9 xthirioux
  let g =
236
    List.fold_left
237
      (fun g lhs -> if ISet.mem lhs mems then add_vertices [lhs; mk_read_var lhs] g else add_vertices [lhs] g) g eq.eq_lhs in
238
  add_dep false eq.eq_lhs eq.eq_rhs (g, g')
239 22fe1c93 ploc
  
240
241
(* Returns the dependence graph for node [n] *)
242 3bfed7f9 xthirioux
let dependence_graph mems inputs node_vars n =
243 22fe1c93 ploc
  instance_var_cpt := 0;
244
  let g = new_graph (), new_graph () in
245
  (* Basic dependencies *)
246 b08ffca7 xthirioux
  let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
247 22fe1c93 ploc
  g
248
249
end
250
251
module NodeDep = struct
252
253
  module ExprModule =
254
  struct
255
    type t = expr
256
    let compare = compare
257
    let hash n = Hashtbl.hash n
258
    let equal n1 n2 = n1 = n2
259
  end
260
261
  module ESet = Set.Make(ExprModule)
262
263
  let rec get_expr_calls prednode expr = 
264
    match expr.expr_desc with
265
      | Expr_const _ 
266
      | Expr_ident _ -> ESet.empty
267
      | Expr_access (e, _)
268
      | Expr_power (e, _) -> get_expr_calls prednode e
269
      | Expr_array t
270
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
271
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
272
      | Expr_fby (e1,e2)
273
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
274
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
275
      | Expr_pre e 
276 01c7d5e1 ploc
      | Expr_when (e,_,_) -> get_expr_calls prednode e
277 22fe1c93 ploc
      | Expr_appl (id,e, _) ->
278
	if not (Basic_library.is_internal_fun id) && prednode id
279
	then ESet.add expr (get_expr_calls prednode e)
280
	else (get_expr_calls prednode e)
281
282
  let get_callee expr =
283
    match expr.expr_desc with
284 7afcba5a xthirioux
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
285
    | _ -> None
286 22fe1c93 ploc
287
  let get_calls prednode eqs =
288
    let deps =
289
      List.fold_left 
290
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
291
	ESet.empty
292
	eqs in
293
    ESet.elements deps
294
295
  let dependence_graph prog =
296
  let g = new_graph () in
297
  let g = List.fold_right 
298
    (fun td accu -> (* for each node we add its dependencies *)
299
      match td.top_decl_desc with 
300
	| Node nd ->
301
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
302
	  let accu = add_vertices [nd.node_id] accu in
303 b08ffca7 xthirioux
	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) (get_node_eqs nd)) in
304 22fe1c93 ploc
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
305
	  add_edges [nd.node_id] deps accu
306
	| _ -> assert false (* should not happen *)
307
      
308
    ) prog g in
309
  g   
310
311
  let rec filter_static_inputs inputs args =
312
   match inputs, args with
313
   | []   , [] -> []
314
   | v::vq, a::aq -> if v.var_dec_const then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq
315
   | _ -> assert false
316
317
  let compute_generic_calls prog =
318
    List.iter
319
      (fun td ->
320
	match td.top_decl_desc with 
321
	| Node nd ->
322
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
323 b08ffca7 xthirioux
	  nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
324 22fe1c93 ploc
	| _ -> ()
325
      
326
      ) prog
327
328
end
329
330
module CycleDetection = struct
331
332
(* ---- Look for cycles in a dependency graph *)
333
  module Cycles = Graph.Components.Make (IdentDepGraph)
334
335
  let mk_copy_var n id =
336 b08ffca7 xthirioux
    let used name =
337
         (List.exists (fun v -> v.var_id = name) n.node_locals)
338
      || (List.exists (fun v -> v.var_id = name) n.node_inputs)
339
      || (List.exists (fun v -> v.var_id = name) n.node_outputs)
340
    in mk_new_name used id
341 22fe1c93 ploc
342
  let mk_copy_eq n var =
343 01c7d5e1 ploc
    let var_decl = get_node_var var n in
344 22fe1c93 ploc
    let cp_var = mk_copy_var n var in
345
    let expr =
346
      { expr_tag = Utils.new_tag ();
347
	expr_desc = Expr_ident var;
348
	expr_type = var_decl.var_type;
349
	expr_clock = var_decl.var_clock;
350
	expr_delay = Delay.new_var ();
351
	expr_annot = None;
352
	expr_loc = var_decl.var_loc } in
353 54d032f5 xthirioux
    { var_decl with var_id = cp_var; var_orig = false },
354 22fe1c93 ploc
    mkeq var_decl.var_loc ([cp_var], expr)
355
356
  let wrong_partition g partition =
357
    match partition with
358
    | [id]    -> IdentDepGraph.mem_edge g id id
359
    | _::_::_ -> true
360
    | []      -> assert false
361
362
(* Checks that the dependency graph [g] does not contain a cycle. Raises
363
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
364
  let check_cycles g =
365
    let scc_l = Cycles.scc_list g in
366
    List.iter (fun partition ->
367
      if wrong_partition g partition then
368
	raise (Cycle partition)
369
      else ()
370
    ) scc_l
371
372
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
373
  let copy_partition g partition =
374
    let copy_g = IdentDepGraph.create () in
375
    IdentDepGraph.iter_edges
376
      (fun src tgt ->
377
	if List.mem src partition && List.mem tgt partition
378
	then IdentDepGraph.add_edge copy_g src tgt)
379
      g
380
381
 
382
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
383
  [head] is a head of a non-trivial scc of [g]. 
384
   In Lustre, this is legal only for mem/mem cycles *)
385
  let break_cycle head cp_head g =
386
    let succs = IdentDepGraph.succ g head in
387
    IdentDepGraph.add_edge g head cp_head;
388 3bfed7f9 xthirioux
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
389 22fe1c93 ploc
    List.iter
390
      (fun s ->
391
	IdentDepGraph.remove_edge g head s;
392
	IdentDepGraph.add_edge    g s cp_head)
393
      succs
394
395
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
396
   belonging in node [node]. Returns:
397
   - a list of new auxiliary variable declarations
398
   - a list of new equations
399
   - a modified acyclic version of [g]
400
*)
401
  let break_cycles node mems g =
402 b08ffca7 xthirioux
    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) (get_node_eqs node) in
403 22fe1c93 ploc
    let rec break vdecls mem_eqs g =
404
      let scc_l = Cycles.scc_list g in
405
      let wrong = List.filter (wrong_partition g) scc_l in
406
      match wrong with
407
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
408
      | [head]::_       ->
409
	begin
410
	  IdentDepGraph.remove_edge g head head;
411
	  break vdecls mem_eqs g
412
	end
413
      | (head::part)::_ -> 
414
	begin
415
	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in
416
	  let pvar v = List.mem v part in
417
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
418
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
419
	  break_cycle head vdecl_cp_head.var_id g;
420
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
421
	end
422
      | _               -> assert false
423
    in break [] mem_eqs g
424
425
end
426
427 8f89eba8 xthirioux
(* Module used to compute static disjunction of variables based upon their clocks. *)
428
module Disjunction =
429
struct
430 add75bcb xthirioux
  module ClockedIdentModule =
431
  struct
432
    type t = var_decl
433
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
434 28c58de1 xthirioux
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
435 add75bcb xthirioux
  end
436
437
  module CISet = Set.Make(ClockedIdentModule)
438 8f89eba8 xthirioux
439 add75bcb xthirioux
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
440
     maybe removing shorter branches *)
441 b6a94a4e xthirioux
  type disjoint_map = (ident, CISet.t) Hashtbl.t
442 8f89eba8 xthirioux
443 a38c681e xthirioux
  let pp_ciset fmt t =
444
    begin
445
      Format.fprintf fmt "{@ ";
446
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
447
      Format.fprintf fmt "}@."
448
    end
449
450 b1a97ade xthirioux
  let clock_disjoint_map vdecls =
451 8f89eba8 xthirioux
    let map = Hashtbl.create 23 in
452
    begin
453 add75bcb xthirioux
      List.iter
454
	(fun v1 -> let disj_v1 =
455
		     List.fold_left
456 b6a94a4e xthirioux
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
457
		       CISet.empty
458 add75bcb xthirioux
		       vdecls in
459
		   (* disjoint vdecls are stored in increasing branch length order *)
460
		   Hashtbl.add map v1.var_id disj_v1)
461
	vdecls;
462 b6a94a4e xthirioux
      (map : disjoint_map)
463 8f89eba8 xthirioux
    end
464 b1a97ade xthirioux
465 45c13277 xthirioux
  (* merge variables [v] and [v'] in disjunction [map]. Then:
466 bb2ca5f4 xthirioux
      - the mapping v' becomes v' |-> (map v) inter (map v')
467
      - the mapping v |-> ... then disappears
468
      - other mappings become x |-> (map x) \ (if v in x then v else v')
469 add75bcb xthirioux
  *)
470 45c13277 xthirioux
  let merge_in_disjoint_map map v v' =
471 add75bcb xthirioux
    begin
472 b6a94a4e xthirioux
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
473
      Hashtbl.remove map v.var_id;
474
      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;
475 add75bcb xthirioux
    end
476
477 45c13277 xthirioux
  (* replace variable [v] by [v'] in disjunction [map].
478
    [v'] is a dead variable. Then:
479
      - the mapping v' becomes v' |-> (map v)
480
      - the mapping v |-> ... then disappears
481
      - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
482
  *)
483
  let replace_in_disjoint_map map v v' =
484
    begin
485
      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
486
      Hashtbl.remove  map v.var_id;
487
      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;
488
    end
489
490
  (* remove variable [v] in disjunction [map]. Then:
491
      - the mapping v |-> ... then disappears
492
      - all mappings become x |-> (map x) \ { v}
493
  *)
494
  let remove_in_disjoint_map map v =
495
    begin
496
      Hashtbl.remove map v.var_id;
497
      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;
498
    end
499
500 b1a97ade xthirioux
  let pp_disjoint_map fmt map =
501
    begin
502
      Format.fprintf fmt "{ /* disjoint map */@.";
503 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;
504 b1a97ade xthirioux
      Format.fprintf fmt "}@."
505
    end
506 8f89eba8 xthirioux
end
507
508 22fe1c93 ploc
let pp_dep_graph fmt g =
509
  begin
510
    Format.fprintf fmt "{ /* graph */@.";
511
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
512
    Format.fprintf fmt "}@."
513
  end
514
515
let pp_error fmt trace =
516
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
517 54d032f5 xthirioux
    (fprintf_list ~sep:", " pp_print_string) trace
518 22fe1c93 ploc
519
(* Merges elements of graph [g2] into graph [g1] *)
520 b1a97ade xthirioux
let merge_with g1 g2 =
521 45c13277 xthirioux
  begin
522 22fe1c93 ploc
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
523
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
524 45c13277 xthirioux
  end
525
526
let add_external_dependency outputs mems g =
527 2822cf55 xthirioux
  let caller ="!!_world" in
528 45c13277 xthirioux
  begin
529
    IdentDepGraph.add_vertex g caller;
530
    ISet.iter (fun o -> IdentDepGraph.add_edge g caller o) outputs;
531
    ISet.iter (fun m -> IdentDepGraph.add_edge g caller m) mems;
532
  end
533 22fe1c93 ploc
534
let global_dependency node =
535
  let mems = ExprDep.node_memory_variables node in
536 3bfed7f9 xthirioux
  let inputs = ExprDep.node_input_variables node in
537 45c13277 xthirioux
  let outputs = ExprDep.node_output_variables node in
538 3bfed7f9 xthirioux
  let node_vars = ExprDep.node_variables node in
539
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
540 22fe1c93 ploc
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
541
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
542
  CycleDetection.check_cycles g_non_mems;
543
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
544
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
545 45c13277 xthirioux
  begin
546
    merge_with g_non_mems g_mems';
547
    add_external_dependency outputs mems g_non_mems;
548 b08ffca7 xthirioux
    { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
549 45c13277 xthirioux
    g_non_mems
550
  end
551 22fe1c93 ploc
552
(* Local Variables: *)
553
(* compile-command:"make -C .." *)
554
(* End: *)