lustrec / src / causality.ml @ e8c0f452
History  View  Annotate  Download (13.7 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 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 nomem 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 (nonmem/nonmem&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 
(* nomem/nomem and mem/nomem 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 userdefined 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 componentwise 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 userdefined 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 subgraph 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 nontrivial 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 
(* compilecommand:"make C .." *) 
401 
(* End: *) 