lustrec / src / causality.ml @ 2196a0a6
History  View  Annotate  Download (15.4 KB)
1 
(*  

2 
* SchedMCore  A MultiCore Scheduling Framework 
3 
* Copyright (C) 20092011, 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 021111307 
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 nomem 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 (nonmem/nonmem&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 
(* nomem/nomem and mem/nomem 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 userdefined 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 componentwise 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 userdefined 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 
(* nomem/nomem and mem/nomem 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 subgraph 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 nontrivial 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 
(* compilecommand:"make C .." *) 
447 
(* End: *) 