lustrec / src / plugins / salsa / machine_salsa_opt.ml @ e8f55c25
History  View  Annotate  Download (35.1 KB)
1 
(* We try to avoid opening modules here *) 

2 
module ST = Salsa.Types 
3 
module SDT = SalsaDatatypes 
4 
module LT = Lustre_types 
5 
module MC = Machine_code 
6  
7 
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *) 
8 
open SalsaDatatypes 
9 

10 
let report = Log.report ~plugin:"salsa" ~verbose_level:Salsa.Log.verbose_level 
11 
(******************************************************************) 
12 
(* TODO Xavier: should those functions be declared more globally? *) 
13  
14 
let fun_types node = 
15 
try 
16 
match node.LT.top_decl_desc with 
17 
 LT.Node nd > 
18 
let tin, tout = Types.split_arrow nd.LT.node_type in 
19 
Types.type_list_of_type tin, Types.type_list_of_type tout 
20 
 _ > Format.eprintf "%a is not a node@.@?" Printers.pp_decl node; assert false 
21 
with Not_found > Format.eprintf "Unable to find type def for function %s@.@?" (Corelang.node_name node); assert false 
22  
23 
let called_node_id m id = 
24 
let td, _ = 
25 
try 
26 
List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *) 
27 
with Not_found > assert false 
28 
in 
29 
td 
30 
(******************************************************************) 
31  
32 
(* Returns the set of vars that appear in the expression *) 
33 
let rec get_expr_real_vars e = 
34 
let open MT in 
35 
match e.value_desc with 
36 
 Var v when Types.is_real_type v.LT.var_type > Vars.singleton v 
37 
 Var _ 
38 
 Cst _ > Vars.empty 
39 
 Fun (_, args) > 
40 
List.fold_left 
41 
(fun acc e > Vars.union acc (get_expr_real_vars e)) 
42 
Vars.empty args 
43 
 Array _ 
44 
 Access _ 
45 
 Power _ > assert false 
46  
47 
(* Extract the variables to appear as free variables in expressions (lhs) *) 
48 
let rec get_read_vars instrs = 
49 
let open MT in 
50 
match instrs with 
51 
[] > Vars.empty 
52 
 i::tl > ( 
53 
let vars_tl = get_read_vars tl in 
54 
match Corelang.get_instr_desc i with 
55 
 MLocalAssign(_,e) 
56 
 MStateAssign(_,e) > Vars.union (get_expr_real_vars e) vars_tl 
57 
 MStep(_, _, el) > List.fold_left (fun accu e > Vars.union (get_expr_real_vars e) accu) vars_tl el 
58 
 MBranch(e, branches) > ( 
59 
let vars = Vars.union (get_expr_real_vars e) vars_tl in 
60 
List.fold_left (fun vars (_, b) > Vars.union vars (get_read_vars b) ) vars branches 
61 
) 
62 
 MReset _ 
63 
 MNoReset _ 
64 
 MSpec _  MComment _ > Vars.empty 
65 
) 
66  
67 
let rec get_written_vars instrs = 
68 
let open MT in 
69 
match instrs with 
70 
[] > Vars.empty 
71 
 i::tl > ( 
72 
let vars_tl = get_written_vars tl in 
73 
match Corelang.get_instr_desc i with 
74 
 MLocalAssign(v,_) 
75 
 MStateAssign(v,_) > Vars.add v vars_tl 
76 
 MStep(vdl, _, _) > List.fold_left (fun accu v > Vars.add v accu) vars_tl vdl 
77 
 MBranch(_, branches) > ( 
78 
List.fold_left (fun vars (_, b) > Vars.union vars (get_written_vars b) ) vars_tl branches 
79 
) 
80 
 MReset _ 
81 
 MNoReset _ 
82 
 MSpec _  MComment _ > Vars.empty 
83 
) 
84  
85 
(* let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range = *) 
86 
(* let new_expr, new_range = *) 
87 
(* Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv *) 
88 
(* in *) 
89 
(* Format.eprintf "New range: %a@." RangesInt.pp_val new_range; *) 
90 
(* if Salsa.Float.errLt new_range old_range < 0 then *) 
91 

92 
(* iterTransformExpr fresh_id new_expr abstractEnv new_range *) 
93 
(* else *) 
94 
(* new_expr, new_range *) 
95  
96  
97 
(* Takes as input a salsa expression and return an optimized one *) 
98 
let opt_num_expr_sliced ranges e_salsa = 
99 
try 
100 
let fresh_id = "toto" in (* TODO more meaningful name *) 
101  
102 
let abstractEnv = RangesInt.to_abstract_env ranges in 
103 
report ~level:2 (fun fmt > Format.fprintf fmt 
104 
"Launching analysis: %s@ " 
105 
(Salsa.Print.printExpression e_salsa)); 
106 
let new_e_salsa, e_val = 
107 
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv 
108 
in 
109 
report ~level:2 (fun fmt > Format.fprintf fmt " Analysis done: %s@ " 
110 
(Salsa.Print.printExpression new_e_salsa)); 
111  
112  
113 
(* (\* Debug *\) *) 
114 
(* Format.eprintf "Salsa:@.input expr: %s@.outputexpr: %s@." *) 
115 
(* (Salsa.Print.printExpression e_salsa) *) 
116 
(* (Salsa.Print.printExpression new_e_salsa); *) 
117 
(* (\* Debug *\) *) 
118 

119 
report ~level:2 (fun fmt > Format.fprintf fmt " Computing range progress@ "); 
120  
121 
let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in 
122 
let expr, expr_range = 
123 
match RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val with 
124 
 true, true > ( 
125 
if !debug then report ~level:2 (fun fmt > 
126 
Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val; 
127 
); 
128 
e_salsa, Some old_val 
129 
) 
130 
 false, true > ( 
131 
if !debug then report ~level:2 (fun fmt > 
132 
Format.fprintf fmt "Improved!@ "; 
133 
); 
134 
new_e_salsa, Some e_val 
135 
) 
136 
 true, false > 
137 
report ~level:2 (fun fmt > 
138 
Format.fprintf fmt 
139 
"CAREFUL  new range is worse!. Restoring provided expression@ "); 
140 
e_salsa, Some old_val 
141  
142 
 false, false > ( 
143 
report ~level:2 (fun fmt > 
144 
Format.fprintf fmt 
145 
"Error; new range is not comparable with old end. It may need some investigation!@. "; 
146 
Format.fprintf fmt "old: %a@.new: %a@ " 
147 
RangesInt.pp_val old_val 
148 
RangesInt.pp_val e_val); 
149 

150 
new_e_salsa, Some e_val 
151 
(* assert false *) 
152 
) 
153 
in 
154 
report ~level:2 (fun fmt > Format.fprintf fmt " Computing range done@ "); 
155  
156 
if !debug then report ~level:2 (fun fmt > 
157 
Format.fprintf fmt 
158 
" @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ " 
159 
(Salsa.Print.printExpression e_salsa) 
160 
(* MC.pp_val e *) 
161 
RangesInt.pp_val old_val 
162 
(Salsa.Print.printExpression new_e_salsa) 
163 
(* MC.pp_val new_e *) 
164 
RangesInt.pp_val e_val; 
165 
); 
166 
expr, expr_range 
167 
with (* Not_found > *) 
168 
 Salsa.Epeg_types.EPEGError _ > ( 
169 
report ~level:2 (fun fmt > 
170 
Format.fprintf fmt 
171 
"BECAUSE OF AN ERROR, Expression %s was not optimized@ " (Salsa.Print.printExpression e_salsa) 
172 
(* MC.pp_val e *)); 
173 
e_salsa, None 
174 
) 
175  
176  
177 

178 
(* Optimize a given expression. It returns the modified expression, a computed range and freshly defined variables. *) 
179 
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : MT.value_t * RangesInt.t option * MT.instr_t list * Vars.VarSet.t = 
180 
let rec opt_expr m vars_env ranges formalEnv e = 
181 
let open MT in 
182 
match e.value_desc with 
183 
 Cst cst > 
184 
(* Format.eprintf "optmizing constant expr @ "; *) 
185 
(* the expression is a constant, we optimize it directly if it is a real 
186 
constant *) 
187 
let typ = Typing.type_const Location.dummy_loc cst in 
188 
if Types.is_real_type typ then 
189 
opt_num_expr m vars_env ranges formalEnv e 
190 
else e, None, [], Vars.empty 
191 
 Var v > 
192 
if not (Vars.mem v printed_vars) && 
193 
(* TODO xavier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *) 
194 
(Types.is_real_type e.value_type  Types.is_real_type v.LT.var_type) 
195 
then 
196 
opt_num_expr m vars_env ranges formalEnv e 
197 
else 
198 
e, None, [], Vars.empty (* Nothing to optimize for expressions containing a single non real variable *) 
199 
(* (\* optimize only numerical vars *\) *) 
200 
(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *) 
201 
(* else e, None *) 
202 
 Fun (fun_id, args) > ( 
203 
(* necessarily, this is a basic function (ie. +  * / &&  mod ... ) *) 
204 
(* if the return type is real then optimize it, otherwise call recusrsively on arguments *) 
205 
if Types.is_real_type e.value_type then 
206 
opt_num_expr m vars_env ranges formalEnv e 
207 
else ( 
208 
(* We do not care for computed local ranges. *) 
209 
let args', il, new_locals = 
210 
List.fold_right ( 
211 
fun arg (al, il, nl) > 
212 
let arg', _, arg_il, arg_nl = 
213 
opt_expr m vars_env ranges formalEnv arg in 
214 
arg'::al, arg_il@il, Vars.union arg_nl nl) 
215 
args 
216 
([], [], Vars.empty) 
217 
in 
218 
{ e with value_desc = Fun(fun_id, args')}, None, il, new_locals 
219 
) 
220 
) 
221 
 Array _ 
222 
 Access _ 
223 
 Power _ > assert false 
224 
and opt_num_expr m vars_env ranges formalEnv e = 
225 
if !debug then ( 
226 
report ~level:2 (fun fmt > Format.fprintf fmt "Optimizing expression @[<hov>%a@]@ " 
227 
(MC.pp_val m) e); 
228 
); 
229 
(* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e; *) 
230 
(* Convert expression *) 
231 
(* List.iter (fun (l,c) > Format.eprintf "%s > %a@ " l Printers.pp_const c) constEnv; *) 
232 
let e_salsa : Salsa.Types.expression = value_t2salsa_expr constEnv e in 
233 
(* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ; *) 
234  
235 
(* Convert formalEnv *) 
236 
(* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *) 
237 
(* if !debug then Format.eprintf "Formal env converted to salsa@ "; *) 
238  
239 
(* Format.eprintf "Expression avant et apres substVars.@.Avant %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ; *) 
240  
241 
(* Substitute all occurences of variables by their definition in env *) 
242 
let (e_salsa: Salsa.Types.expression), _ = 
243 
Salsa.Rewrite.substVars 
244 
e_salsa 
245 
(FormalEnv.to_salsa constEnv formalEnv) 
246 
0 (* TODO: Nasrine, what is this integer value for ? *) 
247 
in 
248  
249 
(* Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ; *) 
250  
251 
(* if !debug then Format.eprintf "Substituted def in expr@ "; *) 
252 
let abstractEnv = RangesInt.to_abstract_env ranges in 
253 
(* List.iter (fun (id, _) > Format.eprintf "absenv: %s@." id) abstractEnv; *) 
254 
(* The expression is partially evaluated by the available ranges 
255 
valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv  on 
256 
garde evalPartExpr remplace les variables e qui sont dans env par la cst 
257 
 on garde *) 
258 
(* if !debug then Format.eprintf "avant avant eval part@ "; *) 
259 
(* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *) 
260 
let e_salsa = 
261 
Salsa.Analyzer.evalPartExpr 
262 
e_salsa 
263 
(Salsa.Analyzer.valEnv2ExprEnv abstractEnv) 
264 
([] (* no blacklisted variables *)) 
265 
([] (* no arrays *)) 
266 
in 
267 
(* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa); *) 
268 
(* Checking if we have all necessary information *) 
269  
270 
let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in 
271 
if Vars.cardinal free_vars > 0 then ( 
272 
report ~level:2 (fun fmt > Format.fprintf fmt 
273 
"Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 
274 
Vars.pp (Vars.fold (fun v accu > 
275 
let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in 
276 
Vars.add v' accu) 
277 
free_vars Vars.empty) 
278 
(MC.pp_val m) (salsa_expr2value_t vars_env constEnv e_salsa)); 
279 
if !debug then report ~level:2 (fun fmt > Format.fprintf fmt "Some free vars, not optimizing@ "); 
280 
if !debug then report ~level:3 (fun fmt > Format.fprintf fmt " ranges: %a@ " 
281 
RangesInt.pp ranges); 
282  
283 
(* if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt "Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *) 
284 

285 

286 
let new_e = try salsa_expr2value_t vars_env constEnv e_salsa with Not_found > assert false in 
287 
new_e, None, [] , Vars.empty 
288 
) 
289 
else ( 
290 

291 
if !debug then 
292 
report ~level:3 (fun fmt > Format.fprintf fmt "@[<v 2>Analyzing expression %a@ with ranges: @[<v>%a@ @]@ @]@ " 
293 
(C_backend_common.pp_c_val m "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa) 
294 
(Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) > Format.fprintf fmt "%s > %a" l FloatIntSalsa.pp r)) abstractEnv) 
295 

296 
; 
297  
298 
(* Slicing expression *) 
299 
let e_salsa, seq = 
300 
try 
301 
Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) 
302 
with _ > Format.eprintf "Issues rewriting express %s@.@?" (Salsa.Print.printExpression e_salsa); assert false 
303 
in 
304 
let def_tmps = Salsa.Utils.flatten_seq seq [] in 
305 
(* Registering tmp ids in vars_env *) 
306 
let vars_env', new_local_vars = List.fold_left 
307 
(fun (vs,vars) (id, _) > 
308 
let vdecl = Corelang.mk_fresh_var 
309 
(nodename.node_id, []) (* TODO check that the empty env is ok. One may need to build or access to the current env *) 
310 
Location.dummy_loc 
311 
e.MT.value_type 
312 
(Clocks.new_var true) 
313 

314 
in 
315 
let vs' = 
316 
VarEnv.add 
317 
id 
318 
{ 
319 
vdecl = vdecl ; 
320 
is_local = true; 
321 
} 
322 
vs 
323 
in 
324 
let vars' = Vars.add vdecl vars in 
325 
vs', vars' 
326 
) 
327 
(vars_env,Vars.empty) 
328 
def_tmps 
329 
in 
330 
(* Debug *) 
331 
if !debug then ( 
332 
report ~level:3 (fun fmt > 
333 
Format.fprintf fmt "List of slices: @[<v 0>%a@]@ " 
334 
(Utils.fprintf_list 
335 
~sep:"@ " 
336 
(fun fmt (id, e_id) > 
337 
Format.fprintf fmt "(%s,%a) > %a" 
338 
id 
339 
Printers.pp_var (get_var vars_env' id).vdecl 
340 
(C_backend_common.pp_c_val m "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_id) 
341 
) 
342 
) 
343 
def_tmps; 
344 
Format.fprintf fmt "Sliced expression: %a@ " 
345 
(C_backend_common.pp_c_val m "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env' constEnv e_salsa) 
346 
; 
347 
)); 
348 
(* Debug *) 
349 

350 
(* Optimize def tmp, and build the associated instructions. Update the 
351 
abstract Env with computed ranges *) 
352 
if !debug && List.length def_tmps >= 1 then ( 
353 
report ~level:3 (fun fmt > Format.fprintf fmt "@[<v 3>Optimizing sliced subexpressions@ ") 
354 
); 
355 
let rev_def_tmp_instrs, ranges = 
356 
List.fold_left (fun (accu_instrs, ranges) (id, e_id) > 
357 
(* Format.eprintf "Cleaning/Optimizing %s@." id; *) 
358 
let e_id', e_range = (*Salsa.MainEPEG.transformExpression id e_id abstractEnv*) 
359 
opt_num_expr_sliced ranges e_id 
360 
in 
361 
let new_e_id' = try salsa_expr2value_t vars_env' constEnv e_id' with Not_found > assert false in 
362  
363 
let vdecl = (get_var vars_env' id).vdecl in 
364 

365 
let new_local_assign = 
366 
(* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *) 
367 
MT.MLocalAssign(vdecl, new_e_id') 
368 
in 
369 
let new_local_assign = { 
370 
MT.instr_desc = new_local_assign; 
371 
MT.lustre_eq = None (* could be Corelang.mkeq Location.dummy_loc 
372 
([vdecl.LT.var_id], e_id) provided it is 
373 
converted as Lustre expression rather than 
374 
a Machine code value *); 
375 
} 
376 
in 
377 
let new_ranges = 
378 
match e_range with 
379 
None > ranges 
380 
 Some e_range > RangesInt.add_def ranges id e_range in 
381 
new_local_assign::accu_instrs, new_ranges 
382 
) ([], ranges) def_tmps 
383 
in 
384 
if !debug && List.length def_tmps >= 1 then ( 
385 
report ~level:3 (fun fmt > Format.fprintf fmt "@]@ ") 
386 
); 
387  
388 
(* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a" (Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *) 
389 

390  
391 
let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in 
392 
let expr = try salsa_expr2value_t vars_env' constEnv expr_salsa with Not_found > assert false in 
393  
394 
expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars 
395  
396  
397  
398 
(* ???? Bout de code dans unstable lors du merge avec salsa ? 
399 
==== 
400  
401 
let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa with Not_found > assert false in 
402 
if !debug then Log.report ~level:2 (fun fmt > 
403 
let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in 
404 
match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val old_range with 
405 
 true, true > Format.fprintf fmt "No improvement on abstract value %a@ " RangesInt.pp_val e_val 
406 
 true, false > ( 
407 
Format.fprintf fmt "Improved!"; 
408 
Format.fprintf fmt 
409 
" @[<v>old_expr: @[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ " 
410 
(MC.pp_val m) e 
411 
RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa abstractEnv []) 
412 
(MC.pp_val m) new_e 
413 
RangesInt.pp_val e_val 
414 
) 
415 
 false, true > Format.eprintf "Error; new range is worse!@.@?"; assert false 
416 
 false, false > Format.eprintf "Error; new range is not comparabe with old end. This should not happen!@.@?"; assert false 
417 
); 
418 
new_e, Some e_val, List.rev rev_def_tmp_instrs 
419 
with (* Not_found > *) 
420 
 Salsa.Epeg_types.EPEGError _ > ( 
421 
Log.report ~level:2 (fun fmt > Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not optimized@ " (MC.pp_val m) e); 
422 
e, None, [] 
423 
) 
424 
>>>>>>> unstable 
425 
*) 
426 
) 
427  
428  
429 

430 
in 
431 
opt_expr m vars_env ranges formalEnv e 
432 

433 

434 
(* Returns a list of assign, for each var in vars_to_print, that produce the 
435 
definition of it according to formalEnv, and driven by the ranges. *) 
436 
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv vars_to_print = 
437 
(* We print thhe expression in the order of definition *) 
438  
439 
let ordered_vars = 
440 
List.stable_sort 
441 
(FormalEnv.get_sort_fun formalEnv) 
442 
(Vars.elements vars_to_print) 
443 
in 
444 
if !debug then report ~level:4 (fun fmt > Format.fprintf fmt 
445 
"Printing vars in the following order: [%a]@ " 
446 
(Utils.fprintf_list ~sep:", " Printers.pp_var) ordered_vars); 
447 

448 
List.fold_right ( 
449 
fun v (accu_instr, accu_ranges, accu_new_locals) > 
450 
if !debug then report ~level:4 (fun fmt > Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id); 
451 
try 
452 
(* Obtaining unfold expression of v in formalEnv *) 
453 
let v_def = FormalEnv.get_def formalEnv v in 
454 
let e, r, il, new_v_locals = 
455 
optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def 
456 
in 
457 
let instr_desc = 
458 
if try (get_var vars_env v.LT.var_id).is_local with Not_found > assert false then 
459 
MT.MLocalAssign(v, e) 
460 
else 
461 
MT.MStateAssign(v, e) 
462 
in 
463 
(il@((Corelang.mkinstr instr_desc)::accu_instr)), 
464 
( 
465 
match r with 
466 
 None > ranges 
467 
 Some v_r > RangesInt.add_def ranges v.LT.var_id v_r), 
468 
(Vars.union accu_new_locals new_v_locals) 
469 
with FormalEnv.NoDefinition _ > ( 
470 
(* It should not happen with C backend, but may happen with Lustre backend *) 
471 
if !Options.output = "lustre" then accu_instr, ranges, Vars.empty else (Format.eprintf "@?"; assert false) 
472 
) 
473 
) ordered_vars ([], ranges, Vars.empty) 
474  
475 
(* Main recursive function: modify the instructions list while preserving the 
476 
order of assigns for state variables. Returns a quintuple: (new_instrs, 
477 
ranges, formalEnv, printed_vars, and remaining vars to be printed) *) 
478 
let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv printed_vars vars_to_print = 
479 
let formal_env_def = FormalEnv.def constEnv vars_env in 
480 
(* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *) 
481 
let assign_vars = assign_vars nodename m constEnv vars_env in 
482 
(* if !debug then ( *) 
483 
(* Log.report ~level:3 (fun fmt > Format.fprintf fmt *) 
484 
(* "Current printed_vars: [%a]@ Vars to print: [%a]@ Formal env is [%a]@ " *) 
485 
(* Vars.pp printed_vars *) 
486 
(* Vars.pp vars_to_print *) 
487 
(* FormalEnv.pp formalEnv) *) 
488 
(* ); *) 
489 
match instrs with 
490 
 [] > 
491 
(* End of instruction list: we produce the definition of each variable that 
492 
appears in vars_to_print. Each of them should be defined in formalEnv *) 
493 
(* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp vars_to_print; *) 
494 
let instrs, ranges', new_expr_locals = assign_vars printed_vars ranges formalEnv vars_to_print in 
495 
instrs, 
496 
ranges', 
497 
formalEnv, 
498 
Vars.union printed_vars vars_to_print, (* We should have printed all required vars *) 
499 
[], (* No more vars to be printed *) 
500 
Vars.empty 
501 

502 
 hd_instr::tl_instrs > 
503 
(* We reformulate hd_instr, producing or not a fresh instruction, updating 
504 
formalEnv, possibly ranges and vars_to_print *) 
505 
begin 
506 
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print, hd_new_locals = 
507 
match Corelang.get_instr_desc hd_instr with 
508 
 MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && not (Vars.mem vd vars_to_print) > 
509 
(* LocalAssign are injected into formalEnv *) 
510 
(* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *) 
511 
(* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *) 
512 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
513 
[], (* no instr generated *) 
514 
ranges, (* no new range computed *) 
515 
formalEnv', 
516 
printed_vars, (* no new printed vars *) 
517 
vars_to_print, (* no more or less variables to print *) 
518 
Vars.empty (* no new locals *) 
519 

520 
 MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print > 
521  
522 
(* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *) 
523 
(* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *) 
524 
(* if !debug then ( *) 
525 
(* Format.eprintf "%a@ " MC.pp_instr hd_instr; *) 
526 
(* Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd; *) 
527 
(* ); *) 
528 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
529 
let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *) 
530 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) 
531 
in 
532 
instrs', 
533 
ranges', (* no new range computed *) 
534 
formalEnv', (* formelEnv already updated *) 
535 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 
536 
Vars.remove vd vars_to_print, (* removed vd from variables to print *) 
537 
expr_new_locals (* adding sliced vardecl to the list *) 
538 

539 
 MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print *)> 
540  
541 
(* StateAssign are produced since they are required by the function. We still 
542 
keep their definition in the formalEnv in case it can optimize later 
543 
outputs. vd is removed from remaining vars_to_print *) 
544 
(* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *) 
545 
(* if !debug then ( *) 
546 
(* Format.eprintf "%a@ " MC.pp_instr hd_instr; *) 
547 
(* Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd; *) 
548 
(* ); *) 
549 
let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 
550 
let instrs', ranges', expr_new_locals = (* printing vd = optimized vt *) 
551 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) 
552 
in 
553 
instrs', 
554 
ranges', (* no new range computed *) 
555 
formalEnv, (* formelEnv already updated *) 
556 
Vars.add vd printed_vars, (* adding vd to new printed vars *) 
557 
Vars.remove vd vars_to_print, (* removed vd from variables to print *) 
558 
expr_new_locals (* adding sliced vardecl to the list *) 
559  
560 
 (MT.MLocalAssign(vd,vt)  MT.MStateAssign(vd,vt)) > 
561 
(* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *) 
562  
563 
(* We have to produce the instruction. But we may have to produce as 
564 
well its dependencies *) 
565 
let required_vars = get_expr_real_vars vt in 
566 
let required_vars = Vars.diff required_vars printed_vars in (* remove 
567 
already 
568 
produced 
569 
variables *) 
570 
(* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *) 
571 
let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in 
572 
let prefix_instr, ranges, new_expr_dep_locals = 
573 
assign_vars printed_vars ranges formalEnv required_vars in 
574  
575 
let vt', _, il, expr_new_locals = optimize_expr nodename m constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in 
576 
let new_instr = 
577 
match Corelang.get_instr_desc hd_instr with 
578 
 MT.MLocalAssign _ > Corelang.update_instr_desc hd_instr (MT.MLocalAssign(vd,vt')) 
579 
 _ > Corelang.update_instr_desc hd_instr (MT.MStateAssign(vd,vt')) 
580 
in 
581 
let written_vars = Vars.add vd required_vars in 
582 
prefix_instr@il@[new_instr], 
583 
ranges, (* no new range computed *) 
584 
formalEnv, (* formelEnv untouched *) 
585 
Vars.union written_vars printed_vars, (* adding vd + dependencies to 
586 
new printed vars *) 
587 
Vars.diff vars_to_print written_vars, (* removed vd + dependencies from 
588 
variables to print *) 
589 
(Vars.union new_expr_dep_locals expr_new_locals) 
590 
 MT.MStep(vdl,id,vtl) > 
591 
(* Format.eprintf "step@."; *) 
592  
593 
(* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr hd_instr; *) 
594 
(* Call of an external function. Input expressions have to be 
595 
optimized, their free variables produced. A fresh range has to be 
596 
computed for each output variable in vdl. Output of the function 
597 
call are removed from vars to be printed *) 
598 
let node = called_node_id m id in 
599 
let node_id = Corelang.node_name node in 
600 
let tin, tout = (* special care for arrow *) 
601 
if node_id = "_arrow" then 
602 
match vdl with 
603 
 [v] > let t = v.LT.var_type in 
604 
[t; t], [t] 
605 
 _ > assert false (* should not happen *) 
606 
else 
607 
fun_types node 
608 
in 
609 
(* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *) 
610 
let vtl', vtl_ranges, il, args_new_locals = List.fold_right2 ( 
611 
fun e typ_e (exprl, range_l, il_l, new_locals)> 
612 
if Types.is_real_type typ_e then 
613 
let e', r', il, new_expr_locals = 
614 
optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e 
615 
in 
616 
e'::exprl, r'::range_l, il@il_l, Vars.union new_locals new_expr_locals 
617 
else 
618 
e::exprl, None::range_l, il_l, new_locals 
619 
) vtl tin ([], [], [], Vars.empty) 
620 
in 
621 
(* if !debug then Format.eprintf "... done@ @]@ "; *) 
622  
623  
624  
625 
(* let required_vars = *) 
626 
(* List.fold_left2 *) 
627 
(* (fun accu e typ_e > *) 
628 
(* if Types.is_real_type typ_e then *) 
629 
(* Vars.union accu (get_expr_real_vars e) *) 
630 
(* else (\* we do not consider non real expressions *\) *) 
631 
(* accu *) 
632 
(* ) *) 
633 
(* Vars.empty *) 
634 
(* vtl' tin *) 
635 
(* in *) 
636 
(* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: [%a]@ Remaining required vars: [%a]@ " *) 
637 
(* Vars.pp required_vars *) 
638 
(* Vars.pp printed_vars *) 
639 
(* Vars.pp (Vars.diff required_vars printed_vars) *) 
640 
(* ; *) 
641 
(* let required_vars = Vars.diff required_vars printed_vars in (\* remove *) 
642 
(* already *) 
643 
(* produced *) 
644 
(* variables *\) *) 
645 
(* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *) 
646 
(* let instrs', ranges' = assign_vars (Vars.union written_vars printed_vars) ranges formalEnv required_vars in *) 
647  
648 
(* instrs' @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *) *) 
649  
650 
let written_vars = Vars.of_list vdl in 
651 

652  
653 

654 
il @ [Corelang.update_instr_desc hd_instr (MT.MStep(vdl,id,vtl'))], (* New instrs *) 
655 
RangesInt.add_call ranges vdl id vtl_ranges, (* add information bounding each vdl var *) 
656 
formalEnv, 
657 
Vars.union written_vars printed_vars, (* adding vdl to new printed vars *) 
658 
Vars.diff vars_to_print written_vars, 
659 
args_new_locals 
660 

661 
 MT.MBranch(vt, branches) > 
662 

663 
(* Required variables to compute vt are introduced. 
664 
Then each branch is refactored specifically 
665 
*) 
666 

667 
(* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *) 
668 
let required_vars = get_expr_real_vars vt in 
669 
let required_vars = Vars.diff required_vars printed_vars in (* remove 
670 
already 
671 
produced 
672 
variables *) 
673 
let vt', _, prefix_instr, prefix_new_locals = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv vt in 
674  
675 
let new_locals = prefix_new_locals in 
676 

677 
(* let prefix_instr, ranges = *) 
678 
(* assign_vars (Vars.union required_vars printed_vars) ranges formalEnv required_vars in *) 
679  
680 
let printed_vars = Vars.union printed_vars required_vars in 
681  
682  
683 
let read_vars_tl = get_read_vars tl_instrs in 
684 
(* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *) 
685 
let branches', written_vars, merged_ranges, new_locals = List.fold_right ( 
686 
fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges, new_locals) > 
687 
let b_write_vars = get_written_vars b_instrs in 
688 
let b_vars_to_print = Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) in 
689 
let b_fe = formalEnv in (* because of side effect 
690 
data, we copy it for 
691 
each branch *) 
692 
let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars, b_new_locals = 
693 
rewrite_instrs nodename m constEnv vars_env m b_instrs ranges b_fe printed_vars b_vars_to_print 
694 
in 
695 
(* b_vars should be empty *) 
696 
let _ = if b_vars != [] then assert false in 
697 

698 
(* Producing the refactored branch *) 
699 
(b_l, b_instrs') :: new_branches, 
700 
Vars.union b_printed written_vars, (* They should coincides. We 
701 
use union instead of 
702 
inter to ease the 
703 
bootstrap *) 
704 
RangesInt.merge merged_ranges b_ranges, 
705 
Vars.union new_locals b_new_locals 
706 

707 
) branches ([], required_vars, ranges, new_locals) 
708 
in 
709 
(* if !debug then Format.eprintf "dealing with branches done@ @]@ "; *) 
710 
prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))], 
711 
merged_ranges, (* Only step functions call within branches may have 
712 
produced new ranges. We merge this data by 
713 
computing the join per variable *) 
714 
formalEnv, (* Thanks to the computation of var_to_print in each 
715 
branch, no new definition should have been computed 
716 
without being already printed *) 
717 
Vars.union written_vars printed_vars, 
718 
Vars.diff vars_to_print written_vars (* We remove vars that have been 
719 
produced within branches *), 
720 
new_locals 
721  
722  
723 
 MT.MReset(_)  MT.MNoReset _  MT.MSpec _  MT.MComment _ > 
724 
(* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr hd_instr; *) 
725  
726 
(* Untouched instruction *) 
727 
[ hd_instr ], (* unmodified instr *) 
728 
ranges, (* no new range computed *) 
729 
formalEnv, (* no formelEnv update *) 
730 
printed_vars, 
731 
vars_to_print, (* no more or less variables to print *) 
732 
Vars.empty (* no new slides vars *) 
733 

734 
in 
735 
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print, tl_new_locals = 
736 
rewrite_instrs 
737 
nodename 
738 
m 
739 
constEnv 
740 
vars_env 
741 
m 
742 
tl_instrs 
743 
ranges 
744 
formalEnv 
745 
printed_vars 
746 
vars_to_print 
747 

748 
in 
749 
hd_instrs @ tl_instrs, 
750 
ranges, 
751 
formalEnv, 
752 
printed_vars, 
753 
vars_to_print, 
754 
(Vars.union hd_new_locals tl_new_locals) 
755 
end 
756  
757  
758  
759  
760  
761  
762 
(* TODO: deal with new variables, ie. tmp *) 
763 
let salsaStep constEnv m s = 
764 
let ranges = RangesInt.empty (* empty for the moment, should be build from 
765 
machine annotations or externally provided information *) in 
766 
let annots = List.fold_left ( 
767 
fun accu annl > 
768 
List.fold_left ( 
769 
fun accu (key, range) > 
770 
match key with 
771 
 ["salsa"; "ranges"; var] > (var, range)::accu 
772 
 _ > accu 
773 
) accu annl.LT.annots 
774 
) [] m.MT.mannot 
775 
in 
776 
let ranges = 
777 
List.fold_left (fun ranges (v, value) > 
778 
match value.LT.eexpr_qfexpr.LT.expr_desc with 
779 
 LT.Expr_tuple [minv; maxv] > ( 
780 
let get_cst e = match e.LT.expr_desc with 
781 
 LT.Expr_const (LT.Const_real r) > 
782 
(* calculer la valeur c * 10^e *) 
783 
Real.to_num r 
784 
 _ > 
785 
Format.eprintf 
786 
"Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@." 
787 
Printers.pp_expr value.LT.eexpr_qfexpr 
788 
Printers.pp_expr e 
789 
; 
790 
assert false 
791 
in 
792 
(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *) 
793 
(* maxv = Salsa.Float.Domain.of_num (get_cst maxv) in *) 
794 
(* if !debug then Format.eprintf "variable %s in [%s, %s]@ " v (Num.string_of_num minv) (Num.string_of_num maxv); *) 
795 
RangesInt.enlarge ranges v (Salsa.Float.Domain.inject_nums (get_cst minv) (get_cst maxv)) 
796 
) 
797 
 _ > 
798 
Format.eprintf 
799 
"Invalid salsa range: %a. It should be a pair of floats.@." 
800 
Printers.pp_expr value.LT.eexpr_qfexpr; 
801 
assert false 
802 
) ranges annots 
803 
in 
804 
let formal_env = FormalEnv.empty () in 
805 
let vars_to_print = 
806 
Vars.real_vars 
807 
( 
808 
Vars.union 
809 
(Vars.of_list m.MT.mmemory) 
810 
(Vars.of_list s.MT.step_outputs) 
811 
) 
812 
in 
813 
(* TODO: should be at least step output + may be memories *) 
814 

815 
let vars_env = compute_vars_env m in 
816 
(* if !debug then Format.eprintf "@[<v 2>Registering node equations@ "; *) 
817 
let new_instrs, _, _, printed_vars, _, new_locals = 
818 
rewrite_instrs 
819 
m.MT.mname 
820 
m 
821 
constEnv 
822 
vars_env 
823 
m 
824 
s.MT.step_instrs 
825 
ranges 
826 
formal_env 
827 
(Vars.real_vars (Vars.of_list s.MT.step_inputs (* printed_vars : real 
828 
inputs are considered as 
829 
already printed *))) 
830 
vars_to_print 
831 

832 
in 
833 
let all_local_vars = Vars.real_vars (Vars.of_list s.MT.step_locals) in 
834 
let unused = (Vars.diff all_local_vars printed_vars) in 
835 
let locals = 
836 
if not (Vars.is_empty unused) then ( 
837 
if !debug then report ~level:2 (fun fmt > Format.fprintf fmt "Unused local vars: [%a]. Removing them.@ " 
838 
Vars.pp unused); 
839 
List.filter (fun v > not (Vars.mem v unused)) s.MT.step_locals 
840 
) 
841 
else 
842 
s.MT.step_locals 
843 
in 
844 
let locals = locals @ Vars.elements new_locals in 
845 
{ s with MT.step_instrs = new_instrs; MT.step_locals = locals } (* we have also to modify local variables to declare new vars *) 
846  
847  
848 
let machine_t2machine_t_optimized_by_salsa constEnv mt = 
849 
try 
850 
if !debug then report ~level:2 (fun fmt > Format.fprintf fmt "@[<v 3>Optimizing machine %s@ " mt.MT.mname.LT.node_id); 
851 
let new_step = salsaStep constEnv mt mt.MT.mstep in 
852 
if !debug then report ~level:2 (fun fmt > Format.fprintf fmt "@]@ "); 
853 
{ mt with MT.mstep = new_step } 
854 

855 

856 
with FormalEnv.NoDefinition v as exp > 
857 
Format.eprintf "No definition for variable %a@.@?" Printers.pp_var v; 
858 
raise exp 
859  
860  
861 
(* Local Variables: *) 
862 
(* compilecommand:"make C ../../.." *) 
863 
(* End: *) 
864 