Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ e8c0f452

History | View | Annotate | Download (13.7 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
(* Tests whether [v] is a root of graph [g], i.e. a source *)
59
let is_graph_root v g =
60
 IdentDepGraph.in_degree g v = 0
61

    
62
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)
63
let graph_roots g =
64
 IdentDepGraph.fold_vertex
65
   (fun v roots -> if is_graph_root v g then v::roots else roots)
66
   g []
67

    
68
let add_edges src tgt g =
69
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)
70
 List.iter
71
   (fun s ->
72
     List.iter
73
       (fun t -> IdentDepGraph.add_edge g s t)
74
       tgt)
75
   src;
76
  g
77

    
78
let add_vertices vtc g =
79
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*)
80
 List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc;
81
  g
82

    
83
let new_graph () =
84
 IdentDepGraph.create ()
85

    
86
module ExprDep = struct
87

    
88
let eq_var_cpt = ref 0
89

    
90
let instance_var_cpt = ref 0
91

    
92
let mk_eq_var id =
93
 incr eq_var_cpt; sprintf "#%s_%d" id !eq_var_cpt
94

    
95
let mk_instance_var id =
96
 incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt
97

    
98
let is_eq_var v = v.[0] = '#'
99

    
100
let is_instance_var v = v.[0] = '!'
101

    
102
let is_ghost_var v = is_instance_var v || is_eq_var v
103

    
104
let eq_memory_variables mems eq =
105
  let rec match_mem lhs rhs mems =
106
    match rhs.expr_desc with
107
    | Expr_fby _
108
    | Expr_pre _    -> List.fold_right ISet.add lhs mems
109
    | Expr_tuple tl -> List.fold_right2 match_mem (transpose_list [lhs]) tl mems
110
    | _             -> mems in
111
  match_mem eq.eq_lhs eq.eq_rhs mems
112

    
113
let node_memory_variables nd =
114
 List.fold_left eq_memory_variables ISet.empty nd.node_eqs
115

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

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

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

    
184
(* Returns the dependence graph for node [n] *)
185
let dependence_graph mems n =
186
  eq_var_cpt := 0;
187
  instance_var_cpt := 0;
188
  let g = new_graph (), new_graph () in
189
  let inputs = List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty n.node_inputs in
190
  (* Basic dependencies *)
191
  let g = List.fold_right (add_eq_dependencies mems inputs) n.node_eqs g in
192
  g
193

    
194
end
195

    
196
module NodeDep = struct
197

    
198
  module ExprModule =
199
  struct
200
    type t = expr
201
    let compare = compare
202
    let hash n = Hashtbl.hash n
203
    let equal n1 n2 = n1 = n2
204
  end
205

    
206
  module ESet = Set.Make(ExprModule)
207

    
208
  let rec get_expr_calls prednode expr = 
209
    match expr.expr_desc with
210
      | Expr_const _ 
211
      | Expr_ident _ -> ESet.empty
212
      | Expr_access (e, _)
213
      | Expr_power (e, _) -> get_expr_calls prednode e
214
      | Expr_array t
215
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
216
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
217
      | Expr_fby (e1,e2)
218
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
219
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
220
      | Expr_pre e 
221
      | Expr_when (e,_,_)
222
      | Expr_uclock (e,_) 
223
      | Expr_dclock (e,_) 
224
      | Expr_phclock (e,_) -> get_expr_calls prednode e
225
      | Expr_appl (id,e, _) ->
226
	if not (Basic_library.is_internal_fun id) && prednode id
227
	then ESet.add expr (get_expr_calls prednode e)
228
	else (get_expr_calls prednode e)
229

    
230
  let get_callee expr =
231
    match expr.expr_desc with
232
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
233
    | _ -> None
234

    
235
  let get_calls prednode eqs =
236
    let deps =
237
      List.fold_left 
238
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
239
	ESet.empty
240
	eqs in
241
    ESet.elements deps
242

    
243
  let dependence_graph prog =
244
  let g = new_graph () in
245
  let g = List.fold_right 
246
    (fun td accu -> (* for each node we add its dependencies *)
247
      match td.top_decl_desc with 
248
	| Node nd ->
249
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
250
	  let accu = add_vertices [nd.node_id] accu in
251
	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) nd.node_eqs) in
252
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
253
	  add_edges [nd.node_id] deps accu
254
	| _ -> assert false (* should not happen *)
255
      
256
    ) prog g in
257
  g   
258

    
259
  let rec filter_static_inputs inputs args =
260
   match inputs, args with
261
   | []   , [] -> []
262
   | 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
263
   | _ -> assert false
264

    
265
  let compute_generic_calls prog =
266
    List.iter
267
      (fun td ->
268
	match td.top_decl_desc with 
269
	| Node nd ->
270
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
271
	  nd.node_gencalls <- get_calls prednode nd.node_eqs
272
	| _ -> ()
273
      
274
      ) prog
275

    
276
end
277

    
278
module CycleDetection = struct
279

    
280
(* ---- Look for cycles in a dependency graph *)
281
  module Cycles = Graph.Components.Make (IdentDepGraph)
282

    
283
  let mk_copy_var n id =
284
    mk_new_name (node_vars n) id
285

    
286
  let mk_copy_eq n var =
287
    let var_decl = node_var var n in
288
    let cp_var = mk_copy_var n var in
289
    let expr =
290
      { expr_tag = Utils.new_tag ();
291
	expr_desc = Expr_ident var;
292
	expr_type = var_decl.var_type;
293
	expr_clock = var_decl.var_clock;
294
	expr_delay = Delay.new_var ();
295
	expr_annot = None;
296
	expr_loc = var_decl.var_loc } in
297
    { var_decl with var_id = cp_var },
298
    mkeq var_decl.var_loc ([cp_var], expr)
299

    
300
  let wrong_partition g partition =
301
    match partition with
302
    | [id]    -> IdentDepGraph.mem_edge g id id
303
    | _::_::_ -> true
304
    | []      -> assert false
305

    
306
(* Checks that the dependency graph [g] does not contain a cycle. Raises
307
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
308
  let check_cycles g =
309
    let scc_l = Cycles.scc_list g in
310
    List.iter (fun partition ->
311
      if wrong_partition g partition then
312
	raise (Cycle partition)
313
      else ()
314
    ) scc_l
315

    
316
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
317
  let copy_partition g partition =
318
    let copy_g = IdentDepGraph.create () in
319
    IdentDepGraph.iter_edges
320
      (fun src tgt ->
321
	if List.mem src partition && List.mem tgt partition
322
	then IdentDepGraph.add_edge copy_g src tgt)
323
      g
324

    
325
 
326
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
327
  [head] is a head of a non-trivial scc of [g]. 
328
   In Lustre, this is legal only for mem/mem cycles *)
329
  let break_cycle head cp_head g =
330
    let succs = IdentDepGraph.succ g head in
331
    IdentDepGraph.add_edge g head cp_head;
332
    List.iter
333
      (fun s ->
334
	IdentDepGraph.remove_edge g head s;
335
	IdentDepGraph.add_edge    g s cp_head)
336
      succs
337

    
338
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
339
   belonging in node [node]. Returns:
340
   - a list of new auxiliary variable declarations
341
   - a list of new equations
342
   - a modified acyclic version of [g]
343
*)
344
  let break_cycles node mems g =
345
    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
346
    let rec break vdecls mem_eqs g =
347
      let scc_l = Cycles.scc_list g in
348
      let wrong = List.filter (wrong_partition g) scc_l in
349
      match wrong with
350
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
351
      | [head]::_       ->
352
	begin
353
	  IdentDepGraph.remove_edge g head head;
354
	  break vdecls mem_eqs g
355
	end
356
      | (head::part)::_ -> 
357
	begin
358
	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in
359
	  let pvar v = List.mem v part in
360
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
361
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
362
	  break_cycle head vdecl_cp_head.var_id g;
363
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
364
	end
365
      | _               -> assert false
366
    in break [] mem_eqs g
367

    
368
end
369

    
370
let pp_dep_graph fmt g =
371
  begin
372
    Format.fprintf fmt "{ /* graph */@.";
373
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
374
    Format.fprintf fmt "}@."
375
  end
376

    
377
let pp_error fmt trace =
378
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
379
    (fprintf_list ~sep:"->" pp_print_string) trace
380

    
381
(* Merges elements of graph [g2] into graph [g1] *)
382
  let merge_with g1 g2 =
383
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
384
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
385

    
386
let global_dependency node =
387
  let mems = ExprDep.node_memory_variables node in
388
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems node in
389
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
390
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
391
  CycleDetection.check_cycles g_non_mems;
392
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
393
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
394
  merge_with g_non_mems g_mems';
395
  { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
396
  g_non_mems
397

    
398

    
399
(* Local Variables: *)
400
(* compile-command:"make -C .." *)
401
(* End: *)