Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / algebraicLoop.ml @ 23ce017b

History | View | Annotate | Download (10 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
open Format
18

    
19
(* An single algebraic loop is defined (partition, node calls, inlined, status)
20
   ie 
21

    
22
   1. the list of variables in the loop, ident list
23
   
24
   2.the possible functions identifier to inline, and whether they have been
25
   inlined yet (ident * tag * bool) list and 
26

    
27
   3. a status whether the inlining is enough bool
28
*)
29

    
30
type call = ident * expr * eq (* fun id, expression, and containing equation *)
31
  
32
type algebraic_loop = ident list * (call * bool) list * bool
33
  
34
exception Error of (node_desc * (algebraic_loop list)) list
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 (_, (vars, calls, status)) = status
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_expr_inlined expr =
93
  match expr.expr_annot with
94
    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
(* Inline the provided expression *)
106
let inline_expr expr =
107
  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
116
  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
135

    
136

    
137
(**********************)
138
(* Returns a modified node, if possible, and an algebraic_loop report *)
139
let rec solving_node nd existing_al partitions =
140
  (* For each partition, we identify the original one *)
141
  let rerun, al = List.fold_left (fun (rerun, al) part ->
142
    let part_vars = ISet.of_list part in 
143
    let match_al (vars, calls, status) =
144
      not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars))  in
145
    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
		    *)
196

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

    
210
(** This function takes a prog and returns (prog', status, alarms)
211
    where prog' is a modified prog with some locally inlined calls
212
    status is true is the final prog' is schedulable, ie no algebraic loop
213
    In case of failure, ie. inlining does not solve the problem; the status is false.
214
    Alarms contain the list of inlining performed or advised for each node. 
215
    This could be provided as a feedback to the user.
216
*)
217
let clean_al prog =
218
(* We iterate over each node *)
219
  let prog, al_list =
220
    List.fold_right (
221
      fun top (prog_accu, al_list) ->
222
	match top.top_decl_desc with
223
	| Node nd -> (
224
	  let error =
225
	    try (* without exception the node is schedulable; nothing to declare *)
226
	      let _ = Scheduling.schedule_node nd in
227
	      None
228
	    with Causality.Error (Causality.DataCycle partitions) -> solving_node nd [] partitions
229
	  in
230
	  match error with
231
	  | None -> top::prog_accu, al_list (* keep it as is *)
232
	  | Some (nd, al) ->
233
	     (* returning the updated node, possible solved, as well as the
234
		generated alarms *)
235
	     {top with top_decl_desc = Node nd}::prog_accu, (nd, al)::al_list 
236
	)	   
237
	| _ -> top::prog_accu, al_list
238
    ) prog ([], []) 
239
  in
240
  prog, List.for_all al_is_solved al_list, al_list
241

    
242

    
243
(* (ident list * (ident * expr* bool) list * bool) *)
244
let pp_al fmt (partition, calls, status) =
245
  fprintf fmt "@[<v 0>";
246
  fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
247
    (fprintf_list ~sep:",@ " pp_print_string) partition;
248
  fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
249
    (fprintf_list ~sep:",@ "
250
       (fun fmt (funid, expr, status) ->
251
	 fprintf fmt "%s" funid;
252
	 if status && is_expr_inlined expr then fprintf fmt " (inlining it solves the alg. loop)";
253
       )
254
    ) calls;
255
  fprintf fmt "@]"
256
     (* TODO ploc:
257
	First analyse the cycle and identify a list of nodes to be inlined, or node instances
258
	Then two behaviors: 
259
	- print that list instead of the unreadable cyclic dependency comment
260
	- modify the node by adding the inline information
261
	- recall the subset of stage1 but restricted to a single node:
262
	- inline locally, typing, clocking (may have to reset the tables first), normalization of the node, mpfr injection
263
        - recall stage2
264
     *)
265
    
266
    
267
let pp_report fmt report =
268
  fprintf fmt "@.Algebraic loops in nodes@.";
269
  fprintf_list ~sep:"@."
270
    (fun fmt (nd, als) ->
271
      let top = Corelang.node_from_name (nd.node_id) in
272
      Error.pp_error top.top_decl_loc
273
	(fun fmt -> 
274
	  fprintf fmt "node %s: {@[<v 0>%a@]}"
275
	    nd.node_id
276
	    (fprintf_list ~sep:"@ " pp_al) als
277
	)
278
    ) fmt report;
279
  fprintf fmt "@."
280
    
281

    
282
let analyze prog =
283
  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
  )