Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / causality.ml @ 1b01da98

History | View | Annotate | Download (16 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 -> 
110
      let lhs' = (transpose_list [lhs]) in
111
      if List.length tl <> List.length lhs' then
112
	assert false;
113
      List.fold_right2 match_mem lhs' tl mems
114
    | _             -> mems in
115
  match_mem eq.eq_lhs eq.eq_rhs mems
116

    
117
let node_memory_variables nd =
118
 List.fold_left eq_memory_variables ISet.empty nd.node_eqs
119

    
120
let node_non_input_variables nd =
121
  let outputs = List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs in
122
  List.fold_left (fun non_inputs v -> ISet.add v.var_id non_inputs) outputs nd.node_locals
123

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

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

    
143

    
144
(* Add dependencies from lhs to rhs in [g, g'], *)
145
(* no-mem/no-mem and mem/no-mem in g            *)
146
(* mem/mem in g'                                *)
147
(* excluding all/[inputs]                       *)
148
let add_eq_dependencies mems non_inputs eq (g, g') =
149
  let add_var lhs_is_mem lhs x (g, g') =
150
    if is_instance_var x || ISet.mem x non_inputs then
151
      match (lhs_is_mem, ISet.mem x mems) with
152
      | (false, true ) -> (add_edges [x] lhs g, g'                  )
153
      | (false, false) -> (add_edges lhs [x] g, g'                  )
154
      | (true , false) -> (add_edges lhs [x] g, g'                  )
155
      | (true , true ) -> (g                  , add_edges [x] lhs g')
156
    else (g, g') in
157
(* Add dependencies from [lhs] to rhs clock [ck]. *)
158
  let rec add_clock lhs_is_mem lhs ck g =
159
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
160
    match (Clocks.repr ck).Clocks.cdesc with
161
    | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
162
    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
163
    | _                         -> g 
164
  in
165
  
166

    
167
  let rec add_dep lhs_is_mem lhs rhs g =
168
    
169
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
170
    (* i.e every input is connected to every output, through a ghost var *)
171
    let mashup_appl_dependencies f e g =
172
      let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in
173
      List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)
174
	(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) 
175
    in
176
    match rhs.expr_desc with
177
    | Expr_const _    -> g
178
    | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
179
    | Expr_pre e      -> add_dep true lhs e g
180
    | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
181
    | Expr_access (e1, _)
182
    | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
183
    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
184
    | Expr_tuple t ->       
185
      if List.length t <> List.length lhs then ( 
186
	match lhs with
187
	| [l] -> List.fold_right (fun r -> add_dep lhs_is_mem [l] r) t g
188
	| _ -> 
189
	  Format.eprintf "Incompatible tuple assign: %a (%i) vs %a (%i)@.@?" 
190
	    (Utils.fprintf_list ~sep:"," (Format.pp_print_string)) lhs 
191
	    (List.length lhs)
192
	    Printers.pp_expr rhs
193
	    (List.length t)
194
	  ;
195
	  assert false
196
      ) 
197
      else
198
	List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
199
    | 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)
200
    | 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))
201
    | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
202
    | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
203
    | Expr_appl (f, e, None) ->
204
      if Basic_library.is_internal_fun f
205
      (* tuple component-wise dependency for internal operators *)
206
      then
207
	List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
208
      (* mashed up dependency for user-defined operators *)
209
      else
210
	mashup_appl_dependencies f e g
211
    | Expr_appl (f, e, Some (r, _)) ->
212
      mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
213
    | Expr_uclock  (e, _)
214
    | Expr_dclock  (e, _)
215
    | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g 
216
  in
217
  add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g')
218
  
219

    
220
(* Returns the dependence graph for node [n] *)
221
let dependence_graph mems non_inputs n =
222
  eq_var_cpt := 0;
223
  instance_var_cpt := 0;
224
  let g = new_graph (), new_graph () in
225
  (* Basic dependencies *)
226
  let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in
227
  g
228

    
229
end
230

    
231
module NodeDep = struct
232

    
233
  module ExprModule =
234
  struct
235
    type t = expr
236
    let compare = compare
237
    let hash n = Hashtbl.hash n
238
    let equal n1 n2 = n1 = n2
239
  end
240

    
241
  module ESet = Set.Make(ExprModule)
242

    
243
  let rec get_expr_calls prednode expr = 
244
    match expr.expr_desc with
245
      | Expr_const _ 
246
      | Expr_ident _ -> ESet.empty
247
      | Expr_access (e, _)
248
      | Expr_power (e, _) -> get_expr_calls prednode e
249
      | Expr_array t
250
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
251
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
252
      | Expr_fby (e1,e2)
253
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
254
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
255
      | Expr_pre e 
256
      | Expr_when (e,_,_)
257
      | Expr_uclock (e,_) 
258
      | Expr_dclock (e,_) 
259
      | Expr_phclock (e,_) -> get_expr_calls prednode e
260
      | Expr_appl (id,e, _) ->
261
	if not (Basic_library.is_internal_fun id) && prednode id
262
	then ESet.add expr (get_expr_calls prednode e)
263
	else (get_expr_calls prednode e)
264

    
265
  let get_callee expr =
266
    match expr.expr_desc with
267
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
268
    | _ -> None
269

    
270
  let get_calls prednode eqs =
271
    let deps =
272
      List.fold_left 
273
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
274
	ESet.empty
275
	eqs in
276
    ESet.elements deps
277

    
278
  let dependence_graph prog =
279
  let g = new_graph () in
280
  let g = List.fold_right 
281
    (fun td accu -> (* for each node we add its dependencies *)
282
      match td.top_decl_desc with 
283
	| Node nd ->
284
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
285
	  let accu = add_vertices [nd.node_id] accu in
286
	  let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) nd.node_eqs) in
287
	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
288
	  add_edges [nd.node_id] deps accu
289
	| _ -> assert false (* should not happen *)
290
      
291
    ) prog g in
292
  g   
293

    
294
  let rec filter_static_inputs inputs args =
295
   match inputs, args with
296
   | []   , [] -> []
297
   | 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
298
   | _ -> assert false
299

    
300
  let compute_generic_calls prog =
301
    List.iter
302
      (fun td ->
303
	match td.top_decl_desc with 
304
	| Node nd ->
305
	  let prednode n = is_generic_node (Hashtbl.find node_table n) in
306
	  nd.node_gencalls <- get_calls prednode nd.node_eqs
307
	| _ -> ()
308
      
309
      ) prog
310

    
311
end
312

    
313
module CycleDetection = struct
314

    
315
(* ---- Look for cycles in a dependency graph *)
316
  module Cycles = Graph.Components.Make (IdentDepGraph)
317

    
318
  let mk_copy_var n id =
319
    mk_new_name (node_vars n) id
320

    
321
  let mk_copy_eq n var =
322
    let var_decl = node_var var n in
323
    let cp_var = mk_copy_var n var in
324
    let expr =
325
      { expr_tag = Utils.new_tag ();
326
	expr_desc = Expr_ident var;
327
	expr_type = var_decl.var_type;
328
	expr_clock = var_decl.var_clock;
329
	expr_delay = Delay.new_var ();
330
	expr_annot = None;
331
	expr_loc = var_decl.var_loc } in
332
    { var_decl with var_id = cp_var },
333
    mkeq var_decl.var_loc ([cp_var], expr)
334

    
335
  let wrong_partition g partition =
336
    match partition with
337
    | [id]    -> IdentDepGraph.mem_edge g id id
338
    | _::_::_ -> true
339
    | []      -> assert false
340

    
341
(* Checks that the dependency graph [g] does not contain a cycle. Raises
342
   [Cycle partition] if the succession of dependencies [partition] forms a cycle *)
343
  let check_cycles g =
344
    let scc_l = Cycles.scc_list g in
345
    List.iter (fun partition ->
346
      if wrong_partition g partition then
347
	raise (Cycle partition)
348
      else ()
349
    ) scc_l
350

    
351
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *)
352
  let copy_partition g partition =
353
    let copy_g = IdentDepGraph.create () in
354
    IdentDepGraph.iter_edges
355
      (fun src tgt ->
356
	if List.mem src partition && List.mem tgt partition
357
	then IdentDepGraph.add_edge copy_g src tgt)
358
      g
359

    
360
 
361
(* Breaks dependency cycles in a graph [g] by inserting aux variables.
362
  [head] is a head of a non-trivial scc of [g]. 
363
   In Lustre, this is legal only for mem/mem cycles *)
364
  let break_cycle head cp_head g =
365
    let succs = IdentDepGraph.succ g head in
366
    IdentDepGraph.add_edge g head cp_head;
367
    List.iter
368
      (fun s ->
369
	IdentDepGraph.remove_edge g head s;
370
	IdentDepGraph.add_edge    g s cp_head)
371
      succs
372

    
373
(* Breaks cycles of the dependency graph [g] of memory variables [mems]
374
   belonging in node [node]. Returns:
375
   - a list of new auxiliary variable declarations
376
   - a list of new equations
377
   - a modified acyclic version of [g]
378
*)
379
  let break_cycles node mems g =
380
    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
381
    let rec break vdecls mem_eqs g =
382
      let scc_l = Cycles.scc_list g in
383
      let wrong = List.filter (wrong_partition g) scc_l in
384
      match wrong with
385
      | []              -> (vdecls, non_mem_eqs@mem_eqs, g)
386
      | [head]::_       ->
387
	begin
388
	  IdentDepGraph.remove_edge g head head;
389
	  break vdecls mem_eqs g
390
	end
391
      | (head::part)::_ -> 
392
	begin
393
	  let vdecl_cp_head, cp_eq = mk_copy_eq node head in
394
	  let pvar v = List.mem v part in
395
	  let fvar v = if v = head then vdecl_cp_head.var_id else v in
396
	  let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in
397
	  break_cycle head vdecl_cp_head.var_id g;
398
	  break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g
399
	end
400
      | _               -> assert false
401
    in break [] mem_eqs g
402

    
403
end
404

    
405
(* Module used to compute static disjunction of variables based upon their clocks. *)
406
module Disjunction =
407
struct
408
  (* map: var |-> list of disjoint vars, sorted in increasing branch length,
409
     maybe removing shorter branches *)
410
  type clock_map = (ident, ident list) Hashtbl.t
411

    
412
  let rec add_vdecl map vdecls =
413
    match vdecls with
414
    | []         -> ()
415
    | vdecl :: q -> begin
416
		      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);
417
                      add_vdecl map q
418
		    end
419

    
420
  let clock_disjoint_map vdecls =
421
    let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock in
422
    let map = Hashtbl.create 23 in
423
    begin
424
      add_vdecl map (List.sort (fun v1 v2 -> compare (root_branch v1) (root_branch v2)) vdecls);
425
      map
426
    end
427

    
428
  let pp_disjoint_map fmt map =
429
    begin
430
      Format.fprintf fmt "{ /* disjoint map */@.";
431
      Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Format.pp_print_string) v) map;
432
      Format.fprintf fmt "}@."
433
    end
434
end
435

    
436
let pp_dep_graph fmt g =
437
  begin
438
    Format.fprintf fmt "{ /* graph */@.";
439
    IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g;
440
    Format.fprintf fmt "}@."
441
  end
442

    
443
let pp_error fmt trace =
444
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
445
    (fprintf_list ~sep:"->" pp_print_string) trace
446

    
447
(* Merges elements of graph [g2] into graph [g1] *)
448
let merge_with g1 g2 =
449
    IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2;
450
    IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
451

    
452
let global_dependency node =
453
  let mems = ExprDep.node_memory_variables node in
454
  let non_inputs = ExprDep.node_non_input_variables node in
455
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in
456
  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;
457
  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)
458
  CycleDetection.check_cycles g_non_mems;
459
  let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in
460
  (*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)
461
  merge_with g_non_mems g_mems';
462
  { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
463
  g_non_mems
464

    
465

    
466
(* Local Variables: *)
467
(* compile-command:"make -C .." *)
468
(* End: *)