Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ b1a97ade

History | View | Annotate | Download (15.5 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
let node_non_input_variables nd =
117
  let outputs = List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs in
118
  List.fold_left (fun non_inputs v -> ISet.add v.var_id non_inputs) outputs nd.node_locals
119

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

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

    
139

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

    
197
(* Returns the dependence graph for node [n] *)
198
let dependence_graph mems non_inputs n =
199
  eq_var_cpt := 0;
200
  instance_var_cpt := 0;
201
  let g = new_graph (), new_graph () in
202
  (* Basic dependencies *)
203
  let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in
204
  g
205

    
206
end
207

    
208
module NodeDep = struct
209

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

    
218
  module ESet = Set.Make(ExprModule)
219

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

    
242
  let get_callee expr =
243
    match expr.expr_desc with
244
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
245
    | _ -> None
246

    
247
  let get_calls prednode eqs =
248
    let deps =
249
      List.fold_left 
250
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
251
	ESet.empty
252
	eqs in
253
    ESet.elements deps
254

    
255
  let dependence_graph prog =
256
  let g = new_graph () in
257
  let g = List.fold_right 
258
    (fun td accu -> (* for each node we add its dependencies *)
259
      match td.top_decl_desc with 
260
	| Node nd ->
261
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
262
	  let accu = add_vertices [nd.node_id] accu in
263
	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) nd.node_eqs) in
264
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
265
	  add_edges [nd.node_id] deps accu
266
	| _ -> assert false (* should not happen *)
267
      
268
    ) prog g in
269
  g   
270

    
271
  let rec filter_static_inputs inputs args =
272
   match inputs, args with
273
   | []   , [] -> []
274
   | 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
275
   | _ -> assert false
276

    
277
  let compute_generic_calls prog =
278
    List.iter
279
      (fun td ->
280
	match td.top_decl_desc with 
281
	| Node nd ->
282
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
283
	  nd.node_gencalls <- get_calls prednode nd.node_eqs
284
	| _ -> ()
285
      
286
      ) prog
287

    
288
end
289

    
290
module CycleDetection = struct
291

    
292
(* ---- Look for cycles in a dependency graph *)
293
  module Cycles = Graph.Components.Make (IdentDepGraph)
294

    
295
  let mk_copy_var n id =
296
    mk_new_name (node_vars n) id
297

    
298
  let mk_copy_eq n var =
299
    let var_decl = node_var var n in
300
    let cp_var = mk_copy_var n var in
301
    let expr =
302
      { expr_tag = Utils.new_tag ();
303
	expr_desc = Expr_ident var;
304
	expr_type = var_decl.var_type;
305
	expr_clock = var_decl.var_clock;
306
	expr_delay = Delay.new_var ();
307
	expr_annot = None;
308
	expr_loc = var_decl.var_loc } in
309
    { var_decl with var_id = cp_var },
310
    mkeq var_decl.var_loc ([cp_var], expr)
311

    
312
  let wrong_partition g partition =
313
    match partition with
314
    | [id]    -> IdentDepGraph.mem_edge g id id
315
    | _::_::_ -> true
316
    | []      -> assert false
317

    
318
(* Checks that the dependency graph [g] does not contain a cycle. Raises
319
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
320
  let check_cycles g =
321
    let scc_l = Cycles.scc_list g in
322
    List.iter (fun partition ->
323
      if wrong_partition g partition then
324
	raise (Cycle partition)
325
      else ()
326
    ) scc_l
327

    
328
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
329
  let copy_partition g partition =
330
    let copy_g = IdentDepGraph.create () in
331
    IdentDepGraph.iter_edges
332
      (fun src tgt ->
333
	if List.mem src partition && List.mem tgt partition
334
	then IdentDepGraph.add_edge copy_g src tgt)
335
      g
336

    
337
 
338
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
339
  [head] is a head of a non-trivial scc of [g]. 
340
   In Lustre, this is legal only for mem/mem cycles *)
341
  let break_cycle head cp_head g =
342
    let succs = IdentDepGraph.succ g head in
343
    IdentDepGraph.add_edge g head cp_head;
344
    List.iter
345
      (fun s ->
346
	IdentDepGraph.remove_edge g head s;
347
	IdentDepGraph.add_edge    g s cp_head)
348
      succs
349

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

    
380
end
381

    
382
(* Module used to compute static disjunction of variables based upon their clocks. *)
383
module Disjunction =
384
struct
385
  (* map: var |-> list of disjoint vars, sorted in increasing branch length,
386
     maybe removing shorter branches *)
387
  type clock_map = (ident, ident list) Hashtbl.t
388

    
389
  let rec add_vdecl map vdecls =
390
    match vdecls with
391
    | []         -> ()
392
    | vdecl :: q -> begin
393
		      Hashtbl.add map vdecl.var_id (List.fold_left (fun r v -> if Clocks.disjoint v.var_clock vdecl.var_clock then v.var_id::r else r) [] q);
394
                      add_vdecl map q
395
		    end
396

    
397
  let clock_disjoint_map vdecls =
398
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock in
399
    let map = Hashtbl.create 23 in
400
    begin
401
      add_vdecl map (List.sort (fun v1 v2 -> compare (root_branch v1) (root_branch v2)) vdecls);
402
      map
403
    end
404

    
405
  let pp_disjoint_map fmt map =
406
    begin
407
      Format.fprintf fmt "{ /* disjoint map */@.";
408
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Format.pp_print_string) v) map;
409
      Format.fprintf fmt "}@."
410
    end
411
end
412

    
413
let pp_dep_graph fmt g =
414
  begin
415
    Format.fprintf fmt "{ /* graph */@.";
416
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
417
    Format.fprintf fmt "}@."
418
  end
419

    
420
let pp_error fmt trace =
421
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
422
    (fprintf_list ~sep:"->" pp_print_string) trace
423

    
424
(* Merges elements of graph [g2] into graph [g1] *)
425
let merge_with g1 g2 =
426
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
427
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
428

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

    
442

    
443
(* Local Variables: *)
444
(* compile-command:"make -C .." *)
445
(* End: *)