lustrec / src / plugins / salsa / machine_salsa_opt.ml @ 53206908
History  View  Annotate  Download (22.7 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 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.MComment _ > Vars.empty 
61 
) 
62  
63 
let rec get_written_vars instrs = 
64 
match instrs with 
65 
[] > Vars.empty 
66 
 i::tl > ( 
67 
let vars_tl = get_written_vars tl in 
68 
match i with 
69 
 LT.MLocalAssign(v,_) 
70 
 LT.MStateAssign(v,_) > Vars.add v vars_tl 
71 
 LT.MStep(vdl, _, _) > List.fold_left (fun accu v > Vars.add v accu) vars_tl vdl 
72 
 LT.MBranch(_, branches) > ( 
73 
List.fold_left (fun vars (_, b) > Vars.union vars (get_written_vars b) ) vars_tl branches 
74 
) 
75 
 LT.MReset _ 
76 
 LT.MComment _ > Vars.empty 
77 
) 
78  
79  
80 
(* Optimize a given expression. It returns another expression and a computed range. *) 
81 
let optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option = 
82 
let rec opt_expr ranges formalEnv e = 
83 
match e.LT.value_desc with 
84 
 LT.Cst cst > 
85 
Format.eprintf "optmizing constant expr ? @ "; 
86 
(* the expression is a constant, we optimize it directly if it is a real 
87 
constant *) 
88 
let typ = Typing.type_const Location.dummy_loc cst in 
89 
if Types.is_real_type typ then 
90 
opt_num_expr ranges formalEnv e 
91 
else e, None 
92 
 LT.LocalVar v 
93 
 LT.StateVar v > 
94 
if not (Vars.mem v printed_vars) && 
95 
(* TODO xAvier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *) 
96 
(Types.is_real_type e.LT.value_type  Types.is_real_type v.LT.var_type) 
97 
then 
98 
opt_num_expr ranges formalEnv e 
99 
else 
100 
e, None (* Nothing to optimize for expressions containing a single non real variable *) 
101 
(* (\* optimize only numerical vars *\) *) 
102 
(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *) 
103 
(* else e, None *) 
104 
 LT.Fun (fun_id, args) > ( 
105 
(* necessarily, this is a basic function (ie. +  * / &&  mod ... ) *) 
106 
(* if the return type is real then optimize it, otherwise call recusrsively on arguments *) 
107 
if Types.is_real_type e.LT.value_type then 
108 
opt_num_expr ranges formalEnv e 
109 
else ( 
110 
(* We do not care for computed local ranges. *) 
111 
let args' = List.map (fun arg > let arg', _ = opt_expr ranges formalEnv arg in arg') args in 
112 
{ e with LT.value_desc = LT.Fun(fun_id, args')}, None 
113 
) 
114 
) 
115 
 LT.Array _ 
116 
 LT.Access _ 
117 
 LT.Power _ > assert false 
118 
and opt_num_expr ranges formalEnv e = 
119 
if debug then Format.eprintf "Optimizing expression %a@ " MC.pp_val e; 
120 
let fresh_id = "toto" in (* TODO more meaningful name *) 
121 
(* Convert expression *) 
122 
List.iter (fun (l,c) > Format.eprintf "%s > %a@ " l Printers.pp_const c) constEnv; 
123 
let e_salsa : Salsa.SalsaTypes.expression = value_t2salsa_expr constEnv e in 
124 
Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](* constEnv *) e_salsa) ; 
125  
126 
(* Convert formalEnv *) 
127 
if debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; 
128 
let formalEnv_salsa = 
129 
FormalEnv.fold (fun id expr accu > 
130 
(id, value_t2salsa_expr constEnv expr)::accu 
131 
) formalEnv [] in 
132 
if debug then Format.eprintf "Formal env converted to salsa@ "; 
133 
(* Substitute all occurences of variables by their definition in env *) 
134 
let (e_salsa: Salsa.SalsaTypes.expression), _ = 
135 
Salsa.Rewrite.substVars 
136 
e_salsa 
137 
formalEnv_salsa 
138 
0 (* TODO: Nasrine, what is this integer value for ? *) 
139 
in 
140 
if debug then Format.eprintf "Substituted def in expr@ "; 
141 
let abstractEnv = Hashtbl.fold 
142 
(fun id value accu > (id,value)::accu) 
143 
ranges 
144 
[] 
145 
in 
146 
(* List.iter (fun (id, _) > Format.eprintf "absenv: %s@." id) abstractEnv; *) 
147 
(* The expression is partially evaluated by the available ranges 
148 
valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv  on 
149 
garde evalPartExpr remplace les variables e qui sont dans env par la cst 
150 
 on garde *) 
151 
if debug then Format.eprintf "avant avant eval part@ "; 
152 
Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); 
153 
let e_salsa = 
154 
Salsa.Float.evalPartExpr 
155 
e_salsa 
156 
(Salsa.Float.valEnv2ExprEnv abstractEnv) 
157 
([] (* no blacklisted variables *)) 
158 
in 
159 
Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); 
160 
(* Checking if we have all necessary information *) 
161  
162 
let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in 
163  
164 
if Vars.cardinal free_vars > 0 then ( 
165 
Format.eprintf "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
166 
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) 
167 
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); 
168 
if debug then Format.eprintf "Some free vars, not optimizing@."; 
169 
let new_e = try salsa_expr2value_t vars_env constEnv e_salsa with Not_found > assert false in 
170 
new_e, None 
171 
) 
172 
else ( 
173 
try 
174 
if debug then 
175 
Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ " 
176 
MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa) 
177 
(Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) > Format.fprintf fmt "%s > %a" l FloatIntSalsa.pp r)) abstractEnv 
178 
; 
179 

180 
let new_e_salsa, e_val = 
181 
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv 
182 
in 
183 
let new_e = try salsa_expr2value_t vars_env constEnv new_e_salsa with Not_found > assert false in 
184 
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; 
185 
new_e, Some e_val 
186 
with Not_found > assert false 
187 
 Salsa.Epeg_types.EPEGError _ > ( 
188 
Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e; 
189 
e, None 
190 
) 
191 
) 
192  
193  
194  
195 
in 
196 
if debug then 
197 
Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ " 
198 
MC.pp_val e 
199 
FormalEnv.pp formalEnv 
200 
RangesInt.pp ranges; 
201 
let res = opt_expr ranges formalEnv e in 
202 
Format.eprintf "@]@ "; 
203 
res 
204  
205 

206 

207 
(* Returns a list of assign, for each var in vars_to_print, that produce the 
208 
definition of it according to formalEnv, and driven by the ranges. *) 
209 
let assign_vars nodename constEnv vars_env printed_vars ranges formalEnv vars_to_print = 
210 
(* We print thhe expression in the order of definition *) 
211  
212 
let ordered_vars = 
213 
List.stable_sort 
214 
(FormalEnv.get_sort_fun formalEnv) 
215 
(Vars.elements vars_to_print) 
216 
in 
217 
Format.eprintf "Printing vars in the following order: [%a]@ " (Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars ; 
218 
List.fold_right ( 
219 
fun v (accu_instr, accu_ranges) > 
220 
if debug then Format.eprintf "Printing assign for variable %s@ " v.LT.var_id; 
221 
try 
222 
(* Obtaining unfold expression of v in formalEnv *) 
223 
let v_def = FormalEnv.get_def formalEnv v in 
224 
let e, r = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv v_def in 
225 
let instr = 
226 
if try (get_var vars_env v.LT.var_id).is_local with Not_found > assert false then 
227 
LT.MLocalAssign(v, e) 
228 
else 
229 
LT.MStateAssign(v, e) 
230 
in 
231 
instr::accu_instr, 
232 
(match r with 
233 
 None > ranges 
234 
 Some v_r > RangesInt.add_def ranges v.LT.var_id v_r) 
235 
with FormalEnv.NoDefinition _ > ( 
236 
(* It should not happen with C backend, but may happen with Lustre backend *) 
237 
if !Options.output = "lustre" then accu_instr, ranges else (Format.eprintf "@?"; assert false) 
238 
) 
239 
) ordered_vars ([], ranges) 
240  
241 
(* Main recursive function: modify the instructions list while preserving the 
242 
order of assigns for state variables. Returns a quintuple: (new_instrs, 
243 
ranges, formalEnv, printed_vars, and remaining vars to be printed) *) 
244 
let rec rewrite_instrs nodename constEnv vars_env m instrs ranges formalEnv printed_vars vars_to_print = 
245 
let assign_vars = assign_vars nodename constEnv vars_env in 
246 
if debug then ( 
247 
Format.eprintf "@ "; 
248 
Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars; 
249 
Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; 
250 
); 
251 
match instrs with 
252 
 [] > 
253 
(* End of instruction list: we produce the definition of each variable that 
254 
appears in vars_to_print. Each of them should be defined in formalEnv *) 
255 
if debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; 
256 
let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in 
257 
instrs, 
258 
ranges', 
259 
formalEnv, 
260 
Vars.union printed_vars vars_to_print, (* We should have printed all required vars *) 
261 
[] (* No more vars to be printed *) 
262  
263 
 hd_instr::tl_instrs > 
264 
(* We reformulate hd_instr, producing or not a fresh instruction, updating 
265 
formalEnv, possibly ranges and vars_to_print *) 
266 
begin 
267 
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
268 
match hd_instr with 
269 
 LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && not (Vars.mem vd vars_to_print) > 
270 
(* LocalAssign are injected into formalEnv *) 
271 
if debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; 
272 
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
273 
[], (* no instr generated *) 
274 
ranges, (* no new range computed *) 
275 
formalEnv', 
276 
printed_vars, (* no new printed vars *) 
277 
vars_to_print (* no more or less variables to print *) 
278 

279 
 LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print > 
280  
281 
if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; 
282 
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
283 
let instrs', ranges' = (* printing vd = optimized vt *) 
284 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) 
285 
in 
286 
instrs', 
287 
ranges', (* no new range computed *) 
288 
formalEnv', (* formelEnv already updated *) 
289 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 
290 
Vars.remove vd vars_to_print (* removed vd from variables to print *) 
291  
292 
 LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print > 
293  
294 
(* StateAssign are produced since they are required by the function. We still 
295 
keep their definition in the formalEnv in case it can optimize later 
296 
outputs. vd is removed from remaining vars_to_print *) 
297 
if debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; 
298 
let formalEnv' = FormalEnv.def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
299 
let instrs', ranges' = (* printing vd = optimized vt *) 
300 
assign_vars printed_vars ranges formalEnv (Vars.singleton vd) 
301 
in 
302 
instrs', 
303 
ranges', (* no new range computed *) 
304 
formalEnv, (* formelEnv already updated *) 
305 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 
306 
Vars.remove vd vars_to_print (* removed vd from variables to print *) 
307  
308 
 (LT.MLocalAssign(vd,vt)  LT.MStateAssign(vd,vt)) > 
309 
(* We have to produce the instruction. But we may have to produce as 
310 
well its dependencies *) 
311 
let required_vars = get_expr_real_vars vt in 
312 
let required_vars = Vars.diff required_vars printed_vars in (* remove 
313 
already 
314 
produced 
315 
variables *) 
316 
let prefix_instr, ranges = 
317 
assign_vars printed_vars ranges formalEnv required_vars in 
318 
let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in 
319 
let new_instr = 
320 
match hd_instr with 
321 
 LT.MLocalAssign _ > LT.MLocalAssign(vd,vt') 
322 
 _ > LT.MStateAssign(vd,vt') 
323 
in 
324 
let written_vars = Vars.add vd required_vars in 
325 
prefix_instr@[new_instr], 
326 
ranges, (* no new range computed *) 
327 
formalEnv, (* formelEnv untouched *) 
328 
Vars.union written_vars printed_vars, (* adding vd + dependencies to 
329 
new printed vars *) 
330 
Vars.diff vars_to_print written_vars (* removed vd + dependencies from 
331 
variables to print *) 
332  
333 
 LT.MStep(vdl,id,vtl) > 
334 
if debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; 
335 
(* Call of an external function. Input expressions have to be 
336 
optimized, their free variables produced. A fresh range has to be 
337 
computed for each output variable in vdl. Output of the function 
338 
call are removed from vars to be printed *) 
339 
let node = called_node_id m id in 
340 
let node_id = Corelang.node_name node in 
341 
let tin, tout = (* special care for arrow *) 
342 
if node_id = "_arrow" then 
343 
match vdl with 
344 
 [v] > let t = v.LT.var_type in 
345 
[t; t], [t] 
346 
 _ > assert false (* should not happen *) 
347 
else 
348 
fun_types node 
349 
in 
350 
if debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; 
351 
let vtl', vtl_ranges = List.fold_right2 ( 
352 
fun e typ_e (exprl, range_l)> 
353 
if Types.is_real_type typ_e then 
354 
let e', r' = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv e in 
355 
e'::exprl, r'::range_l 
356 
else 
357 
e::exprl, None::range_l 
358 
) vtl tin ([], []) 
359 
in 
360 
if debug then Format.eprintf "... done@ @]@ "; 
361 
let required_vars = 
362 
List.fold_left2 
363 
(fun accu e typ_e > 
364 
if Types.is_real_type typ_e then 
365 
Vars.union accu (get_expr_real_vars e) 
366 
else (* we do not consider non real expressions *) 
367 
accu 
368 
) 
369 
Vars.empty 
370 
vtl' tin 
371 
in 
372 
if debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " 
373 
Vars.pp required_vars 
374 
Vars.pp printed_vars 
375 
Vars.pp (Vars.diff required_vars printed_vars) 
376 
; 
377 
let required_vars = Vars.diff required_vars printed_vars in (* remove 
378 
already 
379 
produced 
380 
variables *) 
381 
let written_vars = Vars.union required_vars (Vars.of_list vdl) in 
382 
let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in 
383 
instrs' @ [LT.MStep(vdl,id,vtl')], (* New instrs *) 
384 
RangesInt.add_call ranges' vdl id vtl_ranges, (* add information bounding each vdl var *) 
385 
formalEnv, 
386 
Vars.union written_vars printed_vars, (* adding vdl to new printed vars *) 
387 
Vars.diff vars_to_print written_vars 
388 

389 
 LT.MBranch(vt, branches) > 
390 
(* Required variables to compute vt are introduced. 
391 
Then each branch is refactored specifically 
392 
*) 
393 
if debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; 
394 
let required_vars = get_expr_real_vars vt in 
395 
let required_vars = Vars.diff required_vars printed_vars in (* remove 
396 
already 
397 
produced 
398 
variables *) 
399 
let prefix_instr, ranges = 
400 
assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in 
401  
402 
let printed_vars = Vars.union printed_vars required_vars in 
403  
404 
let vt', _ = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv vt in 
405  
406 
let read_vars_tl = get_read_vars tl_instrs in 
407 
if debug then Format.eprintf "@[<v 2>Dealing with branches@ "; 
408 
let branches', written_vars, merged_ranges = List.fold_right ( 
409 
fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) > 
410 
let b_write_vars = get_written_vars b_instrs in 
411 
let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
412 
let b_fe = formalEnv in (* because of side effect 
413 
data, we copy it for 
414 
each branch *) 
415 
let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 
416 
rewrite_instrs nodename constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
417 
in 
418 
(* b_vars should be empty *) 
419 
let _ = if b_vars != [] then assert false in 
420 

421 
(* Producing the refactored branch *) 
422 
(b_l, b_instrs') :: new_branches, 
423 
Vars.union b_printed written_vars, (* They should coincides. We 
424 
use union instead of 
425 
inter to ease the 
426 
bootstrap *) 
427 
RangesInt.merge merged_ranges b_ranges 
428 

429 
) branches ([], required_vars, ranges) in 
430 
if debug then Format.eprintf "dealing with branches done@ @]@ "; 
431 
prefix_instr@[LT.MBranch(vt', branches')], 
432 
merged_ranges, (* Only step functions call within branches 
433 
may have produced new ranges. We merge this data by 
434 
computing the join per variable *) 
435 
formalEnv, (* Thanks to the computation of var_to_print in each 
436 
branch, no new definition should have been computed 
437 
without being already printed *) 
438 
Vars.union written_vars printed_vars, 
439 
Vars.diff vars_to_print written_vars (* We remove vars that have been 
440 
produced within branches *) 
441  
442  
443 
 LT.MReset(_)  LT.MComment _ > 
444 
if debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; 
445  
446 
(* Untouched instruction *) 
447 
[ hd_instr ], (* unmodified instr *) 
448 
ranges, (* no new range computed *) 
449 
formalEnv, (* no formelEnv update *) 
450 
printed_vars, 
451 
vars_to_print (* no more or less variables to print *) 
452 

453 
in 
454 
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 
455 
rewrite_instrs 
456 
nodename 
457 
constEnv 
458 
vars_env 
459 
m 
460 
tl_instrs 
461 
ranges 
462 
formalEnv 
463 
printed_vars 
464 
vars_to_print 
465 
in 
466 
hd_instrs @ tl_instrs, 
467 
ranges, 
468 
formalEnv, 
469 
printed_vars, 
470 
vars_to_print 
471 
end 
472  
473  
474  
475  
476  
477  
478 
(* TODO: deal with new variables, ie. tmp *) 
479 
let salsaStep constEnv m s = 
480 
let ranges = RangesInt.empty (* empty for the moment, should be build from 
481 
machine annotations or externally provided information *) in 
482 
let annots = List.fold_left ( 
483 
fun accu annl > 
484 
List.fold_left ( 
485 
fun accu (key, range) > 
486 
match key with 
487 
 ["salsa"; "ranges"; var] > (var, range)::accu 
488 
 _ > accu 
489 
) accu annl.LT.annots 
490 
) [] m.MC.mannot 
491 
in 
492 
let ranges = 
493 
List.fold_left (fun ranges (v, value) > 
494 
match value.LT.eexpr_qfexpr.LT.expr_desc with 
495 
 LT.Expr_tuple [minv; maxv] > ( 
496 
let get_cst e = match e.LT.expr_desc with 
497 
 LT.Expr_const (LT.Const_real (c,e,s)) > 
498 
(* calculer la valeur c * 10^e *) 
499 
Num.float_of_num (Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))) 
500 
 _ > 
501 
Format.eprintf 
502 
"Invalid scala range: %a. It should be a pair of constant floats.@." 
503 
Printers.pp_expr value.LT.eexpr_qfexpr; 
504 
assert false 
505 
in 
506 
let minv, maxv = get_cst minv, get_cst maxv in 
507 
if debug then Format.eprintf "%s in [%f, %f]@ " v minv maxv; 
508 
RangesInt.enlarge ranges v (Salsa.SalsaTypes.I(minv, maxv),Salsa.SalsaTypes.J(0.,0.)) 
509 
) 
510 
 _ > 
511 
Format.eprintf 
512 
"Invalid scala range: %a. It should be a pair of floats.@." 
513 
Printers.pp_expr value.LT.eexpr_qfexpr; 
514 
assert false 
515 
) ranges annots 
516 
in 
517 
let formal_env = FormalEnv.empty () in 
518 
let vars_to_print = 
519 
Vars.real_vars 
520 
( 
521 
Vars.union 
522 
(Vars.of_list m.MC.mmemory) 
523 
(Vars.of_list s.MC.step_outputs) 
524 
) 
525 
in 
526 
(* TODO: should be at least step output + may be memories *) 
527 
let vars_env = compute_vars_env m in 
528 
let new_instrs, _, _, printed_vars, _ = 
529 
rewrite_instrs 
530 
m.MC.mname.LT.node_id 
531 
constEnv 
532 
vars_env 
533 
m 
534 
s.MC.step_instrs 
535 
ranges 
536 
formal_env 
537 
(Vars.real_vars (Vars.of_list s.MC.step_inputs (* printed_vars : real 
538 
inputs are considered as 
539 
already printed *))) 
540 
vars_to_print 
541 
in 
542 
let all_local_vars = Vars.real_vars (Vars.of_list s.MC.step_locals) in 
543 
let unused = (Vars.diff all_local_vars printed_vars) in 
544 
let locals = 
545 
if not (Vars.is_empty unused) then ( 
546 
Format.eprintf "Unused local vars: [%a]. Removing them.@.@?" 
547 
Vars.pp unused; 
548 
List.filter (fun v > not (Vars.mem v unused)) s.MC.step_locals 
549 
) 
550 
else 
551 
s.MC.step_locals 
552 
in 
553 
{ s with MC.step_instrs = new_instrs; MC.step_locals = locals } (* we have also to modify local variables to declare new vars *) 
554  
555  
556 
let machine_t2machine_t_optimized_by_salsa constEnv mt = 
557 
try 
558 
if debug then Format.eprintf "@[<v 2> Optimizing machine %s@ " mt.MC.mname.LT.node_id; 
559 
let new_step = salsaStep constEnv mt mt.MC.mstep in 
560 
if debug then Format.eprintf "@]@."; 
561 
{ mt with MC.mstep = new_step } 
562 

563 

564 
with FormalEnv.NoDefinition v as exp > 
565 
Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
566 
raise exp 
567  
568  
569 
(* Local Variables: *) 
570 
(* compilecommand:"make C ../../.." *) 
571 
(* End: *) 
572 