lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 3ca27bc7
History | View | Annotate | Download (23 KB)
1 |
|
---|---|
2 |
(* We try to avoid opening modules here *) |
3 |
module ST = Salsa.SalsaTypes |
4 |
module SDT = SalsaDatatypes |
5 |
module LT = LustreSpec |
6 |
module MC = Machine_code |
7 |
|
8 |
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *) |
9 |
open SalsaDatatypes |
10 |
(******************************************************************) |
11 |
(* TODO Xavier: should those functions be declared more globally? *) |
12 |
|
13 |
let fun_types node = |
14 |
try |
15 |
match node.LT.top_decl_desc with |
16 |
| LT.Node nd -> |
17 |
let tin, tout = Types.split_arrow nd.LT.node_type in |
18 |
Types.type_list_of_type tin, Types.type_list_of_type tout |
19 |
| _ -> Format.eprintf "%a is not a node@.@?" Printers.pp_decl node; assert false |
20 |
with Not_found -> Format.eprintf "Unable to find type def for function %s@.@?" (Corelang.node_name node); assert false |
21 |
|
22 |
let called_node_id m id = |
23 |
let td, _ = |
24 |
try |
25 |
List.assoc id m.MC.mcalls (* TODO Xavier: mcalls or minstances ? *) |
26 |
with Not_found -> assert false |
27 |
in |
28 |
td |
29 |
(******************************************************************) |
30 |
|
31 |
(* Returns the set of vars that appear in the expression *) |
32 |
let rec get_expr_real_vars e = |
33 |
match e.LT.value_desc with |
34 |
| LT.LocalVar v | LT.StateVar v when Types.is_real_type v.LT.var_type -> Vars.singleton v |
35 |
| LT.LocalVar _| LT.StateVar _ |
36 |
| LT.Cst _ -> Vars.empty |
37 |
| LT.Fun (_, args) -> |
38 |
List.fold_left |
39 |
(fun acc e -> Vars.union acc (get_expr_real_vars e)) |
40 |
Vars.empty args |
41 |
| LT.Array _ |
42 |
| LT.Access _ |
43 |
| LT.Power _ -> assert false |
44 |
|
45 |
(* Extract the variables to appear as free variables in expressions (lhs) *) |
46 |
let rec get_read_vars instrs = |
47 |
match instrs with |
48 |
[] -> Vars.empty |
49 |
| i::tl -> ( |
50 |
let vars_tl = get_read_vars tl in |
51 |
match Corelang.get_instr_desc i with |
52 |
| LT.MLocalAssign(_,e) |
53 |
| LT.MStateAssign(_,e) -> Vars.union (get_expr_real_vars e) vars_tl |
54 |
| LT.MStep(_, _, el) -> List.fold_left (fun accu e -> Vars.union (get_expr_real_vars e) accu) vars_tl el |
55 |
| LT.MBranch(e, branches) -> ( |
56 |
let vars = Vars.union (get_expr_real_vars e) vars_tl in |
57 |
List.fold_left (fun vars (_, b) -> Vars.union vars (get_read_vars b) ) vars branches |
58 |
) |
59 |
| LT.MReset _ |
60 |
| LT.MNoReset _ |
61 |
| LT.MComment _ -> Vars.empty |
62 |
) |
63 |
|
64 |
let rec get_written_vars instrs = |
65 |
match instrs with |
66 |
[] -> Vars.empty |
67 |
| i::tl -> ( |
68 |
let vars_tl = get_written_vars tl in |
69 |
match Corelang.get_instr_desc i with |
70 |
| LT.MLocalAssign(v,_) |
71 |
| LT.MStateAssign(v,_) -> Vars.add v vars_tl |
72 |
| LT.MStep(vdl, _, _) -> List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl |
73 |
| LT.MBranch(_, branches) -> ( |
74 |
List.fold_left (fun vars (_, b) -> Vars.union vars (get_written_vars b) ) vars_tl branches |
75 |
) |
76 |
| LT.MReset _ |
77 |
| LT.MNoReset _ |
78 |
| LT.MComment _ -> Vars.empty |
79 |
) |
80 |
|
81 |
|
82 |
(* Optimize a given expression. It returns another expression and a computed range. *) |
83 |
let optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option = |
84 |
let rec opt_expr ranges formalEnv e = |
85 |
match e.LT.value_desc with |
86 |
| LT.Cst cst -> |
87 |
Format.eprintf "optmizing constant expr ? @ "; |
88 |
(* the expression is a constant, we optimize it directly if it is a real |
89 |
constant *) |
90 |
let typ = Typing.type_const Location.dummy_loc cst in |
91 |
if Types.is_real_type typ then |
92 |
opt_num_expr ranges formalEnv e |
93 |
else e, None |
94 |
| LT.LocalVar v |
95 |
| LT.StateVar v -> |
96 |
if not (Vars.mem v printed_vars) && |
97 |
(* TODO xAvier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *) |
98 |
(Types.is_real_type e.LT.value_type || Types.is_real_type v.LT.var_type) |
99 |
then |
100 |
opt_num_expr ranges formalEnv e |
101 |
else |
102 |
e, None (* Nothing to optimize for expressions containing a single non real variable *) |
103 |
(* (\* optimize only numerical vars *\) *) |
104 |
(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *) |
105 |
(* else e, None *) |
106 |
| LT.Fun (fun_id, args) -> ( |
107 |
(* necessarily, this is a basic function (ie. + - * / && || mod ... ) *) |
108 |
(* if the return type is real then optimize it, otherwise call recusrsively on arguments *) |
109 |
if Types.is_real_type e.LT.value_type then |
110 |
opt_num_expr ranges formalEnv e |
111 |
else ( |
112 |
(* We do not care for computed local ranges. *) |
113 |
let args' = List.map (fun arg -> let arg', _ = opt_expr ranges formalEnv arg in arg') args in |
114 |
{ e with LT.value_desc = LT.Fun(fun_id, args')}, None |
115 |
) |
116 |
) |
117 |
| LT.Array _ |
118 |
| LT.Access _ |
119 |
| LT.Power _ -> assert false |
120 |
and opt_num_expr ranges formalEnv e = |
121 |
if debug then Format.eprintf "Optimizing expression %a@ " MC.pp_val e; |
122 |
let fresh_id = "toto" in (* TODO more meaningful name *) |
123 |
(* Convert expression *) |
124 |
List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv; |
125 |
let e_salsa : Salsa.SalsaTypes.expression = value_t2salsa_expr constEnv e in |
126 |
Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](* constEnv *) e_salsa) ; |
127 |
|
128 |
(* Convert formalEnv *) |
129 |
if debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; |
130 |
let formalEnv_salsa = |
131 |
FormalEnv.fold (fun id expr accu -> |
132 |
(id, value_t2salsa_expr constEnv expr)::accu |
133 |
) formalEnv [] in |
134 |
if debug then Format.eprintf "Formal env converted to salsa@ "; |
135 |
(* Substitute all occurences of variables by their definition in env *) |
136 |
let (e_salsa: Salsa.SalsaTypes.expression), _ = |
137 |
Salsa.Rewrite.substVars |
138 |
e_salsa |
139 |
formalEnv_salsa |
140 |
0 (* TODO: Nasrine, what is this integer value for ? *) |
141 |
in |
142 |
if debug then Format.eprintf "Substituted def in expr@ "; |
143 |
let abstractEnv = Hashtbl.fold |
144 |
(fun id value accu -> (id,value)::accu) |
145 |
ranges |
146 |
[] |
147 |
in |
148 |
(* List.iter (fun (id, _) -> Format.eprintf "absenv: %s@." id) abstractEnv; *) |
149 |
(* The expression is partially evaluated by the available ranges |
150 |
valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on |
151 |
garde evalPartExpr remplace les variables e qui sont dans env par la cst |
152 |
- on garde *) |
153 |
if debug then Format.eprintf "avant avant eval part@ "; |
154 |
Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); |
155 |
let e_salsa = |
156 |
Salsa.Float.evalPartExpr |
157 |
e_salsa |
158 |
(Salsa.Float.valEnv2ExprEnv abstractEnv) |
159 |
([] (* no blacklisted variables *)) |
160 |
in |
161 |
Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); |
162 |
(* Checking if we have all necessary information *) |
163 |
|
164 |
let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in |
165 |
|
166 |
if Vars.cardinal free_vars > 0 then ( |
167 |
Format.eprintf "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " |
168 |
Vars.pp (Vars.fold (fun v accu -> let v' = {v with LT.var_id = nodename ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty) |
169 |
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); |
170 |
if debug then Format.eprintf "Some free vars, not optimizing@."; |
171 |
let new_e = try salsa_expr2value_t vars_env constEnv e_salsa with Not_found -> assert false in |
172 |
new_e, None |
173 |
) |
174 |
else ( |
175 |
try |
176 |
if debug then |
177 |
Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ " |
178 |
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa) |
179 |
(Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv |
180 |
; |
181 |
|
182 |
let new_e_salsa, e_val = |
183 |
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv |
184 |
in |
185 |
let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa with Not_found -> assert false in |
186 |
if debug then Format.eprintf "@ @[<v>old: %a@ new: %a@ range: %a@]" MC.pp_val e MC.pp_val new_e RangesInt.pp_val e_val; |
187 |
new_e, Some e_val |
188 |
with Not_found -> assert false |
189 |
| Salsa.Epeg_types.EPEGError _ -> ( |
190 |
Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e; |
191 |
e, None |
192 |
) |
193 |
) |
194 |
|
195 |
|
196 |
|
197 |
in |
198 |
if debug then |
199 |
Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ " |
200 |
MC.pp_val e |
201 |
FormalEnv.pp formalEnv |
202 |
RangesInt.pp ranges; |
203 |
let res = opt_expr ranges formalEnv e in |
204 |
Format.eprintf "@]@ "; |
205 |
res |
206 |
|
207 |
|
208 |
|
209 |
(* Returns a list of assign, for each var in vars_to_print, that produce the |
210 |
definition of it according to formalEnv, and driven by the ranges. *) |
211 |
let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print = |
212 |
(* We print thhe expression in the order of definition *) |
213 |
|
214 |
let ordered_vars = |
215 |
List.stable_sort |
216 |
(FormalEnv.get_sort_fun formalEnv) |
217 |
(Vars.elements vars_to_print) |
218 |
in |
219 |
Format.eprintf "Printing vars in the following order: [%a]@ " (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars ; |
220 |
List.fold_right ( |
221 |
fun v (accu_instr, accu_ranges) -> |
222 |
if debug then Format.eprintf "Printing assign for variable %s@ " v.LT.var_id; |
223 |
try |
224 |
(* Obtaining unfold expression of v in formalEnv *) |
225 |
let v_def = FormalEnv.get_def formalEnv v in |
226 |
let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in |
227 |
let instr_desc = |
228 |
if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then |
229 |
LT.MLocalAssign(v, e) |
230 |
else |
231 |
LT.MStateAssign(v, e) |
232 |
in |
233 |
(Corelang.mkinstr instr_desc)::accu_instr, |
234 |
(match r with |
235 |
| None -> ranges |
236 |
| Some v_r -> RangesInt.add_def ranges v.LT.var_id v_r) |
237 |
with FormalEnv.NoDefinition _ -> ( |
238 |
(* It should not happen with C backend, but may happen with Lustre backend *) |
239 |
if !Options.output = "lustre" then accu_instr, ranges else (Format.eprintf "@?"; assert false) |
240 |
) |
241 |
) ordered_vars ([], ranges) |
242 |
|
243 |
(* Main recursive function: modify the instructions list while preserving the |
244 |
order of assigns for state variables. Returns a quintuple: (new_instrs, |
245 |
ranges, formalEnv, printed_vars, and remaining vars to be printed) *) |
246 |
let rec rewrite_instrs nodename constEnv vars_env m instrs ranges formalEnv printed_vars vars_to_print = |
247 |
let assign_vars = assign_vars nodename constEnv vars_env in |
248 |
if debug then ( |
249 |
Format.eprintf "------------@ "; |
250 |
Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars; |
251 |
Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; |
252 |
); |
253 |
match instrs with |
254 |
| [] -> |
255 |
(* End of instruction list: we produce the definition of each variable that |
256 |
appears in vars_to_print. Each of them should be defined in formalEnv *) |
257 |
if debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; |
258 |
let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in |
259 |
instrs, |
260 |
ranges', |
261 |
formalEnv, |
262 |
Vars.union printed_vars vars_to_print, (* We should have printed all required vars *) |
263 |
[] (* No more vars to be printed *) |
264 |
|
265 |
| hd_instr::tl_instrs -> |
266 |
(* We reformulate hd_instr, producing or not a fresh instruction, updating |
267 |
formalEnv, possibly ranges and vars_to_print *) |
268 |
begin |
269 |
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print = |
270 |
match Corelang.get_instr_desc hd_instr with |
271 |
| LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && not (Vars.mem vd vars_to_print) -> |
272 |
(* LocalAssign are injected into formalEnv *) |
273 |
if debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; |
274 |
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) |
275 |
[], (* no instr generated *) |
276 |
ranges, (* no new range computed *) |
277 |
formalEnv', |
278 |
printed_vars, (* no new printed vars *) |
279 |
vars_to_print (* no more or less variables to print *) |
280 |
|
281 |
| LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print -> |
282 |
|
283 |
if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; |
284 |
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) |
285 |
let instrs', ranges' = (* printing vd = optimized vt *) |
286 |
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) |
287 |
in |
288 |
instrs', |
289 |
ranges', (* no new range computed *) |
290 |
formalEnv', (* formelEnv already updated *) |
291 |
Vars.add vd printed_vars, (* adding vd to new printed vars *) |
292 |
Vars.remove vd vars_to_print (* removed vd from variables to print *) |
293 |
|
294 |
| LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print -> |
295 |
|
296 |
(* StateAssign are produced since they are required by the function. We still |
297 |
keep their definition in the formalEnv in case it can optimize later |
298 |
outputs. vd is removed from remaining vars_to_print *) |
299 |
if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; |
300 |
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) |
301 |
let instrs', ranges' = (* printing vd = optimized vt *) |
302 |
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) |
303 |
in |
304 |
instrs', |
305 |
ranges', (* no new range computed *) |
306 |
formalEnv, (* formelEnv already updated *) |
307 |
Vars.add vd printed_vars, (* adding vd to new printed vars *) |
308 |
Vars.remove vd vars_to_print (* removed vd from variables to print *) |
309 |
|
310 |
| (LT.MLocalAssign(vd,vt) | LT.MStateAssign(vd,vt)) -> |
311 |
(* We have to produce the instruction. But we may have to produce as |
312 |
well its dependencies *) |
313 |
let required_vars = get_expr_real_vars vt in |
314 |
let required_vars = Vars.diff required_vars printed_vars in (* remove |
315 |
already |
316 |
produced |
317 |
variables *) |
318 |
let prefix_instr, ranges = |
319 |
assign_vars printed_vars ranges formalEnv required_vars in |
320 |
let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in |
321 |
let new_instr = |
322 |
match Corelang.get_instr_desc hd_instr with |
323 |
| LT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (LT.MLocalAssign(vd,vt')) |
324 |
| _ -> Corelang.update_instr_desc hd_instr (LT.MStateAssign(vd,vt')) |
325 |
in |
326 |
let written_vars = Vars.add vd required_vars in |
327 |
prefix_instr@[new_instr], |
328 |
ranges, (* no new range computed *) |
329 |
formalEnv, (* formelEnv untouched *) |
330 |
Vars.union written_vars printed_vars, (* adding vd + dependencies to |
331 |
new printed vars *) |
332 |
Vars.diff vars_to_print written_vars (* removed vd + dependencies from |
333 |
variables to print *) |
334 |
|
335 |
| LT.MStep(vdl,id,vtl) -> |
336 |
if debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; |
337 |
(* Call of an external function. Input expressions have to be |
338 |
optimized, their free variables produced. A fresh range has to be |
339 |
computed for each output variable in vdl. Output of the function |
340 |
call are removed from vars to be printed *) |
341 |
let node = called_node_id m id in |
342 |
let node_id = Corelang.node_name node in |
343 |
let tin, tout = (* special care for arrow *) |
344 |
if node_id = "_arrow" then |
345 |
match vdl with |
346 |
| [v] -> let t = v.LT.var_type in |
347 |
[t; t], [t] |
348 |
| _ -> assert false (* should not happen *) |
349 |
else |
350 |
fun_types node |
351 |
in |
352 |
if debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; |
353 |
let vtl', vtl_ranges = List.fold_right2 ( |
354 |
fun e typ_e (exprl, range_l)-> |
355 |
if Types.is_real_type typ_e then |
356 |
let e', r' = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e in |
357 |
e'::exprl, r'::range_l |
358 |
else |
359 |
e::exprl, None::range_l |
360 |
) vtl tin ([], []) |
361 |
in |
362 |
if debug then Format.eprintf "... done@ @]@ "; |
363 |
let required_vars = |
364 |
List.fold_left2 |
365 |
(fun accu e typ_e -> |
366 |
if Types.is_real_type typ_e then |
367 |
Vars.union accu (get_expr_real_vars e) |
368 |
else (* we do not consider non real expressions *) |
369 |
accu |
370 |
) |
371 |
Vars.empty |
372 |
vtl' tin |
373 |
in |
374 |
if debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " |
375 |
Vars.pp required_vars |
376 |
Vars.pp printed_vars |
377 |
Vars.pp (Vars.diff required_vars printed_vars) |
378 |
; |
379 |
let required_vars = Vars.diff required_vars printed_vars in (* remove |
380 |
already |
381 |
produced |
382 |
variables *) |
383 |
let written_vars = Vars.union required_vars (Vars.of_list vdl) in |
384 |
let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in |
385 |
instrs' @ [Corelang.update_instr_desc hd_instr (LT.MStep(vdl,id,vtl'))], (* New instrs *) |
386 |
RangesInt.add_call ranges' vdl id vtl_ranges, (* add information bounding each vdl var *) |
387 |
formalEnv, |
388 |
Vars.union written_vars printed_vars, (* adding vdl to new printed vars *) |
389 |
Vars.diff vars_to_print written_vars |
390 |
|
391 |
| LT.MBranch(vt, branches) -> |
392 |
(* Required variables to compute vt are introduced. |
393 |
Then each branch is refactored specifically |
394 |
*) |
395 |
if debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; |
396 |
let required_vars = get_expr_real_vars vt in |
397 |
let required_vars = Vars.diff required_vars printed_vars in (* remove |
398 |
already |
399 |
produced |
400 |
variables *) |
401 |
let prefix_instr, ranges = |
402 |
assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in |
403 |
|
404 |
let printed_vars = Vars.union printed_vars required_vars in |
405 |
|
406 |
let vt', _ = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv vt in |
407 |
|
408 |
let read_vars_tl = get_read_vars tl_instrs in |
409 |
if debug then Format.eprintf "@[<v 2>Dealing with branches@ "; |
410 |
let branches', written_vars, merged_ranges = List.fold_right ( |
411 |
fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) -> |
412 |
let b_write_vars = get_written_vars b_instrs in |
413 |
let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in |
414 |
let b_fe = formalEnv in (* because of side effect |
415 |
data, we copy it for |
416 |
each branch *) |
417 |
let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = |
418 |
rewrite_instrs nodename constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print |
419 |
in |
420 |
(* b_vars should be empty *) |
421 |
let _ = if b_vars != [] then assert false in |
422 |
|
423 |
(* Producing the refactored branch *) |
424 |
(b_l, b_instrs') :: new_branches, |
425 |
Vars.union b_printed written_vars, (* They should coincides. We |
426 |
use union instead of |
427 |
inter to ease the |
428 |
bootstrap *) |
429 |
RangesInt.merge merged_ranges b_ranges |
430 |
|
431 |
) branches ([], required_vars, ranges) in |
432 |
if debug then Format.eprintf "dealing with branches done@ @]@ "; |
433 |
prefix_instr@[Corelang.update_instr_desc hd_instr (LT.MBranch(vt', branches'))], |
434 |
merged_ranges, (* Only step functions call within branches |
435 |
may have produced new ranges. We merge this data by |
436 |
computing the join per variable *) |
437 |
formalEnv, (* Thanks to the computation of var_to_print in each |
438 |
branch, no new definition should have been computed |
439 |
without being already printed *) |
440 |
Vars.union written_vars printed_vars, |
441 |
Vars.diff vars_to_print written_vars (* We remove vars that have been |
442 |
produced within branches *) |
443 |
|
444 |
|
445 |
| LT.MReset(_) | LT.MNoReset _ | LT.MComment _ -> |
446 |
if debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; |
447 |
|
448 |
(* Untouched instruction *) |
449 |
[ hd_instr ], (* unmodified instr *) |
450 |
ranges, (* no new range computed *) |
451 |
formalEnv, (* no formelEnv update *) |
452 |
printed_vars, |
453 |
vars_to_print (* no more or less variables to print *) |
454 |
|
455 |
in |
456 |
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = |
457 |
rewrite_instrs |
458 |
nodename |
459 |
constEnv |
460 |
vars_env |
461 |
m |
462 |
tl_instrs |
463 |
ranges |
464 |
formalEnv |
465 |
printed_vars |
466 |
vars_to_print |
467 |
in |
468 |
hd_instrs @ tl_instrs, |
469 |
ranges, |
470 |
formalEnv, |
471 |
printed_vars, |
472 |
vars_to_print |
473 |
end |
474 |
|
475 |
|
476 |
|
477 |
|
478 |
|
479 |
|
480 |
(* TODO: deal with new variables, ie. tmp *) |
481 |
let salsaStep constEnv m s = |
482 |
let ranges = RangesInt.empty (* empty for the moment, should be build from |
483 |
machine annotations or externally provided information *) in |
484 |
let annots = List.fold_left ( |
485 |
fun accu annl -> |
486 |
List.fold_left ( |
487 |
fun accu (key, range) -> |
488 |
match key with |
489 |
| ["salsa"; "ranges"; var] -> (var, range)::accu |
490 |
| _ -> accu |
491 |
) accu annl.LT.annots |
492 |
) [] m.MC.mannot |
493 |
in |
494 |
let ranges = |
495 |
List.fold_left (fun ranges (v, value) -> |
496 |
match value.LT.eexpr_qfexpr.LT.expr_desc with |
497 |
| LT.Expr_tuple [minv; maxv] -> ( |
498 |
let get_cst e = match e.LT.expr_desc with |
499 |
| LT.Expr_const (LT.Const_real (c,e,s)) -> |
500 |
(* calculer la valeur c * 10^e *) |
501 |
Num.float_of_num (Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))) |
502 |
| _ -> |
503 |
Format.eprintf |
504 |
"Invalid scala range: %a. It should be a pair of constant floats.@." |
505 |
Printers.pp_expr value.LT.eexpr_qfexpr; |
506 |
assert false |
507 |
in |
508 |
let minv, maxv = get_cst minv, get_cst maxv in |
509 |
if debug then Format.eprintf "%s in [%f, %f]@ " v minv maxv; |
510 |
RangesInt.enlarge ranges v (Salsa.SalsaTypes.I(minv, maxv),Salsa.SalsaTypes.J(0.,0.)) |
511 |
) |
512 |
| _ -> |
513 |
Format.eprintf |
514 |
"Invalid scala range: %a. It should be a pair of floats.@." |
515 |
Printers.pp_expr value.LT.eexpr_qfexpr; |
516 |
assert false |
517 |
) ranges annots |
518 |
in |
519 |
let formal_env = FormalEnv.empty () in |
520 |
let vars_to_print = |
521 |
Vars.real_vars |
522 |
( |
523 |
Vars.union |
524 |
(Vars.of_list m.MC.mmemory) |
525 |
(Vars.of_list s.MC.step_outputs) |
526 |
) |
527 |
in |
528 |
(* TODO: should be at least step output + may be memories *) |
529 |
let vars_env = compute_vars_env m in |
530 |
let new_instrs, _, _, printed_vars, _ = |
531 |
rewrite_instrs |
532 |
m.MC.mname.LT.node_id |
533 |
constEnv |
534 |
vars_env |
535 |
m |
536 |
s.MC.step_instrs |
537 |
ranges |
538 |
formal_env |
539 |
(Vars.real_vars (Vars.of_list s.MC.step_inputs (* printed_vars : real |
540 |
inputs are considered as |
541 |
already printed *))) |
542 |
vars_to_print |
543 |
in |
544 |
let all_local_vars = Vars.real_vars (Vars.of_list s.MC.step_locals) in |
545 |
let unused = (Vars.diff all_local_vars printed_vars) in |
546 |
let locals = |
547 |
if not (Vars.is_empty unused) then ( |
548 |
Format.eprintf "Unused local vars: [%a]. Removing them.@.@?" |
549 |
Vars.pp unused; |
550 |
List.filter (fun v -> not (Vars.mem v unused)) s.MC.step_locals |
551 |
) |
552 |
else |
553 |
s.MC.step_locals |
554 |
in |
555 |
{ s with MC.step_instrs = new_instrs; MC.step_locals = locals } (* we have also to modify local variables to declare new vars *) |
556 |
|
557 |
|
558 |
let machine_t2machine_t_optimized_by_salsa constEnv mt = |
559 |
try |
560 |
if debug then Format.eprintf "@[<v 2>------------------ Optimizing machine %s@ " mt.MC.mname.LT.node_id; |
561 |
let new_step = salsaStep constEnv mt mt.MC.mstep in |
562 |
if debug then Format.eprintf "@]@."; |
563 |
{ mt with MC.mstep = new_step } |
564 |
|
565 |
|
566 |
with FormalEnv.NoDefinition v as exp -> |
567 |
Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; |
568 |
raise exp |
569 |
|
570 |
|
571 |
(* Local Variables: *) |
572 |
(* compile-command:"make -C ../../.." *) |
573 |
(* End: *) |
574 |
|