Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/plugins/salsa/machine_salsa_opt.ml  

6  6  
7  7 
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *) 
8  8 
open SalsaDatatypes 
9 


10 
let report = Log.report ~plugin:"salsa" ~verbose_level:Salsa.Log.verbose_level 

9  
10 
let report = Log.report ~plugin:"salsa" ~verbose_level:Salsa.Log.verbose_level 

11  
11  12 
(******************************************************************) 
12  13 
(* TODO Xavier: should those functions be declared more globally? *) 
13  14  
14 
let fun_types node =


15 
let fun_types node = 

15  16 
try 
16 
match node.LT.top_decl_desc with


17 
 LT.Node nd >


17 
match node.LT.top_decl_desc with 

18 
 LT.Node nd > 

18  19 
let tin, tout = Types.split_arrow nd.LT.node_type in 
19  20 
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 = 

21 
 _ > 

22 
Format.eprintf "%a is not a node@.@?" Printers.pp_decl node; 

23 
assert false 

24 
with Not_found > 

25 
Format.eprintf "Unable to find type def for function %s@.@?" 

26 
(Corelang.node_name node); 

27 
assert false 

28  
29 
let called_node_id m id = 

24  30 
let td, _ = 
25 
try 

26 
List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *) 

31 
try List.assoc id m.MT.mcalls (* TODO Xavier: mcalls or minstances ? *) 

27  32 
with Not_found > assert false 
28  33 
in 
29  34 
td 
30 
(******************************************************************)


35 
(******************************************************************) 

31  36  
32  37 
(* Returns the set of vars that appear in the expression *) 
33  38 
let rec get_expr_real_vars e = 
34 
let open MT in


39 
let open MT in 

35  40 
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)) 

41 
 Var v when Types.is_real_type v.LT.var_type > 

42 
Vars.singleton v 

43 
 Var _  Cst _ > 

44 
Vars.empty 

45 
 Fun (_, args) > 

46 
List.fold_left 

47 
(fun acc e > Vars.union acc (get_expr_real_vars e)) 

42  48 
Vars.empty args 
43 
 Array _ 

44 
 Access _ 

45 
 Power _ > assert false 

49 
 Array _  Access _  Power _ > 

50 
assert false 

46  51  
47  52 
(* Extract the variables to appear as free variables in expressions (lhs) *) 
48  53 
let rec get_read_vars instrs = 
49  54 
let open MT in 
50  55 
match instrs with 
51 
[] > Vars.empty 

52 
 i::tl > ( 

53 
let vars_tl = get_read_vars tl in 

56 
 [] > 

57 
Vars.empty 

58 
 i :: tl > ( 

59 
let vars_tl = get_read_vars tl in 

54  60 
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) > ( 

61 
 MLocalAssign (_, e)  MStateAssign (_, e) > 

62 
Vars.union (get_expr_real_vars e) vars_tl 

63 
 MStep (_, _, el) > 

64 
List.fold_left 

65 
(fun accu e > Vars.union (get_expr_real_vars e) accu) 

66 
vars_tl el 

67 
 MBranch (e, branches) > 

59  68 
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 
) 

69 
List.fold_left 

70 
(fun vars (_, b) > Vars.union vars (get_read_vars b)) 

71 
vars branches 

72 
 MReset _  MNoReset _  MSpec _  MComment _ > 

73 
Vars.empty) 

66  74  
67  75 
let rec get_written_vars instrs = 
68  76 
let open MT in 
69  77 
match instrs with 
70 
[] > Vars.empty 

71 
 i::tl > ( 

72 
let vars_tl = get_written_vars tl in 

78 
 [] > 

79 
Vars.empty 

80 
 i :: tl > ( 

81 
let vars_tl = get_written_vars tl in 

73  82 
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 
) 

83 
 MLocalAssign (v, _)  MStateAssign (v, _) >


84 
Vars.add v vars_tl


85 
 MStep (vdl, _, _) >


86 
List.fold_left (fun accu v > Vars.add v accu) vars_tl vdl


87 
 MBranch (_, branches) >


88 
List.fold_left


89 
(fun vars (_, b) > Vars.union vars (get_written_vars b))


90 
vars_tl branches


91 
 MReset _  MNoReset _  MSpec _  MComment _ >


92 
Vars.empty)


84  93  
85  94 
(* let rec iterTransformExpr fresh_id e_salsa abstractEnv old_range = *) 
86  95 
(* let new_expr, new_range = *) 
...  ...  
88  97 
(* in *) 
89  98 
(* Format.eprintf "New range: %a@." RangesInt.pp_val new_range; *) 
90  99 
(* if Salsa.Float.errLt new_range old_range < 0 then *) 
91 


100  
92  101 
(* iterTransformExpr fresh_id new_expr abstractEnv new_range *) 
93  102 
(* else *) 
94  103 
(* new_expr, new_range *) 
95  104  
96  
97  105 
(* Takes as input a salsa expression and return an optimized one *) 
98  106 
let opt_num_expr_sliced ranges e_salsa = 
99 
try


100 
let fresh_id = "toto" in (* TODO more meaningful name *)


107 
try 

108 
let fresh_id = "toto" in


101  109  
110 
(* TODO more meaningful name *) 

102  111 
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 =


112 
report ~level:2 (fun fmt > 

113 
Format.fprintf fmt "Launching analysis: %s@ "


114 
(Salsa.Print.printExpression e_salsa)); 

115 
let new_e_salsa, e_val = 

107  116 
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv 
108  117 
in 
109 
report ~level:2 (fun fmt > Format.fprintf fmt " Analysis done: %s@ "


110 
(Salsa.Print.printExpression new_e_salsa));


111  
118 
report ~level:2 (fun fmt > 

119 
Format.fprintf fmt " Analysis done: %s@ "


120 
(Salsa.Print.printExpression new_e_salsa)); 

112  121  
113  122 
(* (\* Debug *\) *) 
114  123 
(* Format.eprintf "Salsa:@.input expr: %s@.outputexpr: %s@." *) 
115  124 
(* (Salsa.Print.printExpression e_salsa) *) 
116  125 
(* (Salsa.Print.printExpression new_e_salsa); *) 
117  126 
(* (\* Debug *\) *) 
118 


119 
report ~level:2 (fun fmt > Format.fprintf fmt " Computing range progress@ ");


127 
report ~level:2 (fun fmt > 

128 
Format.fprintf fmt " Computing range progress@ ");


120  129  
121  130 
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 
)


131 
let expr, expr_range = 

132 
match 

133 
RangesInt.Value.leq old_val e_val, RangesInt.Value.leq e_val old_val


134 
with


135 
 true, true >


136 
if !debug then


137 
report ~level:2 (fun fmt >


138 
Format.fprintf fmt "No improvement on abstract value %a@ "


139 
RangesInt.pp_val e_val);


140 
e_salsa, Some old_val


141 
 false, true >


142 
if !debug then


143 
report ~level:2 (fun fmt > Format.fprintf fmt "Improved!@ ");


144 
new_e_salsa, Some e_val


136  145 
 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  146 
report ~level:2 (fun fmt > 
144  147 
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 
) 

148 
"CAREFUL  new range is worse!. Restoring provided expression@ "); 

149 
e_salsa, Some old_val 

150 
 false, false > 

151 
report ~level:2 (fun fmt > 

152 
Format.fprintf fmt 

153 
"Error; new range is not comparable with old end. It may need \ 

154 
some investigation!@. "; 

155 
Format.fprintf fmt "old: %a@.new: %a@ " RangesInt.pp_val old_val 

156 
RangesInt.pp_val e_val); 

157  
158 
new_e_salsa, Some e_val 

159 
(* assert false *) 

153  160 
in 
154  161 
report ~level:2 (fun fmt > Format.fprintf fmt " Computing range done@ "); 
155  162  
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 
); 

163 
if !debug then 

164 
report ~level:2 (fun fmt > 

165 
Format.fprintf fmt 

166 
" @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ \ 

167 
range: %a@]@ @]@ " 

168 
(Salsa.Print.printExpression e_salsa) 

169 
(* MC.pp_val e *) 

170 
RangesInt.pp_val old_val 

171 
(Salsa.Print.printExpression new_e_salsa) 

172 
(* MC.pp_val new_e *) 

173 
RangesInt.pp_val e_val); 

166  174 
expr, expr_range 
167 
with (* Not_found > *)


168 
 Salsa.Epeg_types.EPEGError _ > (


175 
with (* Not_found > *) 

176 
 Salsa.Epeg_types.EPEGError _ > 

169  177 
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 *)); 

178 
Format.fprintf fmt 

179 
"BECAUSE OF AN ERROR, Expression %s was not optimized@ " 

180 
(Salsa.Print.printExpression e_salsa) 

181 
(* MC.pp_val e *)); 

173  182 
e_salsa, None 
174 
) 

175  183  
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 =


184 
(* Optimize a given expression. It returns the modified expression, a computed 

185 
range and freshly defined variables. *) 

186 
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e :


187 
MT.value_t * RangesInt.t option * MT.instr_t list * Vars.VarSet.t =


180  188 
let rec opt_expr m vars_env ranges formalEnv e = 
181  189 
let open MT in 
182  190 
match e.value_desc with 
183  191 
 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 *)


192 
(* Format.eprintf "optmizing constant expr @ "; *) 

193 
(* the expression is a constant, we optimize it directly if it is a real 

194 
constant *)


195 
let typ = Typing.type_const Location.dummy_loc cst in 

196 
if Types.is_real_type typ then opt_num_expr m vars_env ranges formalEnv e


197 
else e, None, [], Vars.empty


198 
 Var v >


199 
if


200 
(not (Vars.mem v printed_vars))


201 
&& (* TODO xavier: comment recuperer le type de l'expression? Parfois


202 
e.value_type vaut 'd *)


203 
(Types.is_real_type e.value_type  Types.is_real_type v.LT.var_type)


204 
then opt_num_expr m vars_env ranges formalEnv e


205 
else e, None, [], Vars.empty


206 
(* Nothing to optimize for expressions containing a single non real variable *)


199  207 
(* (\* optimize only numerical vars *\) *) 
200 
(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *) 

208 
(* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges 

209 
formalEnv e *) 

201  210 
(* 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; *)


211 
 Fun (fun_id, args) > 

212 
if


213 
(* necessarily, this is a basic function (ie. +  * / &&  mod ... ) *)


214 
(* if the return type is real then optimize it, otherwise call


215 
recusrsively on arguments *)


216 
Types.is_real_type e.value_type


217 
then opt_num_expr m vars_env ranges formalEnv e


218 
else


219 
(* We do not care for computed local ranges. *)


220 
let args', il, new_locals =


221 
List.fold_right


222 
(fun arg (al, il, nl) >


223 
let arg', _, arg_il, arg_nl =


224 
opt_expr m vars_env ranges formalEnv arg


225 
in


226 
arg' :: al, arg_il @ il, Vars.union arg_nl nl)


227 
args ([], [], Vars.empty)


228 
in


229 
{ e with value_desc = Fun (fun_id, args') }, None, il, new_locals


230 
 Array _  Access _  Power _ >


231 
assert false


232 
and opt_num_expr m vars_env ranges formalEnv e =


233 
if !debug then


234 
report ~level:2 (fun fmt >


235 
Format.fprintf fmt "Optimizing expression @[<hov>%a@]@ " (MC.pp_val m)


236 
e);


237 
(* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ "


238 
MC.pp_val e; *)


230  239 
(* Convert expression *) 
231 
(* List.iter (fun (l,c) > Format.eprintf "%s > %a@ " l Printers.pp_const c) constEnv; *) 

240 
(* List.iter (fun (l,c) > Format.eprintf "%s > %a@ " l Printers.pp_const 

241 
c) constEnv; *) 

232  242 
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) ; *) 

243  
244 
(* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val 

245 
(salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ; *) 

234  246  
235  247 
(* Convert formalEnv *) 
236 
(* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *) 

248 
(* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp 

249 
formalEnv; *) 

237  250 
(* if !debug then Format.eprintf "Formal env converted to salsa@ "; *) 
238  251  
239 
(* Format.eprintf "Expression avant et apres substVars.@.Avant %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ; *) 

252 
(* Format.eprintf "Expression avant et apres substVars.@.Avant %a@." 

253 
MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ; *) 

240  254  
241  255 
(* 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 ? *) 

256 
let (e_salsa : Salsa.Types.expression), _ = 

257 
Salsa.Rewrite.substVars e_salsa (FormalEnv.to_salsa constEnv formalEnv) 0 

258 
(* TODO: Nasrine, what is this integer value for ? *) 

247  259 
in 
248  260  
249 
(* Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env [] e_salsa) ; *) 

261 
(* Format.eprintf "Apres %a@." MC.pp_val (salsa_expr2value_t vars_env [] 

262 
e_salsa) ; *) 

250  263  
251  264 
(* if !debug then Format.eprintf "Substituted def in expr@ "; *) 
252  265 
let abstractEnv = RangesInt.to_abstract_env ranges in 
...  ...  
256  269 
garde evalPartExpr remplace les variables e qui sont dans env par la cst 
257  270 
 on garde *) 
258  271 
(* 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 *))


272 
(* Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t 

273 
vars_env constEnv e_salsa); *)


274 
let e_salsa =


275 
Salsa.Analyzer.evalPartExpr e_salsa


276 
(Salsa.Analyzer.valEnv2ExprEnv abstractEnv)


277 
[] (* no blacklisted variables *) []


278 
(* no arrays *)


266  279 
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  280  
281 
(* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t 

282 
vars_env constEnv e_salsa); *) 

283 
(* Checking if we have all necessary information *) 

270  284 
let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in 
271  285 
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 
) 

286 
report ~level:2 (fun fmt > 

287 
Format.fprintf fmt 

288 
"Warning: unbounded free vars (%a) in expression %a. We do not \ 

289 
optimize it.@ " 

290 
Vars.pp 

291 
(Vars.fold 

292 
(fun v accu > 

293 
let v' = 

294 
{ 

295 
v with 

296 
LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id; 

297 
} 

298 
in 

299 
Vars.add v' accu) 

300 
free_vars Vars.empty) 

301 
(MC.pp_val m) 

302 
(salsa_expr2value_t vars_env constEnv e_salsa)); 

303 
if !debug then 

304 
report ~level:2 (fun fmt > 

305 
Format.fprintf fmt "Some free vars, not optimizing@ "); 

306 
if !debug then 

307 
report ~level:3 (fun fmt > 

308 
Format.fprintf fmt " ranges: %a@ " RangesInt.pp ranges); 

309  
310 
(* if !debug then Log.report ~level:2 (fun fmt > Format.fprintf fmt 

311 
"Formal env was @[<v 0>%a@]@ " FormalEnv.pp formalEnv); *) 

312 
let new_e = 

313 
try salsa_expr2value_t vars_env constEnv e_salsa 

314 
with Not_found > assert false 

315 
in 

316 
new_e, None, [], Vars.empty) 

289  317 
else ( 
290 


291  318 
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 


319 
report ~level:3 (fun fmt > 

320 
Format.fprintf fmt 

321 
"@[<v 2>Analyzing expression %a@ with ranges: @[<v>%a@ @]@ @]@ " 

322 
(C_backend_common.pp_c_val m "" 

323 
(C_backend_common.pp_c_var_read m)) 

324 
(salsa_expr2value_t vars_env constEnv e_salsa) 

325 
(Utils.fprintf_list ~sep:",@ " (fun fmt (l, r) > 

326 
Format.fprintf fmt "%s > %a" l FloatIntSalsa.pp r)) 

327 
abstractEnv); 

328  
329 
(* Slicing expression *) 

330 
let e_salsa, seq = 

331 
try 

332 
Salsa.Rewrite.sliceExpr e_salsa 0 

333 
(Salsa.Types.Nop (Salsa.Types.Lab 0)) 

334 
with _ > 

335 
Format.eprintf "Issues rewriting express %s@.@?" 

336 
(Salsa.Print.printExpression e_salsa); 

337 
assert false 

338 
in 

339 
let def_tmps = Salsa.Utils.flatten_seq seq [] in 

340 
(* Registering tmp ids in vars_env *) 

341 
let vars_env', new_local_vars = 

342 
List.fold_left 

343 
(fun (vs, vars) (id, _) > 

344 
let vdecl = 

345 
Corelang.mk_fresh_var (nodename.node_id, []) 

346 
(* TODO check that the empty env is ok. One may need to build or 

347 
access to the current env *) 

348 
Location.dummy_loc e.MT.value_type (Clocks.new_var true) 

349 
in 

350  
351 
let vs' = VarEnv.add id { vdecl; is_local = true } vs in 

352 
let vars' = Vars.add vdecl vars in 

353 
vs', vars') 

354 
(vars_env, Vars.empty) def_tmps 

355 
in 

356 
(* Debug *) 

357 
if !debug then 

358 
report ~level:3 (fun fmt > 

359 
Format.fprintf fmt "List of slices: @[<v 0>%a@]@ " 

360 
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, e_id) > 

361 
Format.fprintf fmt "(%s,%a) > %a" id Printers.pp_var 

362 
(get_var vars_env' id).vdecl 

363 
(C_backend_common.pp_c_val m "" 

364 
(C_backend_common.pp_c_var_read m)) 

365 
(salsa_expr2value_t vars_env' constEnv e_id))) 

366 
def_tmps; 

367 
Format.fprintf fmt "Sliced expression: %a@ " 

368 
(C_backend_common.pp_c_val m "" 

369 
(C_backend_common.pp_c_var_read m)) 

370 
(salsa_expr2value_t vars_env' constEnv e_salsa)); 

371  
372 
(* Debug *) 

373  
374 
(* Optimize def tmp, and build the associated instructions. Update the 

375 
abstract Env with computed ranges *) 

376 
if !debug && List.length def_tmps >= 1 then 

377 
report ~level:3 (fun fmt > 

378 
Format.fprintf fmt "@[<v 3>Optimizing sliced subexpressions@ "); 

379 
let rev_def_tmp_instrs, ranges = 

380 
List.fold_left 

381 
(fun (accu_instrs, ranges) (id, e_id) > 

382 
(* Format.eprintf "Cleaning/Optimizing %s@." id; *) 

383 
let e_id', e_range = 

384 
(*Salsa.MainEPEG.transformExpression id e_id abstractEnv*) 

385 
opt_num_expr_sliced ranges e_id 

386 
in 

387 
let new_e_id' = 

388 
try salsa_expr2value_t vars_env' constEnv e_id' 

389 
with Not_found > assert false 

390 
in 

391  
392 
let vdecl = (get_var vars_env' id).vdecl in 

393  
394 
let new_local_assign = 

395 
(* let expr = salsa_expr2value_t vars_env' constEnv e_id' in *) 

396 
MT.MLocalAssign (vdecl, new_e_id') 

397 
in 

398 
let new_local_assign = 

399 
{ 

400 
MT.instr_desc = new_local_assign; 

401 
MT.lustre_eq = 

402 
None 

403 
(* could be Corelang.mkeq Location.dummy_loc 

404 
([vdecl.LT.var_id], e_id) provided it is converted as 

405 
Lustre expression rather than a Machine code value *); 

406 
} 

407 
in 

408 
let new_ranges = 

409 
match e_range with 

410 
 None > 

411 
ranges 

412 
 Some e_range > 

413 
RangesInt.add_def ranges id e_range 

414 
in 

415 
new_local_assign :: accu_instrs, new_ranges) 

416 
([], ranges) def_tmps 

417 
in 

418 
if !debug && List.length def_tmps >= 1 then 

419 
report ~level:3 (fun fmt > Format.fprintf fmt "@]@ "); 

420  
421 
(* Format.eprintf "Optimizing main expression %s@.AbstractEnv is %a" 

422 
(Salsa.Print.printExpression e_salsa) RangesInt.pp ranges; *) 

423 
let expr_salsa, expr_range = opt_num_expr_sliced ranges e_salsa in 

424 
let expr = 

425 
try salsa_expr2value_t vars_env' constEnv expr_salsa 

426 
with Not_found > assert false 

427 
in 

428  
429 
expr, expr_range, List.rev rev_def_tmp_instrs, new_local_vars 

430 
(* ???? Bout de code dans unstable lors du merge avec salsa ? ==== 

431  
432 
let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa with 

433 
Not_found > assert false in if !debug then Log.report ~level:2 (fun 

434 
fmt > let old_range = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] 

435 
in match RangesInt.Value.leq old_range e_val, RangesInt.Value.leq e_val 

436 
old_range with  true, true > Format.fprintf fmt "No improvement on 

437 
abstract value %a@ " RangesInt.pp_val e_val  true, false > ( 

438 
Format.fprintf fmt "Improved!"; Format.fprintf fmt " @[<v>old_expr: 

439 
@[<v 0>%a@ range: %a@]@ new_expr: @[<v 0>%a@ range: %a@]@ @]@ " 

440 
(MC.pp_val m) e RangesInt.pp_val (Salsa.Analyzer.evalExpr e_salsa 

441 
abstractEnv []) (MC.pp_val m) new_e RangesInt.pp_val e_val )  false, 

442 
true > Format.eprintf "Error; new range is worse!@.@?"; assert false  

443 
false, false > Format.eprintf "Error; new range is not comparabe with 

444 
old end. This should not happen!@.@?"; assert false ); new_e, Some 

445 
e_val, List.rev rev_def_tmp_instrs with (* Not_found > *)  

446 
Salsa.Epeg_types.EPEGError _ > ( Log.report ~level:2 (fun fmt > 

447 
Format.fprintf fmt "BECAUSE OF AN ERROR, Expression %a was not 

448 
optimized@ " (MC.pp_val m) e); e, None, [] ) >>>>>>> unstable *)) 

430  449 
in 
431 
opt_expr m vars_env ranges formalEnv e 

432 


433 


450  
451 
opt_expr m vars_env ranges formalEnv e 

452  
434  453 
(* Returns a list of assign, for each var in vars_to_print, that produce the 
435  454 
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 = 

455 
let assign_vars nodename m constEnv vars_env printed_vars ranges formalEnv 

456 
vars_to_print = 

437  457 
(* We print thhe expression in the order of definition *) 
438  
439 
let ordered_vars = 

458 
let ordered_vars = 

440  459 
List.stable_sort 
441 
(FormalEnv.get_sort_fun formalEnv)


442 
(Vars.elements vars_to_print)


460 
(FormalEnv.get_sort_fun formalEnv) 

461 
(Vars.elements vars_to_print) 

443  462 
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); 

463 
if !debug then 

464 
report ~level:4 (fun fmt > 

465 
Format.fprintf fmt "Printing vars in the following order: [%a]@ " 

466 
(Utils.fprintf_list ~sep:", " Printers.pp_var) 

467 
ordered_vars); 

468  
469 
List.fold_right 

470 
(fun v (accu_instr, accu_ranges, accu_new_locals) > 

471 
if !debug then 

472 
report ~level:4 (fun fmt > 

473 
Format.fprintf fmt "Printing assign for variable %s@ " v.LT.var_id); 

451  474 
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) 

475 
(* Obtaining unfold expression of v in formalEnv *) 

476 
let v_def = FormalEnv.get_def formalEnv v in 

477 
let e, r, il, new_v_locals = 

478 
optimize_expr nodename m constEnv printed_vars vars_env ranges 

479 
formalEnv v_def 

480 
in 

481 
let instr_desc = 

482 
if 

483 
try (get_var vars_env v.LT.var_id).is_local 

484 
with Not_found > assert false 

485 
then MT.MLocalAssign (v, e) 

486 
else MT.MStateAssign (v, e) 

487 
in 

488 
( il @ Corelang.mkinstr instr_desc :: accu_instr, 

489 
(match r with 

490 
 None > 

491 
ranges 

492 
 Some v_r > 

493 
RangesInt.add_def ranges v.LT.var_id v_r), 

494 
Vars.union accu_new_locals new_v_locals ) 

495 
with FormalEnv.NoDefinition _ > 

496 
if 

497 
(* It should not happen with C backend, but may happen with Lustre 

498 
backend *) 

499 
!Options.output = "lustre" 

500 
then accu_instr, ranges, Vars.empty 

501 
else ( 

502 
Format.eprintf "@?"; 

503 
assert false)) 

504 
ordered_vars ([], ranges, Vars.empty) 

474  505  
475  506 
(* Main recursive function: modify the instructions list while preserving the 
476  507 
order of assigns for state variables. Returns a quintuple: (new_instrs, 
477  508 
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 = 

509 
let rec rewrite_instrs nodename m constEnv vars_env m instrs ranges formalEnv 

510 
printed_vars vars_to_print = 

479  511 
let formal_env_def = FormalEnv.def constEnv vars_env in 
480  512 
(* Format.eprintf "Rewrite intrs : [%a]@." MC.pp_instrs instrs; *) 
481  513 
let assign_vars = assign_vars nodename m constEnv vars_env in 
...  ...  
487  519 
(* FormalEnv.pp formalEnv) *) 
488  520 
(* ); *) 
489  521 
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 

522 
 [] > 

523 
(* End of instruction list: we produce the definition of each variable that 

524 
appears in vars_to_print. Each of them should be defined in formalEnv *) 

525 
(* if !debug then Format.eprintf "Producing definitions %a@ " Vars.pp 

526 
vars_to_print; *) 

527 
let instrs, ranges', new_expr_locals = 

528 
assign_vars printed_vars ranges formalEnv vars_to_print 

529 
in 

530 
( instrs, 

531 
ranges', 

532 
formalEnv, 

533 
Vars.union printed_vars vars_to_print, 

534 
(* We should have printed all required vars *) 

535 
[], 

536 
(* No more vars to be printed *) 

537 
Vars.empty ) 

538 
 hd_instr :: tl_instrs > 

539 
(* We reformulate hd_instr, producing or not a fresh instruction, updating 

540 
formalEnv, possibly ranges and vars_to_print *) 

541 
let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print, hd_new_locals 

542 
= 

543 
match Corelang.get_instr_desc hd_instr with 

544 
 MT.MLocalAssign (vd, vt) 

545 
when Types.is_real_type vd.LT.var_type 

546 
&& not (Vars.mem vd vars_to_print) > 

547 
(* LocalAssign are injected into formalEnv *) 

548 
(* if !debug then Format.eprintf "Registering local assign %a@ " 

549 
MC.pp_instr hd_instr; *) 

550 
(* if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr; *) 

551 
let formalEnv' = formal_env_def formalEnv vd vt in 

552 
(* formelEnv updated with vd = vt *) 

553 
( [], 

554 
(* no instr generated *) 

555 
ranges, 

556 
(* no new range computed *) 

557 
formalEnv', 

558 
printed_vars, 

559 
(* no new printed vars *) 

560 
vars_to_print, 

561 
(* no more or less variables to print *) 

562 
Vars.empty ) 

563 
(* no new locals *) 

564 
 MT.MLocalAssign (vd, vt) 

565 
when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print > 

566 
(* if !debug then Format.eprintf "Registering and producing state assign 

567 
%a@ " MC.pp_instr hd_instr; *) 

568 
(* if !debug then Format.eprintf "Registering and producing state assign 

569 
%a@ " MC.pp_instr hd_instr; *) 

570 
(* if !debug then ( *) 

571 
(* Format.eprintf "%a@ " MC.pp_instr hd_instr; *) 

572 
(* Format.eprintf "Selected var %a: producing expression@ " 

573 
Printers.pp_var vd; *) 

574 
(* ); *) 

575 
let formalEnv' = formal_env_def formalEnv vd vt in 

576 
(* formelEnv updated with vd = vt *) 

577 
let instrs', ranges', expr_new_locals = 

578 
(* printing vd = optimized vt *) 

579 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) 

580 
in 

581 
( instrs', 

582 
ranges', 

583 
(* no new range computed *) 

584 
formalEnv', 

585 
(* formelEnv already updated *) 

586 
Vars.add vd printed_vars, 

587 
(* adding vd to new printed vars *) 

588 
Vars.remove vd vars_to_print, 

589 
(* removed vd from variables to print *) 

590 
expr_new_locals ) 

591 
(* adding sliced vardecl to the list *) 

592 
 MT.MStateAssign (vd, vt) 

593 
when Types.is_real_type vd.LT.var_type 

594 
(* && Vars.mem vd vars_to_print *) > 

595 
(* StateAssign are produced since they are required by the function. We 

596 
still keep their definition in the formalEnv in case it can optimize 

597 
later outputs. vd is removed from remaining vars_to_print *) 

598 
(* if !debug then Format.eprintf "Registering and producing state assign 

599 
%a@ " MC.pp_instr hd_instr; *) 

600 
(* if !debug then ( *) 

601 
(* Format.eprintf "%a@ " MC.pp_instr hd_instr; *) 

602 
(* Format.eprintf "State assign %a: producing expression@ " 

603 
Printers.pp_var vd; *) 

604 
(* ); *) 

605 
let formalEnv' = formal_env_def formalEnv vd vt in 

606 
(* formelEnv updated with vd = vt *) 

607 
let instrs', ranges', expr_new_locals = 

608 
(* printing vd = optimized vt *) 

609 
assign_vars printed_vars ranges formalEnv' (Vars.singleton vd) 

610 
in 

611 
( instrs', 

612 
ranges', 

613 
(* no new range computed *) 

614 
formalEnv, 

615 
(* formelEnv already updated *) 

616 
Vars.add vd printed_vars, 

617 
(* adding vd to new printed vars *) 

618 
Vars.remove vd vars_to_print, 

619 
(* removed vd from variables to print *) 

620 
expr_new_locals ) 

621 
(* adding sliced vardecl to the list *) 

622 
 MT.MLocalAssign (vd, vt)  MT.MStateAssign (vd, vt) > 

623 
(* Format.eprintf "other assign %a@." MC.pp_instr hd_instr; *) 

624  
625 
(* We have to produce the instruction. But we may have to produce as 

626 
well its dependencies *) 

627 
let required_vars = get_expr_real_vars vt in 

628 
let required_vars = Vars.diff required_vars printed_vars in 

629 
(* remove already produced variables *) 

630 
(* Format.eprintf "Required vars: %a@." Vars.pp required_vars; *) 

631 
let required_vars = 

632 
Vars.diff required_vars (Vars.of_list m.MT.mmemory) 

633 
in 

634 
let prefix_instr, ranges, new_expr_dep_locals = 

635 
assign_vars printed_vars ranges formalEnv required_vars 

636 
in 

756  637  
638 
let vt', _, il, expr_new_locals = 

639 
optimize_expr nodename m constEnv 

640 
(Vars.union required_vars printed_vars) 

641 
vars_env ranges formalEnv vt 

642 
in 

643 
let new_instr = 

644 
match Corelang.get_instr_desc hd_instr with 

645 
 MT.MLocalAssign _ > 

646 
Corelang.update_instr_desc hd_instr (MT.MLocalAssign (vd, vt')) 

647 
 _ > 

648 
Corelang.update_instr_desc hd_instr (MT.MStateAssign (vd, vt')) 

649 
in 

650 
let written_vars = Vars.add vd required_vars in 

651 
( prefix_instr @ il @ [ new_instr ], 

652 
ranges, 

653 
(* no new range computed *) 

654 
formalEnv, 

655 
(* formelEnv untouched *) 

656 
Vars.union written_vars printed_vars, 

657 
(* adding vd + dependencies to new printed vars *) 

658 
Vars.diff vars_to_print written_vars, 

659 
(* removed vd + dependencies from variables to print *) 

660 
Vars.union new_expr_dep_locals expr_new_locals ) 

661 
 MT.MStep (vdl, id, vtl) > 

662 
(* Format.eprintf "step@."; *) 

663  
664 
(* if !debug then Format.eprintf "Call to a node %a@ " MC.pp_instr 

665 
hd_instr; *) 

666 
(* Call of an external function. Input expressions have to be optimized, 

667 
their free variables produced. A fresh range has to be computed for 

668 
each output variable in vdl. Output of the function call are removed 

669 
from vars to be printed *) 

670 
let node = called_node_id m id in 

671 
let node_id = Corelang.node_name node in 

672 
let tin, tout = 

673 
(* special care for arrow *) 

674 
if node_id = "_arrow" then 

675 
match vdl with 

676 
 [ v ] > 

677 
let t = v.LT.var_type in 

678 
[ t; t ], [ t ] 

679 
 _ > 

680 
assert false (* should not happen *) 

681 
else fun_types node 

682 
in 

683 
(* if !debug then Format.eprintf "@[<v 2>... optimizing arguments@ "; *) 

684 
let vtl', vtl_ranges, il, args_new_locals = 

685 
List.fold_right2 

686 
(fun e typ_e (exprl, range_l, il_l, new_locals) > 

687 
if Types.is_real_type typ_e then 

688 
let e', r', il, new_expr_locals = 

689 
optimize_expr nodename m constEnv printed_vars vars_env ranges 

690 
formalEnv e 

691 
in 

692 
( e' :: exprl, 

693 
r' :: range_l, 

694 
il @ il_l, 

695 
Vars.union new_locals new_expr_locals ) 

696 
else e :: exprl, None :: range_l, il_l, new_locals) 

697 
vtl tin ([], [], [], Vars.empty) 

698 
in 

757  699  
700 
(* if !debug then Format.eprintf "... done@ @]@ "; *) 

701  
702 
(* let required_vars = *) 

703 
(* List.fold_left2 *) 

704 
(* (fun accu e typ_e > *) 

705 
(* if Types.is_real_type typ_e then *) 

706 
(* Vars.union accu (get_expr_real_vars e) *) 

707 
(* else (\* we do not consider non real expressions *\) *) 

708 
(* accu *) 

709 
(* ) *) 

710 
(* Vars.empty *) 

711 
(* vtl' tin *) 

712 
(* in *) 

713 
(* if !debug then Format.eprintf "Required vars: [%a]@ Printed vars: 

714 
[%a]@ Remaining required vars: [%a]@ " *) 

715 
(* Vars.pp required_vars *) 

716 
(* Vars.pp printed_vars *) 

717 
(* Vars.pp (Vars.diff required_vars printed_vars) *) 

718 
(* ; *) 

719 
(* let required_vars = Vars.diff required_vars printed_vars in (\* remove *) 

720 
(* already *) 

721 
(* produced *) 

722 
(* variables *\) *) 

723 
(* let written_vars = Vars.union required_vars (Vars.of_list vdl) in *) 

724 
(* let instrs', ranges' = assign_vars (Vars.union written_vars 

725 
printed_vars) ranges formalEnv required_vars in *) 

726  
727 
(* instrs' @ [Corelang.update_instr_desc hd_instr 

728 
(MT.MStep(vdl,id,vtl'))], (* New instrs *) *) 

729 
let written_vars = Vars.of_list vdl in 

730  
731 
( il @ [ Corelang.update_instr_desc hd_instr (MT.MStep (vdl, id, vtl')) ], 

732 
(* New instrs *) 

733 
RangesInt.add_call ranges vdl id vtl_ranges, 

734 
(* add information bounding each vdl var *) 

735 
formalEnv, 

736 
Vars.union written_vars printed_vars, 

737 
(* adding vdl to new printed vars *) 

738 
Vars.diff vars_to_print written_vars, 

739 
args_new_locals ) 

740 
 MT.MBranch (vt, branches) > 

741 
(* Required variables to compute vt are introduced. Then each branch is 

742 
refactored specifically *) 

743  
744 
(* if !debug then Format.eprintf "Branching %a@ " MC.pp_instr hd_instr; *) 

745 
let required_vars = get_expr_real_vars vt in 

746 
let required_vars = Vars.diff required_vars printed_vars in 

747 
(* remove already produced variables *) 

748 
let vt', _, prefix_instr, prefix_new_locals = 

749 
optimize_expr nodename m constEnv printed_vars vars_env ranges 

750 
formalEnv vt 

751 
in 

758  752  
753 
let new_locals = prefix_new_locals in 

754  
755 
(* let prefix_instr, ranges = *) 

756 
(* assign_vars (Vars.union required_vars printed_vars) ranges formalEnv 

757 
required_vars in *) 

758 
let printed_vars = Vars.union printed_vars required_vars in 

759  
760 
let read_vars_tl = get_read_vars tl_instrs in 

761 
(* if !debug then Format.eprintf "@[<v 2>Dealing with branches@ "; *) 

762 
let branches', written_vars, merged_ranges, new_locals = 

763 
List.fold_right 

764 
(fun (b_l, b_instrs) 

765 
(new_branches, written_vars, merged_ranges, new_locals) > 

766 
let b_write_vars = get_written_vars b_instrs in 

767 
let b_vars_to_print = 

768 
Vars.inter b_write_vars (Vars.union read_vars_tl vars_to_print) 

769 
in 

770 
let b_fe = formalEnv in 

771 
(* because of side effect data, we copy it for each branch *) 

772 
let ( b_instrs', 

773 
b_ranges, 

774 
b_formalEnv, 

775 
b_printed, 

776 
b_vars, 

777 
b_new_locals ) = 

778 
rewrite_instrs nodename m constEnv vars_env m b_instrs ranges 

779 
b_fe printed_vars b_vars_to_print 

780 
in 

781 
(* b_vars should be empty *) 

782 
let _ = if b_vars != [] then assert false in 

783  
784 
(* Producing the refactored branch *) 

785 
( (b_l, b_instrs') :: new_branches, 

786 
Vars.union b_printed written_vars, 

787 
(* They should coincides. We use union instead of inter to ease 

788 
the bootstrap *) 

789 
RangesInt.merge merged_ranges b_ranges, 

790 
Vars.union new_locals b_new_locals )) 

791 
branches 

792 
([], required_vars, ranges, new_locals) 

793 
in 

794 
(* if !debug then Format.eprintf "dealing with branches done@ @]@ "; *) 

795 
( prefix_instr 

796 
@ [ 

797 
Corelang.update_instr_desc hd_instr (MT.MBranch (vt', branches')); 

798 
], 

799 
merged_ranges, 

800 
(* Only step functions call within branches may have produced new 

801 
ranges. We merge this data by computing the join per variable *) 

802 
formalEnv, 

803 
(* Thanks to the computation of var_to_print in each branch, no new 

804 
definition should have been computed without being already printed *) 

805 
Vars.union written_vars printed_vars, 

806 
Vars.diff vars_to_print written_vars 

807 
(* We remove vars that have been produced within branches *), 

808 
new_locals ) 

809 
 MT.MReset _  MT.MNoReset _  MT.MSpec _  MT.MComment _ > 

810 
(* if !debug then Format.eprintf "Untouched %a (non real)@ " MC.pp_instr 

811 
hd_instr; *) 

812  
813 
(* Untouched instruction *) 

814 
( [ hd_instr ], 

815 
(* unmodified instr *) 

816 
ranges, 

817 
(* no new range computed *) 

818 
formalEnv, 

819 
(* no formelEnv update *) 

820 
printed_vars, 

821 
vars_to_print, 

822 
(* no more or less variables to print *) 

823 
Vars.empty ) 

824 
(* no new slides vars *) 

825 
in 

759  826  
827 
let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print, tl_new_locals 

828 
= 

829 
rewrite_instrs nodename m constEnv vars_env m tl_instrs ranges formalEnv 

830 
printed_vars vars_to_print 

831 
in 

760  832  
833 
( hd_instrs @ tl_instrs, 

834 
ranges, 

835 
formalEnv, 

836 
printed_vars, 

837 
vars_to_print, 

838 
Vars.union hd_new_locals tl_new_locals ) 

761  839  
762  840 
(* 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 

841 
let salsaStep constEnv m s = 

842 
let ranges = 

843 
RangesInt.empty 

844 
(* empty for the moment, should be build from machine annotations or 

845 
externally provided information *) 

775  846 
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.@." 
Also available in: Unified diff
reformatting