Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ d75eb6f1

History | View | Annotate | Download (25.5 KB)

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