Project

General

Profile

Revision 264a4844 src/algebraicLoop.ml

View differences:

src/algebraicLoop.ml
14 14
open LustreSpec
15 15
open Corelang
16 16
open Utils
17
open Format
18 17

  
19 18
(* An single algebraic loop is defined (partition, node calls, inlined, status)
20 19
   ie 
......
30 29
type call = ident * expr * eq (* fun id, expression, and containing equation *)
31 30
  
32 31
type algebraic_loop = ident list * (call * bool) list * bool
33
  
34
exception Error of (node_desc * (algebraic_loop list)) list
32
type report = (node_desc * algebraic_loop list) list
33
exception Error of report
34

  
35 35

  
36 36
(* Module that extract from the DataCycle the set of node that could be inlined
37 37
   to solve the problem. *)
......
76 76
    Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq
77 77
  ) fmt resolution
78 78
  
79
let al_is_solved (_, (vars, calls, status)) = status
79
let al_is_solved (_, als) = List.for_all (fun (vars, calls, status) -> status) als
80 80
  
81 81
(**********************************************************************)
82 82
(* Functions to access or toggle the local inlining feature of a call *)
......
89 89
    (Corelang.mkexpr loc
90 90
       (Expr_const (Const_tag tag_true) ))
91 91

  
92
let is_expr_inlined expr =
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 =
93 103
  match expr.expr_annot with
94 104
    None -> false
95
  | Some anns -> if List.mem_assoc Inliner.keyword anns.annots then
96
      let status = List.assoc Inliner.keyword anns.annots in
97
      match status.eexpr_qfexpr.expr_desc with
98
      | Expr_const (Const_tag tag) when tag = tag_true ->
99
	 true
100
      | Expr_const (Const_tag tag) when tag = tag_false ->
101
	 false
102
      | _ -> assert false (* expecting true or false value *)	 
103
    else false
104
      
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

  
105 128
(* Inline the provided expression *)
106
let inline_expr expr =
129
let inline_expr node expr =
130
  (* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *)
107 131
  let ann = inline_annotation expr.expr_loc in
108
    match expr.expr_annot with
109
    | None -> expr.expr_annot = Some {annots = [ann]; annot_loc = expr.expr_loc} 
110
    | Some anns -> expr.expr_annot = Some {anns with annots = ann::anns.annots}
111
  
112
(* Inline the call tagged tag in expr: should not be used anymore, thanks to a direct call to inline_expr *)
113
let rec inline_call tag expr =
114
  if expr.expr_tag = tag then
115
    inline_expr expr
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
116 152
  else
117
    let _in = inline_call tag in
118
    let _ins = List.exists _in
119
    in
120
    match expr.expr_desc with
121
    | Expr_const _
122
    | Expr_ident _ -> false
123
    | Expr_tuple el -> _ins el
124
    | Expr_ite (g,t,e) -> _ins [g;t;e]
125
    | Expr_arrow (e1, e2) 
126
    | Expr_fby (e1, e2) -> _ins [e1; e2]
127
    | Expr_array el -> _ins el
128
    | Expr_access (e, _)
129
    | Expr_power (e, _)
130
    | Expr_pre e
131
    | Expr_when (e, _, _) -> _in e
132
    | Expr_merge (_, hl) -> _ins (List.map snd hl)
133
    | Expr_appl (_, arg, Some r) -> _ins [arg; r]
134
    | Expr_appl (_, arg, None) -> _in arg
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;
135 163

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

  
137 168
(**********************)
138 169
(* Returns a modified node, if possible, and an algebraic_loop report *)
139
let rec solving_node nd existing_al partitions =
170
let rec solving_node max_inlines prog nd existing_al partitions =
171
  (* let pp_calls = pp_calls nd in *)
140 172
  (* For each partition, we identify the original one *)
141
  let rerun, al = List.fold_left (fun (rerun, al) part ->
173
  let rerun, max_inlines, al = List.fold_left (fun (rerun, inlines, al) part ->
142 174
    let part_vars = ISet.of_list part in 
175
    (* Useful functions to filter list of elements *)
143 176
    let match_al (vars, calls, status) =
144
      not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars))  in
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 *)
145 179
    let matched, non_matched = List.partition match_al existing_al in
146
    match matched, non_matched with
147
    | [], _ -> ((* A new conflict partition *)
148
      let calls = CycleResolution.resolve nd part in
149
      (* Filter out already inlined calls *)
150
      let already_inlined, possible_resolution =
151
	List.partition (fun (_, expr, _) -> is_expr_inlined expr) calls in
152
      (* Inlining the first uninlined call *)
153
      match possible_resolution with
154
      | (eq, expr, fun_id)::_ -> ((* One could inline expr *)
155
	(* Forcing the expr to be inlined *)
156
	let _ = inline_expr expr in
157
	true, (* we have to rerun to see if the inlined expression solves the issue *)
158
	(
159
	  part,
160
	  List.map (fun (eq, expr2, fcn_name) ->  fcn_name, expr2, (expr2.expr_tag = expr.expr_tag)) calls,
161
	  false (* Status is nok, LA is unsolved yet *)
162
	    
163
	)::non_matched
164
      )	 
165
      | [] -> (* No more calls to inline: algebraic loop is not solvable *)
166
	 rerun, (* we don't force rerun since the current node is not solvable *)
167
	(
168
	  part, (* initial list of troublesome variables *)
169
	  List.map (fun (eq, expr, fcn_name) ->  fcn_name, expr, false) calls,
170
	  false (* Status is nok, LA is unsolved *)
171
	)::non_matched 
172
	  
173
    )
174
    | [vars, calls, status], _ ->
175
       assert false (* Existing partitions were already addressed:
176
		       on peut regarder si la partition courante concerne xxx
177
		       else (* New cycle ??? *)
178
		       
179
		       
180

  
181

  
182
		       Que faut il faire?
183

  
184
		       dans un premiertemps on peut ramasser les contraintes et s'arreter là.
185
		       pas d'appel recursif donc on a toujours des nouvelles partitions
186
		       on calcule les apples, on les associe à faux (on a pas inliné encore)
187
		       et le statue global est à faux (on a rien resolu)
188

  
189
		       comment resoud-on ?
190
		       on ne doit se focaliser que sur les partitions courantes. C'est elle qui sont en conflit
191
		       pour chaque, on pick un call et on l'inlinee
192
		       apres on appel stage1/stage2 pour faire le scheudling du node
193

  
194

  
195
		    *)
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 *)
196 199

  
197
	 
198
  ) (false, existing_al) partitions
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
199 245
  in
200 246
  (* if partition an already identified al ? *)
201 247
  (* if ISet.of_list partition *)
202

  
203
  (* if rerun then *)
204
  (*   assert false (\* the missing part, redo stage 1, ... with the updated inline flags *\) *)
205
  (* ; *)
206
  (* TODO xxx il faut ici ajouter le inline sur le 1er appel,
207
     puis reafaire le stage1 et scheduling du noeud *)
208
  Some(nd, al)
209

  
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
      
210 267
(** This function takes a prog and returns (prog', status, alarms)
211 268
    where prog' is a modified prog with some locally inlined calls
212 269
    status is true is the final prog' is schedulable, ie no algebraic loop
......
214 271
    Alarms contain the list of inlining performed or advised for each node. 
215 272
    This could be provided as a feedback to the user.
216 273
*)
217
let clean_al prog =
274
let clean_al prog : program * bool * report =
275
  let max_inlines = !Options.al_nb_max in
218 276
(* We iterate over each node *)
219
  let prog, al_list =
277
  let _, prog, al_list =
220 278
    List.fold_right (
221
      fun top (prog_accu, al_list) ->
279
      fun top (max_inlines, prog_accu, al_list) ->
222 280
	match top.top_decl_desc with
223 281
	| Node nd -> (
224
	  let error =
282
	  let error, max_inlines =
225 283
	    try (* without exception the node is schedulable; nothing to declare *)
226 284
	      let _ = Scheduling.schedule_node nd in
227
	      None
228
	    with Causality.Error (Causality.DataCycle partitions) -> solving_node nd [] partitions
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
	    )
229 292
	  in
230 293
	  match error with
231
	  | None -> top::prog_accu, al_list (* keep it as is *)
294
	  | None -> max_inlines, top::prog_accu, al_list (* keep it as is *)
232 295
	  | Some (nd, al) ->
233 296
	     (* returning the updated node, possible solved, as well as the
234 297
		generated alarms *)
235
	     {top with top_decl_desc = Node nd}::prog_accu, (nd, al)::al_list 
298
	     max_inlines,
299
	     {top with top_decl_desc = Node nd}::prog_accu,
300
	    (nd, al)::al_list 
236 301
	)	   
237
	| _ -> top::prog_accu, al_list
238
    ) prog ([], []) 
302
	| _ -> max_inlines, top::prog_accu, al_list
303
    ) prog (max_inlines, [], []) 
239 304
  in
240 305
  prog, List.for_all al_is_solved al_list, al_list
241 306

  
242 307

  
243 308
(* (ident list * (ident * expr* bool) list * bool) *)
244
let pp_al fmt (partition, calls, status) =
309
let pp_al nd fmt (partition, calls, status) =
310
  let open Format in
245 311
  fprintf fmt "@[<v 0>";
246 312
  fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
247 313
    (fprintf_list ~sep:",@ " pp_print_string) partition;
248 314
  fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
249 315
    (fprintf_list ~sep:",@ "
250
       (fun fmt (funid, expr, status) ->
316
       (fun fmt ((funid, expr, eq), status) ->
251 317
	 fprintf fmt "%s" funid;
252
	 if status && is_expr_inlined expr then fprintf fmt " (inlining it solves the alg. loop)";
318
	 if status && is_expr_inlined nd expr then fprintf fmt " (inlining it solves the alg. loop)";
253 319
       )
254 320
    ) calls;
255 321
  fprintf fmt "@]"
......
265 331
    
266 332
    
267 333
let pp_report fmt report =
268
  fprintf fmt "@.Algebraic loops in nodes@.";
334
  let open Format in
269 335
  fprintf_list ~sep:"@."
270 336
    (fun fmt (nd, als) ->
271 337
      let top = Corelang.node_from_name (nd.node_id) in
272
      Error.pp_error top.top_decl_loc
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
273 345
	(fun fmt -> 
274
	  fprintf fmt "node %s: {@[<v 0>%a@]}"
346
	  fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}"
275 347
	    nd.node_id
276
	    (fprintf_list ~sep:"@ " pp_al) als
348
	    (fprintf_list ~sep:"@ " (pp_al nd)) als
277 349
	)
278 350
    ) fmt report;
279 351
  fprintf fmt "@."
280 352
    
281 353

  
282
let analyze prog =
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
  );
283 361
  let prog, status_ok, report = clean_al prog in
284
  if !Options.solve_al && status_ok then
285
    Scheduling.schedule_prog prog
286
  else (
287
    (* TODO create a report *)
288
    Format.eprintf "%a" pp_report report;
289
    raise (Corelang.Error (Location.dummy_loc, Error.AlgebraicLoop))
290
  )
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
    

Also available in: Unified diff