Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 53206908

History | View | Annotate | Download (19.7 KB)

1 b38ffff3 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 0cbf0839 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 9aaee7f9 xthirioux
   non-mem variables are:
31 01d48bb0 xthirioux
   - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
32 9aaee7f9 xthirioux
   - 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 0cbf0839 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 d4101ea0 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 0cbf0839 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 9aaee7f9 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 0cbf0839 ploc
let mk_instance_var id =
100
 incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt
101
102 9aaee7f9 xthirioux
let is_read_var v = v.[0] = '#'
103 0cbf0839 ploc
104
let is_instance_var v = v.[0] = '!'
105
106 9aaee7f9 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 0cbf0839 ploc
112 6a1a01d2 xthirioux
let undo_instance_var id =
113
 assert (is_instance_var id);
114
 String.sub id 1 (String.length id - 1)
115
116 0cbf0839 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 d9d34564 ploc
    | Expr_tuple tl -> 
122
      let lhs' = (transpose_list [lhs]) in
123
      List.fold_right2 match_mem lhs' tl mems
124 0cbf0839 ploc
    | _             -> mems in
125
  match_mem eq.eq_lhs eq.eq_rhs mems
126
127
let node_memory_variables nd =
128 1eda3e78 xthirioux
 List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
129 0cbf0839 ploc
130 9aaee7f9 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 d96d54ac 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 9aaee7f9 xthirioux
136 01d48bb0 xthirioux
let node_constant_variables nd =
137
  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
138
139 9aaee7f9 xthirioux
let node_output_variables nd =
140
 List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
141
142 1837ce98 xthirioux
let node_auxiliary_variables nd =
143
 ISet.diff (node_local_variables nd) (node_memory_variables nd)
144
145 9aaee7f9 xthirioux
let node_variables nd =
146
  let inputs = node_input_variables nd in
147
  let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in
148
  List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals
149 84d9893e xthirioux
150 0cbf0839 ploc
(* computes the equivalence relation relating variables 
151
   in the same equation lhs, under the form of a table 
152
   of class representatives *)
153
let node_eq_equiv nd =
154
  let eq_equiv = Hashtbl.create 23 in
155
  List.iter (fun eq ->
156
    let first = List.hd eq.eq_lhs in
157
    List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
158
  )
159 1eda3e78 xthirioux
    (get_node_eqs nd);
160 0cbf0839 ploc
  eq_equiv
161
162
(* Create a tuple of right dimension, according to [expr] type, *)
163
(* filled with variable [v] *)
164
let adjust_tuple v expr =
165
 match expr.expr_type.Types.tdesc with
166
 | Types.Ttuple tl -> duplicate v (List.length tl)
167
 | _         -> [v]
168
169 84d9893e xthirioux
170 0cbf0839 ploc
(* Add dependencies from lhs to rhs in [g, g'], *)
171
(* no-mem/no-mem and mem/no-mem in g            *)
172
(* mem/mem in g'                                *)
173 9aaee7f9 xthirioux
(*     match (lhs_is_mem, ISet.mem x mems) with
174
      | (false, true ) -> (add_edges [x] lhs g,
175
			   g')
176
      | (false, false) -> (add_edges lhs [x] g,
177
			   g')
178
      | (true , false) -> (add_edges lhs [x] g,
179
			   g')
180
      | (true , true ) -> (g,
181
			   add_edges [x] lhs g')
182
*)
183
let add_eq_dependencies mems inputs node_vars eq (g, g') =
184 84d9893e xthirioux
  let add_var lhs_is_mem lhs x (g, g') =
185 9aaee7f9 xthirioux
    if is_instance_var x || ISet.mem x node_vars then
186
      if ISet.mem x mems
187
      then
188
	let g = add_edges lhs [mk_read_var x] g in
189
	if lhs_is_mem
190
	then
191
	  (g, add_edges [x] lhs g')
192
	else
193
	  (add_edges [x] lhs g, g')
194
      else
195
	let x = if ISet.mem x inputs then mk_read_var x else x in
196
	(add_edges lhs [x] g, g')
197 307aba8d xthirioux
    else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) in
198 84d9893e xthirioux
(* Add dependencies from [lhs] to rhs clock [ck]. *)
199
  let rec add_clock lhs_is_mem lhs ck g =
200
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
201
    match (Clocks.repr ck).Clocks.cdesc with
202
    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
203
    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
204 d9d34564 ploc
    | _                         -> g 
205
  in
206 84d9893e xthirioux
  let rec add_dep lhs_is_mem lhs rhs g =
207 d9d34564 ploc
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
208
    (* i.e every input is connected to every output, through a ghost var *)
209 0cbf0839 ploc
    let mashup_appl_dependencies f e g =
210
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
211
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
212 d9d34564 ploc
	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
213
    in
214 0cbf0839 ploc
    match rhs.expr_desc with
215
    | Expr_const _    -> g
216
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
217
    | Expr_pre e      -> add_dep true lhs e g
218 84d9893e xthirioux
    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
219 79614a15 xthirioux
    | Expr_access (e1, d)
220
    | Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
221 0cbf0839 ploc
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
222 67896f6d xthirioux
    | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
223 84d9893e 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)
224 0cbf0839 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))
225
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
226 84d9893e xthirioux
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
227 0cbf0839 ploc
    | Expr_appl (f, e, None) ->
228 53206908 xthirioux
      if Basic_library.is_expr_internal_fun rhs
229 d9d34564 ploc
      (* tuple component-wise dependency for internal operators *)
230 0cbf0839 ploc
      then
231
	List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
232 d9d34564 ploc
      (* mashed up dependency for user-defined operators *)
233 0cbf0839 ploc
      else
234
	mashup_appl_dependencies f e g
235 6a1a01d2 xthirioux
    | Expr_appl (f, e, Some c) ->
236
      mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
237 0cbf0839 ploc
  in
238 9aaee7f9 xthirioux
  let g =
239
    List.fold_left
240
      (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
241
  add_dep false eq.eq_lhs eq.eq_rhs (g, g')
242 0cbf0839 ploc
  
243
244
(* Returns the dependence graph for node [n] *)
245 9aaee7f9 xthirioux
let dependence_graph mems inputs node_vars n =
246 0cbf0839 ploc
  instance_var_cpt := 0;
247
  let g = new_graph (), new_graph () in
248
  (* Basic dependencies *)
249 1eda3e78 xthirioux
  let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
250 0cbf0839 ploc
  g
251
252
end
253
254
module NodeDep = struct
255
256
  module ExprModule =
257
  struct
258
    type t = expr
259
    let compare = compare
260
    let hash n = Hashtbl.hash n
261
    let equal n1 n2 = n1 = n2
262
  end
263
264
  module ESet = Set.Make(ExprModule)
265
266
  let rec get_expr_calls prednode expr = 
267
    match expr.expr_desc with
268
      | Expr_const _ 
269
      | Expr_ident _ -> ESet.empty
270
      | Expr_access (e, _)
271
      | Expr_power (e, _) -> get_expr_calls prednode e
272
      | Expr_array t
273
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
274
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
275
      | Expr_fby (e1,e2)
276
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
277
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
278
      | Expr_pre e 
279 0038002e ploc
      | Expr_when (e,_,_) -> get_expr_calls prednode e
280 0cbf0839 ploc
      | Expr_appl (id,e, _) ->
281 53206908 xthirioux
	if not (Basic_library.is_expr_internal_fun expr) && prednode id
282 0cbf0839 ploc
	then ESet.add expr (get_expr_calls prednode e)
283
	else (get_expr_calls prednode e)
284
285
  let get_callee expr =
286
    match expr.expr_desc with
287 e8c0f452 xthirioux
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
288
    | _ -> None
289 0cbf0839 ploc
290
  let get_calls prednode eqs =
291
    let deps =
292
      List.fold_left 
293
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
294
	ESet.empty
295
	eqs in
296
    ESet.elements deps
297
298
  let dependence_graph prog =
299
  let g = new_graph () in
300
  let g = List.fold_right 
301
    (fun td accu -> (* for each node we add its dependencies *)
302
      match td.top_decl_desc with 
303
	| Node nd ->
304
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
305
	  let accu = add_vertices [nd.node_id] accu in
306 1eda3e78 xthirioux
	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) (get_node_eqs nd)) in
307 0cbf0839 ploc
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
308
	  add_edges [nd.node_id] deps accu
309
	| _ -> assert false (* should not happen *)
310
      
311
    ) prog g in
312
  g   
313
314
  let rec filter_static_inputs inputs args =
315
   match inputs, args with
316
   | []   , [] -> []
317
   | 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
318
   | _ -> assert false
319
320
  let compute_generic_calls prog =
321
    List.iter
322
      (fun td ->
323
	match td.top_decl_desc with 
324
	| Node nd ->
325
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
326 1eda3e78 xthirioux
	  nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
327 0cbf0839 ploc
	| _ -> ()
328
      
329
      ) prog
330
331
end
332
333
module CycleDetection = struct
334
335
(* ---- Look for cycles in a dependency graph *)
336
  module Cycles = Graph.Components.Make (IdentDepGraph)
337
338
  let mk_copy_var n id =
339 1eda3e78 xthirioux
    let used name =
340
         (List.exists (fun v -> v.var_id = name) n.node_locals)
341
      || (List.exists (fun v -> v.var_id = name) n.node_inputs)
342
      || (List.exists (fun v -> v.var_id = name) n.node_outputs)
343
    in mk_new_name used id
344 0cbf0839 ploc
345
  let mk_copy_eq n var =
346 0038002e ploc
    let var_decl = get_node_var var n in
347 0cbf0839 ploc
    let cp_var = mk_copy_var n var in
348
    let expr =
349
      { expr_tag = Utils.new_tag ();
350
	expr_desc = Expr_ident var;
351
	expr_type = var_decl.var_type;
352
	expr_clock = var_decl.var_clock;
353
	expr_delay = Delay.new_var ();
354
	expr_annot = None;
355
	expr_loc = var_decl.var_loc } in
356 6a1a01d2 xthirioux
    { var_decl with var_id = cp_var; var_orig = false },
357 0cbf0839 ploc
    mkeq var_decl.var_loc ([cp_var], expr)
358
359
  let wrong_partition g partition =
360
    match partition with
361
    | [id]    -> IdentDepGraph.mem_edge g id id
362
    | _::_::_ -> true
363
    | []      -> assert false
364
365
(* Checks that the dependency graph [g] does not contain a cycle. Raises
366
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
367
  let check_cycles g =
368
    let scc_l = Cycles.scc_list g in
369
    List.iter (fun partition ->
370
      if wrong_partition g partition then
371
	raise (Cycle partition)
372
      else ()
373
    ) scc_l
374
375
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
376
  let copy_partition g partition =
377
    let copy_g = IdentDepGraph.create () in
378
    IdentDepGraph.iter_edges
379
      (fun src tgt ->
380
	if List.mem src partition && List.mem tgt partition
381
	then IdentDepGraph.add_edge copy_g src tgt)
382
      g
383
384
 
385
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
386
  [head] is a head of a non-trivial scc of [g]. 
387
   In Lustre, this is legal only for mem/mem cycles *)
388
  let break_cycle head cp_head g =
389
    let succs = IdentDepGraph.succ g head in
390
    IdentDepGraph.add_edge g head cp_head;
391 9aaee7f9 xthirioux
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
392 0cbf0839 ploc
    List.iter
393
      (fun s ->
394
	IdentDepGraph.remove_edge g head s;
395
	IdentDepGraph.add_edge    g s cp_head)
396
      succs
397
398
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
399
   belonging in node [node]. Returns:
400
   - a list of new auxiliary variable declarations
401
   - a list of new equations
402
   - a modified acyclic version of [g]
403
*)
404
  let break_cycles node mems g =
405 1eda3e78 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
406 0cbf0839 ploc
    let rec break vdecls mem_eqs g =
407
      let scc_l = Cycles.scc_list g in
408
      let wrong = List.filter (wrong_partition g) scc_l in
409
      match wrong with
410
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
411
      | [head]::_       ->
412
	begin
413
	  IdentDepGraph.remove_edge g head head;
414
	  break vdecls mem_eqs g
415
	end
416
      | (head::part)::_ -> 
417
	begin
418
	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in
419
	  let pvar v = List.mem v part in
420
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
421
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
422
	  break_cycle head vdecl_cp_head.var_id g;
423
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
424
	end
425
      | _               -> assert false
426
    in break [] mem_eqs g
427
428
end
429
430 7a737ed5 xthirioux
(* Module used to compute static disjunction of variables based upon their clocks. *)
431
module Disjunction =
432
struct
433 7ecdb0aa xthirioux
  module ClockedIdentModule =
434
  struct
435
    type t = var_decl
436
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
437 8fa083d5 xthirioux
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
438 7ecdb0aa xthirioux
  end
439
440
  module CISet = Set.Make(ClockedIdentModule)
441 7a737ed5 xthirioux
442 7ecdb0aa xthirioux
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
443
     maybe removing shorter branches *)
444 34a5a072 xthirioux
  type disjoint_map = (ident, CISet.t) Hashtbl.t
445 7a737ed5 xthirioux
446 2cf39a8e xthirioux
  let pp_ciset fmt t =
447
    begin
448
      Format.fprintf fmt "{@ ";
449
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
450
      Format.fprintf fmt "}@."
451
    end
452
453 97498b53 xthirioux
  let clock_disjoint_map vdecls =
454 7a737ed5 xthirioux
    let map = Hashtbl.create 23 in
455
    begin
456 7ecdb0aa xthirioux
      List.iter
457
	(fun v1 -> let disj_v1 =
458
		     List.fold_left
459 34a5a072 xthirioux
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
460
		       CISet.empty
461 7ecdb0aa xthirioux
		       vdecls in
462
		   (* disjoint vdecls are stored in increasing branch length order *)
463
		   Hashtbl.add map v1.var_id disj_v1)
464
	vdecls;
465 34a5a072 xthirioux
      (map : disjoint_map)
466 7a737ed5 xthirioux
    end
467 97498b53 xthirioux
468 01f1a1f4 xthirioux
  (* merge variables [v] and [v'] in disjunction [map]. Then:
469 1837ce98 xthirioux
      - the mapping v' becomes v' |-> (map v) inter (map v')
470
      - the mapping v |-> ... then disappears
471
      - other mappings become x |-> (map x) \ (if v in x then v else v')
472 7ecdb0aa xthirioux
  *)
473 01f1a1f4 xthirioux
  let merge_in_disjoint_map map v v' =
474 7ecdb0aa xthirioux
    begin
475 34a5a072 xthirioux
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
476
      Hashtbl.remove map v.var_id;
477
      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;
478 7ecdb0aa xthirioux
    end
479
480 01f1a1f4 xthirioux
  (* replace variable [v] by [v'] in disjunction [map].
481
    [v'] is a dead variable. Then:
482
      - the mapping v' becomes v' |-> (map v)
483
      - the mapping v |-> ... then disappears
484
      - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
485
  *)
486
  let replace_in_disjoint_map map v v' =
487
    begin
488
      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
489
      Hashtbl.remove  map v.var_id;
490
      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;
491
    end
492
493
  (* remove variable [v] in disjunction [map]. Then:
494
      - the mapping v |-> ... then disappears
495
      - all mappings become x |-> (map x) \ { v}
496
  *)
497
  let remove_in_disjoint_map map v =
498
    begin
499
      Hashtbl.remove map v.var_id;
500
      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;
501
    end
502
503 97498b53 xthirioux
  let pp_disjoint_map fmt map =
504
    begin
505
      Format.fprintf fmt "{ /* disjoint map */@.";
506 34a5a072 xthirioux
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;
507 97498b53 xthirioux
      Format.fprintf fmt "}@."
508
    end
509 7a737ed5 xthirioux
end
510
511 0cbf0839 ploc
let pp_dep_graph fmt g =
512
  begin
513
    Format.fprintf fmt "{ /* graph */@.";
514
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
515
    Format.fprintf fmt "}@."
516
  end
517
518
let pp_error fmt trace =
519
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
520 6a1a01d2 xthirioux
    (fprintf_list ~sep:", " pp_print_string) trace
521 0cbf0839 ploc
522
(* Merges elements of graph [g2] into graph [g1] *)
523 97498b53 xthirioux
let merge_with g1 g2 =
524 01f1a1f4 xthirioux
  begin
525 0cbf0839 ploc
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
526
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
527 01f1a1f4 xthirioux
  end
528
529 812c0369 xthirioux
let world = "!!_world"
530
531 01f1a1f4 xthirioux
let add_external_dependency outputs mems g =
532
  begin
533 812c0369 xthirioux
    IdentDepGraph.add_vertex g world;
534
    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
535
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
536 01f1a1f4 xthirioux
  end
537 0cbf0839 ploc
538
let global_dependency node =
539
  let mems = ExprDep.node_memory_variables node in
540 01d48bb0 xthirioux
  let inputs =
541
    ISet.union
542
      (ExprDep.node_input_variables node)
543
      (ExprDep.node_constant_variables node) in
544 01f1a1f4 xthirioux
  let outputs = ExprDep.node_output_variables node in
545 9aaee7f9 xthirioux
  let node_vars = ExprDep.node_variables node in
546
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
547 0cbf0839 ploc
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
548
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
549
  CycleDetection.check_cycles g_non_mems;
550
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
551
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
552 01f1a1f4 xthirioux
  begin
553
    merge_with g_non_mems g_mems';
554
    add_external_dependency outputs mems g_non_mems;
555 1eda3e78 xthirioux
    { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
556 01f1a1f4 xthirioux
    g_non_mems
557
  end
558 0cbf0839 ploc
559
(* Local Variables: *)
560
(* compile-command:"make -C .." *)
561
(* End: *)