1
|
(* We try to solve all algebraic loops (AL) from prog:
|
2
|
each node is mapped to its own cycles
|
3
|
each cycle is tentatively solved by inlining one of its component
|
4
|
|
5
|
When done, a report is generated.
|
6
|
|
7
|
- for each initial AL, the cycle is presented
|
8
|
- either it is solvable and we provide the set of inlines that solves it
|
9
|
- or it is not and we write the AL as unsolvable by inlining
|
10
|
|
11
|
If the option solve_al is activated, the resulting partially inlined prog is
|
12
|
propagated fur future processing Otherwise the compilation stops
|
13
|
*)
|
14
|
open Lustre_types
|
15
|
open Corelang
|
16
|
open Utils
|
17
|
|
18
|
(* An single algebraic loop is defined (partition, node calls, inlined, status)
|
19
|
ie
|
20
|
|
21
|
1. the list of variables in the loop, ident list
|
22
|
|
23
|
2.the possible functions identifier to inline, and whether they have been
|
24
|
inlined yet (ident * tag * bool) list and
|
25
|
|
26
|
3. a status whether the inlining is enough bool
|
27
|
*)
|
28
|
|
29
|
type call = ident * expr * eq (* fun id, expression, and containing equation *)
|
30
|
|
31
|
type algebraic_loop = ident list * (call * bool) list * bool
|
32
|
type report = (node_desc * algebraic_loop list) list
|
33
|
exception Error of report
|
34
|
|
35
|
|
36
|
(* Module that extract from the DataCycle the set of node that could be inlined
|
37
|
to solve the problem. *)
|
38
|
module CycleResolution =
|
39
|
struct
|
40
|
|
41
|
(* We iter over calls in node defs. If the call defined on of the variable in
|
42
|
the cycle, we store it for future possible inline. *)
|
43
|
let resolve node partition : call list =
|
44
|
let partition = ISet.of_list partition in
|
45
|
(* Preprocessing calls: associate to each of them the eq.lhs associated *)
|
46
|
let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in
|
47
|
let eqs, auts = get_node_eqs node in
|
48
|
assert (auts = []); (* TODO voir si on peut acceder directement aux eqs qui font les calls *)
|
49
|
let calls = List.map (
|
50
|
fun expr ->
|
51
|
let eq = List.find (fun eq ->
|
52
|
Corelang.expr_contains_expr expr.expr_tag eq.eq_rhs
|
53
|
) eqs in
|
54
|
let fun_name = match expr.expr_desc with
|
55
|
| Expr_appl(fun_id, _, _) -> fun_id
|
56
|
| _ -> assert false
|
57
|
in
|
58
|
fun_name, expr, eq
|
59
|
) calls_expr in
|
60
|
List.fold_left (
|
61
|
fun accu ((_, _, eq) as call) ->
|
62
|
let shared_vars = ISet.inter (ISet.of_list eq.eq_lhs) partition in
|
63
|
if not (ISet.is_empty shared_vars) then
|
64
|
(* We have a match: keep the eq and the expr to inline *)
|
65
|
call::accu
|
66
|
else
|
67
|
accu
|
68
|
) [] calls
|
69
|
end
|
70
|
|
71
|
|
72
|
(* Format.fprintf fmt "@[<v 2>Possible resolution:@ %a@]" pp_resolution resolution*)
|
73
|
|
74
|
|
75
|
let pp_resolution fmt resolution =
|
76
|
fprintf_list ~sep:"@ " (fun fmt (eq, tag) ->
|
77
|
Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq
|
78
|
) fmt resolution
|
79
|
|
80
|
let al_is_solved (_, als) = List.for_all (fun (vars, calls, status) -> status) als
|
81
|
|
82
|
(**********************************************************************)
|
83
|
(* Functions to access or toggle the local inlining feature of a call *)
|
84
|
(* expression *)
|
85
|
(**********************************************************************)
|
86
|
|
87
|
let inline_annotation loc =
|
88
|
Inliner.keyword,
|
89
|
Corelang.mkeexpr loc
|
90
|
(Corelang.mkexpr loc
|
91
|
(Expr_const (Const_tag tag_true) ))
|
92
|
|
93
|
let is_inlining_annot (key, status) =
|
94
|
key = Inliner.keyword && (
|
95
|
match status.eexpr_qfexpr.expr_desc with
|
96
|
| Expr_const (Const_tag tag) when tag = tag_true ->
|
97
|
true
|
98
|
| Expr_const (Const_tag tag) when tag = tag_false ->
|
99
|
false
|
100
|
| _ -> assert false (* expecting true or false value *)
|
101
|
)
|
102
|
|
103
|
let is_expr_inlined nd expr =
|
104
|
match expr.expr_annot with
|
105
|
None -> false
|
106
|
| Some anns -> (
|
107
|
(* Sanity check: expr should have the annotation AND the annotation should be declared *)
|
108
|
let local_ann = List.exists is_inlining_annot anns.annots in
|
109
|
let all_expr_inlined = Hashtbl.find_all Annotations.expr_annotations Inliner.keyword in
|
110
|
let registered =
|
111
|
List.exists
|
112
|
(fun (nd_id, expr_tag) -> nd_id = nd.node_id && expr_tag = expr.expr_tag)
|
113
|
all_expr_inlined
|
114
|
in
|
115
|
match local_ann, registered with
|
116
|
| true, true -> true (* Everythin' all righ' ! *)
|
117
|
| false, false -> false (* idem *)
|
118
|
| _ -> assert false
|
119
|
)
|
120
|
|
121
|
let pp_calls nd fmt calls = Format.fprintf fmt "@[<v 0>%a@]"
|
122
|
(fprintf_list ~sep:"@ " (fun fmt (funid,expr, _) -> Format.fprintf fmt "%s: %i (inlined:%b)"
|
123
|
funid
|
124
|
expr.expr_tag
|
125
|
(is_expr_inlined nd expr)
|
126
|
))
|
127
|
calls
|
128
|
|
129
|
(* Inline the provided expression *)
|
130
|
let inline_expr node expr =
|
131
|
(* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *)
|
132
|
let ann = inline_annotation expr.expr_loc in
|
133
|
let ann = {annots = [ann]; annot_loc = expr.expr_loc} in
|
134
|
let res = update_expr_annot node.node_id expr ann in
|
135
|
(* assert (is_expr_inlined node res); *)
|
136
|
(* Format.eprintf "Is expression inlined? %b@." (is_expr_inlined node res); *)
|
137
|
res
|
138
|
|
139
|
(* Perform the steps of stage1/stage2 to revalidate the schedulability of the program *)
|
140
|
let fast_stages_processing prog =
|
141
|
Log.report ~level:3
|
142
|
(fun fmt -> Format.fprintf fmt "@[<v 2>Fast revalidation: normalization + schedulability@ ");
|
143
|
Options.verbose_level := !Options.verbose_level - 2;
|
144
|
|
145
|
(* Mini stage 1 *)
|
146
|
(* Extracting dependencies *)
|
147
|
let dependencies, type_env, clock_env = Compiler_common.import_dependencies prog in
|
148
|
(* Local inlining *)
|
149
|
let prog = Inliner.local_inline prog (* type_env clock_env *) in
|
150
|
(* Checking stateless/stateful status *)
|
151
|
if Plugins.check_force_stateful () then
|
152
|
Compiler_common.force_stateful_decls prog
|
153
|
else
|
154
|
Compiler_common.check_stateless_decls prog;
|
155
|
(* Typing *)
|
156
|
let _ (*computed_types_env*) = Compiler_common.type_decls type_env prog in
|
157
|
(* Clock calculus *)
|
158
|
let _ (*computed_clocks_env*) = Compiler_common.clock_decls clock_env prog in
|
159
|
(* Normalization *)
|
160
|
let prog = Normalization.normalize_prog ~backend:!Options.output prog in
|
161
|
(* Mini stage 2 : Scheduling *)
|
162
|
let res = Scheduling.schedule_prog prog in
|
163
|
Options.verbose_level := !Options.verbose_level + 2;
|
164
|
|
165
|
Log.report ~level:3
|
166
|
(fun fmt -> Format.fprintf fmt "@]@ ");
|
167
|
res
|
168
|
|
169
|
(**********************)
|
170
|
(* Returns a modified node, if possible, and an algebraic_loop report *)
|
171
|
let rec solving_node max_inlines prog nd existing_al partitions =
|
172
|
(* let pp_calls = pp_calls nd in *)
|
173
|
(* For each partition, we identify the original one *)
|
174
|
let rerun, max_inlines, al = List.fold_left (fun (rerun, inlines, al) part ->
|
175
|
let part_vars = ISet.of_list part in
|
176
|
(* Useful functions to filter list of elements *)
|
177
|
let match_al (vars, calls, status) =
|
178
|
not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars)) in
|
179
|
(* Identifying previous alarms that could be associated to current conflict *)
|
180
|
let matched, non_matched = List.partition match_al existing_al in
|
181
|
let previous_calls =
|
182
|
match matched with
|
183
|
| [] -> []
|
184
|
| [_ (*vars*), calls, _ (*status*)] -> List.map fst calls (* we just keep the calls *)
|
185
|
| _ -> (* variable should not belong to two different algrebraic loops. At least I
|
186
|
hope so! *)
|
187
|
assert false
|
188
|
in
|
189
|
let match_previous (eq, expr, fun_id) =
|
190
|
List.exists
|
191
|
(fun (_, expr', _) -> expr'.expr_tag = expr.expr_tag)
|
192
|
previous_calls
|
193
|
in
|
194
|
(* let match_inlined (_, expr, _) = is_expr_inlined nd expr in *)
|
195
|
|
196
|
(* let previous_inlined, previous_no_inlined = List.partition match_inlined previous_calls in *)
|
197
|
(* Format.eprintf "Previous calls: @[<v 0>inlined: {%a}@ no inlined: {%a}@ @]@ " *)
|
198
|
(* pp_calls previous_inlined *)
|
199
|
(* pp_calls previous_no_inlined *)
|
200
|
|
201
|
(* ; *)
|
202
|
|
203
|
let current_calls = CycleResolution.resolve nd part in
|
204
|
(* Format.eprintf "Current calls: %a" pp_calls current_calls; *)
|
205
|
(* Filter out calls from current_calls that were not already in previous calls *)
|
206
|
let current_calls = List.filter (fun c -> not (match_previous c)) current_calls
|
207
|
in
|
208
|
(* Format.eprintf "Current new calls (no old ones): %a" pp_calls current_calls; *)
|
209
|
let calls = previous_calls @ current_calls in
|
210
|
(* Format.eprintf "All calls (previous + new): %a" pp_calls calls; *)
|
211
|
|
212
|
(* Filter out already inlined calls: actually they should not appear
|
213
|
... since they were inlined. We keep it for safety. *)
|
214
|
let _ (* already_inlined *), possible_resolution =
|
215
|
List.partition (fun (_, expr, _) -> is_expr_inlined nd expr) calls in
|
216
|
(* Inlining the first uninlined call *)
|
217
|
match possible_resolution with
|
218
|
| (fun_id, expr, eq)::_ -> ((* One could inline expr *)
|
219
|
Log.report ~level:2 (fun fmt-> Format.fprintf fmt "inlining call to %s@ " fun_id);
|
220
|
(* Forcing the expr to be inlined *)
|
221
|
let _ = inline_expr nd expr in
|
222
|
(* Format.eprintf "Making sure that the inline list evolved: inlined = {%a}" *)
|
223
|
(* pp_calls *)
|
224
|
(* ; *)
|
225
|
true, (* we have to rerun to see if the inlined expression solves the issue *)
|
226
|
max_inlines - 1,
|
227
|
(
|
228
|
part,
|
229
|
List.map (fun ((eq, expr2, fcn_name) as call)-> call, (expr2.expr_tag = expr.expr_tag)) calls,
|
230
|
true (* TODO was false. Should be put it true and expect a final
|
231
|
scheduling to change it to false in case of failure ? *) (*
|
232
|
Status is nok, LA is unsolved yet *)
|
233
|
|
234
|
)::non_matched
|
235
|
)
|
236
|
| [] -> (* No more calls to inline: algebraic loop is not solvable *)
|
237
|
rerun, (* we don't force rerun since the current node is not solvable *)
|
238
|
max_inlines,
|
239
|
(
|
240
|
part, (* initial list of troublesogme variables *)
|
241
|
List.map (fun ((eq, expr, fcn_name) as call) -> call, false) calls,
|
242
|
false (* Status is nok, LA is unsolved *)
|
243
|
)::non_matched
|
244
|
|
245
|
) (false, max_inlines, existing_al) partitions
|
246
|
in
|
247
|
(* if partition an already identified al ? *)
|
248
|
(* if ISet.of_list partition *)
|
249
|
if rerun && max_inlines > 0 then
|
250
|
(* At least one partition could be improved: we try to inline the calls and reschedule the node. *)
|
251
|
try
|
252
|
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "rescheduling node with new inlined call@ ");
|
253
|
let _ = fast_stages_processing prog in
|
254
|
(* If everything went up to here, the problem is solved! All associated
|
255
|
alarms are mapped to valid status. *)
|
256
|
let al = List.map (fun (v,c,_) -> v,c,true) al in
|
257
|
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "AL solved@ ");
|
258
|
Some(nd, al), max_inlines
|
259
|
with Causality.Error (Causality.DataCycle partitions2) -> (
|
260
|
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "AL not solved yet. Further processing.@ ");
|
261
|
solving_node max_inlines prog nd al partitions2
|
262
|
)
|
263
|
else ((* No rerun, we return the current node and computed alarms *)
|
264
|
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "AL not solved yet. Stopping.@ ");
|
265
|
Some(nd, al), max_inlines
|
266
|
)
|
267
|
|
268
|
(** This function takes a prog and returns (prog', status, alarms)
|
269
|
where prog' is a modified prog with some locally inlined calls
|
270
|
status is true is the final prog' is schedulable, ie no algebraic loop
|
271
|
In case of failure, ie. inlining does not solve the problem; the status is false.
|
272
|
Alarms contain the list of inlining performed or advised for each node.
|
273
|
This could be provided as a feedback to the user.
|
274
|
*)
|
275
|
let clean_al prog : program * bool * report =
|
276
|
let max_inlines = !Options.al_nb_max in
|
277
|
(* We iterate over each node *)
|
278
|
let _, prog, al_list =
|
279
|
List.fold_right (
|
280
|
fun top (max_inlines, prog_accu, al_list) ->
|
281
|
match top.top_decl_desc with
|
282
|
| Node nd -> (
|
283
|
let error, max_inlines =
|
284
|
try (* without exception the node is schedulable; nothing to declare *)
|
285
|
let _ = Scheduling.schedule_node nd in
|
286
|
None, max_inlines
|
287
|
with Causality.Error (Causality.DataCycle partitions) -> (
|
288
|
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@[<v 2>AL in node %s@ " nd.node_id);
|
289
|
let error, max_inlines = solving_node max_inlines prog nd [] partitions in
|
290
|
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@ @]");
|
291
|
error, max_inlines
|
292
|
)
|
293
|
in
|
294
|
match error with
|
295
|
| None -> max_inlines, top::prog_accu, al_list (* keep it as is *)
|
296
|
| Some (nd, al) ->
|
297
|
(* returning the updated node, possible solved, as well as the
|
298
|
generated alarms *)
|
299
|
max_inlines,
|
300
|
{top with top_decl_desc = Node nd}::prog_accu,
|
301
|
(nd, al)::al_list
|
302
|
)
|
303
|
| _ -> max_inlines, top::prog_accu, al_list
|
304
|
) prog (max_inlines, [], [])
|
305
|
in
|
306
|
prog, List.for_all al_is_solved al_list, al_list
|
307
|
|
308
|
|
309
|
(* (ident list * (ident * expr* bool) list * bool) *)
|
310
|
let pp_al nd fmt (partition, calls, status) =
|
311
|
let open Format in
|
312
|
fprintf fmt "@[<v 0>";
|
313
|
fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
|
314
|
(fprintf_list ~sep:",@ " pp_print_string) partition;
|
315
|
fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
|
316
|
(fprintf_list ~sep:",@ "
|
317
|
(fun fmt ((funid, expr, eq), status) ->
|
318
|
fprintf fmt "%s" funid;
|
319
|
if status && is_expr_inlined nd expr then fprintf fmt " (inlining it solves the alg. loop)";
|
320
|
)
|
321
|
) calls;
|
322
|
fprintf fmt "@]"
|
323
|
(* TODO ploc:
|
324
|
First analyse the cycle and identify a list of nodes to be inlined, or node instances
|
325
|
Then two behaviors:
|
326
|
- print that list instead of the unreadable cyclic dependency comment
|
327
|
- modify the node by adding the inline information
|
328
|
- recall the subset of stage1 but restricted to a single node:
|
329
|
- inline locally, typing, clocking (may have to reset the tables first), normalization of the node, mpfr injection
|
330
|
- recall stage2
|
331
|
*)
|
332
|
|
333
|
|
334
|
let pp_report fmt report =
|
335
|
let open Format in
|
336
|
fprintf_list ~sep:"@."
|
337
|
(fun fmt (nd, als) ->
|
338
|
let top = Corelang.node_from_name (nd.node_id) in
|
339
|
let pp =
|
340
|
if not !Options.solve_al || List.exists (fun (_,_,valid) -> not valid) als then
|
341
|
Error.pp_error (* at least one failure: erroneous node *)
|
342
|
else
|
343
|
Error.pp_warning (* solvable cases: warning only *)
|
344
|
in
|
345
|
pp top.top_decl_loc
|
346
|
(fun fmt ->
|
347
|
fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}"
|
348
|
nd.node_id
|
349
|
(fprintf_list ~sep:"@ " (pp_al nd)) als
|
350
|
)
|
351
|
) fmt report;
|
352
|
fprintf fmt "@."
|
353
|
|
354
|
|
355
|
|
356
|
let analyze cpt prog =
|
357
|
Log.report ~level:1 (fun fmt ->
|
358
|
Format.fprintf fmt "@[<v 2>Algebraic loop detected: ";
|
359
|
if !Options.solve_al then Format.fprintf fmt "solving mode actived";
|
360
|
Format.fprintf fmt "@ ";
|
361
|
);
|
362
|
let prog, status_ok, report = clean_al prog in
|
363
|
|
364
|
let res =
|
365
|
if cpt > 0 && !Options.solve_al && status_ok then (
|
366
|
try
|
367
|
fast_stages_processing prog
|
368
|
with _ -> assert false (* Should not happen since the error has been
|
369
|
catched already *)
|
370
|
)
|
371
|
else (
|
372
|
(* We stop with unresolved AL *)(* TODO create a report *)
|
373
|
(* Printing the report on stderr *)
|
374
|
Format.eprintf "%a" pp_report report;
|
375
|
raise (Corelang.Error (Location.dummy_loc, Error.AlgebraicLoop))
|
376
|
)
|
377
|
in
|
378
|
(* Printing the report on stderr *)
|
379
|
Format.eprintf "%a" pp_report report;
|
380
|
res
|
381
|
|
382
|
let analyze prog =
|
383
|
analyze !Options.al_nb_max prog
|
384
|
|
385
|
|