Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/checks/algebraicLoop.ml | ||
---|---|---|
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
|
|
1 |
(* We try to solve all algebraic loops (AL) from prog: each node is mapped to
|
|
2 |
its own cycles each cycle is tentatively solved by inlining one of its
|
|
3 |
component
|
|
4 | 4 |
|
5 |
When done, a report is generated. |
|
5 |
When done, a report is generated.
|
|
6 | 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
|
|
7 |
- for each initial AL, the cycle is presented - either it is solvable and we
|
|
8 |
provide the set of inlines that solves it - or it is not and we write the AL
|
|
9 |
as unsolvable by inlining |
|
10 | 10 |
|
11 | 11 |
If the option solve_al is activated, the resulting partially inlined prog is |
12 |
propagated fur future processing Otherwise the compilation stops |
|
13 |
*) |
|
12 |
propagated fur future processing Otherwise the compilation stops *) |
|
14 | 13 |
open Lustre_types |
15 | 14 |
open Corelang |
16 | 15 |
open Utils |
17 | 16 |
|
18 | 17 |
(* An single algebraic loop is defined (partition, node calls, inlined, status) |
19 |
ie
|
|
18 |
ie |
|
20 | 19 |
|
21 | 20 |
1. the list of variables in the loop, ident list |
22 |
|
|
21 |
|
|
23 | 22 |
2.the possible functions identifier to inline, and whether they have been |
24 |
inlined yet (ident * tag * bool) list and |
|
23 |
inlined yet (ident * tag * bool) list and |
|
24 |
|
|
25 |
3. a status whether the inlining is enough bool *) |
|
25 | 26 |
|
26 |
3. a status whether the inlining is enough bool
|
|
27 |
*) |
|
27 |
type call = ident * expr * eq
|
|
28 |
(* fun id, expression, and containing equation *)
|
|
28 | 29 |
|
29 |
type call = ident * expr * eq (* fun id, expression, and containing equation *) |
|
30 |
|
|
31 | 30 |
type algebraic_loop = ident list * (call * bool) list * bool |
31 |
|
|
32 | 32 |
type report = (node_desc * algebraic_loop list) list |
33 |
exception Error of report |
|
34 | 33 |
|
34 |
exception Error of report |
|
35 | 35 |
|
36 | 36 |
(* Module that extract from the DataCycle the set of node that could be inlined |
37 | 37 |
to solve the problem. *) |
38 |
module CycleResolution = |
|
39 |
struct |
|
40 |
|
|
38 |
module CycleResolution = struct |
|
41 | 39 |
(* We iter over calls in node defs. If the call defined on of the variable in |
42 | 40 |
the cycle, we store it for future possible inline. *) |
43 | 41 |
let resolve node partition : call list = |
... | ... | |
45 | 43 |
(* Preprocessing calls: associate to each of them the eq.lhs associated *) |
46 | 44 |
let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in |
47 | 45 |
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 |
|
46 |
assert (auts = []); |
|
47 |
(* TODO voir si on peut acceder directement aux eqs qui font les calls *) |
|
48 |
let calls = |
|
49 |
List.map |
|
50 |
(fun expr -> |
|
51 |
let eq = |
|
52 |
List.find |
|
53 |
(fun eq -> Corelang.expr_contains_expr expr.expr_tag eq.eq_rhs) |
|
54 |
eqs |
|
55 |
in |
|
56 |
let fun_name = |
|
57 |
match expr.expr_desc with |
|
58 |
| Expr_appl (fun_id, _, _) -> |
|
59 |
fun_id |
|
60 |
| _ -> |
|
61 |
assert false |
|
62 |
in |
|
63 |
fun_name, expr, eq) |
|
64 |
calls_expr |
|
65 |
in |
|
66 |
List.fold_left |
|
67 |
(fun accu ((_, _, eq) as call) -> |
|
68 |
let shared_vars = ISet.inter (ISet.of_list eq.eq_lhs) partition in |
|
69 |
if not (ISet.is_empty shared_vars) then |
|
70 |
(* We have a match: keep the eq and the expr to inline *) |
|
71 |
call :: accu |
|
72 |
else accu) |
|
73 |
[] calls |
|
69 | 74 |
end |
70 | 75 |
|
76 |
(* Format.fprintf fmt "@[<v 2>Possible resolution:@ %a@]" pp_resolution |
|
77 |
resolution*) |
|
71 | 78 |
|
72 |
(* Format.fprintf fmt "@[<v 2>Possible resolution:@ %a@]" pp_resolution resolution*) |
|
73 |
|
|
74 |
|
|
75 | 79 |
let pp_resolution fmt resolution = |
76 |
fprintf_list ~sep:"@ " (fun fmt (eq, _) -> |
|
77 |
Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq |
|
78 |
) fmt resolution |
|
79 |
|
|
80 |
fprintf_list ~sep:"@ " |
|
81 |
(fun fmt (eq, _) -> |
|
82 |
Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq) |
|
83 |
fmt resolution |
|
84 |
|
|
80 | 85 |
let al_is_solved (_, als) = List.for_all (fun (_, _, status) -> status) als |
81 |
|
|
86 |
|
|
82 | 87 |
(**********************************************************************) |
83 | 88 |
(* Functions to access or toggle the local inlining feature of a call *) |
84 | 89 |
(* expression *) |
85 | 90 |
(**********************************************************************) |
86 | 91 |
|
87 | 92 |
let inline_annotation loc = |
88 |
Inliner.keyword, |
|
89 |
Corelang.mkeexpr loc |
|
90 |
(Corelang.mkexpr loc |
|
91 |
(Expr_const (Const_tag tag_true) )) |
|
93 |
( Inliner.keyword, |
|
94 |
Corelang.mkeexpr loc (Corelang.mkexpr loc (Expr_const (Const_tag tag_true))) |
|
95 |
) |
|
92 | 96 |
|
93 | 97 |
let is_inlining_annot (key, status) = |
94 |
key = Inliner.keyword && ( |
|
98 |
key = Inliner.keyword |
|
99 |
&& |
|
95 | 100 |
match status.eexpr_qfexpr.expr_desc with |
96 | 101 |
| Expr_const (Const_tag tag) when tag = tag_true -> |
97 |
true
|
|
102 |
true |
|
98 | 103 |
| Expr_const (Const_tag tag) when tag = tag_false -> |
99 |
false |
|
100 |
| _ -> assert false (* expecting true or false value *) |
|
101 |
) |
|
102 |
|
|
104 |
false |
|
105 |
| _ -> |
|
106 |
assert false |
|
107 |
(* expecting true or false value *) |
|
108 |
|
|
103 | 109 |
let is_expr_inlined nd expr = |
104 | 110 |
match expr.expr_annot with |
105 |
None -> false |
|
111 |
| None -> |
|
112 |
false |
|
106 | 113 |
| 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 |
) |
|
114 |
(* Sanity check: expr should have the annotation AND the annotation should |
|
115 |
be declared *) |
|
116 |
let local_ann = List.exists is_inlining_annot anns.annots in |
|
117 |
let all_expr_inlined = |
|
118 |
Hashtbl.find_all Annotations.expr_annotations Inliner.keyword |
|
119 |
in |
|
120 |
let registered = |
|
121 |
List.exists |
|
122 |
(fun (nd_id, expr_tag) -> |
|
123 |
nd_id = nd.node_id && expr_tag = expr.expr_tag) |
|
124 |
all_expr_inlined |
|
125 |
in |
|
126 |
match local_ann, registered with |
|
127 |
| true, true -> |
|
128 |
true (* Everythin' all righ' ! *) |
|
129 |
| false, false -> |
|
130 |
false (* idem *) |
|
131 |
| _ -> |
|
132 |
assert false) |
|
120 | 133 |
|
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 |
|
134 |
let pp_calls nd fmt calls = |
|
135 |
Format.fprintf fmt "@[<v 0>%a@]" |
|
136 |
(fprintf_list ~sep:"@ " (fun fmt (funid, expr, _) -> |
|
137 |
Format.fprintf fmt "%s: %i (inlined:%b)" funid expr.expr_tag |
|
138 |
(is_expr_inlined nd expr))) |
|
139 |
calls |
|
128 | 140 |
|
129 | 141 |
(* Inline the provided expression *) |
130 | 142 |
let inline_expr node expr = |
131 | 143 |
(* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *) |
132 | 144 |
let ann = inline_annotation expr.expr_loc in |
133 |
let ann = {annots = [ann]; annot_loc = expr.expr_loc} in
|
|
145 |
let ann = { annots = [ ann ]; annot_loc = expr.expr_loc } in
|
|
134 | 146 |
let res = update_expr_annot node.node_id expr ann in |
135 | 147 |
(* assert (is_expr_inlined node res); *) |
136 | 148 |
(* Format.eprintf "Is expression inlined? %b@." (is_expr_inlined node res); *) |
137 | 149 |
res |
138 | 150 |
|
139 |
(* Perform the steps of stage1/stage2 to revalidate the schedulability of the program *) |
|
151 |
(* Perform the steps of stage1/stage2 to revalidate the schedulability of the |
|
152 |
program *) |
|
140 | 153 |
let fast_stages_processing prog = |
141 |
Log.report ~level:3 |
|
142 |
(fun fmt -> Format.fprintf fmt "@[<v 2>Fast revalidation: normalization + schedulability@ "); |
|
154 |
Log.report ~level:3 (fun fmt -> |
|
155 |
Format.fprintf fmt |
|
156 |
"@[<v 2>Fast revalidation: normalization + schedulability@ "); |
|
143 | 157 |
Options.verbose_level := !Options.verbose_level - 2; |
144 | 158 |
|
145 | 159 |
(* Mini stage 1 *) |
... | ... | |
150 | 164 |
(* Checking stateless/stateful status *) |
151 | 165 |
if Plugins.check_force_stateful () then |
152 | 166 |
Compiler_common.force_stateful_decls prog |
153 |
else |
|
154 |
Compiler_common.check_stateless_decls prog; |
|
167 |
else Compiler_common.check_stateless_decls prog; |
|
155 | 168 |
(* Typing *) |
156 |
let _ (*computed_types_env*) = Compiler_common.type_decls !Global.type_env prog in |
|
169 |
let _ (*computed_types_env*) = |
|
170 |
Compiler_common.type_decls !Global.type_env prog |
|
171 |
in |
|
157 | 172 |
(* Clock calculus *) |
158 |
let _ (*computed_clocks_env*) = Compiler_common.clock_decls !Global.clock_env prog in |
|
173 |
let _ (*computed_clocks_env*) = |
|
174 |
Compiler_common.clock_decls !Global.clock_env prog |
|
175 |
in |
|
159 | 176 |
(* Normalization *) |
160 | 177 |
let params = Backends.get_normalization_params () in |
161 | 178 |
let prog = Normalization.normalize_prog params prog in |
... | ... | |
163 | 180 |
let res = Scheduling.schedule_prog prog in |
164 | 181 |
Options.verbose_level := !Options.verbose_level + 2; |
165 | 182 |
|
166 |
Log.report ~level:3 |
|
167 |
(fun fmt -> Format.fprintf fmt "@]@ "); |
|
183 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ "); |
|
168 | 184 |
res |
169 | 185 |
|
170 | 186 |
(**********************) |
... | ... | |
172 | 188 |
let rec solving_node max_inlines prog nd existing_al partitions = |
173 | 189 |
(* let pp_calls = pp_calls nd in *) |
174 | 190 |
(* For each partition, we identify the original one *) |
175 |
let rerun, max_inlines, al = List.fold_left (fun (rerun, _, _) part -> |
|
176 |
let part_vars = ISet.of_list part in |
|
177 |
(* Useful functions to filter list of elements *) |
|
178 |
let match_al (vars, _, _) = |
|
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 (_, expr, _) = |
|
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, _)::_ -> ((* 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 ((_, expr2, _) 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 call -> call, false) calls, |
|
243 |
false (* Status is nok, LA is unsolved *) |
|
244 |
)::non_matched |
|
245 |
|
|
246 |
) (false, max_inlines, existing_al) partitions |
|
191 |
let rerun, max_inlines, al = |
|
192 |
List.fold_left |
|
193 |
(fun (rerun, _, _) part -> |
|
194 |
let part_vars = ISet.of_list part in |
|
195 |
(* Useful functions to filter list of elements *) |
|
196 |
let match_al (vars, _, _) = |
|
197 |
not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars)) |
|
198 |
in |
|
199 |
(* Identifying previous alarms that could be associated to current |
|
200 |
conflict *) |
|
201 |
let matched, non_matched = List.partition match_al existing_al in |
|
202 |
let previous_calls = |
|
203 |
match matched with |
|
204 |
| [] -> |
|
205 |
[] |
|
206 |
| [ (_ (*vars*), calls, _) (*status*) ] -> |
|
207 |
List.map fst calls |
|
208 |
(* we just keep the calls *) |
|
209 |
| _ -> |
|
210 |
(* variable should not belong to two different algrebraic loops. At |
|
211 |
least I hope so! *) |
|
212 |
assert false |
|
213 |
in |
|
214 |
let match_previous (_, expr, _) = |
|
215 |
List.exists |
|
216 |
(fun (_, expr', _) -> expr'.expr_tag = expr.expr_tag) |
|
217 |
previous_calls |
|
218 |
in |
|
219 |
|
|
220 |
(* let match_inlined (_, expr, _) = is_expr_inlined nd expr in *) |
|
221 |
|
|
222 |
(* let previous_inlined, previous_no_inlined = List.partition |
|
223 |
match_inlined previous_calls in *) |
|
224 |
(* Format.eprintf "Previous calls: @[<v 0>inlined: {%a}@ no inlined: |
|
225 |
{%a}@ @]@ " *) |
|
226 |
(* pp_calls previous_inlined *) |
|
227 |
(* pp_calls previous_no_inlined *) |
|
228 |
|
|
229 |
(* ; *) |
|
230 |
let current_calls = CycleResolution.resolve nd part in |
|
231 |
(* Format.eprintf "Current calls: %a" pp_calls current_calls; *) |
|
232 |
(* Filter out calls from current_calls that were not already in previous calls *) |
|
233 |
let current_calls = |
|
234 |
List.filter (fun c -> not (match_previous c)) current_calls |
|
235 |
in |
|
236 |
(* Format.eprintf "Current new calls (no old ones): %a" pp_calls |
|
237 |
current_calls; *) |
|
238 |
let calls = previous_calls @ current_calls in |
|
239 |
|
|
240 |
(* Format.eprintf "All calls (previous + new): %a" pp_calls calls; *) |
|
241 |
|
|
242 |
(* Filter out already inlined calls: actually they should not appear ... |
|
243 |
since they were inlined. We keep it for safety. *) |
|
244 |
let _ (* already_inlined *), possible_resolution = |
|
245 |
List.partition (fun (_, expr, _) -> is_expr_inlined nd expr) calls |
|
246 |
in |
|
247 |
(* Inlining the first uninlined call *) |
|
248 |
match possible_resolution with |
|
249 |
| (fun_id, expr, _) :: _ -> |
|
250 |
(* One could inline expr *) |
|
251 |
Log.report ~level:2 (fun fmt -> |
|
252 |
Format.fprintf fmt "inlining call to %s@ " fun_id); |
|
253 |
(* Forcing the expr to be inlined *) |
|
254 |
let _ = inline_expr nd expr in |
|
255 |
(* Format.eprintf "Making sure that the inline list evolved: inlined = {%a}" *) |
|
256 |
(* pp_calls *) |
|
257 |
(* ; *) |
|
258 |
( true, |
|
259 |
(* we have to rerun to see if the inlined expression solves the |
|
260 |
issue *) |
|
261 |
max_inlines - 1, |
|
262 |
( part, |
|
263 |
List.map |
|
264 |
(fun ((_, expr2, _) as call) -> |
|
265 |
call, expr2.expr_tag = expr.expr_tag) |
|
266 |
calls, |
|
267 |
true |
|
268 |
(* TODO was false. Should be put it true and expect a final |
|
269 |
scheduling to change it to false in case of failure ? *) |
|
270 |
(* Status is nok, LA is unsolved yet *) ) |
|
271 |
:: non_matched ) |
|
272 |
| [] -> |
|
273 |
(* No more calls to inline: algebraic loop is not solvable *) |
|
274 |
( rerun, |
|
275 |
(* we don't force rerun since the current node is not solvable *) |
|
276 |
max_inlines, |
|
277 |
( part, |
|
278 |
(* initial list of troublesogme variables *) |
|
279 |
List.map (fun call -> call, false) calls, |
|
280 |
false (* Status is nok, LA is unsolved *) ) |
|
281 |
:: non_matched )) |
|
282 |
(false, max_inlines, existing_al) |
|
283 |
partitions |
|
247 | 284 |
in |
248 | 285 |
(* if partition an already identified al ? *) |
249 | 286 |
(* 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. *) |
|
287 |
if rerun && max_inlines > 0 then ( |
|
288 |
(* At least one partition could be improved: we try to inline the calls and |
|
289 |
reschedule the node. *) |
|
252 | 290 |
try |
253 |
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "rescheduling node with new inlined call@ "); |
|
291 |
Log.report ~level:2 (fun fmt -> |
|
292 |
Format.fprintf fmt "rescheduling node with new inlined call@ "); |
|
254 | 293 |
let _ = fast_stages_processing prog in |
255 | 294 |
(* 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
|
|
295 |
alarms are mapped to valid status. *)
|
|
296 |
let al = List.map (fun (v, c, _) -> v, c, true) al in
|
|
258 | 297 |
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 |
*) |
|
298 |
Some (nd, al), max_inlines
|
|
299 |
with Causality.Error (Causality.DataCycle partitions2) -> |
|
300 |
Log.report ~level:3 (fun fmt -> |
|
301 |
Format.fprintf fmt "AL not solved yet. Further processing.@ ");
|
|
302 |
solving_node max_inlines prog nd al partitions2)
|
|
303 |
else ( |
|
304 |
(* No rerun, we return the current node and computed alarms *)
|
|
305 |
Log.report ~level:3 (fun fmt ->
|
|
306 |
Format.fprintf fmt "AL not solved yet. Stopping.@ ");
|
|
307 |
Some (nd, al), max_inlines) |
|
308 |
|
|
309 |
(** This function takes a prog and returns (prog', status, alarms) where prog'
|
|
310 |
is a modified prog with some locally inlined calls status is true is the
|
|
311 |
final prog' is schedulable, ie no algebraic loop In case of failure, ie.
|
|
312 |
inlining does not solve the problem; the status is false. Alarms contain the
|
|
313 |
list of inlining performed or advised for each node. This could be provided
|
|
314 |
as a feedback to the user. *)
|
|
276 | 315 |
let clean_al prog : program_t * bool * report = |
277 | 316 |
let max_inlines = !Options.al_nb_max in |
278 |
(* We iterate over each node *) |
|
317 |
(* We iterate over each node *)
|
|
279 | 318 |
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, [], []) |
|
319 |
List.fold_right |
|
320 |
(fun top (max_inlines, prog_accu, al_list) -> |
|
321 |
match top.top_decl_desc with |
|
322 |
| Node nd -> ( |
|
323 |
let error, max_inlines = |
|
324 |
try |
|
325 |
(* without exception the node is schedulable; nothing to declare *) |
|
326 |
let _ = Scheduling.schedule_node nd in |
|
327 |
None, max_inlines |
|
328 |
with Causality.Error (Causality.DataCycle partitions) -> |
|
329 |
Log.report ~level:2 (fun fmt -> |
|
330 |
Format.fprintf fmt "@[<v 2>AL in node %s@ " nd.node_id); |
|
331 |
let error, max_inlines = |
|
332 |
solving_node max_inlines prog nd [] partitions |
|
333 |
in |
|
334 |
Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@ @]"); |
|
335 |
error, max_inlines |
|
336 |
in |
|
337 |
match error with |
|
338 |
| None -> |
|
339 |
max_inlines, top :: prog_accu, al_list (* keep it as is *) |
|
340 |
| Some (nd, al) -> |
|
341 |
(* returning the updated node, possible solved, as well as the |
|
342 |
generated alarms *) |
|
343 |
( max_inlines, |
|
344 |
{ top with top_decl_desc = Node nd } :: prog_accu, |
|
345 |
(nd, al) :: al_list )) |
|
346 |
| _ -> |
|
347 |
max_inlines, top :: prog_accu, al_list) |
|
348 |
prog (max_inlines, [], []) |
|
306 | 349 |
in |
307 | 350 |
prog, List.for_all al_is_solved al_list, al_list |
308 | 351 |
|
309 |
|
|
310 | 352 |
(* (ident list * (ident * expr* bool) list * bool) *) |
311 | 353 |
let pp_al nd fmt (partition, calls, _) = |
312 | 354 |
let open Format in |
313 | 355 |
fprintf fmt "@[<v 0>"; |
314 | 356 |
fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ " |
315 |
(fprintf_list ~sep:",@ " pp_print_string) partition; |
|
357 |
(fprintf_list ~sep:",@ " pp_print_string) |
|
358 |
partition; |
|
316 | 359 |
fprintf fmt "@ involved node calls: @[<v 0>%a@]@ " |
317 |
(fprintf_list ~sep:",@ " |
|
318 |
(fun fmt ((funid, expr, _), 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; |
|
360 |
(fprintf_list ~sep:",@ " (fun fmt ((funid, expr, _), status) -> |
|
361 |
fprintf fmt "%s" funid; |
|
362 |
if status && is_expr_inlined nd expr then |
|
363 |
fprintf fmt " (inlining it solves the alg. loop)")) |
|
364 |
calls; |
|
323 | 365 |
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 |
|
|
366 |
(* TODO ploc: First analyse the cycle and identify a list of nodes to be |
|
367 |
inlined, or node instances Then two behaviors: - print that list instead of |
|
368 |
the unreadable cyclic dependency comment - modify the node by adding the |
|
369 |
inline information - recall the subset of stage1 but restricted to a single |
|
370 |
node: - inline locally, typing, clocking (may have to reset the tables |
|
371 |
first), normalization of the node, mpfr injection - recall stage2 *) |
|
372 |
|
|
335 | 373 |
let pp_report fmt report = |
336 | 374 |
let open Format in |
337 | 375 |
fprintf_list ~sep:"@." |
338 | 376 |
(fun _ (nd, als) -> |
339 |
let top = Corelang.node_from_name (nd.node_id) in
|
|
377 |
let top = Corelang.node_from_name nd.node_id in
|
|
340 | 378 |
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 *) |
|
379 |
if |
|
380 |
(not !Options.solve_al) |
|
381 |
|| List.exists (fun (_, _, valid) -> not valid) als |
|
382 |
then Error.pp_error (* at least one failure: erroneous node *) |
|
383 |
else Error.pp_warning |
|
384 |
(* solvable cases: warning only *) |
|
345 | 385 |
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; |
|
386 |
pp top.top_decl_loc (fun fmt -> |
|
387 |
fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}" nd.node_id |
|
388 |
(fprintf_list ~sep:"@ " (pp_al nd)) |
|
389 |
als)) |
|
390 |
fmt report; |
|
353 | 391 |
fprintf fmt "@." |
354 |
|
|
355 |
|
|
356 | 392 |
|
357 | 393 |
let analyze cpt prog = |
358 | 394 |
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 |
); |
|
395 |
Format.fprintf fmt "@[<v 2>Algebraic loop detected: "; |
|
396 |
if !Options.solve_al then Format.fprintf fmt "solving mode actived"; |
|
397 |
Format.fprintf fmt "@ "); |
|
363 | 398 |
let prog, status_ok, report = clean_al prog in |
364 |
|
|
399 |
|
|
365 | 400 |
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 |
) |
|
401 |
if cpt > 0 && !Options.solve_al && status_ok then |
|
402 |
try fast_stages_processing prog with _ -> assert false |
|
403 |
(* Should not happen since the error has been catched already *) |
|
372 | 404 |
else ( |
373 |
(* We stop with unresolved AL *)(* TODO create a report *) |
|
405 |
(* We stop with unresolved AL *) |
|
406 |
(* TODO create a report *) |
|
374 | 407 |
(* Printing the report on stderr *) |
375 | 408 |
Format.eprintf "%a" pp_report report; |
376 |
raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop)) |
|
377 |
) |
|
409 |
raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop))) |
|
378 | 410 |
in |
379 | 411 |
(* Printing the report on stderr *) |
380 | 412 |
Format.eprintf "%a" pp_report report; |
381 | 413 |
res |
382 |
|
|
383 |
let analyze prog = |
|
384 |
analyze !Options.al_nb_max prog |
|
385 |
|
|
386 |
|
|
414 |
|
|
415 |
let analyze prog = analyze !Options.al_nb_max prog |
Also available in: Unified diff
reformatting