Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 2823bc51

History | View | Annotate | Download (21.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
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 c9043042 ploc
    else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)
205
  in
206
  (* Add dependencies from [lhs] to rhs clock [ck]. *)
207 d4807c3d xthirioux
  let rec add_clock lhs_is_mem lhs ck g =
208
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
209
    match (Clocks.repr ck).Clocks.cdesc with
210
    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
211
    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
212 1b01da98 ploc
    | _                         -> g 
213
  in
214 d4807c3d xthirioux
  let rec add_dep lhs_is_mem lhs rhs g =
215 1b01da98 ploc
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
216
    (* i.e every input is connected to every output, through a ghost var *)
217 22fe1c93 ploc
    let mashup_appl_dependencies f e g =
218
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
219
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
220 1b01da98 ploc
	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
221
    in
222 22fe1c93 ploc
    match rhs.expr_desc with
223
    | Expr_const _    -> g
224
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
225
    | Expr_pre e      -> add_dep true lhs e g
226 d4807c3d xthirioux
    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
227 2d179f5b xthirioux
    | Expr_access (e1, d)
228
    | Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
229 22fe1c93 ploc
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
230 df39e35a xthirioux
    | Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
231 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)
232 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))
233
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
234 d4807c3d xthirioux
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
235 22fe1c93 ploc
    | Expr_appl (f, e, None) ->
236 04a63d25 xthirioux
      if Basic_library.is_expr_internal_fun rhs
237 1b01da98 ploc
      (* tuple component-wise dependency for internal operators *)
238 22fe1c93 ploc
      then
239
	List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
240 1b01da98 ploc
      (* mashed up dependency for user-defined operators *)
241 22fe1c93 ploc
      else
242
	mashup_appl_dependencies f e g
243 54d032f5 xthirioux
    | Expr_appl (f, e, Some c) ->
244
      mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
245 22fe1c93 ploc
  in
246 3bfed7f9 xthirioux
  let g =
247
    List.fold_left
248 c9043042 ploc
      (fun g lhs ->
249
	if ISet.mem lhs mems then
250
	  add_vertices [lhs; mk_read_var lhs] g
251
	else
252
	  add_vertices [lhs] g
253
      )
254
      g eq.eq_lhs
255
  in
256 3bfed7f9 xthirioux
  add_dep false eq.eq_lhs eq.eq_rhs (g, g')
257 22fe1c93 ploc
  
258
259
(* Returns the dependence graph for node [n] *)
260 3bfed7f9 xthirioux
let dependence_graph mems inputs node_vars n =
261 22fe1c93 ploc
  instance_var_cpt := 0;
262
  let g = new_graph (), new_graph () in
263
  (* Basic dependencies *)
264 b08ffca7 xthirioux
  let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
265 c9043042 ploc
  (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
266
     faut imposer que les outputs dépendent des asserts pour identifier que les
267
     fcn calls des asserts sont évalués avant le noeuds *)
268
269
  (* (\* In order to introduce dependencies between assert expressions and the node, *)
270
  (*    we build an artificial dependency between node output and each assert *)
271
  (*    expr. While these are not valid equations, they should properly propage in *)
272
  (*    function add_eq_dependencies *\) *)
273
  (* let g = *)
274
  (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
275
  (*   List.fold_left (fun g ae -> *)
276
  (*     let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)
277
  (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
278
  (* ) g n.node_asserts in  *)
279 22fe1c93 ploc
  g
280
281 c9043042 ploc
   end
282
283
   module NodeDep = struct
284
285
   module ExprModule =
286
   struct
287
   type t = expr
288
   let compare = compare
289
   let hash n = Hashtbl.hash n
290
   let equal n1 n2 = n1 = n2
291
   end
292
293
   module ESet = Set.Make(ExprModule)
294
295
   let rec get_expr_calls prednode expr = 
296
   match expr.expr_desc with
297
   | Expr_const _ 
298
   | Expr_ident _ -> ESet.empty
299
   | Expr_access (e, _)
300
   | Expr_power (e, _) -> get_expr_calls prednode e
301
   | Expr_array t
302
   | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
303
   | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
304
   | Expr_fby (e1,e2)
305
   | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
306
   | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
307
   | Expr_pre e 
308
   | Expr_when (e,_,_) -> get_expr_calls prednode e
309
   | Expr_appl (id,e, _) ->
310
   if not (Basic_library.is_expr_internal_fun expr) && prednode id
311
   then ESet.add expr (get_expr_calls prednode e)
312
   else (get_expr_calls prednode e)
313
314
   let get_callee expr =
315
   match expr.expr_desc with
316
   | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
317
   | _ -> None
318
319
   let get_calls prednode eqs =
320
   let deps =
321
   List.fold_left 
322
   (fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
323
   ESet.empty
324
   eqs in
325
   ESet.elements deps
326
327
   let dependence_graph prog =
328
   let g = new_graph () in
329
   let g = List.fold_right 
330
   (fun td accu -> (* for each node we add its dependencies *)
331 22fe1c93 ploc
      match td.top_decl_desc with 
332
	| Node nd ->
333
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
334
	  let accu = add_vertices [nd.node_id] accu in
335 b08ffca7 xthirioux
	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) (get_node_eqs nd)) in
336 22fe1c93 ploc
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
337
	  add_edges [nd.node_id] deps accu
338
	| _ -> assert false (* should not happen *)
339
      
340
    ) prog g in
341
  g   
342
343 eb837d74 xthirioux
  (* keep subgraph of [gr] consisting of nodes accessible from node [v] *)
344
  let slice_graph gr v =
345
    begin
346
      let gr' = new_graph () in
347
      IdentDepGraph.add_vertex gr' v;
348
      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;
349
      gr'
350
    end
351
  
352 22fe1c93 ploc
  let rec filter_static_inputs inputs args =
353
   match inputs, args with
354
   | []   , [] -> []
355 7d640c88 ploc
   | 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
356 22fe1c93 ploc
   | _ -> assert false
357
358
  let compute_generic_calls prog =
359
    List.iter
360
      (fun td ->
361
	match td.top_decl_desc with 
362
	| Node nd ->
363
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
364 b08ffca7 xthirioux
	  nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
365 22fe1c93 ploc
	| _ -> ()
366
      
367
      ) prog
368
369
end
370
371
module CycleDetection = struct
372
373
(* ---- Look for cycles in a dependency graph *)
374
  module Cycles = Graph.Components.Make (IdentDepGraph)
375
376
  let mk_copy_var n id =
377 b08ffca7 xthirioux
    let used name =
378
         (List.exists (fun v -> v.var_id = name) n.node_locals)
379
      || (List.exists (fun v -> v.var_id = name) n.node_inputs)
380
      || (List.exists (fun v -> v.var_id = name) n.node_outputs)
381
    in mk_new_name used id
382 22fe1c93 ploc
383
  let mk_copy_eq n var =
384 01c7d5e1 ploc
    let var_decl = get_node_var var n in
385 22fe1c93 ploc
    let cp_var = mk_copy_var n var in
386
    let expr =
387
      { expr_tag = Utils.new_tag ();
388
	expr_desc = Expr_ident var;
389
	expr_type = var_decl.var_type;
390
	expr_clock = var_decl.var_clock;
391
	expr_delay = Delay.new_var ();
392
	expr_annot = None;
393
	expr_loc = var_decl.var_loc } in
394 54d032f5 xthirioux
    { var_decl with var_id = cp_var; var_orig = false },
395 22fe1c93 ploc
    mkeq var_decl.var_loc ([cp_var], expr)
396
397
  let wrong_partition g partition =
398
    match partition with
399
    | [id]    -> IdentDepGraph.mem_edge g id id
400
    | _::_::_ -> true
401
    | []      -> assert false
402
403
(* Checks that the dependency graph [g] does not contain a cycle. Raises
404
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
405
  let check_cycles g =
406
    let scc_l = Cycles.scc_list g in
407
    List.iter (fun partition ->
408
      if wrong_partition g partition then
409 eb837d74 xthirioux
	raise (Error (DataCycle partition))
410 22fe1c93 ploc
      else ()
411
    ) scc_l
412
413
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
414
  let copy_partition g partition =
415
    let copy_g = IdentDepGraph.create () in
416
    IdentDepGraph.iter_edges
417
      (fun src tgt ->
418
	if List.mem src partition && List.mem tgt partition
419
	then IdentDepGraph.add_edge copy_g src tgt)
420
      g
421
422
 
423
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
424
  [head] is a head of a non-trivial scc of [g]. 
425
   In Lustre, this is legal only for mem/mem cycles *)
426
  let break_cycle head cp_head g =
427
    let succs = IdentDepGraph.succ g head in
428
    IdentDepGraph.add_edge g head cp_head;
429 3bfed7f9 xthirioux
    IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);
430 22fe1c93 ploc
    List.iter
431
      (fun s ->
432
	IdentDepGraph.remove_edge g head s;
433
	IdentDepGraph.add_edge    g s cp_head)
434
      succs
435
436
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
437
   belonging in node [node]. Returns:
438
   - a list of new auxiliary variable declarations
439
   - a list of new equations
440
   - a modified acyclic version of [g]
441
*)
442
  let break_cycles node mems g =
443 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
444 22fe1c93 ploc
    let rec break vdecls mem_eqs g =
445
      let scc_l = Cycles.scc_list g in
446
      let wrong = List.filter (wrong_partition g) scc_l in
447
      match wrong with
448
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
449
      | [head]::_       ->
450
	begin
451
	  IdentDepGraph.remove_edge g head head;
452
	  break vdecls mem_eqs g
453
	end
454
      | (head::part)::_ -> 
455
	begin
456
	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in
457
	  let pvar v = List.mem v part in
458
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
459
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
460
	  break_cycle head vdecl_cp_head.var_id g;
461
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
462
	end
463
      | _               -> assert false
464
    in break [] mem_eqs g
465
466
end
467
468 8f89eba8 xthirioux
(* Module used to compute static disjunction of variables based upon their clocks. *)
469
module Disjunction =
470
struct
471 add75bcb xthirioux
  module ClockedIdentModule =
472
  struct
473
    type t = var_decl
474
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock
475 28c58de1 xthirioux
    let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)
476 add75bcb xthirioux
  end
477
478
  module CISet = Set.Make(ClockedIdentModule)
479 8f89eba8 xthirioux
480 add75bcb xthirioux
  (* map: var |-> list of disjoint vars, sorted in increasing branch length order,
481
     maybe removing shorter branches *)
482 b6a94a4e xthirioux
  type disjoint_map = (ident, CISet.t) Hashtbl.t
483 8f89eba8 xthirioux
484 a38c681e xthirioux
  let pp_ciset fmt t =
485
    begin
486
      Format.fprintf fmt "{@ ";
487
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
488
      Format.fprintf fmt "}@."
489
    end
490
491 b1a97ade xthirioux
  let clock_disjoint_map vdecls =
492 8f89eba8 xthirioux
    let map = Hashtbl.create 23 in
493
    begin
494 add75bcb xthirioux
      List.iter
495
	(fun v1 -> let disj_v1 =
496
		     List.fold_left
497 b6a94a4e xthirioux
		       (fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)
498
		       CISet.empty
499 add75bcb xthirioux
		       vdecls in
500
		   (* disjoint vdecls are stored in increasing branch length order *)
501
		   Hashtbl.add map v1.var_id disj_v1)
502
	vdecls;
503 b6a94a4e xthirioux
      (map : disjoint_map)
504 8f89eba8 xthirioux
    end
505 b1a97ade xthirioux
506 45c13277 xthirioux
  (* merge variables [v] and [v'] in disjunction [map]. Then:
507 bb2ca5f4 xthirioux
      - the mapping v' becomes v' |-> (map v) inter (map v')
508
      - the mapping v |-> ... then disappears
509
      - other mappings become x |-> (map x) \ (if v in x then v else v')
510 add75bcb xthirioux
  *)
511 45c13277 xthirioux
  let merge_in_disjoint_map map v v' =
512 add75bcb xthirioux
    begin
513 b6a94a4e xthirioux
      Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));
514
      Hashtbl.remove map v.var_id;
515
      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;
516 add75bcb xthirioux
    end
517
518 45c13277 xthirioux
  (* replace variable [v] by [v'] in disjunction [map].
519
    [v'] is a dead variable. Then:
520
      - the mapping v' becomes v' |-> (map v)
521
      - the mapping v |-> ... then disappears
522
      - all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
523
  *)
524
  let replace_in_disjoint_map map v v' =
525
    begin
526
      Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);
527
      Hashtbl.remove  map v.var_id;
528
      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;
529
    end
530
531
  (* remove variable [v] in disjunction [map]. Then:
532
      - the mapping v |-> ... then disappears
533
      - all mappings become x |-> (map x) \ { v}
534
  *)
535
  let remove_in_disjoint_map map v =
536
    begin
537
      Hashtbl.remove map v.var_id;
538
      Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map;
539
    end
540
541 b1a97ade xthirioux
  let pp_disjoint_map fmt map =
542
    begin
543
      Format.fprintf fmt "{ /* disjoint map */@.";
544 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;
545 b1a97ade xthirioux
      Format.fprintf fmt "}@."
546
    end
547 8f89eba8 xthirioux
end
548
549 22fe1c93 ploc
let pp_dep_graph fmt g =
550
  begin
551
    Format.fprintf fmt "{ /* graph */@.";
552
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
553
    Format.fprintf fmt "}@."
554
  end
555
556 eb837d74 xthirioux
let pp_error fmt err =
557
  match err with
558
  | DataCycle trace ->
559
     fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
560
       (fprintf_list ~sep:", " pp_print_string) trace
561
  | NodeCycle trace ->
562
     fprintf fmt "@.Causality error, cyclic node calls: %a@."
563
       (fprintf_list ~sep:", " pp_print_string) trace
564 22fe1c93 ploc
565
(* Merges elements of graph [g2] into graph [g1] *)
566 b1a97ade xthirioux
let merge_with g1 g2 =
567 45c13277 xthirioux
  begin
568 22fe1c93 ploc
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
569
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
570 45c13277 xthirioux
  end
571
572 57115ec0 xthirioux
let world = "!!_world"
573
574 45c13277 xthirioux
let add_external_dependency outputs mems g =
575
  begin
576 57115ec0 xthirioux
    IdentDepGraph.add_vertex g world;
577
    ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
578
    ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
579 45c13277 xthirioux
  end
580 22fe1c93 ploc
581
let global_dependency node =
582
  let mems = ExprDep.node_memory_variables node in
583 ec433d69 xthirioux
  let inputs =
584
    ISet.union
585
      (ExprDep.node_input_variables node)
586
      (ExprDep.node_constant_variables node) in
587 45c13277 xthirioux
  let outputs = ExprDep.node_output_variables node in
588 3bfed7f9 xthirioux
  let node_vars = ExprDep.node_variables node in
589
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
590 22fe1c93 ploc
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
591
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
592
  CycleDetection.check_cycles g_non_mems;
593
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
594
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
595 45c13277 xthirioux
  begin
596
    merge_with g_non_mems g_mems';
597
    add_external_dependency outputs mems g_non_mems;
598 b08ffca7 xthirioux
    { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
599 45c13277 xthirioux
    g_non_mems
600
  end
601 22fe1c93 ploc
602
(* Local Variables: *)
603
(* compile-command:"make -C .." *)
604
(* End: *)