Project

General

Profile

Download (15.5 KB) Statistics
| Branch: | Tag: | Revision:
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
  fprintf_list ~sep:"@ "
81
    (fun fmt (eq, _) ->
82
      Format.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
    (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

    
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
    (fprintf_list ~sep:",@ " pp_print_string)
358
    partition;
359
  fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
360
    (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
  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
  fprintf_list ~sep:"@."
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
            (fprintf_list ~sep:"@ " (pp_al nd))
389
            als))
390
    fmt report;
391
  fprintf fmt "@."
392

    
393
let analyze cpt prog =
394
  Log.report ~level:1 (fun fmt ->
395
      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
  let prog, status_ok, report = clean_al prog in
399

    
400
  let res =
401
    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
    else (
405
      (* We stop with unresolved AL *)
406
      (* TODO create a report *)
407
      (* Printing the report on stderr *)
408
      Format.eprintf "%a" pp_report report;
409
      raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop)))
410
  in
411
  (* Printing the report on stderr *)
412
  Format.eprintf "%a" pp_report report;
413
  res
414

    
415
let analyze prog = analyze !Options.al_nb_max prog
(2-2/5)