Project

General

Profile

Download (14.6 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 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
  Global.initialize ();
146
  Corelang.add_internal_funs ();
147

    
148
  (* Mini stage 1 *)
149
  (* Extracting dependencies: fill some table with typing info *)
150
  ignore (Compiler_common.import_dependencies prog);
151
  (* Local inlining *)
152
  let prog = Inliner.local_inline prog (* type_env clock_env *) in
153
  Log.report ~level:3
154
    (fun fmt -> Format.fprintf fmt "Inlined prog: %a@." Printers.pp_prog prog);
155
  (* Checking stateless/stateful status *)
156
  if Plugins.check_force_stateful () then
157
    Compiler_common.force_stateful_decls prog
158
  else
159
    Compiler_common.check_stateless_decls prog;
160
  (* Typing *)
161
  let _ (*computed_types_env*) = Compiler_common.type_decls !Global.type_env prog in
162
  (* Clock calculus *)
163
  let _ (*computed_clocks_env*) = Compiler_common.clock_decls !Global.clock_env prog in
164
  (* Normalization *)
165
  let prog = Normalization.normalize_prog ~backend:!Options.output prog in
166
  (* Mini stage 2 : Scheduling *)
167
  let res = Scheduling.schedule_prog prog in
168
  Options.verbose_level := !Options.verbose_level + 2;
169

    
170
  Log.report ~level:3
171
    (fun fmt -> Format.fprintf fmt "@]@ ");
172
  res
173

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

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

    
313

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

    
360

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