lustrec / src / causality.ml @ f4cba4b8
History | View | Annotate | Download (24.6 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(* This file was originally from the Prelude compiler *) |
11 |
(* *) |
12 |
(********************************************************************) |
13 |
|
14 |
|
15 |
(** Simple modular syntactic causality analysis. Can reject correct |
16 |
programs, especially if the program is not flattened first. *) |
17 |
open Utils |
18 |
open Lustre_types |
19 |
open Corelang |
20 |
open Graph |
21 |
|
22 |
|
23 |
type identified_call = eq * tag |
24 |
type error = |
25 |
| DataCycle of ident list list (* multiple failed partitions at once *) |
26 |
| NodeCycle of ident list |
27 |
|
28 |
exception Error of error |
29 |
|
30 |
|
31 |
|
32 |
(* Dependency of mem variables on mem variables is cut off |
33 |
by duplication of some mem vars into local node vars. |
34 |
Thus, cylic dependency errors may only arise between no-mem vars. |
35 |
non-mem variables are: |
36 |
- constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars |
37 |
- read mems (fake vars): same remark as above. |
38 |
- outputs: decoupled from mems, if necessary |
39 |
- locals |
40 |
- instance vars (fake vars): simplify causality analysis |
41 |
|
42 |
global constants are not part of the dependency graph. |
43 |
|
44 |
no_mem' = combinational(no_mem, mem); |
45 |
=> (mem -> no_mem' -> no_mem) |
46 |
|
47 |
mem' = pre(no_mem, mem); |
48 |
=> (mem' -> no_mem), (mem -> mem') |
49 |
|
50 |
Global roadmap: |
51 |
- compute two dep graphs g (non-mem/non-mem&mem) and g' (mem/mem) |
52 |
- check cycles in g (a cycle means a dependency error) |
53 |
- break cycles in g' (it's legal !): |
54 |
- check cycles in g' |
55 |
- if any, introduce aux var to break cycle, then start afresh |
56 |
- insert g' into g |
57 |
- return g |
58 |
*) |
59 |
|
60 |
(* Tests whether [v] is a root of graph [g], i.e. a source *) |
61 |
let is_graph_root v g = |
62 |
IdentDepGraph.in_degree g v = 0 |
63 |
|
64 |
(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *) |
65 |
let graph_roots g = |
66 |
IdentDepGraph.fold_vertex |
67 |
(fun v roots -> if is_graph_root v g then v::roots else roots) |
68 |
g [] |
69 |
|
70 |
let add_edges src tgt g = |
71 |
(*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*) |
72 |
List.iter |
73 |
(fun s -> |
74 |
List.iter |
75 |
(fun t -> IdentDepGraph.add_edge g s t) |
76 |
tgt) |
77 |
src; |
78 |
g |
79 |
|
80 |
let add_vertices vtc g = |
81 |
(*List.iter (fun t -> Format.eprintf "add %s@." t) vtc;*) |
82 |
List.iter (fun v -> IdentDepGraph.add_vertex g v) vtc; |
83 |
g |
84 |
|
85 |
let new_graph () = |
86 |
IdentDepGraph.create () |
87 |
|
88 |
(* keep subgraph of [gr] consisting of nodes accessible from node [v] *) |
89 |
let slice_graph gr v = |
90 |
begin |
91 |
let gr' = new_graph () in |
92 |
IdentDepGraph.add_vertex gr' v; |
93 |
Bfs.iter_component (fun v -> IdentDepGraph.iter_succ (fun s -> IdentDepGraph.add_vertex gr' s; IdentDepGraph.add_edge gr' v s) gr v) gr v; |
94 |
gr' |
95 |
end |
96 |
|
97 |
|
98 |
module ExprDep = struct |
99 |
let get_node_eqs nd = |
100 |
let eqs, auts = get_node_eqs nd in |
101 |
if auts != [] then assert false (* No call on causality on a Lustre model |
102 |
with automaton. They should be expanded by now. *); |
103 |
eqs |
104 |
|
105 |
let instance_var_cpt = ref 0 |
106 |
|
107 |
(* read vars represent input/mem read-only vars, |
108 |
they are not part of the program/schedule, |
109 |
as they are not assigned, |
110 |
but used to compute useless inputs/mems. |
111 |
a mem read var represents a mem at the beginning of a cycle *) |
112 |
let mk_read_var id = |
113 |
Format.sprintf "#%s" id |
114 |
|
115 |
(* instance vars represent node instance calls, |
116 |
they are not part of the program/schedule, |
117 |
but used to simplify causality analysis |
118 |
*) |
119 |
let mk_instance_var id = |
120 |
incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt |
121 |
|
122 |
let is_read_var v = v.[0] = '#' |
123 |
|
124 |
let is_instance_var v = v.[0] = '!' |
125 |
|
126 |
let is_ghost_var v = is_instance_var v || is_read_var v |
127 |
|
128 |
let undo_read_var id = |
129 |
assert (is_read_var id); |
130 |
String.sub id 1 (String.length id - 1) |
131 |
|
132 |
let undo_instance_var id = |
133 |
assert (is_instance_var id); |
134 |
String.sub id 1 (String.length id - 1) |
135 |
|
136 |
let eq_memory_variables mems eq = |
137 |
let rec match_mem lhs rhs mems = |
138 |
match rhs.expr_desc with |
139 |
| Expr_fby _ |
140 |
| Expr_pre _ -> List.fold_right ISet.add lhs mems |
141 |
| Expr_tuple tl -> |
142 |
let lhs' = (transpose_list [lhs]) in |
143 |
List.fold_right2 match_mem lhs' tl mems |
144 |
| _ -> mems in |
145 |
match_mem eq.eq_lhs eq.eq_rhs mems |
146 |
|
147 |
let node_memory_variables nd = |
148 |
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd) |
149 |
|
150 |
let node_input_variables nd = |
151 |
List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty |
152 |
(if nd.node_iscontract then |
153 |
nd.node_inputs@nd.node_outputs |
154 |
else |
155 |
nd.node_inputs) |
156 |
|
157 |
let node_output_variables nd = |
158 |
List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty |
159 |
(if nd.node_iscontract then [] else nd.node_outputs) |
160 |
|
161 |
let node_local_variables nd = |
162 |
List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals |
163 |
|
164 |
let node_constant_variables nd = |
165 |
List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals |
166 |
|
167 |
let node_auxiliary_variables nd = |
168 |
ISet.diff (node_local_variables nd) (node_memory_variables nd) |
169 |
|
170 |
let node_variables nd = |
171 |
let inputs = node_input_variables nd in |
172 |
let inoutputs = List.fold_left (fun inoutputs v -> ISet.add v.var_id inoutputs) inputs nd.node_outputs in |
173 |
List.fold_left (fun vars v -> ISet.add v.var_id vars) inoutputs nd.node_locals |
174 |
|
175 |
(* computes the equivalence relation relating variables |
176 |
in the same equation lhs, under the form of a table |
177 |
of class representatives *) |
178 |
let eqs_eq_equiv eqs = |
179 |
let eq_equiv = Hashtbl.create 23 in |
180 |
List.iter (fun eq -> |
181 |
let first = List.hd eq.eq_lhs in |
182 |
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs |
183 |
) |
184 |
eqs; |
185 |
eq_equiv |
186 |
|
187 |
let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd) |
188 |
|
189 |
(* Create a tuple of right dimension, according to [expr] type, *) |
190 |
(* filled with variable [v] *) |
191 |
let adjust_tuple v expr = |
192 |
match expr.expr_type.Types.tdesc with |
193 |
| Types.Ttuple tl -> duplicate v (List.length tl) |
194 |
| _ -> [v] |
195 |
|
196 |
|
197 |
(* Add dependencies from lhs to rhs in [g, g'], *) |
198 |
(* no-mem/no-mem and mem/no-mem in g *) |
199 |
(* mem/mem in g' *) |
200 |
(* match (lhs_is_mem, ISet.mem x mems) with |
201 |
| (false, true ) -> (add_edges [x] lhs g, |
202 |
g') |
203 |
| (false, false) -> (add_edges lhs [x] g, |
204 |
g') |
205 |
| (true , false) -> (add_edges lhs [x] g, |
206 |
g') |
207 |
| (true , true ) -> (g, |
208 |
add_edges [x] lhs g') |
209 |
*) |
210 |
let add_eq_dependencies mems inputs node_vars eq (g, g') = |
211 |
let add_var lhs_is_mem lhs x (g, g') = |
212 |
if is_instance_var x || ISet.mem x node_vars then |
213 |
if ISet.mem x mems |
214 |
then |
215 |
let g = add_edges lhs [mk_read_var x] g in |
216 |
if lhs_is_mem |
217 |
then |
218 |
(g, add_edges [x] lhs g') |
219 |
else |
220 |
(add_edges [x] lhs g, g') |
221 |
else |
222 |
let x = if ISet.mem x inputs then mk_read_var x else x in |
223 |
(add_edges lhs [x] g, g') |
224 |
else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) |
225 |
in |
226 |
(* Add dependencies from [lhs] to rhs clock [ck]. *) |
227 |
let rec add_clock lhs_is_mem lhs ck g = |
228 |
(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*) |
229 |
match (Clocks.repr ck).Clocks.cdesc with |
230 |
| Clocks.Con (ck', cr, _) -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g) |
231 |
| Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g |
232 |
| _ -> g |
233 |
in |
234 |
let rec add_dep lhs_is_mem lhs rhs g = |
235 |
(* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *) |
236 |
(* i.e every input is connected to every output, through a ghost var *) |
237 |
let mashup_appl_dependencies f e g = |
238 |
let f_var = mk_instance_var (Format.sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in |
239 |
List.fold_right (fun rhs -> add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs) |
240 |
(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g) |
241 |
in |
242 |
match rhs.expr_desc with |
243 |
| Expr_const _ -> g |
244 |
| Expr_fby (e1, e2) -> add_dep true lhs e2 (add_dep false lhs e1 g) |
245 |
| Expr_pre e -> add_dep true lhs e g |
246 |
| Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) |
247 |
| Expr_access (e1, d) |
248 |
| Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g) |
249 |
| Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g |
250 |
| Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g |
251 |
| 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) |
252 |
| 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)) |
253 |
| Expr_arrow (e1, e2) -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g) |
254 |
| Expr_when (e, c, _) -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g) |
255 |
| Expr_appl (f, e, None) -> |
256 |
if Basic_library.is_expr_internal_fun rhs |
257 |
(* tuple component-wise dependency for internal operators *) |
258 |
then |
259 |
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g |
260 |
(* mashed up dependency for user-defined operators *) |
261 |
else |
262 |
mashup_appl_dependencies f e g |
263 |
| Expr_appl (f, e, Some c) -> |
264 |
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g) |
265 |
in |
266 |
let g = |
267 |
List.fold_left |
268 |
(fun g lhs -> |
269 |
if ISet.mem lhs mems then |
270 |
add_vertices [lhs; mk_read_var lhs] g |
271 |
else |
272 |
add_vertices [lhs] g |
273 |
) |
274 |
g eq.eq_lhs |
275 |
in |
276 |
add_dep false eq.eq_lhs eq.eq_rhs (g, g') |
277 |
|
278 |
|
279 |
(* Returns the dependence graph for node [n] *) |
280 |
let dependence_graph mems inputs node_vars n = |
281 |
instance_var_cpt := 0; |
282 |
let g = new_graph (), new_graph () in |
283 |
(* Basic dependencies *) |
284 |
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in |
285 |
(* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il |
286 |
faut imposer que les outputs dépendent des asserts pour identifier que les |
287 |
fcn calls des asserts sont évalués avant le noeuds *) |
288 |
|
289 |
(* (\* In order to introduce dependencies between assert expressions and the node, *) |
290 |
(* we build an artificial dependency between node output and each assert *) |
291 |
(* expr. While these are not valid equations, they should properly propage in *) |
292 |
(* function add_eq_dependencies *\) *) |
293 |
(* let g = *) |
294 |
(* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *) |
295 |
(* List.fold_left (fun g ae -> *) |
296 |
(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *) |
297 |
(* add_eq_dependencies mems inputs node_vars fake_eq g *) |
298 |
(* ) g n.node_asserts in *) |
299 |
g |
300 |
|
301 |
end |
302 |
|
303 |
module NodeDep = struct |
304 |
|
305 |
module ExprModule = |
306 |
struct |
307 |
type t = expr |
308 |
let compare = compare |
309 |
let hash n = Hashtbl.hash n |
310 |
let equal n1 n2 = n1 = n2 |
311 |
end |
312 |
|
313 |
module ESet = Set.Make(ExprModule) |
314 |
|
315 |
let rec get_expr_calls prednode expr = |
316 |
match expr.expr_desc with |
317 |
| Expr_const _ |
318 |
| Expr_ident _ -> ESet.empty |
319 |
| Expr_access (e, _) |
320 |
| Expr_power (e, _) -> get_expr_calls prednode e |
321 |
| Expr_array t |
322 |
| Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty |
323 |
| Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty |
324 |
| Expr_fby (e1,e2) |
325 |
| Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) |
326 |
| Expr_ite (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) |
327 |
| Expr_pre e |
328 |
| Expr_when (e,_,_) -> get_expr_calls prednode e |
329 |
| Expr_appl (id,e, _) -> |
330 |
if not (Basic_library.is_expr_internal_fun expr) && prednode id |
331 |
then ESet.add expr (get_expr_calls prednode e) |
332 |
else (get_expr_calls prednode e) |
333 |
|
334 |
let get_callee expr = |
335 |
match expr.expr_desc with |
336 |
| Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args) |
337 |
| _ -> None |
338 |
|
339 |
let get_calls prednode nd = |
340 |
let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl in |
341 |
let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in |
342 |
let rec get_stmt_calls s = |
343 |
match s with Eq eq -> get_eq_calls eq | Aut aut -> get_aut_calls aut |
344 |
and get_aut_calls aut = |
345 |
let get_handler_calls h = |
346 |
let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in |
347 |
let until = get_cond_calls h.hand_until in |
348 |
let unless = get_cond_calls h.hand_unless in |
349 |
let calls = ESet.union until unless in |
350 |
let calls = accu get_stmt_calls calls h.hand_stmts in |
351 |
let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in |
352 |
(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *) |
353 |
calls |
354 |
in |
355 |
accu get_handler_calls ESet.empty aut.aut_handlers |
356 |
in |
357 |
let eqs, auts = get_node_eqs nd in |
358 |
let deps = accu get_eq_calls ESet.empty eqs in |
359 |
let deps = accu get_aut_calls deps auts in |
360 |
ESet.elements deps |
361 |
|
362 |
let dependence_graph prog = |
363 |
let g = new_graph () in |
364 |
let g = List.fold_right |
365 |
(fun td accu -> (* for each node we add its dependencies *) |
366 |
match td.top_decl_desc with |
367 |
| Node nd -> |
368 |
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) |
369 |
let accu = add_vertices [nd.node_id] accu in |
370 |
let deps = List.map |
371 |
(fun e -> fst (desome (get_callee e))) |
372 |
(get_calls (fun _ -> true) nd) |
373 |
in |
374 |
(* Adding assert expressions deps *) |
375 |
let deps_asserts = |
376 |
let prednode = (fun _ -> true) in (* what is this about? *) |
377 |
List.map |
378 |
(fun e -> fst (desome (get_callee e))) |
379 |
(ESet.elements |
380 |
(List.fold_left |
381 |
(fun accu assert_expr -> ESet.union accu (get_expr_calls prednode assert_expr)) |
382 |
ESet.empty |
383 |
(List.map (fun _assert -> _assert.assert_expr) nd.node_asserts) |
384 |
) |
385 |
) |
386 |
in |
387 |
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) |
388 |
add_edges [nd.node_id] (deps@deps_asserts) accu |
389 |
| _ -> assert false (* should not happen *) |
390 |
|
391 |
) prog g in |
392 |
g |
393 |
|
394 |
let rec filter_static_inputs inputs args = |
395 |
match inputs, args with |
396 |
| [] , [] -> [] |
397 |
| v::vq, a::aq -> if v.var_dec_const && Types.is_dimension_type v.var_type then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq |
398 |
| _ -> assert false |
399 |
|
400 |
let compute_generic_calls prog = |
401 |
List.iter |
402 |
(fun td -> |
403 |
match td.top_decl_desc with |
404 |
| Node nd -> |
405 |
let prednode n = is_generic_node (node_from_name n) in |
406 |
nd.node_gencalls <- get_calls prednode nd |
407 |
| _ -> () |
408 |
|
409 |
) prog |
410 |
|
411 |
end |
412 |
|
413 |
|
414 |
module CycleDetection = struct |
415 |
|
416 |
(* ---- Look for cycles in a dependency graph *) |
417 |
module Cycles = Graph.Components.Make (IdentDepGraph) |
418 |
|
419 |
let mk_copy_var n id = |
420 |
let used name = |
421 |
(List.exists (fun v -> v.var_id = name) n.node_locals) |
422 |
|| (List.exists (fun v -> v.var_id = name) n.node_inputs) |
423 |
|| (List.exists (fun v -> v.var_id = name) n.node_outputs) |
424 |
in mk_new_name used id |
425 |
|
426 |
let mk_copy_eq n var = |
427 |
let var_decl = get_node_var var n in |
428 |
let cp_var = mk_copy_var n var in |
429 |
let expr = |
430 |
{ expr_tag = Utils.new_tag (); |
431 |
expr_desc = Expr_ident var; |
432 |
expr_type = var_decl.var_type; |
433 |
expr_clock = var_decl.var_clock; |
434 |
expr_delay = Delay.new_var (); |
435 |
expr_annot = None; |
436 |
expr_loc = var_decl.var_loc } in |
437 |
{ var_decl with var_id = cp_var; var_orig = false }, |
438 |
mkeq var_decl.var_loc ([cp_var], expr) |
439 |
|
440 |
let wrong_partition g partition = |
441 |
match partition with |
442 |
| [id] -> IdentDepGraph.mem_edge g id id |
443 |
| _::_::_ -> true |
444 |
| [] -> assert false |
445 |
|
446 |
(* Checks that the dependency graph [g] does not contain a cycle. Raises |
447 |
[Cycle partition] if the succession of dependencies [partition] forms a cycle *) |
448 |
let check_cycles g = |
449 |
let scc_l = Cycles.scc_list g in |
450 |
let algebraic_loops = List.filter (wrong_partition g) scc_l in |
451 |
if List.length algebraic_loops > 0 then |
452 |
raise (Error (DataCycle algebraic_loops)) |
453 |
(* We extract a hint to resolve the cycle: for each variable in the cycle |
454 |
which is defined by a call, we return the name of the node call and |
455 |
its specific id *) |
456 |
|
457 |
(* Creates the sub-graph of [g] restricted to vertices and edges in partition *) |
458 |
let copy_partition g partition = |
459 |
let copy_g = IdentDepGraph.create () in |
460 |
IdentDepGraph.iter_edges |
461 |
(fun src tgt -> |
462 |
if List.mem src partition && List.mem tgt partition |
463 |
then IdentDepGraph.add_edge copy_g src tgt) |
464 |
g |
465 |
|
466 |
|
467 |
(* Breaks dependency cycles in a graph [g] by inserting aux variables. |
468 |
[head] is a head of a non-trivial scc of [g]. |
469 |
In Lustre, this is legal only for mem/mem cycles *) |
470 |
let break_cycle head cp_head g = |
471 |
let succs = IdentDepGraph.succ g head in |
472 |
IdentDepGraph.add_edge g head cp_head; |
473 |
IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head); |
474 |
List.iter |
475 |
(fun s -> |
476 |
IdentDepGraph.remove_edge g head s; |
477 |
IdentDepGraph.add_edge g s cp_head) |
478 |
succs |
479 |
|
480 |
(* Breaks cycles of the dependency graph [g] of memory variables [mems] |
481 |
belonging in node [node]. Returns: |
482 |
- a list of new auxiliary variable declarations |
483 |
- a list of new equations |
484 |
- a modified acyclic version of [g] |
485 |
*) |
486 |
let break_cycles node mems g = |
487 |
let eqs , auts = get_node_eqs node in |
488 |
assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *) |
489 |
let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in |
490 |
let rec break vdecls mem_eqs g = |
491 |
let scc_l = Cycles.scc_list g in |
492 |
let wrong = List.filter (wrong_partition g) scc_l in |
493 |
match wrong with |
494 |
| [] -> (vdecls, non_mem_eqs@mem_eqs, g) |
495 |
| [head]::_ -> |
496 |
begin |
497 |
IdentDepGraph.remove_edge g head head; |
498 |
break vdecls mem_eqs g |
499 |
end |
500 |
| (head::part)::_ -> |
501 |
begin |
502 |
let vdecl_cp_head, cp_eq = mk_copy_eq node head in |
503 |
let pvar v = List.mem v part in |
504 |
let fvar v = if v = head then vdecl_cp_head.var_id else v in |
505 |
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in |
506 |
break_cycle head vdecl_cp_head.var_id g; |
507 |
break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g |
508 |
end |
509 |
| _ -> assert false |
510 |
in break [] mem_eqs g |
511 |
|
512 |
end |
513 |
|
514 |
(* Module used to compute static disjunction of variables based upon their clocks. *) |
515 |
module Disjunction = |
516 |
struct |
517 |
module ClockedIdentModule = |
518 |
struct |
519 |
type t = var_decl |
520 |
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock |
521 |
let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id) |
522 |
end |
523 |
|
524 |
module CISet = Set.Make(ClockedIdentModule) |
525 |
|
526 |
(* map: var |-> list of disjoint vars, sorted in increasing branch length order, |
527 |
maybe removing shorter branches *) |
528 |
type disjoint_map = (ident, CISet.t) Hashtbl.t |
529 |
|
530 |
let pp_ciset fmt t = |
531 |
begin |
532 |
Format.fprintf fmt "{@ "; |
533 |
CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t; |
534 |
Format.fprintf fmt "}@." |
535 |
end |
536 |
|
537 |
let clock_disjoint_map vdecls = |
538 |
let map = Hashtbl.create 23 in |
539 |
begin |
540 |
List.iter |
541 |
(fun v1 -> let disj_v1 = |
542 |
List.fold_left |
543 |
(fun res v2 -> if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res) |
544 |
CISet.empty |
545 |
vdecls in |
546 |
(* disjoint vdecls are stored in increasing branch length order *) |
547 |
Hashtbl.add map v1.var_id disj_v1) |
548 |
vdecls; |
549 |
(map : disjoint_map) |
550 |
end |
551 |
|
552 |
(* merge variables [v] and [v'] in disjunction [map]. Then: |
553 |
- the mapping v' becomes v' |-> (map v) inter (map v') |
554 |
- the mapping v |-> ... then disappears |
555 |
- other mappings become x |-> (map x) \ (if v in x then v else v') |
556 |
*) |
557 |
let merge_in_disjoint_map map v v' = |
558 |
begin |
559 |
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); |
560 |
Hashtbl.remove map v.var_id; |
561 |
Hashtbl.iter (fun x map_x -> Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map; |
562 |
end |
563 |
|
564 |
(* replace variable [v] by [v'] in disjunction [map]. |
565 |
[v'] is a dead variable. Then: |
566 |
- the mapping v' becomes v' |-> (map v) |
567 |
- the mapping v |-> ... then disappears |
568 |
- all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x) |
569 |
*) |
570 |
let replace_in_disjoint_map map v v' = |
571 |
begin |
572 |
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); |
573 |
Hashtbl.remove map v.var_id; |
574 |
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx) else CISet.remove v' mapx)) map; |
575 |
end |
576 |
|
577 |
(* remove variable [v] in disjunction [map]. Then: |
578 |
- the mapping v |-> ... then disappears |
579 |
- all mappings become x |-> (map x) \ { v} |
580 |
*) |
581 |
let remove_in_disjoint_map map v = |
582 |
begin |
583 |
Hashtbl.remove map v.var_id; |
584 |
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map; |
585 |
end |
586 |
|
587 |
let pp_disjoint_map fmt map = |
588 |
begin |
589 |
Format.fprintf fmt "{ /* disjoint map */@."; |
590 |
Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; |
591 |
Format.fprintf fmt "}@." |
592 |
end |
593 |
end |
594 |
|
595 |
|
596 |
let pp_dep_graph fmt g = |
597 |
begin |
598 |
Format.fprintf fmt "{ /* graph */@."; |
599 |
IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g; |
600 |
Format.fprintf fmt "}@." |
601 |
end |
602 |
|
603 |
let pp_error fmt err = |
604 |
match err with |
605 |
| NodeCycle trace -> |
606 |
Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ " |
607 |
(fprintf_list ~sep:",@ " Format.pp_print_string) trace |
608 |
| DataCycle traces -> ( |
609 |
Format.fprintf fmt "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ " |
610 |
(fprintf_list ~sep:";@ " |
611 |
(fun fmt trace -> |
612 |
Format.fprintf fmt "@[<v 0>{%a}@]" |
613 |
(fprintf_list ~sep:",@ " Format.pp_print_string) |
614 |
trace |
615 |
)) traces |
616 |
) |
617 |
|
618 |
(* Merges elements of graph [g2] into graph [g1] *) |
619 |
let merge_with g1 g2 = |
620 |
begin |
621 |
IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2; |
622 |
IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2 |
623 |
end |
624 |
|
625 |
let world = "!!_world" |
626 |
|
627 |
let add_external_dependency outputs mems g = |
628 |
begin |
629 |
IdentDepGraph.add_vertex g world; |
630 |
ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs; |
631 |
ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems; |
632 |
end |
633 |
|
634 |
(* Takes a node and return a pair (node', graph) where node' is node |
635 |
rebuilt with the equations enriched with new ones introduced to |
636 |
"break cycles" *) |
637 |
let global_dependency node = |
638 |
let mems = ExprDep.node_memory_variables node in |
639 |
let inputs = |
640 |
ISet.union |
641 |
(ExprDep.node_input_variables node) |
642 |
(ExprDep.node_constant_variables node) in |
643 |
let outputs = ExprDep.node_output_variables node in |
644 |
let node_vars = ExprDep.node_variables node in |
645 |
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in |
646 |
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; |
647 |
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) |
648 |
try |
649 |
CycleDetection.check_cycles g_non_mems; |
650 |
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in |
651 |
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) |
652 |
begin |
653 |
merge_with g_non_mems g_mems'; |
654 |
add_external_dependency outputs mems g_non_mems; |
655 |
{ node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, |
656 |
g_non_mems |
657 |
end |
658 |
with Error (DataCycle _ as exc) -> ( |
659 |
raise (Error (exc)) |
660 |
) |
661 |
|
662 |
(* A module to sort dependencies among local variables when relying on clocked declarations *) |
663 |
module VarClockDep = |
664 |
struct |
665 |
let rec get_clock_dep ck = |
666 |
match ck.Clocks.cdesc with |
667 |
| Clocks.Con (ck ,c ,l) -> l::(get_clock_dep ck) |
668 |
| Clocks.Clink ck' |
669 |
| Clocks.Ccarrying (_, ck') -> get_clock_dep ck' |
670 |
| _ -> [] |
671 |
|
672 |
let sort locals = |
673 |
let g = new_graph () in |
674 |
let g = List.fold_left ( |
675 |
fun g var_decl -> |
676 |
let deps = get_clock_dep var_decl.var_clock in |
677 |
add_edges [var_decl.var_id] deps g |
678 |
) g locals |
679 |
in |
680 |
let sorted, no_deps = |
681 |
TopologicalDepGraph.fold (fun vid (accu, remaining) -> ( |
682 |
let select v = v.var_id = vid in |
683 |
let selected, not_selected = List.partition select remaining in |
684 |
selected@accu, not_selected |
685 |
)) g ([],locals) |
686 |
in |
687 |
no_deps @ sorted |
688 |
|
689 |
end |
690 |
|
691 |
(* Local Variables: *) |
692 |
(* compile-command:"make -C .." *) |
693 |
(* End: *) |