Project

General

Profile

Download (15.5 KB) Statistics
| Branch: | Tag: | Revision:
1 ca7ff3f7 Lélio Brun
(* 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 9094307a ploc
5 ca7ff3f7 Lélio Brun
   When done, a report is generated.
6 9094307a ploc
7 ca7ff3f7 Lélio Brun
   - 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 9094307a ploc
11
   If the option solve_al is activated, the resulting partially inlined prog is
12 ca7ff3f7 Lélio Brun
   propagated fur future processing Otherwise the compilation stops *)
13 8446bf03 ploc
open Lustre_types
14 9094307a ploc
open Corelang
15
open Utils
16
17
(* An single algebraic loop is defined (partition, node calls, inlined, status)
18 ca7ff3f7 Lélio Brun
   ie
19 23ce017b ploc
20
   1. the list of variables in the loop, ident list
21 ca7ff3f7 Lélio Brun
22 23ce017b ploc
   2.the possible functions identifier to inline, and whether they have been
23 ca7ff3f7 Lélio Brun
   inlined yet (ident * tag * bool) list and
24
25
   3. a status whether the inlining is enough bool *)
26 23ce017b ploc
27 ca7ff3f7 Lélio Brun
type call = ident * expr * eq
28
(* fun id, expression, and containing equation *)
29 23ce017b ploc
30
type algebraic_loop = ident list * (call * bool) list * bool
31 ca7ff3f7 Lélio Brun
32 264a4844 ploc
type report = (node_desc * algebraic_loop list) list
33
34 ca7ff3f7 Lélio Brun
exception Error of report
35 9094307a ploc
36
(* Module that extract from the DataCycle the set of node that could be inlined
37
   to solve the problem. *)
38 ca7ff3f7 Lélio Brun
module CycleResolution = struct
39 9094307a ploc
  (* 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 23ce017b ploc
  let resolve node partition : call list =
42 9094307a ploc
    let partition = ISet.of_list partition in
43
    (* Preprocessing calls: associate to each of them the eq.lhs associated *)
44 333e3a25 ploc
    let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in
45
    let eqs, auts = get_node_eqs node in
46 ca7ff3f7 Lélio Brun
    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 9094307a ploc
end
75
76 ca7ff3f7 Lélio Brun
(* Format.fprintf fmt "@[<v 2>Possible resolution:@ %a@]" pp_resolution
77
   resolution*)
78 9094307a ploc
79
let pp_resolution fmt resolution =
80 ca7ff3f7 Lélio Brun
  fprintf_list ~sep:"@ "
81
    (fun fmt (eq, _) ->
82
      Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq)
83
    fmt resolution
84
85 ca7e8027 Lélio Brun
let al_is_solved (_, als) = List.for_all (fun (_, _, status) -> status) als
86 ca7ff3f7 Lélio Brun
87 23ce017b ploc
(**********************************************************************)
88
(* Functions to access or toggle the local inlining feature of a call *)
89
(* expression                                                         *)
90
(**********************************************************************)
91 9094307a ploc
92
let inline_annotation loc =
93 ca7ff3f7 Lélio Brun
  ( Inliner.keyword,
94
    Corelang.mkeexpr loc (Corelang.mkexpr loc (Expr_const (Const_tag tag_true)))
95
  )
96 9094307a ploc
97 264a4844 ploc
let is_inlining_annot (key, status) =
98 ca7ff3f7 Lélio Brun
  key = Inliner.keyword
99
  &&
100 264a4844 ploc
  match status.eexpr_qfexpr.expr_desc with
101
  | Expr_const (Const_tag tag) when tag = tag_true ->
102 ca7ff3f7 Lélio Brun
    true
103 264a4844 ploc
  | Expr_const (Const_tag tag) when tag = tag_false ->
104 ca7ff3f7 Lélio Brun
    false
105
  | _ ->
106
    assert false
107
(* expecting true or false value *)
108
109 264a4844 ploc
let is_expr_inlined nd expr =
110 9094307a ploc
  match expr.expr_annot with
111 ca7ff3f7 Lélio Brun
  | None ->
112
    false
113 264a4844 ploc
  | Some anns -> (
114 ca7ff3f7 Lélio Brun
    (* 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 264a4844 ploc
134 ca7ff3f7 Lélio Brun
let pp_calls nd fmt calls =
135
  Format.fprintf fmt "@[<v 0>%a@]"
136
    (fprintf_list ~sep:"@ " (fun fmt (funid, expr, _) ->
137
         Format.fprintf fmt "%s: %i (inlined:%b)" funid expr.expr_tag
138
           (is_expr_inlined nd expr)))
139
    calls
140 264a4844 ploc
141 9094307a ploc
(* Inline the provided expression *)
142 264a4844 ploc
let inline_expr node expr =
143
  (* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *)
144 9094307a ploc
  let ann = inline_annotation expr.expr_loc in
145 ca7ff3f7 Lélio Brun
  let ann = { annots = [ ann ]; annot_loc = expr.expr_loc } in
146 264a4844 ploc
  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 ca7ff3f7 Lélio Brun
(* Perform the steps of stage1/stage2 to revalidate the schedulability of the
152
   program *)
153 264a4844 ploc
let fast_stages_processing prog =
154 ca7ff3f7 Lélio Brun
  Log.report ~level:3 (fun fmt ->
155
      Format.fprintf fmt
156
        "@[<v 2>Fast revalidation: normalization + schedulability@ ");
157 264a4844 ploc
  Options.verbose_level := !Options.verbose_level - 2;
158
159
  (* Mini stage 1 *)
160 0d54d8a8 ploc
  (* Extracting dependencies: fill some table with typing info *)
161 2200179c ploc
  (* ignore (Modules.load ~is_header:false prog); REMOVED on 2019/07/16 *)
162 264a4844 ploc
  (* 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 ca7ff3f7 Lélio Brun
  else Compiler_common.check_stateless_decls prog;
168 264a4844 ploc
  (* Typing *)
169 ca7ff3f7 Lélio Brun
  let _ (*computed_types_env*) =
170
    Compiler_common.type_decls !Global.type_env prog
171
  in
172 264a4844 ploc
  (* Clock calculus *)
173 ca7ff3f7 Lélio Brun
  let _ (*computed_clocks_env*) =
174
    Compiler_common.clock_decls !Global.clock_env prog
175
  in
176 264a4844 ploc
  (* Normalization *)
177 ad4774b0 ploc
  let params = Backends.get_normalization_params () in
178
  let prog = Normalization.normalize_prog params prog in
179 264a4844 ploc
  (* Mini stage 2 : Scheduling *)
180
  let res = Scheduling.schedule_prog prog in
181
  Options.verbose_level := !Options.verbose_level + 2;
182 9094307a ploc
183 ca7ff3f7 Lélio Brun
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ ");
184 264a4844 ploc
  res
185 9094307a ploc
186
(**********************)
187
(* Returns a modified node, if possible, and an algebraic_loop report *)
188 264a4844 ploc
let rec solving_node max_inlines prog nd existing_al partitions =
189
  (* let pp_calls = pp_calls nd in *)
190 9094307a ploc
  (* For each partition, we identify the original one *)
191 ca7ff3f7 Lélio Brun
  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 9094307a ploc
  in
285
  (* if partition an already identified al ? *)
286
  (* if ISet.of_list partition *)
287 ca7ff3f7 Lélio Brun
  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 264a4844 ploc
    try
291 ca7ff3f7 Lélio Brun
      Log.report ~level:2 (fun fmt ->
292
          Format.fprintf fmt "rescheduling node with new inlined call@ ");
293 264a4844 ploc
      let _ = fast_stages_processing prog in
294
      (* If everything went up to here, the problem is solved! All associated
295 ca7ff3f7 Lélio Brun
         alarms are mapped to valid status. *)
296
      let al = List.map (fun (v, c, _) -> v, c, true) al in
297 264a4844 ploc
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "AL solved@ ");
298 ca7ff3f7 Lélio Brun
      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 ad4774b0 ploc
let clean_al prog : program_t * bool * report =
316 264a4844 ploc
  let max_inlines = !Options.al_nb_max in
317 ca7ff3f7 Lélio Brun
  (* We iterate over each node *)
318 264a4844 ploc
  let _, prog, al_list =
319 ca7ff3f7 Lélio Brun
    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 9094307a ploc
  in
350
  prog, List.for_all al_is_solved al_list, al_list
351
352
(* (ident list * (ident * expr* bool) list * bool) *)
353 ca7e8027 Lélio Brun
let pp_al nd fmt (partition, calls, _) =
354 264a4844 ploc
  let open Format in
355 9094307a ploc
  fprintf fmt "@[<v 0>";
356
  fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
357 ca7ff3f7 Lélio Brun
    (fprintf_list ~sep:",@ " pp_print_string)
358
    partition;
359 9094307a ploc
  fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
360 ca7ff3f7 Lélio Brun
    (fprintf_list ~sep:",@ " (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 9094307a ploc
  fprintf fmt "@]"
366 ca7ff3f7 Lélio Brun
(* 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 9094307a ploc
let pp_report fmt report =
374 264a4844 ploc
  let open Format in
375 9094307a ploc
  fprintf_list ~sep:"@."
376 ca7e8027 Lélio Brun
    (fun _ (nd, als) ->
377 ca7ff3f7 Lélio Brun
      let top = Corelang.node_from_name nd.node_id in
378 264a4844 ploc
      let pp =
379 ca7ff3f7 Lélio Brun
        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 264a4844 ploc
      in
386 ca7ff3f7 Lélio Brun
      pp top.top_decl_loc (fun fmt ->
387
          fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}" nd.node_id
388
            (fprintf_list ~sep:"@ " (pp_al nd))
389
            als))
390
    fmt report;
391 9094307a ploc
  fprintf fmt "@."
392 264a4844 ploc
393
let analyze cpt prog =
394
  Log.report ~level:1 (fun fmt ->
395 ca7ff3f7 Lélio Brun
      Format.fprintf fmt "@[<v 2>Algebraic loop detected: ";
396
      if !Options.solve_al then Format.fprintf fmt "solving mode actived";
397
      Format.fprintf fmt "@ ");
398 9094307a ploc
  let prog, status_ok, report = clean_al prog in
399 ca7ff3f7 Lélio Brun
400 264a4844 ploc
  let res =
401 ca7ff3f7 Lélio Brun
    if cpt > 0 && !Options.solve_al && status_ok then
402
      try fast_stages_processing prog with _ -> assert false
403
      (* Should not happen since the error has been catched already *)
404 264a4844 ploc
    else (
405 ca7ff3f7 Lélio Brun
      (* We stop with unresolved AL *)
406
      (* TODO create a report *)
407 264a4844 ploc
      (* Printing the report on stderr *)
408
      Format.eprintf "%a" pp_report report;
409 ca7ff3f7 Lélio Brun
      raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop)))
410 264a4844 ploc
  in
411
  (* Printing the report on stderr *)
412
  Format.eprintf "%a" pp_report report;
413
  res
414 ca7ff3f7 Lélio Brun
415
let analyze prog = analyze !Options.al_nb_max prog