Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 22fe1c93

History | View | Annotate | Download (13.3 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 LustreSpec
28
open Corelang
29
open Graph
30
open Format
31

    
32
exception Cycle of ident list
33

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

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

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

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

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

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

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

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

    
76
module ExprDep = struct
77

    
78
let eq_var_cpt = ref 0
79

    
80
let instance_var_cpt = ref 0
81

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

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

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

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

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

    
94
let eq_memory_variables mems eq =
95
  let rec match_mem lhs rhs mems =
96
    match rhs.expr_desc with
97
    | Expr_fby _
98
    | Expr_pre _    -> List.fold_right ISet.add lhs mems
99
    | Expr_tuple tl -> List.fold_right2 match_mem (transpose_list [lhs]) tl mems
100
    | _             -> mems in
101
  match_mem eq.eq_lhs eq.eq_rhs mems
102

    
103
let node_memory_variables nd =
104
 List.fold_left eq_memory_variables ISet.empty nd.node_eqs
105

    
106
(* computes the equivalence relation relating variables 
107
   in the same equation lhs, under the form of a table 
108
   of class representatives *)
109
let node_eq_equiv nd =
110
  let eq_equiv = Hashtbl.create 23 in
111
  List.iter (fun eq ->
112
    let first = List.hd eq.eq_lhs in
113
    List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
114
  )
115
    nd.node_eqs;
116
  eq_equiv
117

    
118
(* Create a tuple of right dimension, according to [expr] type, *)
119
(* filled with variable [v] *)
120
let adjust_tuple v expr =
121
 match expr.expr_type.Types.tdesc with
122
 | Types.Ttuple tl -> duplicate v (List.length tl)
123
 | _         -> [v]
124

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

    
174
(* Returns the dependence graph for node [n] *)
175
let dependence_graph mems n =
176
  eq_var_cpt := 0;
177
  instance_var_cpt := 0;
178
  let g = new_graph (), new_graph () in
179
  let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty n.node_inputs in
180
  (* Basic dependencies *)
181
  let g = List.fold_right (add_eq_dependencies mems inputs) n.node_eqs g in
182
  g
183

    
184
end
185

    
186
module NodeDep = struct
187

    
188
  module ExprModule =
189
  struct
190
    type t = expr
191
    let compare = compare
192
    let hash n = Hashtbl.hash n
193
    let equal n1 n2 = n1 = n2
194
  end
195

    
196
  module ESet = Set.Make(ExprModule)
197

    
198
  let rec get_expr_calls prednode expr = 
199
    match expr.expr_desc with
200
      | Expr_const _ 
201
      | Expr_ident _ -> ESet.empty
202
      | Expr_access (e, _)
203
      | Expr_power (e, _) -> get_expr_calls prednode e
204
      | Expr_array t
205
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
206
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
207
      | Expr_fby (e1,e2)
208
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
209
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
210
      | Expr_pre e 
211
      | Expr_when (e,_,_)
212
      | Expr_uclock (e,_) 
213
      | Expr_dclock (e,_) 
214
      | Expr_phclock (e,_) -> get_expr_calls prednode e
215
      | Expr_appl (id,e, _) ->
216
	if not (Basic_library.is_internal_fun id) && prednode id
217
	then ESet.add expr (get_expr_calls prednode e)
218
	else (get_expr_calls prednode e)
219

    
220
  let get_callee expr =
221
    match expr.expr_desc with
222
    | Expr_appl (id, args, _) -> id, expr_list_of_expr args
223
    | _ -> assert false
224

    
225
  let get_calls prednode eqs =
226
    let deps =
227
      List.fold_left 
228
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
229
	ESet.empty
230
	eqs in
231
    ESet.elements deps
232

    
233
  let dependence_graph prog =
234
  let g = new_graph () in
235
  let g = List.fold_right 
236
    (fun td accu -> (* for each node we add its dependencies *)
237
      match td.top_decl_desc with 
238
	| Node nd ->
239
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
240
	  let accu = add_vertices [nd.node_id] accu in
241
	  let deps = List.map (fun e -> fst (get_callee e)) (get_calls (fun _ -> true) nd.node_eqs) in
242
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
243
	  add_edges [nd.node_id] deps accu
244
	| _ -> assert false (* should not happen *)
245
      
246
    ) prog g in
247
  g   
248

    
249
  let rec filter_static_inputs inputs args =
250
   match inputs, args with
251
   | []   , [] -> []
252
   | 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
253
   | _ -> assert false
254

    
255
  let compute_generic_calls prog =
256
    List.iter
257
      (fun td ->
258
	match td.top_decl_desc with 
259
	| Node nd ->
260
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
261
	  nd.node_gencalls <- get_calls prednode nd.node_eqs
262
	| _ -> ()
263
      
264
      ) prog
265

    
266
end
267

    
268
module CycleDetection = struct
269

    
270
(* ---- Look for cycles in a dependency graph *)
271
  module Cycles = Graph.Components.Make (IdentDepGraph)
272

    
273
  let mk_copy_var n id =
274
    mk_new_name (node_vars n) id
275

    
276
  let mk_copy_eq n var =
277
    let var_decl = node_var var n in
278
    let cp_var = mk_copy_var n var in
279
    let expr =
280
      { expr_tag = Utils.new_tag ();
281
	expr_desc = Expr_ident var;
282
	expr_type = var_decl.var_type;
283
	expr_clock = var_decl.var_clock;
284
	expr_delay = Delay.new_var ();
285
	expr_annot = None;
286
	expr_loc = var_decl.var_loc } in
287
    { var_decl with var_id = cp_var },
288
    mkeq var_decl.var_loc ([cp_var], expr)
289

    
290
  let wrong_partition g partition =
291
    match partition with
292
    | [id]    -> IdentDepGraph.mem_edge g id id
293
    | _::_::_ -> true
294
    | []      -> assert false
295

    
296
(* Checks that the dependency graph [g] does not contain a cycle. Raises
297
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
298
  let check_cycles g =
299
    let scc_l = Cycles.scc_list g in
300
    List.iter (fun partition ->
301
      if wrong_partition g partition then
302
	raise (Cycle partition)
303
      else ()
304
    ) scc_l
305

    
306
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
307
  let copy_partition g partition =
308
    let copy_g = IdentDepGraph.create () in
309
    IdentDepGraph.iter_edges
310
      (fun src tgt ->
311
	if List.mem src partition && List.mem tgt partition
312
	then IdentDepGraph.add_edge copy_g src tgt)
313
      g
314

    
315
 
316
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
317
  [head] is a head of a non-trivial scc of [g]. 
318
   In Lustre, this is legal only for mem/mem cycles *)
319
  let break_cycle head cp_head g =
320
    let succs = IdentDepGraph.succ g head in
321
    IdentDepGraph.add_edge g head cp_head;
322
    List.iter
323
      (fun s ->
324
	IdentDepGraph.remove_edge g head s;
325
	IdentDepGraph.add_edge    g s cp_head)
326
      succs
327

    
328
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
329
   belonging in node [node]. Returns:
330
   - a list of new auxiliary variable declarations
331
   - a list of new equations
332
   - a modified acyclic version of [g]
333
*)
334
  let break_cycles node mems g =
335
    let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) node.node_eqs in
336
    let rec break vdecls mem_eqs g =
337
      let scc_l = Cycles.scc_list g in
338
      let wrong = List.filter (wrong_partition g) scc_l in
339
      match wrong with
340
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
341
      | [head]::_       ->
342
	begin
343
	  IdentDepGraph.remove_edge g head head;
344
	  break vdecls mem_eqs g
345
	end
346
      | (head::part)::_ -> 
347
	begin
348
	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in
349
	  let pvar v = List.mem v part in
350
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
351
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
352
	  break_cycle head vdecl_cp_head.var_id g;
353
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
354
	end
355
      | _               -> assert false
356
    in break [] mem_eqs g
357

    
358
end
359

    
360
let pp_dep_graph fmt g =
361
  begin
362
    Format.fprintf fmt "{ /* graph */@.";
363
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
364
    Format.fprintf fmt "}@."
365
  end
366

    
367
let pp_error fmt trace =
368
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
369
    (fprintf_list ~sep:"->" pp_print_string) trace
370

    
371
(* Merges elements of graph [g2] into graph [g1] *)
372
  let merge_with g1 g2 =
373
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
374
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
375

    
376
let global_dependency node =
377
  let mems = ExprDep.node_memory_variables node in
378
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems node in
379
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
380
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
381
  CycleDetection.check_cycles g_non_mems;
382
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
383
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
384
  merge_with g_non_mems g_mems';
385
  { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
386
  g_non_mems
387

    
388

    
389
(* Local Variables: *)
390
(* compile-command:"make -C .." *)
391
(* End: *)