Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / checks / algebraicLoop.ml @ 0d54d8a8

History | View | Annotate | Download (14.4 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 (Compiler_common.import_dependencies 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 prog = Normalization.normalize_prog ~backend:!Options.output prog in
161
  (* Mini stage 2 : Scheduling *)
162
  let res = Scheduling.schedule_prog prog in
163
  Options.verbose_level := !Options.verbose_level + 2;
164

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

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

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

    
308

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

    
355

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