Project

General

Profile

Download (14.5 KB) Statistics
| Branch: | Tag: | Revision:
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 Lustrec
15
open Lustre_types
16
open Corelang
17
open Utils
18

    
19
(* An single algebraic loop is defined (partition, node calls, inlined, status)
20
   ie 
21

    
22
   1. the list of variables in the loop, ident list
23
   
24
   2.the possible functions identifier to inline, and whether they have been
25
   inlined yet (ident * tag * bool) list and 
26

    
27
   3. a status whether the inlining is enough bool
28
*)
29

    
30
type call = ident * expr * eq (* fun id, expression, and containing equation *)
31
  
32
type algebraic_loop = ident list * (call * bool) list * bool
33
type report = (node_desc * algebraic_loop list) list
34
exception Error of report
35

    
36

    
37
(* Module that extract from the DataCycle the set of node that could be inlined
38
   to solve the problem. *)
39
module CycleResolution =
40
struct
41

    
42
  (* We iter over calls in node defs. If the call defined on of the variable in
43
     the cycle, we store it for future possible inline. *)
44
  let resolve node partition : call list =
45
    let partition = ISet.of_list partition in
46
    (* Preprocessing calls: associate to each of them the eq.lhs associated *)
47
    let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in
48
    let eqs, auts = get_node_eqs node in
49
    assert (auts = []); (* TODO voir si on peut acceder directement aux eqs qui font les calls *)
50
    let calls = List.map (
51
      fun expr ->
52
	let eq = List.find (fun eq ->
53
	  Corelang.expr_contains_expr expr.expr_tag eq.eq_rhs 
54
	) eqs in
55
	let fun_name = match expr.expr_desc with
56
	  | Expr_appl(fun_id, _, _) -> fun_id
57
	  | _ -> assert false
58
	in
59
	fun_name, expr, eq
60
    ) calls_expr in
61
    List.fold_left (
62
      fun accu ((_, _, eq) as call) ->
63
	let shared_vars = ISet.inter (ISet.of_list eq.eq_lhs) partition in
64
	if not (ISet.is_empty shared_vars) then
65
	  (* We have a match: keep the eq and the expr to inline *)
66
	  call::accu
67
	else
68
	  accu
69
    ) [] calls
70
end
71

    
72

    
73
(* Format.fprintf fmt "@[<v 2>Possible resolution:@ %a@]" pp_resolution resolution*)
74

    
75
    
76
let pp_resolution fmt resolution =
77
  fprintf_list ~sep:"@ " (fun fmt (eq, tag) ->
78
    Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq
79
  ) fmt resolution
80
  
81
let al_is_solved (_, als) = List.for_all (fun (vars, calls, status) -> status) als
82
  
83
(**********************************************************************)
84
(* Functions to access or toggle the local inlining feature of a call *)
85
(* expression                                                         *)
86
(**********************************************************************)
87

    
88
let inline_annotation loc =
89
  Inliner.keyword,
90
  Corelang.mkeexpr loc
91
    (Corelang.mkexpr loc
92
       (Expr_const (Const_tag tag_true) ))
93

    
94
let is_inlining_annot (key, status) =
95
key = Inliner.keyword && (
96
  match status.eexpr_qfexpr.expr_desc with
97
  | Expr_const (Const_tag tag) when tag = tag_true ->
98
     true
99
  | Expr_const (Const_tag tag) when tag = tag_false ->
100
     false
101
  | _ -> assert false (* expecting true or false value *)	 
102
)
103
  
104
let is_expr_inlined nd expr =
105
  match expr.expr_annot with
106
    None -> false
107
  | Some anns -> (
108
     (* Sanity check: expr should have the annotation AND the annotation should be declared *)
109
     let local_ann = List.exists is_inlining_annot anns.annots in
110
     let all_expr_inlined = Hashtbl.find_all Annotations.expr_annotations Inliner.keyword in
111
     let registered =
112
       List.exists
113
	 (fun (nd_id, expr_tag) -> nd_id = nd.node_id && expr_tag = expr.expr_tag)
114
	 all_expr_inlined
115
     in
116
     match local_ann, registered with
117
     | true, true -> true (* Everythin' all righ' ! *)
118
     | false, false -> false (* idem *)
119
     | _ -> assert false 
120
  )
121

    
122
let pp_calls nd fmt calls = Format.fprintf fmt "@[<v 0>%a@]"
123
  (fprintf_list ~sep:"@ " (fun fmt (funid,expr, _) -> Format.fprintf fmt "%s: %i (inlined:%b)"
124
    funid
125
    expr.expr_tag
126
    (is_expr_inlined nd expr)
127
   ))
128
  calls
129

    
130
(* Inline the provided expression *)
131
let inline_expr node expr =
132
  (* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *)
133
  let ann = inline_annotation expr.expr_loc in
134
  let ann = {annots = [ann]; annot_loc = expr.expr_loc} in
135
  let res = update_expr_annot node.node_id expr ann in
136
  (* assert (is_expr_inlined node res); *)
137
  (* Format.eprintf "Is expression inlined? %b@." (is_expr_inlined node res); *)
138
  res
139

    
140
(* Perform the steps of stage1/stage2 to revalidate the schedulability of the program *)
141
let fast_stages_processing prog =
142
  Log.report ~level:3
143
    (fun fmt -> Format.fprintf fmt "@[<v 2>Fast revalidation: normalization + schedulability@ ");
144
  Options.verbose_level := !Options.verbose_level - 2;
145

    
146
  (* Mini stage 1 *)
147
  (* Extracting dependencies: fill some table with typing info *)
148
  (* ignore (Modules.load ~is_header:false prog); REMOVED on 2019/07/16 *)
149
  (* Local inlining *)
150
  let prog = Inliner.local_inline prog (* type_env clock_env *) in
151
  (* Checking stateless/stateful status *)
152
  if Plugins.check_force_stateful () then
153
    Compiler_common.force_stateful_decls prog
154
  else
155
    Compiler_common.check_stateless_decls prog;
156
  (* Typing *)
157
  let _ (*computed_types_env*) = Compiler_common.type_decls !Global.type_env prog in
158
  (* Clock calculus *)
159
  let _ (*computed_clocks_env*) = Compiler_common.clock_decls !Global.clock_env prog in
160
  (* Normalization *)
161
  let params = Backends.get_normalization_params () in
162
  let prog = Normalization.normalize_prog params prog in
163
  (* Mini stage 2 : Scheduling *)
164
  let res = Scheduling.schedule_prog prog in
165
  Options.verbose_level := !Options.verbose_level + 2;
166

    
167
  Log.report ~level:3
168
    (fun fmt -> Format.fprintf fmt "@]@ ");
169
  res
170

    
171
(**********************)
172
(* Returns a modified node, if possible, and an algebraic_loop report *)
173
let rec solving_node max_inlines prog nd existing_al partitions =
174
  (* let pp_calls = pp_calls nd in *)
175
  (* For each partition, we identify the original one *)
176
  let rerun, max_inlines, al = List.fold_left (fun (rerun, inlines, al) part ->
177
    let part_vars = ISet.of_list part in 
178
    (* Useful functions to filter list of elements *)
179
    let match_al (vars, calls, status) =
180
      not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars)) in
181
    (* Identifying previous alarms that could be associated to current conflict *)
182
    let matched, non_matched = List.partition match_al existing_al in
183
    let previous_calls =
184
      match matched with
185
      | [] -> []
186
      | [_ (*vars*), calls, _ (*status*)] -> List.map fst calls (* we just keep the calls *)
187
      | _ -> (* variable should not belong to two different algrebraic loops. At least I
188
		hope so! *)
189
	 assert false
190
    in
191
    let match_previous (eq, expr, fun_id) =
192
      List.exists
193
	(fun (_, expr', _) -> expr'.expr_tag = expr.expr_tag)
194
	previous_calls
195
    in
196
    (* let match_inlined (_, expr, _) = is_expr_inlined nd expr in *)
197
    
198
    (* let previous_inlined, previous_no_inlined = List.partition match_inlined previous_calls in *)
199
    (* Format.eprintf "Previous calls: @[<v 0>inlined: {%a}@ no inlined: {%a}@ @]@ " *)
200
    (*   pp_calls previous_inlined *)
201
    (*   pp_calls previous_no_inlined *)
202

    
203
    (* ; *)
204
    
205
    let current_calls = CycleResolution.resolve nd part in
206
    (* Format.eprintf "Current calls: %a" pp_calls current_calls; *)
207
    (* Filter out calls from current_calls that were not already in previous calls *)
208
    let current_calls = List.filter (fun c -> not (match_previous c)) current_calls
209
    in
210
    (* Format.eprintf "Current new calls (no old ones): %a" pp_calls current_calls; *)
211
    let calls = previous_calls @ current_calls in
212
    (* Format.eprintf "All calls (previous + new): %a" pp_calls calls; *)
213
    
214
    (* Filter out already inlined calls: actually they should not appear
215
       ... since they were inlined. We keep it for safety. *)
216
    let _ (* already_inlined *), possible_resolution =
217
      List.partition (fun (_, expr, _) -> is_expr_inlined nd expr) calls in
218
    (* Inlining the first uninlined call *)
219
    match possible_resolution with
220
    | (fun_id, expr, eq)::_ -> ((* One could inline expr *)
221
      Log.report ~level:2 (fun fmt-> Format.fprintf fmt "inlining call to %s@ " fun_id); 
222
      (* Forcing the expr to be inlined *)
223
      let _ = inline_expr nd expr in
224
      (* Format.eprintf "Making sure that the inline list evolved: inlined = {%a}" *)
225
      (* 	pp_calls  *)
226
      (* ; *)
227
      true, (* we have to rerun to see if the inlined expression solves the issue *)
228
      max_inlines - 1,
229
      (
230
	part,
231
	List.map (fun ((eq, expr2, fcn_name) as call)->  call, (expr2.expr_tag = expr.expr_tag)) calls,
232
	true (* TODO was false. Should be put it true and expect a final
233
		scheduling to change it to false in case of failure ? *) (*
234
									   Status is nok, LA is unsolved yet *)
235
	  
236
      )::non_matched
237
    )	 
238
    | [] -> (* No more calls to inline: algebraic loop is not solvable *)
239
       rerun, (* we don't force rerun since the current node is not solvable *)
240
      max_inlines,
241
      (
242
	part, (* initial list of troublesogme variables *)
243
	List.map (fun ((eq, expr, fcn_name) as call) ->  call, false) calls,
244
	false (* Status is nok, LA is unsolved *)
245
      )::non_matched 
246
	
247
  ) (false, max_inlines, existing_al) partitions
248
  in
249
  (* if partition an already identified al ? *)
250
  (* if ISet.of_list partition *)
251
  if rerun && max_inlines > 0 then
252
    (* At least one partition could be improved: we try to inline the calls and reschedule the node. *)
253
    try
254
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "rescheduling node with new inlined call@ ");
255
      let _ = fast_stages_processing prog in
256
      (* If everything went up to here, the problem is solved! All associated
257
	 alarms are mapped to valid status. *)
258
      let al = List.map (fun (v,c,_) -> v,c,true) al in
259
      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "AL solved@ ");
260
      Some(nd, al), max_inlines
261
    with Causality.Error (Causality.DataCycle partitions2) -> (
262
      Log.report ~level:3 (fun fmt -> Format.fprintf fmt "AL not solved yet. Further processing.@ ");
263
      solving_node max_inlines prog nd al partitions2
264
    )
265
  else ((* No rerun, we return the current node and computed alarms *)
266
    Log.report ~level:3 (fun fmt -> Format.fprintf fmt "AL not solved yet. Stopping.@ ");
267
    Some(nd, al), max_inlines
268
  )
269
      
270
(** This function takes a prog and returns (prog', status, alarms)
271
    where prog' is a modified prog with some locally inlined calls
272
    status is true is the final prog' is schedulable, ie no algebraic loop
273
    In case of failure, ie. inlining does not solve the problem; the status is false.
274
    Alarms contain the list of inlining performed or advised for each node. 
275
    This could be provided as a feedback to the user.
276
*)
277
let clean_al prog : program_t * bool * report =
278
  let max_inlines = !Options.al_nb_max in
279
(* We iterate over each node *)
280
  let _, prog, al_list =
281
    List.fold_right (
282
      fun top (max_inlines, prog_accu, al_list) ->
283
	match top.top_decl_desc with
284
	| Node nd -> (
285
	  let error, max_inlines =
286
	    try (* without exception the node is schedulable; nothing to declare *)
287
	      let _ = Scheduling.schedule_node nd in
288
	      None, max_inlines
289
	    with Causality.Error (Causality.DataCycle partitions) -> (
290
	      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@[<v 2>AL in node %s@ " nd.node_id);
291
	      let error, max_inlines = solving_node max_inlines prog nd [] partitions in
292
	      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@ @]");
293
	      error, max_inlines
294
	    )
295
	  in
296
	  match error with
297
	  | None -> max_inlines, top::prog_accu, al_list (* keep it as is *)
298
	  | Some (nd, al) ->
299
	     (* returning the updated node, possible solved, as well as the
300
		generated alarms *)
301
	     max_inlines,
302
	     {top with top_decl_desc = Node nd}::prog_accu,
303
	    (nd, al)::al_list 
304
	)	   
305
	| _ -> max_inlines, top::prog_accu, al_list
306
    ) prog (max_inlines, [], []) 
307
  in
308
  prog, List.for_all al_is_solved al_list, al_list
309

    
310

    
311
(* (ident list * (ident * expr* bool) list * bool) *)
312
let pp_al nd fmt (partition, calls, status) =
313
  let open Format in
314
  fprintf fmt "@[<v 0>";
315
  fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
316
    (fprintf_list ~sep:",@ " pp_print_string) partition;
317
  fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
318
    (fprintf_list ~sep:",@ "
319
       (fun fmt ((funid, expr, eq), status) ->
320
	 fprintf fmt "%s" funid;
321
	 if status && is_expr_inlined nd expr then fprintf fmt " (inlining it solves the alg. loop)";
322
       )
323
    ) calls;
324
  fprintf fmt "@]"
325
     (* TODO ploc:
326
	First analyse the cycle and identify a list of nodes to be inlined, or node instances
327
	Then two behaviors: 
328
	- print that list instead of the unreadable cyclic dependency comment
329
	- modify the node by adding the inline information
330
	- recall the subset of stage1 but restricted to a single node:
331
	- inline locally, typing, clocking (may have to reset the tables first), normalization of the node, mpfr injection
332
        - recall stage2
333
     *)
334
    
335
    
336
let pp_report fmt report =
337
  let open Format in
338
  fprintf_list ~sep:"@."
339
    (fun fmt (nd, als) ->
340
      let top = Corelang.node_from_name (nd.node_id) in
341
      let pp =
342
	if not !Options.solve_al || List.exists (fun (_,_,valid) -> not valid) als then
343
	  Error.pp_error (* at least one failure: erroneous node *)
344
	else
345
	  Error.pp_warning (* solvable cases: warning only *)
346
      in
347
      pp top.top_decl_loc
348
	(fun fmt -> 
349
	  fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}"
350
	    nd.node_id
351
	    (fprintf_list ~sep:"@ " (pp_al nd)) als
352
	)
353
    ) fmt report;
354
  fprintf fmt "@."
355
    
356

    
357

    
358
let analyze cpt prog =
359
  Log.report ~level:1 (fun fmt ->
360
    Format.fprintf fmt "@[<v 2>Algebraic loop detected: ";
361
    if !Options.solve_al then Format.fprintf fmt "solving mode actived";
362
    Format.fprintf fmt "@ ";    
363
  );
364
  let prog, status_ok, report = clean_al prog in
365
  
366
  let res =
367
    if cpt > 0 && !Options.solve_al && status_ok then (
368
      try
369
	fast_stages_processing prog
370
      with _ -> assert false (* Should not happen since the error has been
371
				catched already *)
372
    )
373
    else (
374
      (* We stop with unresolved AL *)(* TODO create a report *)
375
      (* Printing the report on stderr *)
376
      Format.eprintf "%a" pp_report report;
377
      raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop))
378
    )
379
  in
380
  (* Printing the report on stderr *)
381
  Format.eprintf "%a" pp_report report;
382
  res
383
    
384
let analyze prog =
385
  analyze !Options.al_nb_max prog
386
    
387
    
(2-2/23)