Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 2196a0a6

History | View | Annotate | Download (15.4 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- *)
22

    
23

    
24
(** Simple modular syntactic causality analysis. Can reject correct
25
    programs, especially if the program is not flattened first. *)
26
open Utils
27
open Corelang
28
open Graph
29
open Format
30

    
31
exception Cycle of ident list
32

    
33
module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)
34

    
35
(*module IdentDepGraphUtil = Oper.P(IdentDepGraph)*)
36

    
37
(* Dependency of mem variables on mem variables is cut off 
38
   by duplication of some mem vars into local node vars.
39
   Thus, cylic dependency errors may only arise between no-mem vars.
40
   
41
no_mem' = combinational(no_mem, mem);
42
=> (mem -> no_mem' -> no_mem)
43

    
44
mem' = pre(no_mem, mem);
45
=> (mem' -> no_mem), (mem -> mem')
46

    
47
   Global roadmap:
48
   - compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem)
49
   - check cycles in g (a cycle means a dependency error)
50
   - break cycles in g' (it's legal !):
51
     - check cycles in g'
52
     - if any, introduce aux var to break cycle, then start afresh
53
   - insert g' into g
54
   - return g
55
*)
56

    
57
let add_edges src tgt g =
58
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)
59
 List.iter
60
   (fun s ->
61
     List.iter
62
       (fun t -> IdentDepGraph.add_edge g s t)
63
       tgt)
64
   src;
65
  g
66

    
67
let add_vertices vtc g =
68
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
69
 List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
70
  g
71

    
72
let new_graph () =
73
 IdentDepGraph.create ()
74

    
75
module ExprDep = struct
76

    
77
  let eq_var_cpt = ref 0
78

    
79
let instance_var_cpt = ref 0
80

    
81
let mk_eq_var id =
82
 incr eq_var_cpt; sprintf "#%s_%d" id !eq_var_cpt
83

    
84
let mk_instance_var id =
85
 incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt
86

    
87
let is_eq_var v = v.[0] = '#'
88

    
89
let is_instance_var v = v.[0] = '!'
90

    
91
let is_ghost_var v = is_instance_var v || is_eq_var v
92

    
93
let eq_memory_variables mems eq =
94
  let rec match_mem lhs rhs mems =
95
    match rhs.expr_desc with
96
    | Expr_fby _
97
    | Expr_pre _    -> List.fold_right ISet.add lhs mems
98
    | Expr_tuple tl -> 
99
      let lhs'= (transpose_list [lhs]) in
100
      if List.length lhs' = List.length tl then
101
	List.fold_right2 match_mem lhs' tl mems
102
      else
103
	assert false
104
    | _             -> mems in
105
  match_mem eq.eq_lhs eq.eq_rhs mems
106

    
107

    
108
let eqs_memory_variables eqs =
109
 List.fold_left eq_memory_variables ISet.empty eqs
110

    
111
(* computes the equivalence relation relating variables 
112
   in the same equation lhs, under the form of a table 
113
   of class representatives *)
114
let eqs_equiv eqs = 
115
  let eq_equiv = Hashtbl.create 23 in
116
  List.iter (fun eq ->
117
    let first = List.hd eq.eq_lhs in
118
    List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
119
  )
120
    eqs;
121
  eq_equiv
122
    
123
let node_eq_equiv nd =
124
  eqs_equiv nd.node_eqs
125

    
126
(* Create a tuple of right dimension, according to [expr] type, *)
127
(* filled with variable [v] *)
128
let adjust_tuple v expr =
129
 match expr.expr_type.Types.tdesc with
130
 | Types.Ttuple tl -> duplicate v (List.length tl)
131
 | _         -> [v]
132

    
133
(* Add dependencies from lhs to rhs in [g, g'], *)
134
(* no-mem/no-mem and mem/no-mem in g            *)
135
(* mem/mem in g'                                *)
136
(* excluding all/[inputs]                       *)
137
let add_eq_dependencies mems inputs eq (g, g') =
138
  let rec add_dep lhs_is_mem lhs rhs g =
139
    let add_var x (g, g') =
140
      if ISet.mem x inputs then (g, g') else
141
	match (lhs_is_mem, ISet.mem x mems) with
142
	| (false, true ) -> (add_edges [x] lhs g, g'                  )
143
	| (false, false) -> (add_edges lhs [x] g, g'                  )
144
	| (true , false) -> (add_edges lhs [x] g, g'                  )
145
	| (true , true ) -> (g                  , add_edges [x] lhs g') in
146
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
147
    (* i.e every input is connected to every output, through a ghost var *)
148
    let mashup_appl_dependencies f e g =
149
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
150
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
151
	(expr_list_of_expr e) (add_var f_var g) in
152
    match rhs.expr_desc with
153
    | Expr_const _    -> g
154
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
155
    | Expr_pre e      -> add_dep true lhs e g
156
    | Expr_ident x -> add_var x g
157
    | Expr_access (e1, _)
158
    | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
159
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
160
    | Expr_tuple t -> 
161
      List.fold_right (
162
	fun l g' -> 
163
	  List.fold_right (fun r g'' -> add_dep lhs_is_mem [l] r g'') t g' 
164
	    
165
      ) lhs g
166
    | Expr_merge (c, hl) -> add_var c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
167
    | 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))
168
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
169
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var c g)
170
    | Expr_appl (f, e, None) ->
171
      if Basic_library.is_internal_fun f
172
      (* tuple component-wise dependency for internal operators *)
173
      then
174
	List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
175
      (* mashed up dependency for user-defined operators *)
176
      else
177
	mashup_appl_dependencies f e g
178
    | Expr_appl (f, e, Some (r, _)) ->
179
      mashup_appl_dependencies f e (add_var r g)
180
    | Expr_uclock  (e, _)
181
    | Expr_dclock  (e, _)
182
    | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g 
183
  in
184
  add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g')
185
  
186

    
187

    
188
(* Iterate over equations *)
189
(* Add dependencies from lhs to rhs in [g, g'], *)
190
(* no-mem/no-mem and mem/no-mem in g            *)
191
(* mem/mem in g'                                *)
192
(* excluding all/[inputs]                       *)
193

    
194
let dependence_graph mems inputs eqs =
195
  eq_var_cpt := 0;
196
  instance_var_cpt := 0;
197
  let g = new_graph (), new_graph () in
198
  let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty inputs in
199
  (* Basic dependencies *)
200
  let g = List.fold_right (add_eq_dependencies mems inputs) eqs g in
201
  g
202

    
203
(* Returns the dependence graph for node [n] *)
204
let node_dependence_graph mems n =
205
  dependence_graph mems n.node_inputs n.node_eqs
206

    
207
end
208

    
209
module NodeDep = struct
210

    
211
  module ExprModule =
212
  struct
213
    type t = expr
214
    let compare = compare
215
    let hash n = Hashtbl.hash n
216
    let equal n1 n2 = n1 = n2
217
  end
218

    
219
  module ESet = Set.Make(ExprModule)
220

    
221
  let rec get_expr_calls prednode expr = 
222
    match expr.expr_desc with
223
      | Expr_const _ 
224
      | Expr_ident _ -> ESet.empty
225
      | Expr_access (e, _)
226
      | Expr_power (e, _) -> get_expr_calls prednode e
227
      | Expr_array t
228
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
229
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
230
      | Expr_fby (e1,e2)
231
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
232
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
233
      | Expr_pre e 
234
      | Expr_when (e,_,_)
235
      | Expr_uclock (e,_) 
236
      | Expr_dclock (e,_) 
237
      | Expr_phclock (e,_) -> get_expr_calls prednode e
238
      | Expr_appl (id,e, _) ->
239
	if not (Basic_library.is_internal_fun id) && prednode id
240
	then ESet.add expr (get_expr_calls prednode e)
241
	else (get_expr_calls prednode e)
242

    
243
  let get_callee expr =
244
    match expr.expr_desc with
245
    | Expr_appl (id, args, _) -> id, expr_list_of_expr args
246
    | _ -> assert false
247

    
248
  let get_calls prednode nd =
249
    let deps =
250
      List.fold_left 
251
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
252
	ESet.empty
253
	nd.node_eqs in
254
    let deps = 
255
      List.fold_left (fun accu ee -> ESet.union accu (get_expr_calls prednode ee.eexpr_qfexpr))
256
	deps
257
	(
258
	  (match nd.node_spec with None -> [] | Some s ->
259
	    s.requires @ s.ensures @ (List.fold_left (fun accu (_, assumes, ensures, _) -> accu @ assumes @ ensures) [] s.behaviors)
260
	  )
261
	  @ (List.flatten (List.map (fun ann -> List.map snd ann.annots) nd.node_annot))
262
	)
263
    in
264
    ESet.elements deps
265

    
266
  let dependence_graph prog =
267
  let g = new_graph () in
268
  let g = List.fold_right 
269
    (fun td accu -> (* for each node we add its dependencies *)
270
      match td.top_decl_desc with 
271
	| Node nd ->
272
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
273
	  let accu = add_vertices [nd.node_id] accu in
274
	  let deps = List.map (fun e -> fst (get_callee e)) (get_calls (fun _ -> true) nd) in
275
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
276
	  add_edges [nd.node_id] deps accu
277
	| _ -> assert false (* should not happen *)
278
      
279
    ) prog g in
280
  g   
281

    
282
  let rec filter_static_inputs inputs args =
283
   match inputs, args with
284
   | []   , [] -> []
285
   | 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
286
   | _ -> assert false
287

    
288
  let compute_generic_calls prog =
289
    List.iter
290
      (fun td ->
291
	match td.top_decl_desc with 
292
	| Node nd ->
293
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
294
	  nd.node_gencalls <- get_calls prednode nd
295
	| _ -> ()
296
      
297
      ) prog
298

    
299
end
300

    
301
module CycleDetection = struct
302

    
303
(* ---- Look for cycles in a dependency graph *)
304
  module Cycles = Graph.Components.Make (IdentDepGraph)
305

    
306
  let mk_copy_eq vars var =
307
    let var_decl =  try List.find (fun v -> v.var_id = var) vars with Not_found -> (
308
      Format.eprintf "Causality: Impossible to find variable %s in vars [%a]@.@?"
309
	var
310
	(Utils.fprintf_list ~sep:", " Printers.pp_var) vars;
311
      assert false
312
    )
313
    in
314
    let cp_var = mk_new_name vars var in
315
    let expr =
316
      { expr_tag = Utils.new_tag ();
317
	expr_desc = Expr_ident var;
318
	expr_type = var_decl.var_type;
319
	expr_clock = var_decl.var_clock;
320
	expr_delay = Delay.new_var ();
321
	expr_annot = None;
322
	expr_loc = var_decl.var_loc } in
323
    { var_decl with var_id = cp_var },
324
    mkeq var_decl.var_loc ([cp_var], expr)
325

    
326
  let wrong_partition g partition =
327
    match partition with
328
    | [id]    -> IdentDepGraph.mem_edge g id id
329
    | _::_::_ -> true
330
    | []      -> assert false
331

    
332
(* Checks that the dependency graph [g] does not contain a cycle. Raises
333
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
334
  let check_cycles g =
335
    let scc_l = Cycles.scc_list g in
336
    List.iter (fun partition ->
337
      if wrong_partition g partition then
338
	raise (Cycle partition)
339
      else ()
340
    ) scc_l
341

    
342
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
343
  let copy_partition g partition =
344
    let copy_g = IdentDepGraph.create () in
345
    IdentDepGraph.iter_edges
346
      (fun src tgt ->
347
	if List.mem src partition && List.mem tgt partition
348
	then IdentDepGraph.add_edge copy_g src tgt)
349
      g
350

    
351
 
352
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
353
  [head] is a head of a non-trivial scc of [g]. 
354
   In Lustre, this is legal only for mem/mem cycles *)
355
  let break_cycle head cp_head g =
356
    let succs = IdentDepGraph.succ g head in
357
    IdentDepGraph.add_edge g head cp_head;
358
    List.iter
359
      (fun s ->
360
	IdentDepGraph.remove_edge g head s;
361
	IdentDepGraph.add_edge    g s cp_head)
362
      succs
363

    
364
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
365
   belonging in node [node]. Returns:
366
   - a list of new auxiliary variable declarations
367
   - a list of new equations
368
   - a modified acyclic version of [g]
369
*)
370
  let break_cycles vars eqs mems g =
371
    let (mem_eqs, non_mem_eqs) = 
372
      List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in
373
    let rec break vdecls mem_eqs g =
374
      let scc_l = Cycles.scc_list g in
375
      let wrong = List.filter (wrong_partition g) scc_l in
376
      match wrong with
377
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
378
      | [head]::_       ->
379
	begin
380
	  IdentDepGraph.remove_edge g head head;
381
	  break vdecls mem_eqs g
382
	end
383
      | (head::part)::_ -> 
384
	begin
385
	  let vdecl_cp_head, cp_eq = mk_copy_eq vars head in
386
	  let pvar v = List.mem v part in
387
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
388
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
389
	  break_cycle head vdecl_cp_head.var_id g;
390
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
391
	end
392
      | _               -> assert false
393
    in break [] mem_eqs g
394

    
395
end
396

    
397
let pp_dep_graph fmt g =
398
  begin
399
    Format.fprintf fmt "{ /* graph */@.";
400
    Format.fprintf fmt "nodes: ";
401
    IdentDepGraph.iter_vertex (fun v -> Format.fprintf fmt "%s " v) g;
402
    Format.fprintf fmt "@.";
403
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
404
    Format.fprintf fmt "}@."
405
  end
406

    
407
let pp_error fmt trace =
408
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
409
    (fprintf_list ~sep:"->" pp_print_string) trace
410

    
411
(* Merges elements of graph [g2] into graph [g1] *)
412
  let merge_with g1 g2 =
413
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
414
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
415

    
416
let global_dependency_eqs inputs vars eqs =
417
  
418
  (* Format.eprintf "@.%a@." (Utils.fprintf_list ~sep:"@." Printers.pp_node_eq) eqs; *)
419
  (* Format.eprintf "inputs: %a@." (Utils.fprintf_list ~sep:"@." Printers.pp_var) inputs; *)
420
  let mems = ExprDep.eqs_memory_variables eqs in
421
  (* Format.eprintf "@.global dep; mems: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) (ISet.elements mems);  *)
422
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs eqs in
423
  (* Format.eprintf "g_non_mems: %a@.@?" pp_dep_graph g_non_mems; *)
424
  (* Format.eprintf "g_mems: %a@.@?" pp_dep_graph g_mems; *)
425
  CycleDetection.check_cycles g_non_mems;
426
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles vars eqs mems g_mems in
427
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
428
  merge_with g_non_mems g_mems';
429
  eqs', vdecls', g_non_mems
430

    
431
let global_dependency node =
432
  let mems = ExprDep.eqs_memory_variables node.node_eqs in
433
  let (g_non_mems, g_mems) = ExprDep.node_dependence_graph mems node in
434
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
435
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
436
  CycleDetection.check_cycles g_non_mems;
437
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles (node_vars node) node.node_eqs mems g_mems in
438
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
439
  merge_with g_non_mems g_mems';
440
  { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
441
  g_non_mems
442

    
443

    
444

    
445
(* Local Variables: *)
446
(* compile-command:"make -C .." *)
447
(* End: *)