Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / checks / algebraicLoop.ml @ 5fccce23

History | View | Annotate | Download (14.5 KB)

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

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

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

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

    
309

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

    
356

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