Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 08fd9ec8

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