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