Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / algebraicLoop.ml @ 264a4844

History | View | Annotate | Download (14.3 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 LustreSpec
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 eqs = get_node_eqs node in
47
    let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) eqs in
48
    let calls = List.map (
49
      fun expr ->
50
	let eq = List.find (fun eq ->
51
	  Corelang.expr_contains_expr expr.expr_tag eq.eq_rhs 
52
	) eqs in
53
	let fun_name = match expr.expr_desc with
54
	  | Expr_appl(fun_id, _, _) -> fun_id
55
	  | _ -> assert false
56
	in
57
	fun_name, expr, eq
58
    ) calls_expr in
59
    List.fold_left (
60
      fun accu ((_, _, eq) as call) ->
61
	let shared_vars = ISet.inter (ISet.of_list eq.eq_lhs) partition in
62
	if not (ISet.is_empty shared_vars) then
63
	  (* We have a match: keep the eq and the expr to inline *)
64
	  call::accu
65
	else
66
	  accu
67
    ) [] calls
68
end
69

    
70

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

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

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

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

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

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

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

    
144
  (* Mini stage 1 *)
145
  (* Extracting dependencies *)
146
  let dependencies, type_env, clock_env = Compiler_common.import_dependencies prog in
147
  (* Local inlining *)
148
  let prog = Inliner.local_inline prog (* type_env clock_env *) in
149
  (* Checking stateless/stateful status *)
150
  if Plugins.check_force_stateful () then
151
    Compiler_common.force_stateful_decls prog
152
  else
153
    Compiler_common.check_stateless_decls prog;
154
  (* Typing *)
155
  let _ (*computed_types_env*) = Compiler_common.type_decls type_env prog in
156
  (* Clock calculus *)
157
  let _ (*computed_clocks_env*) = Compiler_common.clock_decls clock_env prog in
158
  (* Normalization *)
159
  let prog = Normalization.normalize_prog ~backend:!Options.output prog in
160
  (* Mini stage 2 : Scheduling *)
161
  let res = Scheduling.schedule_prog prog in
162
  Options.verbose_level := !Options.verbose_level + 2;
163

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

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

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

    
307

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

    
354

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